Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.4 Groupoids
A category is called a groupoid if all its morphisms are invertible. In the synthetic setting, we need to phrase this condition for arbitrary terms of the arrow category, as follows.
Definition 2.4.1 (Groupoid). We say that a category \(C\) is a groupoid if in an arbitrary categorical context, every morphism expression \(f\colon x \to y\) in \(C\) is an isomorphism. Explicitly: for every category \(\Gamma \) and every functor \(f\colon \Gamma \to \Ar (C)\), there exists a dashed arrow \(\tilde {f}\) making the following diagram commute:
Agda Groupoids
AllArrowsInvertible
Definition, checked
AllArrowsInvertible : CAT Γ → Set (c ⊔ m)
Proof / implementation
AllArrowsInvertible C = {P : CAT Γ} → (f : MAP P (Ar C)) → Factorization (isoArrow C) f
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereAbout this correspondence
The formalization packages invertibility as lifting each arrow family through Iso. The equivalence with inverse-family data is proved in InvertibleMorphismFamilies.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The following result provides various alternative formulations for a category to be a groupoid:
Proposition 2.4.2. Let \(X\) be a category. Then the following conditions are equivalent:
Agda Characterizations of groupoids
lifting-to-groupoid
Derivation, checked
lifting-to-groupoid : {C : CAT Γ} → AllArrowsInvertible C → IsGroupoid C
Proof / implementation
lifting-to-groupoid given = identity-section-to-groupoid (iso-section-to-identity-section (lifting-to-section given))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} wheregroupoid-to-lifting
Derivation, checked
groupoid-to-lifting : {C : CAT Γ} → IsGroupoid C → AllArrowsInvertible C
Proof / implementation
groupoid-to-lifting given = section-to-lifting (identity-section-to-iso-section (groupoid-to-identity-section given))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} wherelifting-to-section
Definition, checked
lifting-to-section : {C : CAT Γ} → AllArrowsInvertible C → Section (isoArrow C)
Proof / implementation
lifting-to-section {C} given = record { section = factor universal ; section-law = (triangle universal) ⁻¹ } where universal : Factorization (isoArrow C) (id (Ar C)) universal = given {P = Ar C} (id (Ar C))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} wheresection-to-lifting
Definition, checked
section-to-lifting : {C : CAT Γ} → Section (isoArrow C) → AllArrowsInvertible C
Proof / implementation
section-to-lifting {C} given f = functor-over (Section.section given ∘ f) (comp-unitˡ f ∙ (((Section.section-law given) ⁻¹ ▷ f) ∙ (comp-assoc f (Section.section given) (isoArrow C)) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereiso-section-to-identity-section
Definition, checked
iso-section-to-identity-section : {C : CAT Γ} → Section (isoArrow C) → Section (identityArrow {C = C})
Proof / implementation
iso-section-to-identity-section {C} given = record { section = j ∘ s ; section-law = comp-assoc s j (identityArrow {C = C}) ∙ (((inverse-image ▷ s) ⁻¹) ∙ Section.section-law given) } where s : MAP (Ar C) (Iso C) s = Section.section given j : MAP (Iso C) C j = IsEquiv.inverse (rezk-isEquiv C) inverse-image : (identityArrow {C = C} ∘ j) =₁ isoArrow C inverse-image = comp-unitʳ (isoArrow C) ∙ (((isoArrow C) ◁ ((IsEquiv.right-inverse-law (rezk-isEquiv C)) ⁻¹)) ∙ (comp-assoc j (identityIso C) (isoArrow C) ∙ (identityIso-arrow C ▷ j) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereidentity-section-to-iso-section
Definition, checked
identity-section-to-iso-section : {C : CAT Γ} → Section (identityArrow {C = C}) → Section (isoArrow C)
Proof / implementation
identity-section-to-iso-section {C} given = record { section = identityIso C ∘ s ; section-law = comp-assoc s (identityIso C) (isoArrow C) ∙ (((identityIso-arrow C ▷ s) ⁻¹) ∙ Section.section-law given) } where s : MAP (Ar C) C s = Section.section given
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereidentity-section-to-groupoid
Derivation, checked
identity-section-to-groupoid : {C : CAT Γ} → Section (identityArrow {C = C}) → IsGroupoid C
Proof / implementation
identity-section-to-groupoid {C} given = section-retraction-isEquiv given (record { retraction = ev₀ {C = C} ; retraction-law = (identity-source {C = C}) ⁻¹ })
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.Groupoids where
module _ {Γ : Context} wheregroupoid-to-identity-section
Derivation, checked
groupoid-to-identity-section : {C : CAT Γ} → IsGroupoid C → Section (identityArrow {C = C})
Proof / implementation
groupoid-to-identity-section {C} = equiv-section {f = identityArrow {C = C}}
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.Groupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
- (1)
-
The category \(X\) is a groupoid;
- (2)
-
The functor \(\pi _{\Iso }\colon \Iso (X) \to \Ar (X)\) admits a section, in the sense of Definition 1.3.2;
- (3)
-
The functor \(p_{[1]}^*\colon X \to \Ar (X)\), induced by the map \(p_{[1]}\colon [1] \to *\), admits a section;
- (4)
-
The functor \(p_{[1]}^*\colon X \to \Ar (X)\) is an equivalence.
Proof
Proof. To see that (1) implies (2), take \(\Gamma = \Ar (X)\) and let \(f = \id _{\Ar (X)}\), so that \(s = \tilde {f}\) provides a section. Conversely, if \(s\colon \Ar (X) \to \Iso (X)\) is a section of \(\pi _{\Iso }\), a lift \(\tilde {f}\) of \(f\) may be given as \(\tilde {f} := s \circ f\).
Agda The groupoid lifting criterion
lifting-to-section
Definition, checked
lifting-to-section : {C : CAT Γ} → AllArrowsInvertible C → Section (isoArrow C)
Proof / implementation
lifting-to-section {C} given = record { section = factor universal ; section-law = (triangle universal) ⁻¹ } where universal : Factorization (isoArrow C) (id (Ar C)) universal = given {P = Ar C} (id (Ar C))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Agda The groupoid lifting criterion
section-to-lifting
Definition, checked
section-to-lifting : {C : CAT Γ} → Section (isoArrow C) → AllArrowsInvertible C
Proof / implementation
section-to-lifting {C} given f = functor-over (Section.section given ∘ f) (comp-unitˡ f ∙ (((Section.section-law given) ⁻¹ ▷ f) ∙ (comp-assoc f (Section.section given) (isoArrow C)) ⁻¹))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.GroupoidCharacterization where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
The fact that (2) and (3) are equivalent is immediate from the following commutative diagram:
using that the map \(i\) is an equivalence by Axiom F. Finally, note that the functor \((p_{[1]})^*\) always admits a retraction given by \(\ev _0\colon \Ar (X) \to X\), and thus the equivalence between (3) and (4) is an instance of Lemma 1.3.3. □
Convention 2.4.3. From now on we will mostly take (4) as our working definition of groupoids.
Agda The constant-arrow definition
IsGroupoid
Definition, checked
IsGroupoid : CAT Γ → Set m
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.Groupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Example 2.4.4. The terminal category \(*\) is a groupoid: there is a commutative triangle
Agda The terminal category is a groupoid
terminal-isGroupoid
Derivation, checked
terminal-isGroupoid : IsGroupoid (One {Γ = Γ})
Proof / implementation
terminal-isGroupoid = groupoid-from-source-equivalence {C = One {Γ = Γ}} (equiv-transport (terminal-identification (terminate (Ar (One {Γ = Γ}))) (ev₀ {C = One {Γ = Γ}})) (funTerminal-isEquiv ([1] {Γ = Γ})))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.BasicClosure where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
and since the bottom and right diagonal maps are equivalences (see Lemma 1.7.9) the claim follows by 2-out-of-3.
Example 2.4.5. If \(X\) and \(Y\) are groupoids, then their product \(X \times Y\) is a groupoid. This is an immediate consequence of Lemma 1.7.10.
Agda Products of groupoids
product-isGroupoid
Derivation, checked
product-isGroupoid : {C D : CAT Γ} → IsGroupoid C → IsGroupoid D → IsGroupoid (C × D)
Proof / implementation
product-isGroupoid {C} {D} left right = equiv-cancel-left (identityArrow {C = C × D}) (ProductComparison.forward [1] C D) (ProductComparison.forward-isEquiv [1] C D) (equiv-transport ((constant-product [1] C D) ⁻¹) (productMap-isEquiv (identityArrow {C = C}) (identityArrow {C = D}) left right))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.BasicClosure where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Lemma 2.4.6. Let \(C \to D\) be an equivalence of categories. Then \(C\) is a groupoid if and only if \(D\) is a groupoid.
Agda Invariance under equivalence
equivalence-preserves-groupoid
Derivation, checked
equivalence-preserves-groupoid : {C D : CAT Γ} (F : MAP C D) → IsEquiv F → IsGroupoid C → IsGroupoid D
Proof / implementation
equivalence-preserves-groupoid {C} {D} F e given = equiv-cancel-right F (identityArrow {C = D}) e (equiv-transport (constant-natural [1] {C = C} {D = D} F) (equiv-compose (identityArrow {C = C}) (funPost {C = [1]} F) given (funPost-isEquiv {A = [1]} F e)))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.BasicClosure where
module _ {Γ : Context} whereequivalence-reflects-groupoid
Derivation, checked
equivalence-reflects-groupoid : {C D : CAT Γ} (F : MAP C D) → IsEquiv F → IsGroupoid D → IsGroupoid C
Proof / implementation
equivalence-reflects-groupoid {C} {D} F e = equivalence-preserves-groupoid {C = D} {D = C} (IsEquiv.inverse e) (equiv-inverse e)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.BasicClosure where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This follows from the following commutative diagram:
Here the bottom functor is again an equivalence by the functoriality of functor categories, Construction 1.7.7. □
Lemma 2.4.7. Let \(X\) be a groupoid. Then for every category \(C\), the functor category \(\Fun (C,X)\) is a groupoid.
Agda Functor categories into groupoids
functor-isGroupoid
Derivation, checked
functor-isGroupoid : (K : CAT Γ) {X : CAT Γ} → IsGroupoid X → IsGroupoid (Fun K X)
Proof / implementation
functor-isGroupoid K {X} given = equiv-cancel-left (identityArrow {C = Fun K X}) (ExponentialLaw.forward [1] K X) (ExponentialLaw.forward-isEquiv [1] K X) (equiv-cancel-left (ExponentialLaw.forward [1] K X ∘ identityArrow {C = Fun K X}) (funPre {D = X} (swap {C = K} {D = [1]})) (funPre-isEquiv {E = X} (swap {C = K} {D = [1]}) (swap-isEquiv K [1])) (equiv-transport ((constant-exponential [1] K X) ⁻¹) (equiv-compose (funPost {C = K} (identityArrow {C = X})) (ExponentialLaw.forward K [1] X) (funPost-isEquiv {A = K} (identityArrow {C = X}) given) (ExponentialLaw.forward-isEquiv K [1] X))))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.FunctorGroupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. This follows from the fact that the map \(\Fun (C,X) \to \Ar (\Fun (C,X))\) is equivalent to the map \(\Fun (C,X) \to \Fun (C,\Ar (X))\) induced by the equivalence \(X \iso \Ar (X)\). □
Lemma 2.4.8. Groupoids are closed under retracts: if \(X\) is a groupoid and \(Y\) is a retract of \(X\), then \(Y\) is also a groupoid.
Agda Retracts of groupoids
retract-isGroupoid
Derivation, checked
retract-isGroupoid : {X Y : CAT Γ} (s : MAP Y X) (r : MAP X Y) → (r ∘ s) =₁ id Y → IsGroupoid X → IsGroupoid Y
Proof / implementation
retract-isGroupoid {X} {Y} s r ε given = identity-section-to-groupoid {C = Y} (constant-section-retract [1] {X = X} {Y = Y} s r ε (groupoid-to-identity-section {C = X} given))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.RetractGroupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. If \(Y\) is a retract of \(X\), then the functor \(Y \to \Ar (Y)\) is a retract of the functor \(X \to \Ar (X)\). In particular, if the latter is an equivalence then so is the former by Lemma 1.3.9. □
Lemma 2.4.9. Consider functors \(f\colon X \to C\) and \(g\colon Y \to C\) and assume that \(X\) and \(Y\) are groupoids. Then the pullback \(X \times _C Y\) is a groupoid.
Agda Pullbacks of groupoids over a category
pullback-isGroupoid
Derivation, checked
pullback-isGroupoid : {X Y C : CAT Γ} (f : MAP X C) (g : MAP Y C) → IsGroupoid X → IsGroupoid Y → IsGroupoid (Pullback f g)
Proof / implementation
pullback-isGroupoid = PullbackGroupoid.isGroupoid
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.PullbackGroupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. The functor \(X \times _C Y \to \Ar (X \times _C Y)\) factors as \[ X \times _C Y \iso X \times _{\Ar (C)} Y \iso \Ar (X) \times _{\Ar (C)} \Ar (Y) \simeq \Ar (X \times _C Y). \] Here the second functor is an equivalence since \(X\) and \(Y\) are groupoids. The last equivalence is Lemma 1.7.11. Finally, we claim that the first functor is a pullback of the diagonal of the embedding \(i\colon C \to \Ar (C)\) from Corollary 2.3.7 and hence is an equivalence. To see this, consider the following commutative diagram:
The right bottom square, the right outer rectangle and the top outer rectangle are pullback squares by Lemma 1.6.13. It thus follows from Lemma 1.6.11 that also the top left square is a pullback square. □
Lemma 2.4.10. Consider a pullback square
Agda Pullback squares of groupoids
pullback-square-isGroupoid
Derivation, checked
pullback-square-isGroupoid : {X Y C T : CAT Γ} {f : MAP X C} {g : MAP Y C} (s : Cone f g T) → IsPullback s → IsGroupoid X → IsGroupoid Y → IsGroupoid T
Proof / implementation
pullback-square-isGroupoid {f = f} {g} s es ex ey = equivalence-reflects-groupoid (pullback-factor s) es (pullback-isGroupoid f g ex ey)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.PullbackGroupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
of categories. If \(X\), \(Y\) and \(Y'\) are groupoids, then so is \(X'\).
Proof
Proof. This is a special case of Lemma 2.4.9. □
Lemma 2.4.11. The empty category \(\emptyset \) is a groupoid.
Agda The empty category is a groupoid
empty-isGroupoid
Derivation, checked
empty-isGroupoid : IsGroupoid (Zero {Γ = Γ})
Proof / implementation
empty-isGroupoid = groupoid-from-source-equivalence {C = Zero {Γ = Γ}} (into-zero-isEquiv (ev₀ {C = Zero {Γ = Γ}}))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.Groupoids where
module _ {Γ : Context} whereAbout this correspondence
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Proof
Proof. We need to show that the functor \(\emptyset \to \Ar (\emptyset )\) is an equivalence, or equivalently that the map \(\ev _0\colon \Ar (\emptyset ) \to \emptyset \) is an equivalence. But this is immediate from Axiom B.4’. □
Supplementary notes
- Constant diagrams and the exponential law AI-generated