5

Double Groupoids and Crossed Modules in HoTT

 3 years ago
source link: https://homotopytypetheory.org/2015/06/02/double-groupoids-and-crossed-modules-in-hott/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

Double Groupoids and Crossed Modules in HoTT

The past eight months I spent at CMU for my master thesis project. I ended up formalizing some algebraic structures used in Ronald Brown’s book “Non-Abelian Algebraic Topology”: Double groupoids with thin structure and crossed modules over groupoids.

As the language for the formalizations I chose the newly developed theorem prover Lean. Lean is developed by Leonardo de Moura at Microsoft Research and provides a dependently typed language similar to Agda or Coq. Currently, there are two modes for Lean: A proof-irrelevant mode and a HoTT mode. The HoTT library was written at the same time as my project, mainly by Floris van Doorn and, for a smaller part, me. You can find papers about Lean and its elaboration algorithm on the website, as well as a link to a version of Lean that runs in your web browser.

Double groupoids are a special case double categories which, besides objects and morphisms, specify a set of two-cells for each (not necessarily commuting) square diagram in a way such that the two-cells form a category with respect to vertical and to horizontal composition. That includes the existence of vertically and horizontally degenerate fillers of square diagrams with the identity on two opposing sides and the same morphism on the other side. The vertically degenerate squares should distribute over the horizontal composition of morphisms and vice versa. Furthermore, the vertically and horizontally degenerate square along the identity should be the same. A last axiom is the interchange law which ensures that, in the case of two-cells which are composable in a 2×2-grid, it doesn’t matter whether to first compose vertically or horizontally.

I decided to formalize double categories in the same way categories are usually formalized using dependent types using a type of two-cells depending on four points and four morphisms:

D_2 : \prod_{a, b, c, d : D_0} \text{hom}(a,b) \to \text{hom}(c,d) \to \text{hom}(a,c) \to \text{hom}(b,d) \to \mathcal{U}.In the formalization, I first define a worm precategory which only allows for two-cell composition in one direction. Then, I use Lean’s inheritance mechanism to get the full notion of a double (pre)category:

structure worm_precat {D₀ : Type} (C  : precategory D₀)
(D₂ : Π ⦃a b c d : D₀⦄
(f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type) :=
(comp₁ : proof Π ⦃a b c₁ d₁ c₂ d₂ : D₀⦄
⦃f₁ : hom a b⦄ ⦃g₁ : hom c₁ d₁⦄ ⦃h₁ : hom a c₁⦄ ⦃i₁ : hom b d₁⦄
⦃g₂ : hom c₂ d₂⦄ ⦃h₂ : hom c₁ c₂⦄ ⦃i₂ : hom d₁ d₂⦄,
(D₂ g₁ g₂ h₂ i₂) → (D₂ f₁ g₁ h₁ i₁)
→ (@D₂ a b c₂ d₂ f₁ g₂ (h₂ ∘ h₁) (i₂ ∘ i₁)) qed)
(ID₁ : proof Π ⦃a b : D₀⦄ (f : hom a b), D₂ f f (ID a) (ID b) qed)
(assoc₁ : proof Π ⦃a b c₁ d₁ c₂ d₂ c₃ d₃ : D₀⦄
⦃f  : hom a b⦄   ⦃g₁ : hom c₁ d₁⦄ ⦃h₁ : hom a c₁⦄ ⦃i₁ : hom b d₁⦄
⦃g₂ : hom c₂ d₂⦄ ⦃h₂ : hom c₁ c₂⦄ ⦃i₂ : hom d₁ d₂⦄
⦃g₃ : hom c₃ d₃⦄ ⦃h₃ : hom c₂ c₃⦄ ⦃i₃ : hom d₂ d₃⦄
(w : D₂ g₂ g₃ h₃ i₃) (v : D₂ g₁ g₂ h₂ i₂) (u : D₂ f g₁ h₁ i₁),
(assoc i₃ i₂ i₁) ▹ ((assoc h₃ h₂ h₁) ▹
(comp₁ w (comp₁ v u))) = (comp₁ (comp₁ w v) u) qed)
...
structure dbl_precat {D₀ : Type} (C : precategory D₀)
(D₂ : Π ⦃a b c d : D₀⦄
(f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
extends worm_precat C D₂,
worm_precat C (λ ⦃a b c d : D₀⦄ f g h i, D₂ h i f g)
renaming comp₁→comp₂ ID₁→ID₂ assoc₁→assoc₂
id_left₁→id_left₂ id_right₁→id_right₂ homH'→homH'_dontuse :=
...
(interchange : proof Π {a₀₀ a₀₁ a₀₂ a₁₀ a₁₁ a₁₂ a₂₀ a₂₁ a₂₂ : D₀}
{f₀₀ : hom a₀₀ a₀₁} {f₀₁ : hom a₀₁ a₀₂} {f₁₀ : hom a₁₀ a₁₁}
{f₁₁ : hom a₁₁ a₁₂} {f₂₀ : hom a₂₀ a₂₁} {f₂₁ : hom a₂₁ a₂₂}
{g₀₀ : hom a₀₀ a₁₀} {g₀₁ : hom a₀₁ a₁₁} {g₀₂ : hom a₀₂ a₁₂}
{g₁₀ : hom a₁₀ a₂₀} {g₁₁ : hom a₁₁ a₂₁} {g₁₂ : hom a₁₂ a₂₂}
(x : D₂ f₁₁ f₂₁ g₁₁ g₁₂) (w : D₂ f₁₀ f₂₀ g₁₀ g₁₁)
(v : D₂ f₀₁ f₁₁ g₀₁ g₀₂) (u : D₂ f₀₀ f₁₀ g₀₀ g₀₁),
comp₁ (comp₂ x w) (comp₂ v u) = comp₂ (comp₁ x v) (comp₁ w u) qed)

Double groupoids are double categories where all three categories involved — the underlying category of points and morphisms, the vertical category of two-cells, and the horizontal category of two-cells — are groupoids and that are equipped with a thin structure: A selection of a unique thin filler of each commutative square shell which is closed under composition and degenerate squares.

It turns out that a category equivalent to the one of double groupoids is the category of crossed modules over a groupoid. A crossed module is defined as a groupoid $P$ together with a family (M_p)_{p \in P} of groups (or, equivalently, a totally disconnected groupoid) on the objects of P and for each p \in P a group homomorphism \mu_p : M_p \to \text{hom}(p,p) and a groupoid action \phi of P on the (M_p)_{p \in P}. The family of homomorphisms and the action should interact by resembling conjugation via \mu_q(\phi(f,x)) = f \circ \mu_p(x) \circ f^{-1} and \phi(\mu_p(c),x) = c \cdot x \cdot c^{-1} for each p, q \in P, $f \in \text{hom}_P(p,q)$ and c, x \in M_p.

structure xmod {P₀ : Type} [P : groupoid P₀] (M : P₀ → Group) :=
(P₀_hset : is_hset P₀)
(μ : Π ⦃p : P₀⦄, M p → hom p p)
(μ_respect_comp : Π ⦃p : P₀⦄ (b a : M p), μ (b * a) = μ b ∘ μ a)
(μ_respect_id : Π (p : P₀), μ 1 = ID p)
(φ : Π ⦃p q : P₀⦄, hom p q → M p → M q)
(φ_respect_id : Π ⦃p : P₀⦄ (x : M p), φ (ID p) x = x)
(φ_respect_P_comp : Π ⦃p q r : P₀⦄ (b : hom q r) (a : hom p q) (x : M p),
φ (b ∘ a) x = φ b (φ a x))
(φ_respect_M_comp : Π ⦃p q : P₀⦄ (a : hom p q) (y x : M p),
φ a (y * x) = (φ a y) * (φ a x))
(CM1 : Π ⦃p q : P₀⦄ (a : hom p q) (x : M p), μ (φ a x) = a ∘ (μ x) ∘ a⁻¹)
(CM2 : Π ⦃p : P₀⦄ (c x : M p), φ (μ c) x = c * (x * c⁻¹ᵍ))

After formlizing both categories, DGpd and Xmod including the definition of their respective morphisms, I defined the functors \gamma and \lambda which establish their equivalence.

definition gamma.functor :
functor Cat_dbl_gpd.{l₁ l₂ l₃} Cat_xmod.{(max l₁ l₂) l₂ l₃} :=
begin
fapply functor.mk,
intro G, apply (gamma.on_objects G),
intros [G, H, F], apply (gamma.on_morphisms F),
intro G, cases G,
fapply xmod_morphism_congr, apply idp, apply idp,
repeat ( apply eq_of_homotopy ; intros), cases x_1, apply idp,
...
end

Since establishing the functors was quite tedious, I didn’t finish proving the equivalence, but I might do that in the future.

As a little application on 2-types I instantiated the fundamental double groupoid of a 2-type X which is presented by a set C and a 1-type A by arbitrary functions \iota : C \to A and \iota' : A \to X. Here, the type of objects is the set C, the set of morphisms between a, b : C is the identity type \iota(a) =_A \iota(b), and the set of two-cells associated to four points a, b, c, d : C and paths f, g, h, i on the top, bottom, left and right of a diagram is the set \text{ap}_{\iota'}(h) \cdot \text{ap}_{\iota'}(g) = \text{ap}_{\iota'}(f) \cdot \text{ap}_{\iota'}(i). This could serve as the starting point to formalize a 2-dimensional Seifert-van Kampen theorem using double groupoids or crossed modules.

You can find my thesis here. The Lean code used can be found on github, due to recent changes in Lean, it most probably won’t compile with the newest version of Lean but with an older snapshot that can be found here.

This entry was posted in Code, Homotopy Theory. Bookmark the permalink.

31 Responses to Double Groupoids and Crossed Modules in HoTT

  1. jessemckeown says:

    One obtuse question: what is “Lean’s inheritance mechanism”?

    • In the definition of a structure, Lean allows to state multiple parent structures. Lean automatically creates coercions to all those parent structures and merges fields with the same name.

  2. Mike Shulman says:

    I think this is our first blog post about a formalization in the new proof assistant Lean! Congrats.

    Can you say any more about the n-type level restrictions that you used? Are the types of 1-morphisms sets or 1-types? How about the types of objects and 2-cells?

    Also, what does it mean to “select a unique thin filler”? Are you saying the thin fillers are asserted to be unique such that some properties hold?

    • Steve Awodey says:

      Ah yes, we should have said something about Lean in general. Jakob, since you have been involved in the development of it, maybe you could add a few words of “introduction”?

    • Morphisms and two-cells are both assumed to be sets. I started out without a restriction on the object type, but of course, to instantiate the type of double groupoids as a (pre)category, I had to restrict it to set-based object types.

      A thin structure consists of a function \mathsf{thin} : \prod_{a,b,c,d : D_0, f, g, h, i : \ldots} h \cdot g = f \cdot i \to D_2(f,g,h,i) and witnesses that the (vertical and horizontal) composition of thin fillers is thin and that identity squares are thin.

      • Mike Shulman says:

        Thanks! How essential are those restrictions? I would naturally expect the type of 2-cells to be a set, the type of 1-cells to be a 1-type, and the type of objects to be a 2-type.

        It sounds like you didn’t really mean to say “unique”, then?

  3. Has any work been done on a kind of low-dimensional homotopy hypothesis internally to HoTT? The kind of thing I am thinking of would say something like: every 1-type (in the HoTT sense) is equivalent to a groupoid (formalising the latter notion internally to HoTT); every 2-type (in the HoTT sense) is equivalent to a cubical 2-groupoid (formalising the latter notion internally to HoTT, as you have done in your thesis for one variant of this notion).

    I once had a discussion with Mike at the n-café where we discussed something related to this, but I don’t think we addressed this point specifically. I am interested because I can prove both of these facts in a category theoretic foundations (and higher versions), but can imagine that a proof would look quite different in HoTT, and would be very intrigued to see how it is done.

    For this kind of question, I usually work with cubical 2-groupoids with connections rather than thin structures, because I find the former to be better from a ‘structural’/’categorical’ point of view.

    • Mike Shulman says:

      “Every 1-type is equivalent to a groupoid” is true fairly trivially if by “groupoid” you mean one in the sense of the HoTT book which has a 1-type of objects. But it’s false if by “groupoid” you mean one that has a set of objects; there are (intended) models in which not every 1-type admits any surjection from a set, so can’t be presented in terms of sets.

      • I should have written a little more than ‘every 1-type is equivalent to a groupoid’, because I had something different in mind than either of these two interpretations! The second I would regard as a misinterpretation of the homotopy hypothesis, as I wrote in the n-café discussion, at the following link.

        https://golem.ph.utexas.edu/category/2014/07/the_categorical_origins_of_leb.html#c046828

        No need to take up that discussion again!

        The first is, as you say, trivial, rather than capturing the way in which the homotopy hypothesis should work: the groupoid cooked from up a 1-type should be a ‘nerve’ construction (this may seem the wrong way around, but I don’t think it is, as I will explain below), and the equivalence between 1-types and groupoids should in one direction involve this.

        To explain what I had in mind, I’ll work with ‘the internal language of groupoids’, namely a 1-truncation of HoTT, rather than full HoTT.

        1) We can express the notion of a groupoid in the internal language of groupoids, in a similar way to the definition of a complete Segal space: we have a groupoid of objects, a groupoid of arrows, source and target functors, etc, along with a completeness axiom. I think that a groupoid is defined in HoTT in this way, in one of the definitions at least.

        2) Given a groupoid (in the primitive sense), one can construct a ‘nerve’ of it, which is a groupoid in the sense of 1).

        3) Given a groupoid in the sense of 1), one can construct a ‘fundamental groupoid’ of it, which is a groupoid in the primitive sense.

        4) The constructions of 2) and 3) should define an ‘equivalence’ between groupoids in the primitive sense and groupoids in the sense of 1).

        I’m pretty sure that these constructions can be carried out, and 4) can be proven, in a set-theoretic foundations. Indeed, I’m pretty sure that one has a model structure on ‘Rezk groupoids’ such that 4) defines a Quillen equivalence between it and the folk model structure on ‘ordinary groupoids’. Maybe this is even in the literature.

        However, I’ve not looked into whether this ‘equivalence’ can be carried out ‘synthetically’, i.e., in the internal language of groupoids. This was the kind of thing that I was asking about. Of course, one doesn’t need to use the language of Quillen equivalences, etc, one would just be asking that the constructions of 2) and 3) are inverse in the appropriate sense.

        It would be especially interesting if this could be carried out for 2-groupoids, because I think there is a possibility that one might be able to generalise such a proof to higher dimensions, without running into the difficulties that one usually does once one reaches 3-groupoids (that the strict notion cannot be used). If so, one would have a very interesting version of the homotopy hypothesis. Not the full strength of the original one, but very interesting nonetheless.

        Incidentally, I would feel that a ‘homotopy hypothesis’ in this sense would be much better evidence that HoTT is a synthetic theory of infinity-groupoids, as opposed to a synthetic homotopy theory. A primitive object in a synthetic theory of infinity-groupoids should, it seems to me, be equipped with internal notions of object, arrow, 2-arrow, etc. If it can be proven internally to HoTT that any primitive object in HoTT is essentially determined by its objects, 1-arrows, etc, in this sense, then that is certainly a reasonable and non-trivial way in which it is a synthetic theory of infinity-groupoids.

        • Mike Shulman says:

          I don’t see how that’s different from the first approach that I said was trivial.

          • I thought that you were saying an analogue of the following, which is certainly trivial: given any set (regarded as a 0-type), there is a groupoid/higher groupoid which is equivalent to it after taking the nerve of the groupoid/higher groupoid.

            The equivalence between Rezk groupoids and ordinary groupoids that I described is not trivial in this sense (the ‘fundamental groupoid’ functor does not send a groupoid to the ‘discrete’ Rezk groupoid on it). Are you saying that an equivalence of the kind I described is proven in HoTT? If so, could you give a reference? And is it similarly ‘trivial’ for 2-groupoids?

            • Mike Shulman says:

              Let’s say “1-type” and “groupoid” respectively to avoid confusion.

              I don’t know what you mean by a “discrete” Rezk groupoid. The Rezk groupoid N X that corresponds to a 1-type X has X as its type of objects and \mathrm{Hom}_{N X}(x,y) = \mathrm{Id}_X(x,y). If you formulate that with “a type of arrows” rather than hom-types dependent on two copies of the objects (which is, I think, the wrong way to do it, but it’s equivalent in this case) then the type of arrows will be \sum_{x,y:X} \mathrm{Id}_X(x,y), which is equivalent to X. So it is “discrete” in the sense that its type of objects and type of arrows are equivalent. But I can’t imagine any other Rezk groupoid that you could construct out of X.

              • Richard says:

                Ah, I am thinking of defining the Rezk groupoid of X using an internal notion of object and arrow (I mentioned that this was central to how I am viewing the homotopy hypothesis). For instance, one defines the type of objects of X to be the type of functions from the ‘walking object’ into X, and the type of arrows of X to be the type of functions from the ‘walking arrow’ into X, and builds the Rezk nerve of X from these. This Rezk nerve is certainly not the same as the one you describe (e.g. the type of objects is discrete). And the ‘fundamental 1-type’ of a Rezk groupoid is similarly non-trivial.

                The Rezk nerve that you describe is indeed discrete in the sense I had in mind.

                PS – Where I wrote ‘fundamental groupoid’ in my previous comment, I should have written ‘nerve’. Too used to thinking of the usual homotopy hypothesis (despite my remarking on this very point in the comment before that!). Thank you for silently correcting it!

                • Mike Shulman says:

                  What is the “walking object”? Is it something that exists in HoTT, or is it something you want to add to the theory?

                  If by “the type of objects is discrete” you mean that the type of objects is a 0-type (a set), then I don’t think that any nerve of that sort can provably satisfy the HH in HoTT, since as I said there are models in which not every 1-type admits any surjection from a 0-type.

                  • Richard says:

                    The remark about the type of objects being discrete was nonsense, my apologies.

                    The ‘walking object’ should (of course!) ‘be’ the free \infty-groupoid on one object. In HoTT this would (presumably) be taken to be a type for which we prescribe a single term, but nothing else (‘singleton type’). So certainly this can be constructed rather than hypothesised if we have inductive types, etc.

                    The ‘walking arrow’ should ‘be’ the free \infty-groupoid on a single arrow. In HoTT this would presumably be taken to be a type for which we prescribe two terms 0 and 1, and a single term of type \mathsf{Id}(0,1), but nothing else. I am not familiar enough with the precise details of HoTT to know if this can be constructed in it, but I would not be surprised if it can be.

                    The question then is: can one prove, internally to HoTT, that, for a 1-type, the type of functions from the ‘walking object’ to a type X is a 1-type that is equivalent to X, and that the type of functions from the ‘walking arrow’ to a 1-type X is a 1-type equivalent to a dependent sum of identity types of X of the kind you wrote down? If so, then we just have recovered the ‘discrete’ Rezk nerve that you described, and I can imagine that a proof of the equivalence I described will just boil down to formulating the completeness axiom correctly, and thus will indeed, as you suggested, be more or less trivial (and my remarks about it being a ‘very interesting’ version of the homotopy hypothesis would not apply, as the kind of things that I was imagining would need to be considered as part of a proof would in fact not need to be).

                    I would be somewhat surprised if the answer to my question is positive, though. I don’t think, for instance, that what I ask about can be proven working in the ‘internal language of groupoids’.

    • Steve Awodey says:

      Using HITs, one can define the “groupoid quotient” BG for any pregroupoid G, and given a “set presented” groupoid S –>> G, one gets a pregroupoid in the expected way (as a kernel), and this gives an adjoint equivalence. The same thing works in higher finite dimensions, and Egbert and I have been working out the generalization to infinity groupoids — but of course, there are coherence issues.

      • This sounds very interesting, but I lack enough familiarity with the terminology to understand it! Could you possibly translate it to the language of groupoids? By a pre-groupoid, I guess you would then mean a ‘Rezk groupoid’ in the sense I defined in discussion with Mike, except that there is no ‘completeness’? What exactly, then, is BG? And what exactly is a ‘set presented’ groupoid?

        On a different note, when you say there are coherence issues, do you mean only in the infinity case? Because, at least thinking of the homotopy hypothesis in the usual sense, this would be very strange! And if you do mean only in the infinity case, and what you have proven in the finite cases does correspond roughly to the usual homotopy hypothesis, then what you are claiming is rather an important result! For a start: what is the notion of 3-groupoid (or set-presented 3-groupoid, i.e., the non-primitive notion) that you work with?

    • Mike Shulman says:

      Popping back out of the comment nesting, and continuing to say “type” and “∞-groupoid” for clarity:

      Your “free type on one object” is indeed the singleton or unit type 1, and the mapping type 1\to X is equivalent to X. Your “free type on one morphism” does exist, is generally called the interval type, and is contractible (equivalent to 1); thus the mapping type \mathrm{Interval} \to X is also equivalent to X, and hence also to \sum_{x,y:X} \mathrm{Id}_X(x,y). So the statement is true.

      • But this equivalence between the mapping type 1 \rightarrow X and X, and similarly for the interval type, cannot, surely, be constructively valid? Is a non-constructive principle explicitly assumed here, or does the equivalence follow only from univalence, etc? This is why I wrote that I would be surprised by a result of this kind: in the kind of internal language of groupoids that I would work with, one would not be able to prove that this kind of equivalence holds. One can force it to hold, but only in non-constructive ways.

        I agree, as in my previous comment, that if one has these equivalences, then the equivalence between Rezk groupoids and 1-types is more or less trivial (namely following from a correct definition of completeness), as you wrote originally. Of course, the content of this equivalence does not bear any significant resemblance to the homotopy hypothesis.

        But if one does not allow oneself to use these kind equivalences, but rather makes direct use of the internal object and arrow point of view, and gives a proof in this language, then I think that one may well end up doing the same kind of things as one does when proving the homotopy hypothesis for groupoids in a set theoretic, or category theoretic, foundations, but in a different language. It was this that I had in mind when I wrote that this kind of homotopy hypothesis would be very interesting.

        • Mike Shulman says:

          No, they are completely constructive. What makes you think they wouldn’t be?

          • The issue can be seen just looking at sets. Constructively, I would regard there as being a difference between a set and its elements. In other words, I would not regard an extensionality principle that identifies a set with its elements as constructively valid.

            Think for example of the coproduct 1 \sqcup 1, where 1 is a final object of the category of sets. Now there are of course two canonical ‘objects’ of 1 \sqcup 1 which one can construct. And, by the universal property of 1 \sqcup 1, one can construct maps out of it just as one would expect to with a set of two elements. But if you give me an arrow 1 \rightarrow 1 \sqcup 1, there is no way that I can prove that this arrow is one of the two canonical arrows, just making use of the definition of 1 \sqcup 1, that is to say, making use of the definition of a binary coproduct and of a final object. In other words, intensionally, that is to say, from the meaning of 1 \sqcup 1, we cannot conclude that it only has two objects, the canonical ones.

            One can add something to one’s foundations which forces all objects of 1 \sqcup 1 to be equal to one of the canonical two. But this is fundamentally non-constructive.

            In ‘ordinary’ intensional Martin-Löf type theory, this kind of ‘forcing’ does not occur. Thus, if it is provable in HoTT, it must come from univalence or something else that is added.

            • Mike Shulman says:

              Actually, it is possible in MLTT to prove that every element of 1\sqcup 1 is equal to one of the injections. It follows easily from the induction principle that expresses the universal property of 1\sqcup 1 in a dependently typed way.

            • Mike Shulman says:

              The proof that 1\to X is equivalent to X doesn’t use univalence; the only thing beyond MLTT that it needs is function extensionality. The analogous proof for the interval is the same, except that of course it also needs the interval (which is a HIT and not part of MLTT). Neither requires univalence.

  4. Richard says:

    Pursuing my line of questioning on a slightly different note… in the thesis, a fundamental 2-groupoid of a 2-type is defined.

    1) Why the restriction to a 2-type? I think there is some explanation of this in the thesis, but maybe someone can give an intuitive explanation.

    2) What is the relationship of this fundamental 2-groupoid to the original 2-type? I take it from Mike’s comments that it is not equivalent to it? Is it then just to be viewed as a useful invariant? If HoTT is to be thought of as a synthetic theory of infinity-groupoids, it seems rather strange to extract ‘algebraic’ invariants, which the theory is supposed to be capturing in the first place!

    3) What is the relationship between the work that Steve Awodey describes and fundamental groupoids/2-groupoids?

    4) Can can express what the types arising as ‘fundamental groupoids’/’fundamental 2-groupoids’ look like in general. In other words, can one recognise which types arise as the fundamental groupoids/2-groupoids of other types?

  5. Replying here to Mike’s two comments at 16:42 – 16:44 on the 6th of June.

    Yes, I suspected function extensionality would be needed (but since, as far I have heard, univalence implies it, univalence would be equally culpable).

    Regarding proving that every element of 1 \sqcup 1 is one of the canonical ones in MLTT: the point I am making is a general one, not tied to MLTT specifically. I am absolutely certain that this cannot be proven on the basis of the intensional meaning of 1 \sqcup 1 alone, in the categorical sense I have in mind, and don’t think that you would disagree with this. If it happens to be provable in MLTT, then I would reject as not constructively valid those aspects of MLTT which ensure that it is.

    However, I suspect there is something in the way you have formalised the statement in MLTT that would go against the principle I stated, rather than there being something in MLTT itself which I would disagree with. That is to say, the meaning of 1 \sqcup 1 in the way you have formalised it is, I suspect, different from the categorical one I have in mind. If one takes just a fragment of MLTT (dependent sums are in particular not needed), and builds a category theoretic foundations on top of it, then, defining 1 \sqcup 1 in these categorical foundations, what I wrote will be the case: it will not be possible to prove that every arrow 1 \rightarrow 1 \sqcup 1 is canonical.

    • Mike Shulman says:

      It’s true that one shouldn’t expect to prove based on the universal property of a coproduct in a category that every morphism 1\to 1\sqcup 1 in that category is one of the injections (since there are categories in which it’s false). But MLTT is the internal logic of a category, and it is true in the internal logic of a category that every element of 1\sqcup 1 is one of the canonical ones, even if as an external statement about that (same!) category there are more than two morphisms 1\to 1\sqcup 1.

      Put differently, while it is not part of the “meaning” of a coproduct in an arbitrary category that there are only two elements of 1\sqcup 1, it is part of the meaning of a coproduct of sets (or ∞-groupoids), because in that case coproducts are disjoint unions.

      Regardless, I don’t think I recall ever hearing anyone suggest that there is anything nonconstructive about extensionality.

    • Mike Shulman says:

      I am, by the way, talking about the utterly standard way to define coproducts in MLTT; so there are lots and lots of constructive type theorists, including Martin-Löf himself, who haven’t found it to be lacking in constructivity.

      I’m not sure exactly what you mean by “taking just a fragment of MLTT and building a category theoretic foundations on top of it”, but one possibility I can think of is that you want to introduce the type A\sqcup B by a universal property of the sort \mathrm{Hom}(A\sqcup B,C) \simeq \mathrm{Hom}(A,C) \times \mathrm{Hom}(B,C) (rather than by an induction principle in the usual way). This definition ought still to allow you to prove that every element of 1\sqcup 1 is canonical. Let C be the subset of 1\sqcup 1 consisting of the canonical elements, i.e.

      C= \{ z : 1\sqcup 1 \mid (\exists x:1, z = \mathrm{inl}(x)) \vee (\exists x:1, z = \mathrm{inr}(x)) \}.

      Then \mathrm{inl} and \mathrm{inr} give maps 1\to C and 1\to C, which by the universal property induce a map 1\sqcup 1 \to C, and by the uniqueness part of the universal property this map is a section of the inclusion C\to 1\sqcup 1; thus every element of 1\sqcup 1 lies in C. Admittedly this argument does require the ability to form the subset corresponding to a predicate, which is usually implemented in MLTT as a dependent sum; but it’s hard for me to imagine that you could do very much mathematics without the ability to make subsets like that (or to form existential quantifications, which are also dependent sums).

      This discussion has, however, drifted rather far from the original topic of this post, so perhaps we should wrap it up soon. I would summarize it by saying that the answer to your original question is, as I first said, “yes, it’s fairly trivial”, but that you seem to want to ask a different question (which I don’t fully understand) that perhaps cannot be formulated in HoTT.

      • Regarding your last pararaph: yes, I was about to the say the same, I think that what we are now discussing is probably too far away from HoTT itself for it to be appropriate for this blog.

        A slight qualification to your summary in this last paragraph: I have agreed that there is a more or less trivial way to formulate the homotopy hypothesis for 1-types in HoTT (which doesn’t bear any significance resemblance in content to the original one). What I am suggesting is that a subtle difference in this formulation might lead to a more interesting proof, the content of which more closely resembles the usual proofs of the homotopy hypothesis for 1-types, and which is closer to the kind of thing I was looking for, and felt might be possible, when I posed my original question. To try to explain how this might be possible, I have tried to explain that whether one can identify the function type 1 \rightarrow X with X is something that I feel is a foundational matter, i.e., I feel that a priori there is a significant difference in intensional meaning. Thus, working with one rather than the other, without making use of an identification between them, could lead to significantly different flavours of proof.

        Steve Awodey also appears to be suggesting a different way to formulate the homotopy hypothesis in HoTT, which might also be close to the kind of thing I had in mind when I posed the original question (I am not yet sure).

        Regarding the non-constructivity of extensionality: I am also not aware of anywhere where this has been argued, but it is something that I feel to be the case. This point of view is strongly influenced by the way in which I have been thinking and working on foundational matters, which is in the setting of what I think of as ‘synthetic category theory’ (where notions of category, functor, etc, are taken as primitive). This is not the place to go into this further, I think.

        I am entirely aware that the way you are suggesting to define 1 \sqcup 1 is standard, and of the points you make concerning this. However, there are very many tacit assumptions in your statement that MLTT is the internal logic of a category, on which this ‘standard definition’ rests. These assumptions are not to do with MLTT itself, but with the foundations in which the category lives. It is these foundations to which my point applies.

        As I have written elsewhere, I regard the basic semantics of MLTT, as a foundation for constructive mathematics, as very carefully justified philosophically. I would regard it as highly unlikely that something in MLTT itself would contradict the point about non-constructivity of extensionality that I am making. As I already tried to explain, it is not this basic, motivational semantics which guides the formulation of 1 \sqcup 1 in MLTT that you are referring to, but semantics which rely on foundational assumptions outside of MLTT.

        The way in which I am thinking of building category theory on top of MLTT is completely different. It is an extension of it: one has a primitive type of categories, of functors, etc. The fragment of MLTT itself that is used does not have any intended categorical semantics, it is just used as a formal language (which adheres to the same constructive principles that I wish to follow in the category theoretic foundations itself).

        Regarding your suggestion that 1\sqcup 1 having exactly two elements is part of the meaning of a coproduct of sets: my point is precisely that I do not regard it as constructively justifiable to assert this (as it must be asserted, one way or another).

        I also disagree strongly with the suggestion that one cannot do much mathematics without dependent sums, but this would take us into a different discussion, not relevant to this blog. What I wrote about not having dependent sums was in this instance just intended to give some feeling for what I meant by a ‘fragment’ of MLTT.

Leave a Reply Cancel reply


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK