Chapter 1 code: rebuild2 edition, checked 14 October 2026. Included modules and omissions.
Read the Agda code alongside the book.Click dotted-underlined prose to read its Agda code alongside the book. Browse all code.
1.4 Mapping animae
We now introduce the mapping anima between two categories \(C\) and \(D\): an anima whose objects are functors from \(C\) to \(D\). The mapping animae will play an important role in the development of the theory: frequently, we may check conditions at the level of mapping animae. We introduce \(\Map (C,D)\) via its universal property in terms of currying/uncurrying functors.
Axiom B.3 (Evaluation and currying for mapping animae). For categories \(C,D\), there is an anima \(\Map (C,D)\) equipped with an evaluation functor \[ \ev _{\Map }\colon \Map (C,D)\times C\longrightarrow D. \] If \(X\) is an anima and \(h:X\times C\to D\) is a functor, there is a functor \(h_c\colon X\to \Map (C,D)\) equipped with an identification \((h_c)^u= h\), where \[ a^u:=\ev _{\Map }\circ (a\times \id _C):X\times C\longrightarrow D. \] For any \(a,b\colon X\to \Map (C,D)\), the functor \[ (-)^u\colon (a= b)\longrightarrow (a^u= b^u) \] induced by product functoriality and postwhiskering with evaluation is an equivalence.
Agda Evaluation and currying
Map
Assumption, type checked
Map : CAT Γ → 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} wheremap-isAn
Assumption, type checked
map-isAn : (C D : CAT Γ) → isAn (Map 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} wheremapEval
Assumption, type checked
mapEval : {C D : CAT Γ} → MAP (Map C D × 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} wheremapCurry
Assumption, type checked
mapCurry : {C D : CAT Γ} → isAn A → MAP (A × C) D → Term (Map 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} wheremapCurry-β
Assumption, type checked
mapCurry-β : {C D : CAT Γ} (aAn : isAn A) (h : MAP (A × C) D) → uncurry (mapCurry aAn h) =₁ 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereuncurry⁼-isEquiv
Assumption, type checked
uncurry⁼-isEquiv : {C D : CAT Γ} (aAn : isAn A) (f g : Term (Map C D)) → IsEquiv (uncurry⁼-functor f g)
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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 mapping anima
Map
Assumption, type checked
Map : CAT Γ → 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} wheremap-isAn
Assumption, type checked
map-isAn : (C D : CAT Γ) → isAn (Map 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 evaluation functor
mapEval
Assumption, type checked
mapEval : {C D : CAT Γ} → MAP (Map C D × 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Currying with an anima parameter
mapCurry
Assumption, type checked
mapCurry : {C D : CAT Γ} → isAn A → MAP (A × C) D → Term (Map 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 currying beta comparison
mapCurry-β
Assumption, type checked
mapCurry-β : {C D : CAT Γ} (aAn : isAn A) (h : MAP (A × C) D) → uncurry (mapCurry aAn h) =₁ 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Definition of uncurrying
uncurry
Definition, checked
uncurry : {C D : CAT Γ} → Term (Map C D) → MAP (A × 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Uncurrying on isomorphism animae
uncurry⁼-functor
Derivation, checked
uncurry⁼-functor : {C D : CAT Γ} (f g : Term (Map C D)) → MAP (Equal f g) (Equal (uncurry f) (uncurry g))
Proof / implementation
uncurry⁼-functor {C = C} f g = postWhisker mapEval ∘ productMap-cong (id (Equal f g)) (const (id₌ (id 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 uncurrying action is an equivalence
uncurry⁼-isEquiv
Assumption, type checked
uncurry⁼-isEquiv : {C D : CAT Γ} (aAn : isAn A) (f g : Term (Map C D)) → IsEquiv (uncurry⁼-functor f g)
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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 refer to the functor \(h_c\) as the currying of \(h\), and to \(a^u\) as the uncurrying of \(a\). Note that the universal property of \(\Map \) only holds for anima parameters. A more general form of currying with an arbitrary category as parameter will be provided by functor categories in Section 1.7.
Agda The anima-parameter hypothesis
mapCurry
Assumption, type checked
mapCurry : {C D : CAT Γ} → isAn A → MAP (A × C) D → Term (Map 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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereuncurry⁼-isEquiv
Assumption, type checked
uncurry⁼-isEquiv : {C D : CAT Γ} (aAn : isAn A) (f g : Term (Map C D)) → IsEquiv (uncurry⁼-functor f g)
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.Chapter01.Section04.MappingAnimae where
module _ {Γ : Context} where
module _ {A : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 1.4.1 (Functors as points of mapping animae). A functor \(f\colon C\to D\) determines a point \(\ulcorner f\urcorner \colon *\to \Map (C,D)\) by currying \(f\pr _2\colon * \; \times \; C\to D\). Conversely, a point \(a:*\to \Map (C,D)\) determines the functor \[ C\simeq *\times C\xrightarrow {a\times \id _C}\Map (C,D)\times C \xrightarrow {\ev _{\Map }}D. \] The functor represented by \(\ulcorner f\urcorner \) is identified with \(f\). Moreover, for two points \(a,b\), uncurrying followed by prewhiskering with \(C\simeq *\times C\) gives an equivalence from \((a= b)\) to the anima of identifications between their represented functors, where we use Lemma 1.3.10. This equivalence also identifies a point with the representative of its represented functor.
Agda Representing a functor by a point
name
Definition, checked
name : MAP C D → Term (Map C D)
Proof / implementation
name f = CurriedRepresentation.term (name-representation 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.Chapter01.Section04.Points where
module _ {Γ : Context} {C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Decoding a point
decode
Definition, checked
decode : Term (Map C D) → MAP 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.Chapter01.Section04.Points where
module _ {Γ : Context} {C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Decoding the representative
decode-name
Derivation, checked
decode-name : (f : MAP C D) → decode (name f) =₁ f
Proof / implementation
decode-name f = comp-unitʳ f ∙ ((f ◁ product-unitˡ-pr₂-inverse C) ∙ (comp-assoc (product-unitˡ-inverse C) pr₂ f ∙ (CurriedRepresentation.evaluation (name-representation f) ▷ product-unitˡ-inverse 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.Chapter01.Section04.Points where
module _ {Γ : Context} {C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Isomorphisms between represented functors
decode⁼-isEquiv
Derivation, checked
decode⁼-isEquiv : (a b : Term (Map C D)) → IsEquiv (decode⁼-functor a b)
Proof / implementation
decode⁼-isEquiv a b = equiv-compose (uncurry⁼-functor a b) (preWhisker (product-unitˡ-inverse C)) (uncurry⁼-isEquiv one-isAn a b) (preWhisker-isEquiv (product-unitˡ-inverse C) (product-unitˡ-inverse-isEquiv C) (uncurry a) (uncurry b))
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.Chapter01.Section04.Points where
module _ {Γ : Context} {C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Representing a decoded point
name-decode
Derivation, checked
name-decode : (a : Term (Map C D)) → name (decode a) =₁ a
Proof / implementation
name-decode a = uncurry-reflect one-isAn _ a (comp-unitʳ (uncurry a) ∙ ((uncurry a ◁ product-unitˡ-inverse-pr₂ C) ∙ (comp-assoc pr₂ (product-unitˡ-inverse C) (uncurry a) ∙ CurriedRepresentation.evaluation (name-representation (decode a)))))
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.Chapter01.Section04.Points where
module _ {Γ : Context} {C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
From now on we pass freely back and forth between a functor and its representing point using the comparisons just described; in particular, we will usually denote the point \(\ulcorner f\urcorner \) simply by \(f\).
Accordingly, a functor \(H\colon \Map (A,B)\to \Map (C,D)\) sends a functor \(f\colon A\to B\) to a functor \(H(f)\colon C\to D\), and induces a functor \[ (f=g)\longrightarrow (H(f)=H(g)). \] These operations respect composition and identities. If \(H\) is an equivalence, the induced functor on identification animae is an equivalence as well.
Agda Specialization
specialize-map
Definition, checked
specialize-map : {A B C D : CAT Γ} → MAP (Map A B) (Map C D) → MAP A B → MAP 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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Specialization preserves identity and composition
specialize-map-id
Derivation, checked
specialize-map-id : {A B : CAT Γ} (f : MAP A B) → specialize-map (id (Map A B)) f =₁ f
Proof / implementation
specialize-map-id f = decode-name f ∙ decode⁼ (comp-unitˡ (name 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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} wherespecialize-map-comp
Derivation, checked
specialize-map-comp : {A B C D E F : CAT Γ} (H : MAP (Map A B) (Map C D)) (K : MAP (Map C D) (Map E F)) (f : MAP A B) → specialize-map (K ∘ H) f =₁ specialize-map K (specialize-map H f)
Proof / implementation
specialize-map-comp H K f = decode⁼ ((K ◁ name-decode (H ∘ name f)) ⁻¹ ∙ comp-assoc (name f) H K)
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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Specialization on isomorphisms and identifications
specialize⁼
Derivation, checked
specialize⁼ : {A B C D : CAT Γ} (H : MAP (Map A B) (Map C D)) {f g : MAP A B} → f ＝ g → specialize-map H f ＝ specialize-map H g
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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherespecialize⁼-cong
Derivation, checked
specialize⁼-cong : {A B C D : CAT Γ} (H : MAP (Map A B) (Map C D)) {f g : MAP A B} {α β : f ＝ g} → α =₁ β → specialize⁼ H α =₁ specialize⁼ 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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Lifting and reflection through specialization
specialize⁼-isEquiv
Derivation, checked
specialize⁼-isEquiv : {A B C D : CAT Γ} (H : MAP (Map A B) (Map C D)) → IsEquiv H → (f g : MAP A B) → IsEquiv (specialize⁼-functor H f g)
Proof / implementation
specialize⁼-isEquiv H e f g = equiv-compose (postWhisker H ∘ name⁼-functor f g) (decode⁼-functor (H ∘ name f) (H ∘ name g)) (equiv-compose (name⁼-functor f g) (postWhisker H) (name⁼-isEquiv f g) (postWhisker-isEquiv H e (name f) (name g))) (decode⁼-isEquiv (H ∘ name f) (H ∘ name g))
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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} wherespecialize-reflect-β
Derivation, checked
specialize-reflect-β : {A B C D : CAT Γ} (H : MAP (Map A B) (Map C D)) (e : IsEquiv H) (f g : MAP A B) (α : specialize-map H f ＝ specialize-map H g) → specialize⁼ H (specialize-reflect H e f g α) =₁ α
Proof / implementation
specialize-reflect-β H e f g α = Fact.triangle (specialization-reflection H e f g α)
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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} wherefactor-through-specialize⁼
Derivation, checked
factor-through-specialize⁼ : {A B C D : CAT Γ} (H : MAP (Map A B) (Map C D)) (e : IsEquiv H) {f g : MAP A B} (α β : f ＝ g) (p : specialize⁼ H α =₁ specialize⁼ H β) → Fact.Factorization (postWhisker (specialize⁼-functor H f g)) p
Proof / implementation
factor-through-specialize⁼ H e {f} {g} α β p = factor-through-postWhisker (specialize⁼-functor H f g) (specialize⁼-isEquiv H e f g) p
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.Chapter01.Section04.MappingSpecialization where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 1.4.2 (Uncurrying). For every anima \(X\) and categories \(C,D\), uncurrying is represented by an equivalence \[ (-)^u\colon \Map \bigl (X,\Map (C,D)\bigr ) \iso \Map (X\times C,D). \]
Agda The uncurrying equivalence
mapUncurrying
Derivation, checked
mapUncurrying : (X C D : CAT Γ) → MAP (Map X (Map C D)) (Map (X × C) D)
Proof / implementation
mapUncurrying X C D = ExponentialLaw.forward X 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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} wheremapUncurrying-isEquiv
Derivation, checked
mapUncurrying-isEquiv : (X C D : CAT Γ) (xAn : isAn X) → IsEquiv (mapUncurrying X 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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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. Put \(P:=\Map (X,\Map (C,D))\). Iterated evaluation gives a functor \[ P\times X\times C \longrightarrow \Map (C,D)\times C \xrightarrow {\ev _{\Map }}D. \] Since \(P\) is an anima, currying this functor constructs an actual functor \((-)^u\colon P\to \Map (X\times C,D)\).
Agda Double evaluation in the uncurrying proof
doubleEvaluation
Derivation, checked
doubleEvaluation : MAP ((Nested × X) × 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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Constructing the uncurrying functor
forward
Derivation, checked
forward : MAP Nested Flat
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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
For the inverse, put \(Q:=\Map (X\times C,D)\), and consider the evaluation functor \(Q\times X\times C\to D\). If we first curry in the variable \(C\), with anima parameter \(Q\times X\), and then curry in the variable \(X\), with anima parameter \(Q\), we obtain a functor \(Q\to P\). To verify that both composites are the identity, it suffices by Axiom B.3 to uncurry: once in \(X \times C\) for the composite on \(Q\), and successively in \(X\) and \(C\) for the composite on \(P\). In both cases, the resulting identification follows from the defining identifications for currying. □
Agda Constructing its inverse
backwardFirstCurry
Derivation, checked
backwardFirstCurry : MAP (Flat × X) (Map C D)
Proof / implementation
backwardFirstCurry = mapCurry (product-isAn (map-isAn (X × C) D) xAn) backwardEvaluation
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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) where
module _ (xAn : isAn X) wherebackward
Derivation, checked
backward : MAP Flat Nested
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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) where
module _ (xAn : isAn X) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 comparisons
forward-backward
Derivation, checked
forward-backward : (forward ∘ backward) =₁ (id Flat)
Proof / implementation
forward-backward = let regroup : MAP (Flat × (X × C)) ((Flat × X) × C) regroup = Associativity.backward Flat X C uncurried-equation : (uncurry (forward ∘ backward)) =₁ (uncurry (id Flat)) uncurried-equation = (uncurry-id (X × C) D) ⁻¹ ∙ (comp-unitʳ mapEval ∙ ((mapEval ◁ Associativity.forward-backward Flat X C) ∙ (comp-assoc regroup (Associativity.forward Flat X C) mapEval ∙ ((backward-β ▷ regroup) ∙ forward-represents backward)))) in uncurry-reflect (map-isAn (X × C) D) (forward ∘ backward) (id Flat) uncurried-equation
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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) where
module _ (xAn : isAn X) wherebackward-forward
Derivation, checked
backward-forward : (backward ∘ forward) =₁ (id Nested)
Proof / implementation
backward-forward = let regroup : MAP ((Nested × X) × C) (Nested × (X × C)) regroup = Associativity.forward Nested X C uncurried-equation : (doubleUncurry (backward ∘ forward)) =₁ (doubleUncurry (id Nested)) uncurried-equation = doubleUncurry-id ⁻¹ ∙ (comp-unitʳ doubleEvaluation ∙ ((doubleEvaluation ◁ Associativity.backward-forward Nested X C) ∙ (comp-assoc regroup (Associativity.backward Nested X C) doubleEvaluation ∙ ((forward-β ▷ regroup) ∙ backward-represents forward)))) in doubleUncurry-reflect (map-isAn X (Map C D)) (backward ∘ forward) (id Nested) uncurried-equation
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.Chapter01.Section04.Uncurrying where
module _ {Γ : Context} where
module ExponentialLaw (X C D : CAT Γ) where
module _ (xAn : isAn X) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 1.4.3. The mapping animae are covariantly functorial in the second variable and contravariantly functorial in the first. For \(g\colon D\to E\), curry the composite \[ \Map (C,D)\times C\xrightarrow {\ev _{\Map }}D\xrightarrow {g}E \] to obtain \(g_*\colon \Map (C,D)\to \Map (C,E)\). For \(f\colon B\to C\), curry evaluation precomposed with \(\id _{\Map (C,D)}\times f\) to obtain \(f^*\colon \Map (C,D)\to \Map (B,D)\). We call these functors postcomposition with \(g\) and precomposition with \(f\), respectively.
Agda Postcomposition
mapPost
Definition, checked
mapPost : {C D E : CAT Γ} → MAP D E → MAP (Map C D) (Map C 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} wheremapPost-β
Derivation, checked
mapPost-β : {C D E : CAT Γ} (g : MAP D E) → (uncurry (mapPost {C = C} g)) =₁ (g ∘ mapEval)
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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Precomposition
mapPre
Definition, checked
mapPre : {B C D : CAT Γ} → MAP B C → MAP (Map C D) (Map B D)
Proof / implementation
mapPre {C = C} {D} f = mapCurry (map-isAn C D) (mapEval ∘ productMap (id (Map C D)) 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} wheremapPre-β
Derivation, checked
mapPre-β : {B C D : CAT Γ} (f : MAP B C) → (uncurry (mapPre {D = D} f)) =₁ (mapEval ∘ productMap (id (Map C D)) f)
Proof / implementation
mapPre-β {C = C} {D} f = mapCurry-β (map-isAn C D) (mapEval ∘ productMap (id (Map C D)) 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 identification \(\gamma \colon g= g'\) induces an identification \(\gamma _*\colon g_*= g'_*\). Indeed, whisker \(\gamma \) with evaluation and use the uncurrying comparisons for \(g_*\) and \(g'_*\) to obtain an identification between their uncurried functors. Lift this through the equivalence of animae of identifications in the mapping-anima rule. Similarly, for \(\varphi \colon f= f'\), pair \(\varphi \) with the identity on \(\Map (C,D)\), postcompose with evaluation, and lift to obtain \(\varphi ^*\colon f^*= f'^*\).
Agda Postcomposition of a identification
mapPost⁼
Derivation, checked
mapPost⁼ : {C D E : CAT Γ} {f g : MAP D E} → f ＝ g → mapPost {C = C} f ＝ mapPost g
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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Precomposition of a identification
mapPre⁼
Derivation, checked
mapPre⁼ : {B C D : CAT Γ} {f g : MAP B C} → f ＝ g → mapPre {D = D} f ＝ mapPre g
Proof / implementation
mapPre⁼ {C = C} {D} α = curry⁼ (map-isAn C D) (mapEval ◁ productMap-cong (const (id₌ (id (Map 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 must show that the functor \(\Map (C,*)\to *\) is an equivalence. An inverse is given by the functor \(*\to \Map (C,*)\) obtained by currying the terminal functor \(*\times C\to *\). The composite on \(*\) is automatically identified with the identity. For the composite on \(\Map (C,*)\), it suffices by the mapping-anima axiom to compare the two uncurried functors \(\Map (C,*)\times C\to *\). These are again identified by the terminal-category axiom. □
Proposition 1.4.5. For categories \(C,D,E\), the projections induce an equivalence \[ (\pr _{1,*},\pr _{2,*})\colon \Map (E,C\times D)\iso \Map (E,C)\times \Map (E,D). \]
Agda Mapping into a product
forward
Derivation, checked
forward : MAP Source Target
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) whereforward-isEquiv
Derivation, checked
forward-isEquiv : IsEquiv forward
Proof / implementation
forward-isEquiv = record { inverse = backward ; left-inverse-law = backward-forward ⁻¹ ; right-inverse-law = forward-backward ⁻¹ }
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 define a functor \[ h\colon \Map (E,C)\times \Map (E,D)\longrightarrow \Map (E,C\times D) \] by pairing the two functors \[ \begin {aligned} (\Map (E,C)\times \Map (E,D))\times E &\xrightarrow {\pr _1\times \id _E}\Map (E,C)\times E \xrightarrow {\ev _{\Map }}C,\\ (\Map (E,C)\times \Map (E,D))\times E &\xrightarrow {\pr _2\times \id _E}\Map (E,D)\times E \xrightarrow {\ev _{\Map }}D, \end {aligned} \] and currying the resulting functor to \(C\times D\). This is possible since \(\Map (E,C)\times \Map (E,D)\) is an anima.
Agda Constructing the product comparison inverse
backward
Derivation, checked
backward : MAP Target Source
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 start by showing that the composite \((\pr _{1,*},\pr _{2,*})\circ h\) is identified with the identity. It will suffice to show this after projecting to both factors, and by symmetry we may just do this for \(\Map (E,C)\). In other words, we must show that \(\pr _{1,*}\circ h\) is identified with \(\pr _1\). It will in turn suffice to show this after uncurrying. But the uncurrying of both functors is identified with \[ (\Map (E,C)\times \Map (E,D))\times E \xrightarrow {\pr _1\times \id _E}\Map (E,C)\times E \xrightarrow {\ev _{\Map }}C, \] by the construction of \(h\) and the definition of postcomposition.
We will now show that also the composite \(h\circ (\pr _{1,*},\pr _{2,*})\) is identified with the identity. Uncurrying reduces this to comparing two functors \[ \Map (E,C\times D)\times E\longrightarrow C\times D. \] It suffices to compare their two projections, and again we may just consider the \(C\)-component. The projection of the uncurried identity is \(\pr _1\circ \ev _{\Map }\); the projection of the other functor is \(\ev _{\Map }\circ (\pr _{1,*}\times \id _E)\). These are identified by the defining commutative square for postcomposition:
The product axiom and then the mapping-anima axiom give the desired identification. □
Agda The product comparison inverse laws
forward-backward
Derivation, checked
forward-backward : (forward ∘ backward) =₁ (id Target)
Proof / implementation
forward-backward = pair₌ ((comp-unitʳ pr₁) ⁻¹ ∙ (forward-backward-first ∙ project-pair₁ (mapPost pr₁) (mapPost pr₂) backward)) ((comp-unitʳ pr₂) ⁻¹ ∙ (forward-backward-second ∙ project-pair₂ (mapPost pr₁) (mapPost pr₂) backward))
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) wherebackward-forward
Derivation, checked
backward-forward : (backward ∘ forward) =₁ (id Source)
Proof / implementation
backward-forward = uncurry-reflect (map-isAn E (C × D)) _ _ ((uncurry-id E (C × D)) ⁻¹ ∙ backward-forward-uncurried)
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 next compare uncurrying with substitution in the anima parameter.
Lemma 1.4.6 (Uncurrying and substitution). Let \(C,D\) be categories, \(X,Y\) animae, and \(f\colon X\to \Map (C,D)\) and \(\sigma \colon Y\to X\) functors. Uncurrying commutes with substitution: there is an identification \[ (f\circ \sigma )^u=f^u\circ (\sigma \times \id _C). \] This comparison is compatible with identifications of the input functors, with successive substitution, and with substitution by an identity functor, using the associativity and unitality identifications. Moreover, uncurrying preserves identity identifications and their vertical composition.
Agda Uncurrying and substitution
uncurry-restrict
Derivation, checked
uncurry-restrict : {R : CAT Γ} (f : Term (Map C D)) (σ : MAP R A) → uncurry (f ∘ σ) =₁ (uncurry f ∘ productMap σ (id C))
Proof / implementation
uncurry-restrict f σ = (comp-assoc (productMap σ (id C)) (productMap f (id C)) mapEval) ⁻¹ ∙ (mapEval ◁ (productMap-cong (id₌ (f ∘ σ)) (comp-unitˡ (id C)) ∙ productMap-comp σ f (id C) (id 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.Chapter01.Section04.Currying where
module _ {Γ : Context} {A C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Naturality of the substitution comparison
uncurry-restrict-natural
Derivation, checked
uncurry-restrict-natural : {R : CAT Γ} {x y : Term (Map C D)} {r s : MAP R P} (α : x ＝ y) (γ : r ＝ s) → SquareCell₌ (uncurry⁼ (α ⋆ γ)) (uncurry⁼ α ⋆ productMap-cong γ (const (id₌ (id C)))) (const (uncurry-restrict x r)) (const (uncurry-restrict y s))
Proof / implementation
uncurry-restrict-natural {x = x} {s = s} α γ = replace-edges₌ ((uncurry⁼-composition (α ▷ s) (x ◁ γ)) ⁻¹) (id₌ _) (adjoin-square₌ (uncurry-restrict-substitution x γ) (uncurry-restrict-inputs α s))
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.Chapter01.Section04.UncurryingRestriction where
module _ {Γ : Context} {X : CAT Γ} where
module _ {P C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Uncurrying preserves identity and composition
uncurry⁼-identity
Derivation, checked
uncurry⁼-identity : (f : Term (Map C D)) → uncurry⁼ (const {P = X} (id₌ f)) =₁ const (id₌ (uncurry f))
Proof / implementation
uncurry⁼-identity f = const-cong (postWhisker-id₌ mapEval (productMap f (id C))) ∙ (post-constant mapEval (id₌ (productMap f (id C))) ∙ ((postWhisker mapEval ◁ productMap-cong-id f (id C)) ∙ uncurry⁼-evaluate (const (id₌ 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.Chapter01.Section04.Currying where
module _ {Γ : Context} {A C D : CAT Γ} where
module _ {X : CAT Γ} whereuncurry⁼-composition
Derivation, checked
uncurry⁼-composition : {f g h : Term (Map C D)} (β : g ＝ h) (α : f ＝ g) → uncurry⁼ (β ∙ α) =₁ (uncurry⁼ β ∙ uncurry⁼ α)
Proof / implementation
uncurry⁼-composition β α = let identity = const {P = X} (id₌ (id C)) in (comp₌-cong (uncurry⁼-evaluate β) (uncurry⁼-evaluate α)) ⁻¹ ∙ (postWhisker-comp₌ mapEval (productMap-cong β identity) (productMap-cong α identity) ∙ ((postWhisker mapEval ◁ (productMap-cong-comp β α identity identity ∙ productMap-cong₂ (id₌ (β ∙ α)) ((comp₌-unitˡ identity) ⁻¹))) ∙ uncurry⁼-evaluate (β ∙ α)))
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.Chapter01.Section04.Currying where
module _ {Γ : Context} {A C D : CAT Γ} where
module _ {X : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Iterated substitution
uncurry-restrict-iterated
Derivation, checked
uncurry-restrict-iterated : {W R : CAT Γ} (x : Term (Map C D)) (r : MAP R P) (s : MAP W R) → (uncurry-restrict x (r ∘ s) ∙ uncurry⁼ (comp-assoc s r x)) =₂ ((uncurry x ◁ productMap-first-comp r s) ∙ (comp-assoc (productMap s (id C)) (productMap r (id C)) (uncurry x) ∙ ((uncurry-restrict x r ▷ productMap s (id C)) ∙ uncurry-restrict (x ∘ r) s)))
Proof / implementation
uncurry-restrict-iterated x r s = RestrictionIteration.transfer x r s (productMap-first-comp-assoc C x r s)
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.Chapter01.Section04.UncurryingRestriction where
module _ {Γ : Context} where
module _ {P C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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. Using the definition of uncurrying, functoriality of products, and associativity, we obtain identifications \[ \begin {aligned} (f\circ \sigma )^u &=\ev _{\Map }\circ ((f\circ \sigma )\times \id _C)\\ &=\ev _{\Map }\circ (f\times \id _C)\circ (\sigma \times \id _C)\\ &=f^u\circ (\sigma \times \id _C). \end {aligned} \] The compatibilities follow from those for pairing and composition, as in Lemma 1.3.16; the unit comparison also uses equation (1.1). Preservation of identity identifications and vertical composition follows from the corresponding properties of products and whiskering with evaluation. We leave the details to the reader. □
We can now lift composition of functors to an operation on mapping animae.
Construction 1.4.7. For categories \(C\), \(D\) and \(E\), consider the double evaluation functor \[ \Map (D,E)\times \Map (C,D)\times C\xrightarrow {\id \times \ev } \Map (D,E) \times D \xrightarrow {\ev } E. \] Currying in \(C\) defines a functor \[ \mu _{C,D,E} \colon \Map (D,E)\times \Map (C,D)\longrightarrow \Map (C,E), \] which by construction comes with an identification \[ \ev _{\Map }\bigl (\mu (g,f),c\bigr ) = \ev _{\Map }\bigl (g,\ev _{\Map }(f,c)\bigr ). \] The projection \(*\times C\to C\) similarly curries to a functor \[ \eta _C\colon *\longrightarrow \Map (C,C), \] whose evaluation is identified with that projection.
Agda Composition in the mapping anima
mapComp
Definition, checked
mapComp : {C D E : CAT Γ} → MAP (Map D E × Map C D) (Map C E)
Proof / implementation
mapComp {C} {D} {E} = mapCurry (product-isAn (map-isAn D E) (map-isAn C D)) doubleEvaluation
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.Chapter01.Section04.Composition where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Evaluation of composition
mapComp-β
Derivation, checked
mapComp-β : {C D E : CAT Γ} → uncurry (mapComp {C} {D} {E}) =₁ doubleEvaluation
Proof / implementation
mapComp-β {C} {D} {E} = mapCurry-β (product-isAn (map-isAn D E) (map-isAn C D)) doubleEvaluation
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.Chapter01.Section04.Composition where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 representing identity
mapId
Definition, checked
mapId : (C : CAT Γ) → MAP (One {Γ}) (Map 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.Chapter01.Section04.Composition where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Evaluation of the representing identity
mapId-β
Derivation, checked
mapId-β : (C : CAT Γ) → uncurry (mapId C) =₁ 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.Chapter01.Section04.Composition where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 may use these functors to obtain composition and evaluation for term expressions. Given terms \[ \Gamma \vdash f:\Map (C,D) \qquadtext {and} \Gamma \vdash g:\Map (D,E), \] we may form \[ \Gamma \vdash g\circ f:=\mu _{C,D,E}(g,f):\Map (C,E). \] Likewise, given a term \(\Gamma \vdash f:\Map (C,D)\) and \(\Gamma \vdash x:C\), we define \[ \Gamma \vdash f(x):=\ev _{\Map }(f,x):D. \]
Agda Composition of terms
compose
Definition, checked
compose : {C D E : CAT Γ} → Term (Map D E) → Term (Map C D) → Term (Map C E)
Proof / implementation
compose = Binary.binary-apply mapComp
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.Chapter01.Section04.Composition where
module _ {Γ : Context} where
module _ {P : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Application of a term
apply-map
Definition, checked
apply-map : {C D : CAT Γ} → Term (Map C D) → Term C → Term D
Proof / implementation
apply-map = Binary.binary-apply mapEval
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.Chapter01.Section04.Composition where
module _ {Γ : Context} where
module _ {P : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 1.4.8 (Coherence of composition). Composition in mapping animae has specified left and right unitors and an associator. These satisfy the triangle and pentagon identities through specified identifications.
Agda Restricting the whole coherence identity
restrict
Derivation, checked
restrict : {T : CAT Γ} (σ : MAP T parameter) → (TriangleSource (compositionTriangle inner outer) ▷ σ) =₂ (TriangleTarget (compositionTriangle inner outer) ▷ σ)
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.Chapter01.Section04.Coherence where
module _ {Γ : Context} where
module UniversalTriangle (A B C : CAT Γ) whererestrict
Derivation, checked
restrict : {T : CAT Γ} (σ : MAP T parameter) → (PentagonSource (compositionPentagon first second third fourth) ▷ σ) =₂ (PentagonTarget (compositionPentagon first second third fourth) ▷ σ)
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.Chapter01.Section04.Coherence where
module _ {Γ : Context} where
module UniversalPentagon (A B C D E : CAT Γ) whereAbout this correspondence
The universal anima-parameter diagrams and their literal restrictions are checked. This does not assert freshly normalized default coherence at an arbitrary categorical term source.
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. Throughout the proof, we make use of the following notation: Given a ‘parameter anima’ \(P\) and a functor \(f\colon P\to \Map (C,D)\), we define \[ \widetilde {f} \; := \; (\pr _1,f^u) \colon P \times C \to P \times D. \] If \(g\colon P\to \Map (D,E)\) is any other functor, then there is an identification \[ \widetilde {g} \circ \widetilde {f} = \widetilde {g \circ f}; \] indeed, we may construct this identification componentwise, where it is clear for the first component and follows from the defining property of \(\mu _{C,D,E}\) in the second component. The compatibility with the primitive coherence identifications and change of parameter can likewise be checked after both projections, using Lemmas 1.4.6 and 1.3.16 and the coherence axioms for composition.
Agda Evaluation retaining its parameter
evaluation-over
Definition, checked
evaluation-over : {P C D : CAT Γ} → MAP P (Map C D) → FunctorOverBase (product-over P C) (product-over P 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.Chapter01.Section04.EvaluationOverBase where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Retained composition and identity comparisons
evaluation-compose
Derivation, checked
evaluation-compose : {P C D E : CAT Γ} (g : MAP P (Map D E)) (f : MAP P (Map C D)) → IdentificationOver {A = One} (evaluation-over (compose g f)) (comp-over (evaluation-over g) (evaluation-over f))
Proof / implementation
evaluation-compose {P} g f = let open OverFirstFactor P middle = pair-pr₁-over (uncurry g ∘ pair-pr₁ (uncurry f)) first : IdentificationOver {A = One} (evaluation-over (compose g f)) middle first = identification-over (pair-pr₁-cong-One (uncurry-compose g f)) (pair-pr₁-cong-over-One (uncurry-compose g f)) second : IdentificationOver {A = One} (comp-over (evaluation-over g) (evaluation-over f)) middle second = identification-over (pair-pr₁-compose (uncurry g) (uncurry f)) (pair-pr₁-compose-over (uncurry g) (uncurry f)) in comp-identification-over (inverse-identification-over second) first
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.Chapter01.Section04.EvaluationOverBase where
module _ {Γ : Context} whereevaluation-identity
Derivation, checked
evaluation-identity : (P C : CAT Γ) → IdentificationOver {A = One} (evaluation-over (identity-map {P = P} C)) (id-over (product-over P C))
Proof / implementation
evaluation-identity P C = let open OverFirstFactor P first : IdentificationOver {A = One} (evaluation-over (identity-map {P = P} C)) (pair-pr₁-over pr₂) first = identification-over (pair-pr₁-cong-One (uncurry-identity P C)) (pair-pr₁-cong-over-One (uncurry-identity P C)) second : IdentificationOver {A = One} (pair-pr₁-over pr₂) (id-over (product-over P C)) second = identification-over (pair-pr₁-id C) (pair-pr₁-id-over C) in comp-identification-over second first
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.Chapter01.Section04.EvaluationOverBase where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Evaluation and change of parameter
compatibility
Derivation, checked
compatibility : CompatibleOver pr₁ (FunctorOverBase.cell (comp-over-map r (change-parameter r) (evaluation-over (x ∘ r)))) (pair-β₁ (r ∘ pr₁) (uncurry x ∘ source-change)) (input-route x)
Proof / implementation
compatibility = comp₌-assoc (r ◁ pair-β₁ pr₁ v) (comp-assoc R pr₁ r) projection ∙ (comp₌-cong (comp₌-unitˡ-One first) (id₌ projection) ∙ (pair-evaluation-over₁-One (r ∘ pr₁) (id D ∘ pr₂) R (id₌ (r ∘ pr₁) ∙ first) (finish ∙ second) ∙ comp₌-cong (id₌ (pair-β₁ (r ∘ pr₁) (uncurry x ∘ source-change))) (postWhisker pr₁ ◁ normalization)))
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.Chapter01.Section04.EvaluationRestriction where
module _ {Γ : Context} {P Q C D : CAT Γ} where
module ParameterChange (r : MAP Q P) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 now use this to construct the associator. Given a third functor \(h\colon P \to \Map (E,F)\), we obtain three composable functors \[ P\times C \xrightarrow {\widetilde {f}} P\times D \xrightarrow {\widetilde {g}} P\times E \xrightarrow {\widetilde {h}} P\times F. \] Using the primitive associator and the previous comparisons, we get identifications \begin {align*} \widetilde {(h \circ g) \circ f} &= \widetilde {h \circ g} \circ \widetilde {f} = (\widetilde {h} \circ \widetilde {g}) \circ \widetilde {f} = \widetilde {h} \circ (\widetilde {g} \circ \widetilde {f}) = \widetilde {h} \circ \widetilde {g \circ f} = \widetilde {h \circ (g \circ f)}. \end {align*}
Passing to the second component of this identification, we obtain an identification between the uncurrying of \((h\circ g)\circ f\) and that of \(h\circ (g\circ f)\); we may then use the mapping-anima axiom to lift this to the desired associator.
Agda Constructing the universal associator
mapComp-assoc
Derivation, checked
mapComp-assoc : (A B C D : CAT Γ) → let P = (Map C D × Map B C) × Map A B z : MAP P (Map C D) z = pr₁ ∘ pr₁ y : MAP P (Map B C) y = pr₂ ∘ pr₁ x : MAP P (Map A B) x = pr₂ in compose (compose z y) x =₁ compose z (compose y x)
Proof / implementation
mapComp-assoc A B C D = Recovered.assoc (product-isAn (product-isAn (map-isAn C D) (map-isAn B C)) (map-isAn A B)) (pr₁ ∘ pr₁) (pr₂ ∘ pr₁) 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.Chapter01.Section04.CompositionLaws where
module _ {Γ : Context} wherecompose-assoc
Derivation, checked
compose-assoc : {A B C D : CAT Γ} (z : Term (Map C D)) (y : Term (Map B C)) (x : Term (Map A B)) → compose (compose z y) x =₁ compose z (compose y x)
Proof / implementation
compose-assoc {A} {B} {C} {D} z y x = let triple = pair (pair z y) x first = pair-β₁ z y ∙ ((pr₁ ◁ pair-β₁ (pair z y) x) ∙ comp-assoc triple pr₁ pr₁) second = pair-β₂ z y ∙ ((pr₂ ◁ pair-β₁ (pair z y) x) ∙ comp-assoc triple pr₁ pr₂) third = pair-β₂ (pair z y) x in specialize (mapComp-assoc A B C D) triple (compose-evaluate (compose (pr₁ ∘ pr₁) (pr₂ ∘ pr₁)) pr₂ triple (compose-evaluate (pr₁ ∘ pr₁) (pr₂ ∘ pr₁) triple first second) third) (compose-evaluate (pr₁ ∘ pr₁) (compose (pr₂ ∘ pr₁) pr₂) triple first (compose-evaluate (pr₂ ∘ pr₁) pr₂ triple second third))
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.Chapter01.Section04.CompositionLaws where
module _ {Γ : Context} where
module _ {P : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
For the unitors, note that the constant functor \(\const _{\id _C}\colon P \to \Map (C,C)\) corresponds under (un)currying to the projection functor \(\pr _2\colon P \times C \to C\), and so the associated functor \(\widetilde {\const _{\id _C}}\colon P \times C \to P \times C\) is identified with the identity. We then consider the unitors \(\lambda _{\widetilde {f}} : \id _{P \times D} \circ \widetilde {f} = \widetilde {f}\) and \(\rho _{\widetilde {f}} : \widetilde {f} \circ \id _{P \times C} = \widetilde {f}\), and with the same arguments as above deduce the desired relations \(\id _D \circ f = f\) and \(f \circ \id _C = f\).
Agda Constructing the universal unitors
mapComp-unitˡ
Derivation, checked
mapComp-unitˡ : (C D : CAT Γ) → compose (identity-map D) (id (Map C D)) =₁ id (Map 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.Chapter01.Section04.CompositionLaws where
module _ {Γ : Context} wheremapComp-unitʳ
Derivation, checked
mapComp-unitʳ : (C D : CAT Γ) → compose (id (Map C D)) (identity-map C) =₁ id (Map 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.Chapter01.Section04.CompositionLaws where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
Observe that both of these constructions are compatible with substitution in the parameter anima \(P\): given a map of animae \(\sigma \colon Q \to P\), we can construct identifications \[ \alpha ^P_{h,g,f} \star \sigma = \alpha ^Q_{h\sigma ,g\sigma ,f\sigma }, \qquad \lambda _f^P \star \sigma = \lambda _{f\sigma }^Q, \qquad \rho _f^P \star \sigma = \rho _{f \sigma }^Q, \] up to the substitution comparisons relating e.g. \(((h \circ g) \circ f)\sigma \) to \(((h \sigma ) \circ (g \sigma )) \circ f\sigma \). To see this, note that by Lemma 1.4.6 there is a commutative square
Agda Restricting universal associator and unitors
compose-assoc-agreement
Derivation, checked
compose-assoc-agreement : (pAn : isAn P) (z : MAP P (Map C D)) (y : MAP P (Map B C)) (x : MAP P (Map A B)) → compose-assoc z y x =₂ Recovered.assoc pAn z y x
Proof / implementation
compose-assoc-agreement pAn z y x = let U = (Map C D × Map B C) × Map A B uAn = product-isAn (product-isAn (map-isAn C D) (map-isAn B C)) (map-isAn A B) z₀ : MAP U (Map C D) z₀ = pr₁ ∘ pr₁ y₀ : MAP U (Map B C) y₀ = pr₂ ∘ pr₁ x₀ : MAP U (Map A B) x₀ = pr₂ triple = pair (pair z y) x first = pair-β₁ z y ∙ ((pr₁ ◁ pair-β₁ (pair z y) x) ∙ comp-assoc triple pr₁ pr₁) second = pair-β₂ z y ∙ ((pr₂ ◁ pair-β₁ (pair z y) x) ∙ comp-assoc triple pr₁ pr₂) third = pair-β₂ (pair z y) x module Frames = AssociatorEndpointFactorization {P = P} {U = U} {A = A} {B = B} {C = C} {D = D} triple z₀ y₀ x₀ first second third using (δL; δR; λL; λR; Ldefault; Rdefault; left-factorization; right-factorization) module Raw = RawAssociatorRestriction {P = U} {Q = P} {A = A} {B = B} {C = C} {D = D} triple z₀ y₀ x₀ using (recovered-restriction) universal = mapComp-assoc A B C D ▷ triple factor-frames = comp₌-cong Frames.right-factorization (comp₌-cong (id₌ universal) (inv₌ ◁ Frames.left-factorization)) raw = Raw.recovered-restriction uAn pAn normalized = square-to-changeEndpoints Frames.λL Frames.λR (Recovered.assoc pAn (z₀ ∘ triple) (y₀ ∘ triple) (x₀ ∘ triple)) (Recovered.assoc pAn z y x) (transpose-square₌ (RecoveredNaturality.assoc-natural-One pAn first second third)) in normalized ∙ (changeEndpoints-cong Frames.λL Frames.λR raw ∙ ((changeEndpoints-iterated Frames.δL Frames.δR Frames.λL Frames.λR universal) ⁻¹ ∙ factor-frames))
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.Chapter01.Section04.CompositionLawRestriction where
module _ {Γ : Context} {P A B C D : CAT Γ} wheredefault-unitˡ-recovered
Derivation, checked
default-unitˡ-recovered : (qAn : isAn Q) (x : MAP Q (Map C D)) → compose-unitˡ x =₂ Recovered.unitˡ qAn x
Proof / implementation
default-unitˡ-recovered qAn x = let i = id (Map C D) module Unit = UnitRestriction {P = Map C D} {Q = Q} {C = C} {D = D} x i x (comp-unitˡ x) using (left-frame; left-natural) in evaluation-recover-specialize qAn x (mapComp-unitˡ C D) Unit.left-frame (comp-unitˡ x) (IdentificationOver.identification (evaluation-unitˡ i)) (Recovered.unitˡ-image (map-isAn C D) i) (evaluation-unitˡ x) Unit.left-natural
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.Chapter01.Section04.CompositionLawRestriction where
module _ {Γ : Context} {Q C D : CAT Γ} wheredefault-unitʳ-recovered
Derivation, checked
default-unitʳ-recovered : (qAn : isAn Q) (x : MAP Q (Map C D)) → compose-unitʳ x =₂ Recovered.unitʳ qAn x
Proof / implementation
default-unitʳ-recovered qAn x = let i = id (Map C D) module Unit = UnitRestriction {P = Map C D} {Q = Q} {C = C} {D = D} x i x (comp-unitˡ x) using (right-frame; right-natural) in evaluation-recover-specialize qAn x (mapComp-unitʳ C D) Unit.right-frame (comp-unitˡ x) (IdentificationOver.identification (evaluation-unitʳ i)) (Recovered.unitʳ-image (map-isAn C D) i) (evaluation-unitʳ x) Unit.right-natural
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.Chapter01.Section04.CompositionLawRestriction where
module _ {Γ : Context} {Q C D : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Composition and change of parameter
compose-pre
Derivation, checked
compose-pre : {Q C D E : CAT Γ} (y : Term (Map D E)) (x : Term (Map C D)) (r : MAP Q P) → (compose y x ∘ r) =₁ compose {P = Q} (y ∘ r) (x ∘ r)
Proof / implementation
compose-pre = Binary.binary-pre mapComp
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.Chapter01.Section04.Composition where
module _ {Γ : Context} where
module _ {P : CAT Γ} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
Using this for \(f\), \(g\) and \(h\) and applying the interchange law and the various primitive coherence identities, we get the relation on associators after uncurrying, which suffices to establish the relation. The analogous argument applies to the unitors.
For the pentagon, assume given a fourth map \(k\colon P \to \Map (F,G)\), and consider the primitive pentagon identification for the four functors \[ P\times C \xrightarrow {\widetilde {f}} P\times D \xrightarrow {\widetilde {g}} P\times E \xrightarrow {\widetilde {h}} P\times F \xrightarrow {\widetilde {k}} P \times G. \] For each of the five vertices of the resulting pentagon, we may use iterated identifications of the form \(\widetilde {g} \circ \widetilde {f} = \widetilde {g \circ f}\) to put them into the form \(\widetilde {u}\) for some \(u\). By the construction of the associator, the substitution compatibility, and interchange, projecting the five edges of the resulting pentagon to the second component identifies them with the uncurryings of the five edges of the desired pentagon. The primitive pentagon identification therefore gives an identification between the uncurryings of the two composites around this pentagon. The mapping-anima axiom then provides the desired pentagon identification.
Agda The universal pentagon identity
law
Derivation, checked
law : PentagonCommutes (compositionPentagon first second third fourth)
Proof / implementation
law = pentagon (product-isAn (product-isAn (product-isAn (map-isAn D E) (map-isAn C D)) (map-isAn B C)) (map-isAn A B)) first second third fourth
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.Chapter01.Section04.Coherence where
module _ {Γ : Context} where
module UniversalPentagon (A B C D E : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Reflecting the pentagon through uncurrying
pentagon
Derivation, checked
pentagon : {P A B C D E : CAT Γ} (pAn : isAn P) (x : MAP P (Map A B)) (y : MAP P (Map B C)) (z : MAP P (Map C D)) (w : MAP P (Map D E)) → PentagonCommutes (compositionPentagon x y z w)
Proof / implementation
pentagon pAn x y z w = let first-short-change = compose-assoc-agreement pAn (compose w z) y x second-short-change = compose-assoc-agreement pAn w z (compose y x) first-long-change = Binary.binary-cong₂ mapComp (compose-assoc-agreement pAn w z y) (id₌ (id₌ x)) middle-long-change = compose-assoc-agreement pAn w (compose z y) x last-long-change = Binary.binary-cong₂ mapComp (id₌ (id₌ w)) (compose-assoc-agreement pAn z y x) short-change = comp₌-cong second-short-change first-short-change long-change = comp₌-cong (comp₌-cong last-long-change middle-long-change) first-long-change in long-change ⁻¹ ∙ (recovered-pentagon pAn x y z w ∙ short-change)
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.Chapter01.Section04.Coherence where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 triangle identification is obtained by similar means. □
Agda The universal triangle identity
law
Derivation, checked
law : TriangleCommutes (compositionTriangle inner outer)
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.Chapter01.Section04.Coherence where
module _ {Γ : Context} where
module UniversalTriangle (A B C : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 end the section by establishing various further properties about mapping animae.
Proposition 1.4.9. For functors \(f\colon A\to B\) and \(g\colon B\to C\) and any category \(E\), there is a canonical identification \[ g_*\circ f_*=(g\circ f)_* \] of functors \(\Map (E,A)\to \Map (E,C)\).
Agda Postcomposition respects composition
mapPost-comp
Derivation, checked
mapPost-comp : {A B C D : CAT Γ} (f : MAP B C) (g : MAP C D) → (mapPost {C = A} g ∘ mapPost f) =₁ (mapPost (g ∘ f))
Proof / implementation
mapPost-comp {A} {B} f g = uncurry-reflect (map-isAn A B) _ _ ((mapPost-β (g ∘ f)) ⁻¹ ∙ ((comp-assoc mapEval f g) ⁻¹ ∙ ((g ◁ mapPost-β f) ∙ mapPost-uncurry g (mapPost 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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. After uncurrying, both sides evaluate a functor \(E\to A\) and then compose it with \(f\) and \(g\). The primitive associator gives the comparison between these uncurried functors, and we may lift it by Axiom B.3. □
Proposition 1.4.10. For functors \(f\colon A\to B\) and \(g\colon B\to C\) and any category \(E\), there is a canonical identification \[ f^*\circ g^*=(g\circ f)^* \] of functors \(\Map (C,E)\to \Map (A,E)\).
Agda Precomposition respects composition
mapPre-comp
Derivation, checked
mapPre-comp : {A B C D : CAT Γ} (f : MAP A B) (g : MAP B C) → (mapPre {D = D} f ∘ mapPre g) =₁ (mapPre (g ∘ f))
Proof / implementation
mapPre-comp {C = C} {D} f g = uncurry-reflect (map-isAn C D) _ _ ((mapPre-β (g ∘ f)) ⁻¹ ∙ ((mapEval ◁ (productMap-cong (comp-unitˡ (id (Map C D))) (id₌ (g ∘ f)) ∙ productMap-comp (id (Map C D)) (id (Map C D)) f g)) ∙ (comp-assoc (productMap (id (Map C D)) f) (productMap (id (Map C D)) g) mapEval ∙ ((mapPre-β g ▷ productMap (id (Map C D)) f) ∙ mapPre-uncurry f (mapPre g)))))
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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 is proved in the same way, using the primitive associator after uncurrying. □
Proposition 1.4.11. For a functor \(f\colon C\to D\), the following are equivalent:
Agda Detecting equivalences with mapping animae
post-tests-all
Derivation, checked
post-tests-all : {C D : CAT Γ} (f : MAP C D) → ((E : CAT Γ) → IsEquiv (mapPost {C = E} f)) → IsEquiv 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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} wherepre-tests-all
Derivation, checked
pre-tests-all : {C D : CAT Γ} (f : MAP C D) → ((E : CAT Γ) → IsEquiv (mapPre {D = E} f)) → IsEquiv 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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} wheremapPost-isEquiv
Derivation, checked
mapPost-isEquiv : {A C D : CAT Γ} (f : MAP C D) → IsEquiv f → IsEquiv (mapPost {C = A} f)
Proof / implementation
mapPost-isEquiv {A} {C} {D} f e = record { inverse = mapPost (IsEquiv.inverse e) ; left-inverse-law = (mapPost-comp f (IsEquiv.inverse e)) ⁻¹ ∙ (mapPost⁼ (IsEquiv.left-inverse-law e) ∙ (mapPost-id A C) ⁻¹) ; right-inverse-law = (mapPost-comp (IsEquiv.inverse e) f) ⁻¹ ∙ (mapPost⁼ (IsEquiv.right-inverse-law e) ∙ (mapPost-id A 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} wheremapPre-isEquiv
Derivation, checked
mapPre-isEquiv : {C D E : CAT Γ} (f : MAP C D) → IsEquiv f → IsEquiv (mapPre {D = E} f)
Proof / implementation
mapPre-isEquiv {C} {D} {E} f e = record { inverse = mapPre (IsEquiv.inverse e) ; left-inverse-law = (mapPre-comp (IsEquiv.inverse e) f) ⁻¹ ∙ (mapPre⁼ (IsEquiv.right-inverse-law e) ∙ (mapPre-id D E) ⁻¹) ; right-inverse-law = (mapPre-comp f (IsEquiv.inverse e)) ⁻¹ ∙ (mapPre⁼ (IsEquiv.left-inverse-law e) ∙ (mapPre-id C 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.
- (i)
-
The functor \(f\) is an equivalence.
- (ii)
-
For every category \(E\), the functor \(f_*\colon \Map (E,C)\to \Map (E,D)\) is an equivalence.
- (iii)
-
For every category \(E\), the functor \(f^*\colon \Map (D,E)\to \Map (C,E)\) is an equivalence.
If \(C\) and \(D\) are animae, it suffices in (ii) or (iii) to let \(E\) range over animae.
Agda Testing only against animae
post-tests-animae
Derivation, checked
post-tests-animae : {C D : CAT Γ} → isAn C → isAn D → (f : MAP C D) → ((E : CAT Γ) → isAn E → IsEquiv (mapPost {C = E} f)) → IsEquiv f
Proof / implementation
post-tests-animae {C} {D} cAn dAn f tests = post-tests-isEquiv f (tests C cAn) (tests D 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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} wherepre-tests-animae
Derivation, checked
pre-tests-animae : {C D : CAT Γ} → isAn C → isAn D → (f : MAP C D) → ((E : CAT Γ) → isAn E → IsEquiv (mapPre {D = E} f)) → IsEquiv f
Proof / implementation
pre-tests-animae {C} {D} cAn dAn f tests = pre-tests-isEquiv f (tests C cAn) (tests D 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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 prove (i) \(\Leftrightarrow \) (ii); the other case is dual. An inverse of \(f\) induces an inverse of every \(f_*\). Conversely, pick an inverse of \(f_*\colon \Map (D,C)\to \Map (D,D)\), and let \(g\colon D \to C\) be the evaluation of this inverse at \(\id _D\). The unit of the equivalence and the beta comparison for postcomposition give an identification \(f\circ g=\id _D\). Now, since \(f_*\colon \Map (C,C)\to \Map (C,D)\) is an equivalence, it induces an equivalence on animae of identifications. It follows that the chain of identifications \[ f \circ (g \circ f) = (f \circ g) \circ f = \id _D \circ f = f = f \circ \id _C \] lifts to an identification \(g\circ f=\id _C\). Here we use Construction 1.4.1 and the beta comparison to identify the action of \(f_*\) on functors with postcomposition by \(f\). If \(C\) and \(D\) are animae, both choices of \(E\) in this argument are animae, showing the final claim. □
Agda Postcomposition preserves equivalences
mapPost-isEquiv
Derivation, checked
mapPost-isEquiv : {A C D : CAT Γ} (f : MAP C D) → IsEquiv f → IsEquiv (mapPost {C = A} f)
Proof / implementation
mapPost-isEquiv {A} {C} {D} f e = record { inverse = mapPost (IsEquiv.inverse e) ; left-inverse-law = (mapPost-comp f (IsEquiv.inverse e)) ⁻¹ ∙ (mapPost⁼ (IsEquiv.left-inverse-law e) ∙ (mapPost-id A C) ⁻¹) ; right-inverse-law = (mapPost-comp (IsEquiv.inverse e) f) ⁻¹ ∙ (mapPost⁼ (IsEquiv.right-inverse-law e) ∙ (mapPost-id A 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Finding a section by specialization
mapPost-section
Derivation, checked
mapPost-section : {C D : CAT Γ} (f : MAP C D) → IsEquiv (mapPost {C = D} f) → Section f
Proof / implementation
mapPost-section {C} {D} f e = record { section = decode point ; section-law = (name-reflect _ _ (triangle chosen ∙ ((mapPost f ◁ name-decode point) ∙ (mapPost-name f (decode point)) ⁻¹))) ⁻¹ } where chosen : Factorization (mapPost f) (name (id D)) chosen = factor-through-equiv e (name (id D)) point : Obj-abs (Map D C) point = factor chosen
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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Reflecting the second inverse comparison
mapPost-reflect
Derivation, checked
mapPost-reflect : {B C D : CAT Γ} (f : MAP C D) → IsEquiv (mapPost {C = B} f) → (g h : MAP B C) → (f ∘ g) =₁ (f ∘ h) → g =₁ h
Proof / implementation
mapPost-reflect f e g h α = name-reflect g h (equiv-reflect e (name g) (name h) ((mapPost-name f h) ⁻¹ ∙ (name⁼ α ∙ mapPost-name f g)))
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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} wherepost-tests-isEquiv
Derivation, checked
post-tests-isEquiv : {C D : CAT Γ} (f : MAP C D) → IsEquiv (mapPost {C = C} f) → IsEquiv (mapPost {C = D} f) → IsEquiv f
Proof / implementation
post-tests-isEquiv {C} {D} f source-test target-test = record { inverse = g ; left-inverse-law = (mapPost-reflect f source-test (g ∘ f) (id C) ((comp-unitʳ f) ⁻¹ ∙ (comp-unitˡ f ∙ (((Section.section-law s) ⁻¹ ▷ f) ∙ (comp-assoc f g f) ⁻¹)))) ⁻¹ ; right-inverse-law = Section.section-law s } where s : Section f s = mapPost-section f target-test g : MAP D C g = Section.section s
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.Chapter01.Section04.EquivalenceDetection where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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.4.1 Collections of objects
We now define the groupoid core of a category, which we may think of as its collection of objects.
Definition 1.4.12. For any category \(C\), we define the groupoid core of \(C\) to be \[ C^\simeq :=\Map (*,C). \] It comes equipped with the canonical functor \[ \imath _C\colon C^\simeq \simeq C^\simeq \times * \xrightarrow {\ev _{\Map }}C. \]
Agda The groupoid core and its inclusion
Core
Definition, checked
Core : 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.Chapter01.Section04.Core where
module _ {Γ : Context} wherecoreInclusion
Definition, checked
coreInclusion : (C : CAT Γ) → MAP (Core C) C
Proof / implementation
coreInclusion C = mapEval ∘ product-unitʳ-inverse (Core 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.Chapter01.Section04.Core where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 functor \(\imath _C\) displays the objects of \(C\) with the anima \(C^\simeq \) as parameter. It is universal among functors from animae in the following sense.
Corollary 1.4.13 (Universal property of the groupoid core). For any anima \(X\) and any category \(D\), postcomposition induces an equivalence \[ (\imath _D)_*\colon \Map (X,D^\simeq )\iso \Map (X,D). \]
Agda Universal property of the groupoid core
core-universal
Derivation, checked
core-universal : (X C : CAT Γ) → isAn X → IsEquiv (mapPost {C = X} (coreInclusion C))
Proof / implementation
core-universal = Universality.postcomposition-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.Chapter01.Section04.Core where
module _ {Γ : Context} whereroute-is-postcomposition
Derivation, checked
route-is-postcomposition : uncurrying-route =₁ (mapPost (coreInclusion C))
Proof / implementation
route-is-postcomposition = uncurry-reflect (map-isAn X (Core C)) _ _ ((mapPost-β (coreInclusion C)) ⁻¹ ∙ (core-evaluation (mapEval {C = X} {D = Core C}) ∙ ((uncurry (mapEval {C = X} {D = Core C}) ◁ regroup-insert) ∙ (comp-assoc (productMap (id N) (product-unitʳ-inverse X)) (Associativity.backward N X One) (uncurry (mapEval {C = X} {D = Core C})) ∙ ((ExponentialLaw.forward-β X One C ▷ productMap (id N) (product-unitʳ-inverse X)) ∙ mapPre-uncurry (product-unitʳ-inverse X) (mapUncurrying X One 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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module Universality (X C : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Proposition 1.4.2 and the equivalence \(X\times *\simeq X\), there are equivalences \[ \Map (X,D^\simeq ) =\Map (X,\Map (*,D)) \simeq \Map (X\times *,D) \simeq \Map (X,D). \] By the definition of \(\imath _D\), their composite is postcomposition with \(\imath _D\). □
Remark 1.4.14. The anima \(C^\simeq \) also describes all functors of the form \(x\colon \Gamma \to C\) where \(\Gamma \) is an anima. By the previous result, it suffices to understand the universal such functor, i.e. \(\imath _C\colon C^\simeq \to C\).
Proposition 1.4.15. For every anima \(A\), the canonical functor \(\imath _A\colon A^\simeq \to A\) is an equivalence. Its inverse is obtained by currying the projection \(A\times *\to A\).
Agda Absolute objects and the terminal context
backward
Derivation, checked
backward : MAP (Map One A) A
Proof / implementation
backward = coreInclusion A
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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module AnimaCoreEquivalence (A : CAT Γ) (aAn : isAn A) whereforward
Derivation, checked
forward : MAP A (Map One A)
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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module AnimaCoreEquivalence (A : CAT Γ) (aAn : isAn A) wherecore-of-anima
Derivation, checked
core-of-anima : (C : CAT Γ) → isAn C → IsEquiv (coreInclusion C)
Proof / implementation
core-of-anima C cAn = post-tests-animae (core-isAn C) cAn (coreInclusion C) (λ X xAn → core-universal X C xAn)
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.Chapter01.Section04.Core where
module _ {Γ : Context} whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 Evaluation as the inverse for absolute objects
forward
Definition, checked
forward : MAP A (Map One A)
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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module AnimaCoreEquivalence (A : CAT Γ) (aAn : isAn A) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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. For every anima \(X\), postcomposition with \(\imath _A\) induces an equivalence by Corollary 1.4.13. Since both \(A^\simeq \) and \(A\) are animae, Proposition 1.4.11 shows that \(\imath _A\) is an equivalence. The defining identification for currying identifies its composite with the stated inverse with \(\id _A\). □
Agda The two comparisons for absolute objects
backward-forward
Derivation, checked
backward-forward : (backward ∘ forward) =₁ (id A)
Proof / implementation
backward-forward = pair-β₁ (id A) (terminate A) ∙ ((forward-β ▷ product-unitʳ-inverse A) ∙ ((comp-assoc (product-unitʳ-inverse A) (productMap forward (id One)) mapEval) ⁻¹ ∙ ((mapEval ◁ (product-unitʳ-inverse-natural forward) ⁻¹) ∙ comp-assoc forward (product-unitʳ-inverse (Map One A)) mapEval)))
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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module AnimaCoreEquivalence (A : CAT Γ) (aAn : isAn A) whereforward-backward
Derivation, checked
forward-backward : (forward ∘ backward) =₁ (id (Map One A))
Proof / implementation
forward-backward = equiv-reflect backward-isEquiv _ _ ((comp-unitʳ backward) ⁻¹ ∙ (comp-unitˡ backward ∙ ((backward-forward ▷ backward) ∙ (comp-assoc backward forward backward) ⁻¹)))
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.Chapter01.Section04.Core where
module _ {Γ : Context} where
module AnimaCoreEquivalence (A : CAT Γ) (aAn : isAn A) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 1.4.16. A functor \(f\colon C\to D\) induces a functor \[ f^\simeq :=f_*\colon C^\simeq =\Map (*,C)\longrightarrow \Map (*,D)=D^\simeq . \] The defining identification for postcomposition makes the square
Agda Functoriality of cores
mapPost
Definition, checked
mapPost : {C D E : CAT Γ} → MAP D E → MAP (Map C D) (Map C 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.Chapter01.Section04.Functoriality where
module _ {Γ : Context} whereAbout this correspondence
Core is Map(One,-), so its action is the terminal-source specialization of mapPost. The older Chapter 2 naturality declaration is not part of this edition.
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.
commute. There are identifications \((\id _C)^\simeq =\id _{C^\simeq }\) and \(g^\simeq \circ f^\simeq =(g\circ f)^\simeq \), obtained by uncurrying and using the unit and associativity identifications for functors; the latter is the case \(E=*\) of Proposition 1.4.9. An identification \(\alpha :f=f'\) similarly induces an identification \(\alpha ^\simeq :f^\simeq =(f')^\simeq \), by whiskering \(\alpha \) with evaluation and then currying.
Lemma 1.4.17. For categories \(C\) and \(D\), the functor \((\pr _{C}^{\simeq }, \pr _{D}^{\simeq })\colon (C \times D)^{\simeq } \to C^{\simeq } \times D^{\simeq }\) is an equivalence.
Agda Cores preserve products
forward-isEquiv
Derivation, checked
forward-isEquiv : IsEquiv forward
Proof / implementation
forward-isEquiv = record { inverse = backward ; left-inverse-law = backward-forward ⁻¹ ; right-inverse-law = forward-backward ⁻¹ }
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.Chapter01.Section04.MappingProducts where
module _ {Γ : Context} where
module ProductEquivalence (E C D : CAT Γ) whereAbout this correspondence
This links to the current context-indexed formalization in rebuild2. The hypotheses are shown in the declaration and its enclosing context.
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 is a special case of Proposition 1.4.5. □
Supplementary notes
- Decoding mapping animae and restriction AI-generated