Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
2.3 The Rezk axiom
The notions of identity morphisms and composition of morphisms in categories, provided by the Segal axiom, lead to the notion of an isomorphism in a category:
Definition 2.3.1 (Isomorphisms). Consider a morphism \(f\colon x \to y\) in a category \(C\). We say that \(f\) is invertible, or that it is an isomorphism, if there are commutative triangles in \(C\) of the form
Agda Invertible morphisms
InverseFamily
Definition, checked
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m where field left-inverse right-inverse : MorphismFamily y x left-law : MorphismFamilyIdentification One (MC.Composition.compose C segal left-inverse f) (identity-family x) right-law : MorphismFamilyIdentification One (MC.Composition.compose C segal f right-inverse) (identity-family y)
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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} whereinverse-family-lift
Derivation, checked
inverse-family-lift : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → InverseFamily segal f → IsoLift (MorphismFamily.arrow f)
Proof / implementation
inverse-family-lift = FromInverseFamily.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} wherelift-inverse-family
Derivation, checked
lift-inverse-family : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → IsoLift (MorphismFamily.arrow f) → InverseFamily segal f
Proof / implementation
lift-inverse-family = FromLift.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} whereAbout this correspondence
The book uses two inverse triangles. Rebuild2 packages left and right inverses with composition laws in InverseFamily; inverse-family-lift and lift-inverse-family relate this presentation to the category of pairs of inverse triangles.
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 two inverse triangles
left-inverse
Definition, checked
left-inverse right-inverse : MorphismFamily y 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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} where
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m whereright-inverse
Definition, checked
left-inverse right-inverse : MorphismFamily y 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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} where
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m whereleft-law
Definition, checked
left-law : MorphismFamilyIdentification One (MC.Composition.compose C segal left-inverse f) (identity-family 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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} where
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m whereright-law
Definition, checked
right-law : MorphismFamilyIdentification One (MC.Composition.compose C segal f right-inverse) (identity-family y)
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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} where
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m whereinverse-family-lift
Derivation, checked
inverse-family-lift : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → InverseFamily segal f → IsoLift (MorphismFamily.arrow f)
Proof / implementation
inverse-family-lift = FromInverseFamily.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} wherelift-inverse-family
Derivation, checked
lift-inverse-family : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → IsoLift (MorphismFamily.arrow f) → InverseFamily segal f
Proof / implementation
lift-inverse-family = FromLift.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} whereAbout this correspondence
The book uses two inverse triangles. Rebuild2 packages left and right inverses with composition laws in InverseFamily; inverse-family-lift and lift-inverse-family relate this presentation to the category of pairs of inverse triangles.
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.
An invertible natural transformation is called a natural isomorphism. The Rezk axiom will relate invertible morphisms to the primitive identifications of objects from Definition 1.1.2. We start by defining the category \(\Iso (C)\) of isomorphisms in \(C\).
Agda Invertible natural transformations
InverseFamily
Definition, checked
record InverseFamily (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) : Set m where field left-inverse right-inverse : MorphismFamily y x left-law : MorphismFamilyIdentification One (MC.Composition.compose C segal left-inverse f) (identity-family x) right-law : MorphismFamilyIdentification One (MC.Composition.compose C segal f right-inverse) (identity-family y)
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.Section03.InverseMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} whereinverse-family-lift
Derivation, checked
inverse-family-lift : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → InverseFamily segal f → IsoLift (MorphismFamily.arrow f)
Proof / implementation
inverse-family-lift = FromInverseFamily.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} wherelift-inverse-family
Derivation, checked
lift-inverse-family : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → IsoLift (MorphismFamily.arrow f) → InverseFamily segal f
Proof / implementation
lift-inverse-family = FromLift.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} whereAbout this correspondence
The book uses two inverse triangles. Rebuild2 packages left and right inverses with composition laws in InverseFamily; inverse-family-lift and lift-inverse-family relate this presentation to the category of pairs of inverse triangles.
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.
Definition 2.3.2. Given a category \(C\), we define the category \(\Iso (C)\) via the following pullback diagram:
Agda The category of isomorphisms
Iso
Definition, checked
Iso : CAT Γ → CAT Γ
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.Section03.Isomorphisms where
module _ {Γ : Context} whereInverseTriangles
Definition, checked
InverseTriangles : CAT Γ → CAT Γ
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.Section03.Isomorphisms where
module _ {Γ : Context} whereinverseLongEdges
Definition, checked
inverseLongEdges : (C : CAT Γ) → MAP (InverseTriangles C) (Ar C × Ar C)
Proof / implementation
inverseLongEdges C = pair (edge₁ ∘ firstInverseTriangle C) (edge₁ ∘ secondInverseTriangle 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.Section03.Isomorphisms where
module _ {Γ : Context} whereinverseIdentityEdges
Definition, checked
inverseIdentityEdges : (C : CAT Γ) → MAP (C × C) (Ar C × Ar C)
Proof / implementation
inverseIdentityEdges C = pair (identityArrow ∘ pr₂) (identityArrow ∘ pr₁)
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.Section03.Isomorphisms 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.
Explicitly, an absolute object of \(\Iso (C)\) is a commutative diagram in \(C\) of the form
Agda The two triangles and two objects
isoTriangles
Definition, checked
isoTriangles : (C : CAT Γ) → MAP (Iso C) (InverseTriangles C)
Proof / implementation
isoTriangles C = pullback₁ {f = inverseLongEdges C} {g = inverseIdentityEdges 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.Section03.Isomorphisms where
module _ {Γ : Context} whereisoObjects
Definition, checked
isoObjects : (C : CAT Γ) → MAP (Iso C) (C × C)
Proof / implementation
isoObjects C = pullback₂ {f = inverseLongEdges C} {g = inverseIdentityEdges 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.Section03.Isomorphisms 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.
We denote the composite functor at the top of the diagram by \[ \pi _{\Iso }\colon \Iso (C) \to \Ar (C). \]
Agda The underlying arrow
isoArrow
Definition, checked
isoArrow : (C : CAT Γ) → MAP (Iso C) (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.Section03.Isomorphisms 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.
Notice that by definition a morphism \(f \in \Ar (C)\) is invertible in \(C\) if and only if it lifts to an absolute object of \(\Iso (C)\). We may therefore think of the fiber of \(\pi _{\Iso }\) over \(f\) as the category of ‘proofs that \(f\) is invertible’. The following lemma shows that there is at most one such proof:
Agda A lift to the isomorphism category
IsoLift
Definition, checked
IsoLift : MAP P (Ar C) → 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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} whereinverse-family-lift
Derivation, checked
inverse-family-lift : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → InverseFamily segal f → IsoLift (MorphismFamily.arrow f)
Proof / implementation
inverse-family-lift = FromInverseFamily.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} wherelift-inverse-family
Derivation, checked
lift-inverse-family : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → IsoLift (MorphismFamily.arrow f) → InverseFamily segal f
Proof / implementation
lift-inverse-family = FromLift.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} 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.3.3. For a category \(C\), the map \(\pi _{\Iso }\colon \Iso (C) \to \Ar (C)\) is an embedding.
Agda Isomorphisms embed into arrows
isoArrow-isEmbedding
Derivation, checked
isoArrow-isEmbedding : IsEmbedding (isoArrow C)
Proof / implementation
isoArrow-isEmbedding = embedding-cong Comparison.comparison-arrow (Intersection.embedding (change-right-projection rightInverseArrow Comparison.comparison-arrow (UniversalInverseFibers.right-projection-isEquiv C)) (change-right-projection leftInverseArrow Comparison.comparison-arrow (UniversalInverseFibers.left-projection-isEquiv C))) where module Comparison = InverseComparison C using (square; square-isPullback; comparison-arrow) module Intersection = IntersectionEmbedding rightInverseArrow leftInverseArrow Comparison.square Comparison.square-isPullback using (embedding)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section03.IsomorphismEmbedding where
module _ {Γ : Context} (C : CAT Γ) 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 use the unit and associativity comparisons over prescribed vertices established in Lemma 2.2.6 and Proposition 2.2.7. We need to show that the diagonal \[ \Delta \colon \Iso (C) \to \Iso (C) \times _{\Ar (C)} \Iso (C) \] is an equivalence, or equivalently that the first projection \[ \pr _1\colon \Iso (C) \times _{\Ar (C)} \Iso (C) \to \Iso (C) \] is an equivalence. To this end, consider the two functors \begin {align*} \Ar (C) \times _{\ev _1,C,\ev _0} \Iso (C) &\to \Ar (C) \times _{\ev _1,C,\ev _1} \Iso (C), \qquad (g,f) \mapsto (f \circ g, f) \\ \Iso (C) \times _{\ev _1,C,\ev _0} \Ar (C) &\to \Iso (C) \times _{\ev _0,C,\ev _0} \Ar (C), \qquad (f,h) \mapsto (f,h \circ f). \end {align*}
We claim that these functors are equivalences. For the first functor, note that for \(f \in \Iso (C)\) we may functorially extract both a left inverse \(f_l\) with an identification \(f_l \circ f = \id _{s(f)}\) as well as a right inverse \(f_r\) with an identification \(f \circ f_r = \id _{t(f)}\). Using associativity of composition, a left inverse to the first functor is then given by \((g' ,f) \mapsto (f_l \circ g', f)\), while a right inverse is given by \((g',f) \mapsto (f_r \circ g', f)\). One argues similarly for the second functor.
The claim now follows from the observation that the projection \(\pr _1\) is the left vertical map in the following pullback square, where the right vertical map is the fiber product over \(\Iso (C)\) of the two equivalences just constructed, hence an equivalence itself:
As one expects, the identity morphism of any term \(\Gamma \vdash x:C\) is invertible in the same context:
Agda Identity morphisms are invertible
identityIso
Definition, checked
identityIso : (C : CAT Γ) → MAP C (Iso C)
Proof / implementation
identityIso C = pullback-factor (Identity.identities 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.Section03.Isomorphisms where
module _ {Γ : Context} whereidentityIso-arrow
Derivation, checked
identityIso-arrow : (C : CAT Γ) → (isoArrow C ∘ identityIso C) =₁ identityArrow
Proof / implementation
identityIso-arrow C = constant-restriction d₀ ∙ ((edge₀ ◁ ConeIdentification₁.left (Identity.triangles-image C)) ∙ (comp-assoc (Identity.triangles C) (firstInverseTriangle C) edge₀ ∙ (((edge₀ ∘ firstInverseTriangle C) ◁ identityIso-triangles C) ∙ comp-assoc (identityIso C) (isoTriangles C) (edge₀ ∘ firstInverseTriangle 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.Section03.Isomorphisms where
module _ {Γ : Context} wherelift-inverse-family
Derivation, checked
lift-inverse-family : (segal : IsEquiv (short-edges C)) (f : MorphismFamily x y) → IsoLift (MorphismFamily.arrow f) → InverseFamily segal f
Proof / implementation
lift-inverse-family = FromLift.value
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.Section03.InvertibleMorphismFamilies where
module _ {Γ : Context} {P C : CAT Γ} {x y : MAP P C} 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.
Construction 2.3.4. We construct a functor \(i\colon C \to \Iso (C)\) lifting the functor \(1\colon C \to \Ar (C)\) given by \(x \mapsto \id _x\). Informally, \(i\) sends \(x\) to the following commutative diagram in \(C\):
Agda The identity-isomorphism functor
identityIso
Definition, checked
identityIso : (C : CAT Γ) → MAP C (Iso C)
Proof / implementation
identityIso C = pullback-factor (Identity.identities 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.Section03.Isomorphisms where
module _ {Γ : Context} whereidentityIso-arrow
Derivation, checked
identityIso-arrow : (C : CAT Γ) → (isoArrow C ∘ identityIso C) =₁ identityArrow
Proof / implementation
identityIso-arrow C = constant-restriction d₀ ∙ ((edge₀ ◁ ConeIdentification₁.left (Identity.triangles-image C)) ∙ (comp-assoc (Identity.triangles C) (firstInverseTriangle C) edge₀ ∙ (((edge₀ ∘ firstInverseTriangle C) ◁ identityIso-triangles C) ∙ comp-assoc (identityIso C) (isoTriangles C) (edge₀ ∘ firstInverseTriangle 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.Section03.Isomorphisms 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.
More formally, restriction along the map \(p_{[2]}\colon [2] \to [0]\) induces a functor \(p_{[2]}^*\colon C \to \Triang (C)\), giving a functor \((p_{[2]}^*,p_{[2]}^*)\colon C \to \Triang (C) \times _{\Ar (C)} \Triang (C)\). Since the two relevant edges of this diagram are both the identity on \(x\), this functor factors through \(\Iso (C)\), providing the desired functor \(i\colon C \to \Iso (C)\).
Agda The constant triangle
triangle
Definition, checked
triangle : MAP C (Triangles C)
Proof / implementation
triangle = constantArrow [2] 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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) 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 Two constant triangles with a common edge
triangles
Definition, checked
triangles : MAP C (InverseTriangles C)
Proof / implementation
triangles = pullback-factor common-edge
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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) wherecommon-edge
Definition, checked
common-edge : Cone (edge₀ {C = C}) edge₂ C
Proof / implementation
common-edge = record { left = triangle; right = triangle ; match = (constant-restriction d₂) ⁻¹ ∙ constant-restriction 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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) 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 Both long edges are identities
first-long
Derivation, checked
first-long : ((edge₁ ∘ firstInverseTriangle C) ∘ triangles) =₁ identityArrow
Proof / implementation
first-long = long-edge (firstInverseTriangle C) (ConeIdentification₁.left triangles-image)
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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) wheresecond-long
Derivation, checked
second-long : ((edge₁ ∘ secondInverseTriangle C) ∘ triangles) =₁ identityArrow
Proof / implementation
second-long = long-edge (secondInverseTriangle C) (ConeIdentification₁.right triangles-image)
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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) 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 Factor through the isomorphism category
identities
Definition, checked
identities : Cone (inverseLongEdges C) (inverseIdentityEdges C) C
Proof / implementation
identities = record { left = triangles; right = pair (id C) (id C) ; match = identity-pair ⁻¹ ∙ (pair⁼ first-long second-long ∙ pair-pre (edge₁ ∘ firstInverseTriangle C) (edge₁ ∘ secondInverseTriangle C) triangles) }
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.Section03.Isomorphisms where
module _ {Γ : Context} where
module Identity (C : CAT Γ) whereidentityIso
Definition, checked
identityIso : (C : CAT Γ) → MAP C (Iso C)
Proof / implementation
identityIso C = pullback-factor (Identity.identities 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.Section03.Isomorphisms 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.
By construction the following diagram commutes:
Axiom F (Rezk axiom). For any category \(C\), the functor \(i\colon C \to \Iso (C)\) is an equivalence.
Agda The Rezk axiom
rezk-isEquiv
Assumption, type checked
rezk-isEquiv : (C : CAT Γ) → IsEquiv (identityIso 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.Section03.RezkAxiom 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.
Together with representability of identifications, the Rezk axiom identifies the anima of identifications between two objects with the category of isomorphisms between them:
Corollary 2.3.5. For every category \(C\) and absolute objects \(x,y\) of \(C\), there is an equivalence \[ (x=y)\simeq *\times _{C\times C}\Iso (C), \] where the maps defining the fiber product are \((x,y)\colon *\to C\times C\) and \((\ev _0,\ev _1)\colon \Iso (C)\to C\times C\).
Agda Identifications and invertible arrows
identification-to-iso-isEquiv
Derivation, checked
identification-to-iso-isEquiv : IsEquiv identification-to-iso
Proof / implementation
identification-to-iso-isEquiv = equiv-compose diagonal-factor (pullback-map change) diagonal-isPullback Change.pullback-map-isEquiv
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.Section03.RezkFibers where
module _ {Γ : Context} where
module IdentificationFiber (C : CAT Γ) (R : IsEquiv (identityIso C))
(x y : MAP One C) whereIsoBetween
Definition, checked
IsoBetween : {C : CAT Γ} → MAP One C → MAP One C → CAT Γ
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.Section03.RezkFibers 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. By Axiom B.7, the anima \((x=y)\) is the pullback of \(x,y\colon *\to C\). Applying Lemma 1.6.13, we obtain a pullback square
Agda The diagonal square representing identifications
diagonal-cone
Definition, checked
diagonal-cone : Cone point diagonal (Equal x y)
Proof / implementation
diagonal-cone = cone-swap D.diagonal-cone
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.Section03.RezkFibers where
module _ {Γ : Context} where
module IdentificationFiber (C : CAT Γ) (R : IsEquiv (identityIso C))
(x y : MAP One C) wherediagonal-isPullback
Derivation, checked
diagonal-isPullback : IsPullback diagonal-cone
Proof / implementation
diagonal-isPullback = SwappedCone.isPullback D.diagonal-cone D.diagonal-isPullback
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.Section03.RezkFibers where
module _ {Γ : Context} where
module IdentificationFiber (C : CAT Γ) (R : IsEquiv (identityIso C))
(x y : MAP One C) 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 Rezk axiom identifies \(C\) with \(\Iso (C)\) through the equivalence \(i\), and \((\ev _0,\ev _1)i=\Delta \). Replacing \(C\) by \(\Iso (C)\) therefore identifies this pullback with the required fiber. □
Agda The Rezk equivalence used in the fiber comparison
identification-to-iso
Definition, checked
identification-to-iso : MAP (Equal x y) (IsoBetween x y)
Proof / implementation
identification-to-iso = pullback-map change ∘ diagonal-factor
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.Section03.RezkFibers where
module _ {Γ : Context} where
module IdentificationFiber (C : CAT Γ) (R : IsEquiv (identityIso C))
(x y : MAP One C) whereidentification-to-iso-isEquiv
Derivation, checked
identification-to-iso-isEquiv : IsEquiv identification-to-iso
Proof / implementation
identification-to-iso-isEquiv = equiv-compose diagonal-factor (pullback-map change) diagonal-isPullback Change.pullback-map-isEquiv
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.Section03.RezkFibers where
module _ {Γ : Context} where
module IdentificationFiber (C : CAT Γ) (R : IsEquiv (identityIso C))
(x y : MAP One C) 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.
Corollary 2.3.6. For functors \(f,g\colon C\to D\), there is an equivalence \[ (f=g)\simeq *\times _{\Fun (C,D)\times \Fun (C,D)}\Iso (\Fun (C,D)), \] where the maps defining the fiber product are \((f,g)\) and \((\ev _0,\ev _1)\). Thus identifications of functors are equivalently natural isomorphisms of functors.
Agda Identifications and natural isomorphisms
identification-to-natural-iso-isEquiv
Derivation, checked
identification-to-natural-iso-isEquiv : IsEquiv identification-to-natural-iso
Proof / implementation
identification-to-natural-iso-isEquiv = equiv-compose Names.naming Fiber.identification-to-iso Names.naming-isEquiv Fiber.identification-to-iso-isEquiv
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.Section03.NaturalIsomorphisms where
module _ {Γ : Context} where
module NaturalIdentification {C D : CAT Γ}
(R : IsEquiv (identityIso (Fun C D))) (f g : MAP C D) 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 natural-isomorphism fiber
NatIsoBetween
Definition, checked
NatIsoBetween : {C D : CAT Γ} → MAP C D → MAP C D → CAT Γ
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.Section03.NaturalIsomorphisms where
module _ {Γ : Context} whereidentification-to-natural-iso
Definition, checked
identification-to-natural-iso : MAP (Equal f g) (NatIsoBetween f g)
Proof / implementation
identification-to-natural-iso = Fiber.identification-to-iso ∘ Names.naming
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.Section03.NaturalIsomorphisms where
module _ {Γ : Context} where
module NaturalIdentification {C D : CAT Γ}
(R : IsEquiv (identityIso (Fun C D))) (f g : MAP C D) 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. By Definition 1.7.3, currying identifies the anima \((f=g)\) with the anima of identifications between the corresponding absolute objects of \(\Fun (C,D)\). Applying Corollary 2.3.5 to these objects gives the asserted equivalence. □
Agda Currying identifications of functors
naming
Definition, checked
naming : MAP (Equal f g) (Equal (funName f) (funName g))
Proof / implementation
naming = IsEquiv.inverse decoding-isEquiv
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.Section03.NaturalIsomorphisms where
module IdentificationNames {Γ : Context} {C D : CAT Γ} (f g : MAP C D) wherenaming-isEquiv
Derivation, checked
naming-isEquiv : IsEquiv naming
Proof / implementation
naming-isEquiv = equiv-inverse decoding-isEquiv
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.Section03.NaturalIsomorphisms where
module IdentificationNames {Γ : Context} {C D : CAT Γ} (f g : MAP C D) 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.
Corollary 2.3.7. For a category \(C\), the functor \(p_{[1]}^*\colon C \to \Ar (C)\) is an embedding.
Agda Constant arrows form an embedding
identityArrow-isEmbedding
Derivation, checked
identityArrow-isEmbedding : (C : CAT Γ) → IsEmbedding (identityArrow {C = C})
Proof / implementation
identityArrow-isEmbedding C = ConditionalEmbedding.identityArrow-isEmbedding C (rezk-isEquiv 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.Section03.RezkAxiom 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 functor factors as \(C \xrightarrow {i} \Iso (C) \xrightarrow {\pi _{\Iso }} \Ar (C)\). The first functor is an equivalence by the Rezk axiom, while the second one is an embedding by Lemma 2.3.3. The claim follows. □
Agda Factor the identity-arrow functor
identityIso-arrow
Derivation, checked
identityIso-arrow : (C : CAT Γ) → (isoArrow C ∘ identityIso C) =₁ identityArrow
Proof / implementation
identityIso-arrow C = constant-restriction d₀ ∙ ((edge₀ ◁ ConeIdentification₁.left (Identity.triangles-image C)) ∙ (comp-assoc (Identity.triangles C) (firstInverseTriangle C) edge₀ ∙ (((edge₀ ∘ firstInverseTriangle C) ◁ identityIso-triangles C) ∙ comp-assoc (identityIso C) (isoTriangles C) (edge₀ ∘ firstInverseTriangle 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.Section03.Isomorphisms 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 first factor is an equivalence
rezk-isEquiv
Assumption, type checked
rezk-isEquiv : (C : CAT Γ) → IsEquiv (identityIso 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.Section03.RezkAxiom where
module _ {Γ : Context} whereidentityArrow-isEmbedding
Derivation, checked
identityArrow-isEmbedding : (C : CAT Γ) → IsEmbedding (identityArrow {C = C})
Proof / implementation
identityArrow-isEmbedding C = ConditionalEmbedding.identityArrow-isEmbedding C (rezk-isEquiv 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.Section03.RezkAxiom 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.
Supplementary notes
- Reordering inverse conditions AI-generated