Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.5 Recognizing animae
Animae enter the foundational language primitively as homotopy-coherent collections, whereas the groupoid condition is a property of a category expressed by invertibility of its morphisms. The two notions enter the theory independently. The following axiom asserts that they determine the same class of categories, allowing us to pass between collection-oriented anima language and structural groupoid arguments.
Axiom G (Groupoid recognition axiom). A category is an anima if and only if it is a groupoid.
Agda Groupoid recognition
anima-isGroupoid
Assumption, type checked
anima-isGroupoid : {C : CAT Γ} → isAn C → IsGroupoid 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.Section05.Recognition where
module _ {Γ : Context} wheregroupoid-isAn
Assumption, type checked
groupoid-isAn : {C : CAT Γ} → IsGroupoid C → isAn 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.Section05.Recognition 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.
Proposition 2.5.1. For any anima \(X\) and any category \(A\), the canonical functor \[ \imath _{A,X}\colon \Map (A,X)\iso \Fun (A,X) \] is an equivalence.
Agda Mapping into an anima
mappingInclusion-isEquiv
Derivation, checked
mappingInclusion-isEquiv : (A X : CAT Γ) → isAn X → IsEquiv (mappingInclusion A X)
Proof / implementation
mappingInclusion-isEquiv A X h = equiv-transport (coreFunComparison-inclusion A X) (equiv-compose (coreFunComparison A X) (coreInclusion (Fun A X)) (coreFunComparison-isEquiv A X) (core-of-anima (Fun A X) (functor-isAn A X h)))
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.Section05.AnimaTargets 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
Lemma 2.5.2. For functors \(X\to C\) and \(Y\to C\) with \(X\) and \(Y\) animae, the pullback \(X\times _C Y\) is an anima.
Agda Pullbacks of animae
pullback-of-animae
Derivation, checked
pullback-of-animae : {X Y C : CAT Γ} (f : MAP X C) (g : MAP Y C) → isAn X → isAn Y → isAn (Pullback f g)
Proof / implementation
pullback-of-animae f g ex ey = groupoid-isAn (pullback-isGroupoid f g (anima-isGroupoid ex) (anima-isGroupoid 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.Section05.PullbackAnimae 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 Lemma 2.4.9 and the groupoid recognition axiom. □
Corollary 2.5.3. Let \(C\) be a category. Then the functor \(\imath _C\colon C^{\simeq } \to C\) is an embedding.
Agda The core inclusion is an embedding
coreInclusion-isEmbedding
Derivation, checked
coreInclusion-isEmbedding : (C : CAT Γ) → IsEmbedding (coreInclusion C)
Proof / implementation
coreInclusion-isEmbedding C = embedding-from-projection-isEquiv i (post-tests-animae (pullback-of-animae i i (core-isAn C) (core-isAn C)) (core-isAn C) projection tested) where i : MAP (Core C) C i = coreInclusion C projection : MAP (Pullback i i) (Core C) projection = pullback₁ {f = i} {g = i} tested : (X : CAT Γ) → isAn X → IsEquiv (mapPost {C = X} projection) tested X xAn = left-isEquiv-from-isPullback (core-universal X C xAn) (MappingPullback.square X i i) (MappingPullback.square-isPullback X i i)
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.Section05.PullbackAnimae 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 diagonal \(C^{\simeq } \to C^{\simeq } \times _C C^{\simeq }\) is an equivalence. Its source is an anima, and its target is an anima by Lemma 2.5.2. By Proposition 1.4.11, it therefore suffices to show that for every anima \(Z\) the induced map \[ \Map (Z,C^{\simeq }) \to \Map (Z,C^{\simeq } \times _C C^{\simeq }) \simeq \Map (Z,C^{\simeq }) \times _{\Map (Z,C)} \Map (Z,C^{\simeq }) \] is an equivalence, i.e. we need to show that the map \(\Map (Z,C^{\simeq }) \to \Map (Z,C)\) is an embedding. But this map is even an equivalence by Corollary 1.4.13. □
Lemma 2.5.4. For any two categories \(C\) and \(D\), the canonical map \[ \Ar (C) \sqcup \Ar (D) \to \Ar (C \sqcup D) \] is an equivalence.
Agda Arrows in a coproduct
arrowCopair-isEquiv
Derivation, checked
arrowCopair-isEquiv : (C D : CAT Γ) → IsEquiv (arrowCopair C D)
Proof / implementation
arrowCopair-isEquiv C D = pullback-cover-isEquiv (funPost {C = [1]} in₁) (funPost {C = [1]} in₂) (funPost {C = [1]} (coproductMap (terminate C) (terminate D))) (mappedCone [1] (coproductSquare₁ (terminate C) (terminate D))) (mappedCone [1] (coproductSquare₂ (terminate C) (terminate D))) (fun-preserves-pullback [1] _ (inclusion₁-isPullback (terminate C) (terminate D))) (fun-preserves-pullback [1] _ (inclusion₂-isPullback (terminate C) (terminate D))) two-point-cover
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.Section05.ArrowCoproducts 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. When \(C = * = D\), we have \(\Ar (*) \simeq *\) and the statement says that the map \(* \sqcup * \to \Ar (* \sqcup *)\) is an equivalence. Since \(*\sqcup *\) is an anima, it is a groupoid by the recognition axiom. The claim follows, since for a groupoid \(X\) the functor \(X \to \Ar (X)\) is an equivalence. For arbitrary \(C\) and \(D\), it follows from Lemma 1.7.11 that there are pullback squares
Agda The two-point case
two-point-isAn
Derivation, checked
two-point-isAn : isAn (One {Γ = Γ} ⊔ One)
Proof / implementation
two-point-isAn = equivalence-reflects-anima intervalCore intervalCore-isEquiv (core-isAn [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.Section05.ArrowCoproducts where
module _ {Γ : Context} wheretwo-point-cover
Derivation, checked
two-point-cover : IsEquiv (arrowCopair (One {Γ = Γ}) One)
Proof / implementation
two-point-cover = equiv-cancel-right (coproductMap identityArrow identityArrow) (arrowCopair One One) (coproductMap-isEquiv identityArrow identityArrow terminal-isGroupoid terminal-isGroupoid) (equiv-transport ((identity-copair One One) ⁻¹) (anima-isGroupoid two-point-isAn))
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.Section05.ArrowCoproducts 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 claim thus follows from Lemma 1.6.16. □
Corollary 2.5.5. Let \(X\) and \(Y\) be groupoids. Then their disjoint union \(X \sqcup Y\) is a groupoid.
Agda Coproducts of groupoids
coproduct-isGroupoid
Derivation, checked
coproduct-isGroupoid : (C D : CAT Γ) → IsGroupoid C → IsGroupoid D → IsGroupoid (C ⊔ D)
Proof / implementation
coproduct-isGroupoid C D eC eD = equiv-transport (identity-copair C D) (equiv-compose (coproductMap identityArrow identityArrow) (arrowCopair C D) (coproductMap-isEquiv identityArrow identityArrow eC eD) (arrowCopair-isEquiv C D))
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.Section05.ArrowCoproducts 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 map \(X \sqcup Y \to \Ar (X \sqcup Y)\) factors as \[ X \sqcup Y \to \Ar (X) \sqcup \Ar (Y) \to \Ar (X \sqcup Y), \] where the first map is the disjoint union of the two equivalences \(X \iso \Ar (X)\) and \(Y \iso \Ar (Y)\), while the second is the equivalence from Lemma 2.5.4. □
Corollary 2.5.6. The empty category \(\emptyset \) is an anima. For animae \(X\) and \(Y\), the coproduct \(X\sqcup Y\) is an anima.
Agda The initial category is an anima
zero-isAn
Derivation, checked
zero-isAn : isAn (Zero {Γ = Γ})
Proof / implementation
zero-isAn = groupoid-isAn empty-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.Section05.Recognition 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 Coproducts of animae
coproduct-isAn
Derivation, checked
coproduct-isAn : (C D : CAT Γ) → isAn C → isAn D → isAn (C ⊔ D)
Proof / implementation
coproduct-isAn C D cAn dAn = groupoid-isAn (coproduct-isGroupoid C D (anima-isGroupoid cAn) (anima-isGroupoid dAn))
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.Section05.ArrowCoproducts 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 Initial category and coproducts of animae
zero-isAn
Derivation, checked
zero-isAn : isAn (Zero {Γ = Γ})
Proof / implementation
zero-isAn = groupoid-isAn empty-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.Section05.Recognition where
module _ {Γ : Context} wherecoproduct-isAn
Derivation, checked
coproduct-isAn : (C D : CAT Γ) → isAn C → isAn D → isAn (C ⊔ D)
Proof / implementation
coproduct-isAn C D cAn dAn = groupoid-isAn (coproduct-isGroupoid C D (anima-isGroupoid cAn) (anima-isGroupoid dAn))
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.Section05.ArrowCoproducts 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
Supplementary notes
- Constant diagrams and the exponential law AI-generated