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.7 Functor categories
Given two categories \(C\) and \(D\), we are interested in forming the functor category \(\Fun (C,D)\) whose objects are precisely the functors from \(C\) to \(D\).
Agda Functor categories
Fun
Assumption, type checked
Fun : 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.Section07.FunctorCategories 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.
Given any functor \(e \colon F \times C\to D\) and any category \(T\), we can form a functor \[ \mathit {u}_T\colon \Map (T,F)\to \Map (T\times C,D) \] by currying the composite \[ \Map (T,F)\times T\times C \xrightarrow {\ev _{\Map } \times \id _C} F\times C\xrightarrow {e} D. \] It satisfies the property that it evaluations on an absolute object of \(\Map (T,F)\), corresponding to a functor \(g\colon T\to F\), as \[ \mathit {u}_T(g)= e\circ (g\times \id _C). \]
Agda The evaluation-induced functor
evaluation-forward
Derivation, checked
evaluation-forward : MAP (Map T F) (Map (T × C) D)
Proof / implementation
evaluation-forward = mapCurry (map-isAn T F) evaluation-universal
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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : CAT Γ) whereevaluation-represents
Derivation, checked
evaluation-represents : {P : CAT Γ} (g : MAP P (Map T F)) → uncurry (evaluation-forward ∘ g) =₁ (evaluate (uncurry g) ∘ Associativity.backward P T C)
Proof / implementation
evaluation-represents {P} g = ((evaluate-restrict mapEval (productMap g (id T))) ⁻¹ ▷ Associativity.backward P T C) ∙ ((comp-assoc (Associativity.backward P T C) (productMap (productMap g (id T)) (id C)) (evaluate mapEval)) ⁻¹ ∙ (((evaluate mapEval) ◁ Reassociation.backward-natural g) ∙ (comp-assoc (productMap g (id (T × C))) (Associativity.backward (Map T F) T C) (evaluate mapEval) ∙ ((mapCurry-β (map-isAn T F) evaluation-universal ▷ productMap g (id (T × C))) ∙ Mapping.uncurry-restrict evaluation-forward 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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : 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 Currying the evaluation family
evaluation-forward
Derivation, checked
evaluation-forward : MAP (Map T F) (Map (T × C) D)
Proof / implementation
evaluation-forward = mapCurry (map-isAn T F) evaluation-universal
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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : CAT Γ) whereevaluation-represents
Derivation, checked
evaluation-represents : {P : CAT Γ} (g : MAP P (Map T F)) → uncurry (evaluation-forward ∘ g) =₁ (evaluate (uncurry g) ∘ Associativity.backward P T C)
Proof / implementation
evaluation-represents {P} g = ((evaluate-restrict mapEval (productMap g (id T))) ⁻¹ ▷ Associativity.backward P T C) ∙ ((comp-assoc (Associativity.backward P T C) (productMap (productMap g (id T)) (id C)) (evaluate mapEval)) ⁻¹ ∙ (((evaluate mapEval) ◁ Reassociation.backward-natural g) ∙ (comp-assoc (productMap g (id (T × C))) (Associativity.backward (Map T F) T C) (evaluate mapEval) ∙ ((mapCurry-β (map-isAn T F) evaluation-universal ▷ productMap g (id (T × C))) ∙ Mapping.uncurry-restrict evaluation-forward 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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : 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 Evaluation on a represented functor
evaluation-specialize
Derivation, checked
evaluation-specialize : (g : MAP T F) → specialize-map evaluation-forward g =₁ evaluate g
Proof / implementation
evaluation-specialize g = evaluate-cong (decode-name g) ∙ evaluation-decode (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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : 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.
Definition 1.7.1. A functor category from \(C\) to \(D\) is a category \(F\) equipped with a functor \(e\colon F\times C\to D\) such that, for any category \(T\), the induced map \[ \mathit {u}_T\colon \Map (T,F)\iso \Map (T\times C,D) \] is an equivalence. We then call \(F\) the category of functors from \(C\) to \(D\) and \(e\) the evaluation functor.
Agda The universal property of a functor category
IsFunctorCategory
Definition, checked
IsFunctorCategory : {F C D : CAT Γ} → MAP (F × C) D → Set (c ⊔ m)
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.FunctorCategories 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.
Proposition 1.7.2. If \(F\) and \(F'\) both are categories of functors from \(C\) to \(D\) with evaluation functors \(e\) and \(e'\) respectively, then there is an equivalence \(\varphi \colon F'\iso F\) as well as \(\sigma \colon e\circ (\varphi \times \id _C)= e'\).
Agda Uniqueness of functor categories
functor-category-comparison-isEquiv
Derivation, checked
functor-category-comparison-isEquiv : IsEquiv functor-category-comparison
Proof / implementation
functor-category-comparison-isEquiv = record { inverse = back; left-inverse-law = left ⁻¹; right-inverse-law = right ⁻¹ } where back : MAP G F back = curry e u d left : (back ∘ functor-category-comparison) =₁ id F left = reflect e u _ _ ((evaluate-id e) ⁻¹ ∙ (functor-category-comparison-β ∙ ((curry-β e u d ▷ productMap functor-category-comparison (id C)) ∙ evaluate-restrict e back functor-category-comparison))) right : (functor-category-comparison ∘ back) =₁ id G right = reflect d v _ _ ((evaluate-id d) ⁻¹ ∙ (curry-β e u d ∙ ((functor-category-comparison-β ▷ productMap back (id C)) ∙ evaluate-restrict d functor-category-comparison back)))
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.Section07.Currying where
module _ {Γ : Context} {F G C D : CAT Γ}
(e : MAP (F × C) D) (u : IsFunctorCategory e)
(d : MAP (G × C) D) (v : IsFunctorCategory d) 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. Let \(v\) be an inverse of the equivalence \(u_{F'}\colon \Map (F',F)\iso \Map (F'\times C,D)\) and define \(\varphi :=v(e')\colon F'\to F\). By Construction 1.4.1, the identification \(u_{F'}\circ v=\id \) and the beta comparison for \(u_{F'}\) provide \[ \sigma \colon e\circ (\varphi \times \id _C)= e'. \] Exchanging the roles of \((F,e)\) and \((F',e')\), we similarly obtain a functor \(\psi \colon F\to F'\) together with \(e'\circ (\psi \times \id _C)= e\). Combining the two, the uncurried functors associated to \(\varphi \circ \psi \) and \(\id _F\) are identified: \[ e\circ ((\varphi \circ \psi )\times \id _C) = e'\circ (\psi \times \id _C) = e = e\circ (\id _F\times \id _C). \] Since \(u_F\) is an equivalence, it reflects this identification and gives \(\varphi \circ \psi =\id _F\). The same argument shows \(\psi \circ \varphi =\id _{F'}\), so \(\varphi \) is an equivalence with inverse \(\psi \). □
Agda Constructing the comparison functor
functor-category-comparison
Definition, checked
functor-category-comparison : MAP 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.Section07.Currying where
module _ {Γ : Context} {F G C D : CAT Γ}
(e : MAP (F × C) D) (u : IsFunctorCategory e)
(d : MAP (G × C) D) (v : IsFunctorCategory d) 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 comparison with evaluation
functor-category-comparison-β
Derivation, checked
functor-category-comparison-β : evaluate d functor-category-comparison =₁ 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.Section07.Currying where
module _ {Γ : Context} {F G C D : CAT Γ}
(e : MAP (F × C) D) (u : IsFunctorCategory e)
(d : MAP (G × C) D) (v : IsFunctorCategory d) 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 comparison in the opposite direction
functor-category-comparison-isEquiv
Derivation, checked
functor-category-comparison-isEquiv : IsEquiv functor-category-comparison
Proof / implementation
functor-category-comparison-isEquiv = record { inverse = back; left-inverse-law = left ⁻¹; right-inverse-law = right ⁻¹ } where back : MAP G F back = curry e u d left : (back ∘ functor-category-comparison) =₁ id F left = reflect e u _ _ ((evaluate-id e) ⁻¹ ∙ (functor-category-comparison-β ∙ ((curry-β e u d ▷ productMap functor-category-comparison (id C)) ∙ evaluate-restrict e back functor-category-comparison))) right : (functor-category-comparison ∘ back) =₁ id G right = reflect d v _ _ ((evaluate-id d) ⁻¹ ∙ (curry-β e u d ∙ ((functor-category-comparison-β ▷ productMap back (id C)) ∙ evaluate-restrict d functor-category-comparison back)))
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.Section07.Currying where
module _ {Γ : Context} {F G C D : CAT Γ}
(e : MAP (F × C) D) (u : IsFunctorCategory e)
(d : MAP (G × C) D) (v : IsFunctorCategory d) 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 two inverse comparisons
functor-category-comparison-isEquiv
Derivation, checked
functor-category-comparison-isEquiv : IsEquiv functor-category-comparison
Proof / implementation
functor-category-comparison-isEquiv = record { inverse = back; left-inverse-law = left ⁻¹; right-inverse-law = right ⁻¹ } where back : MAP G F back = curry e u d left : (back ∘ functor-category-comparison) =₁ id F left = reflect e u _ _ ((evaluate-id e) ⁻¹ ∙ (functor-category-comparison-β ∙ ((curry-β e u d ▷ productMap functor-category-comparison (id C)) ∙ evaluate-restrict e back functor-category-comparison))) right : (functor-category-comparison ∘ back) =₁ id G right = reflect d v _ _ ((evaluate-id d) ⁻¹ ∙ (curry-β e u d ∙ ((functor-category-comparison-β ▷ productMap back (id C)) ∙ evaluate-restrict d functor-category-comparison back)))
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.Section07.Currying where
module _ {Γ : Context} {F G C D : CAT Γ}
(e : MAP (F × C) D) (u : IsFunctorCategory e)
(d : MAP (G × C) D) (v : IsFunctorCategory d) 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.
Axiom B.8 (Functor category). For any two categories \(C\) and \(D\), there is a category \(\Fun (C, D)\) equipped with an evaluation functor \(\ev \colon \Fun (C,D) \times C \to D\) that exhibits it as a functor category from \(C\) to \(D\).
Agda The functor-category axiom
Fun
Assumption, type checked
Fun : 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.Section07.FunctorCategories where
module _ {Γ : Context} wherefunEval
Assumption, type checked
funEval : {C D : CAT Γ} → MAP (Fun 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.Section07.FunctorCategories where
module _ {Γ : Context} wherefunUniversal
Assumption, type checked
funUniversal : (C D : CAT Γ) → IsFunctorCategory (funEval {C = C} {D = 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.Section07.FunctorCategories 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.
Definition 1.7.3. Given another category \(T\), choose an inverse \(v_T\) of the equivalence \(\mathit {u}_T\). For a functor \(f\colon T\times C\to D\), define its currying by applying \(v_T\): \[ f_c:=v_T(f)\colon T\longrightarrow \Fun (C,D). \] It comes equipped with a commutative diagram as follows:
Agda Currying
curry
Definition, checked
curry : {T : CAT Γ} → MAP (T × C) D → MAP T F
Proof / implementation
curry f = SpecializationFactorization.factor (chosen-factor 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) 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 computation comparison
curry-β
Derivation, checked
curry-β : {T : CAT Γ} (f : MAP (T × C) D) → evaluate e (curry f) =₁ f
Proof / implementation
curry-β {T} f = SpecializationFactorization.triangle (chosen-factor f) ∙ (evaluation-specialize e T (curry 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) 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.
Conversely, given a functor \(g\colon T \to \Fun (C,D)\), we call the composite \[ T \times C \xrightarrow {g \times \id _C} \Fun (C,D) \times C \xrightarrow {\ev } D \] the uncurrying of \(g\) and denote it by \(g^u\). The discussion before shows it is identified with \(\mathit {u}_T(g)\). Similarly, an identification \(\beta \colon g= h\) induces an identification \(\beta ^u\colon g^u= h^u\). At the level of mapping animae, uncurrying is the equivalence \[ (-)^u \colon \Map (T,\Fun (C,D))\iso \Map (T\times C,D) \] with inverse defined by currying.
Agda Uncurrying
funUncurry
Definition, checked
funUncurry : {T : CAT Γ} → MAP T (Fun C D) → MAP (T × 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.Section07.Currying 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 The mapping-anima beta comparison
evaluation-specialize
Derivation, checked
evaluation-specialize : (g : MAP T F) → specialize-map evaluation-forward g =₁ evaluate g
Proof / implementation
evaluation-specialize g = evaluate-cong (decode-name g) ∙ evaluation-decode (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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : 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 identifications
evaluate⁼
Derivation, checked
evaluate⁼ : {T : CAT Γ} {f g : MAP T F} → f ＝ g → evaluate f ＝ evaluate 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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) 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 Currying is inverse to uncurrying
curry-β
Derivation, checked
curry-β : {T : CAT Γ} (f : MAP (T × C) D) → evaluate e (curry f) =₁ f
Proof / implementation
curry-β {T} f = SpecializationFactorization.triangle (chosen-factor f) ∙ (evaluation-specialize e T (curry 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) wherecurry-η
Derivation, checked
curry-η : {T : CAT Γ} (g : MAP T F) → curry (evaluate e g) =₁ g
Proof / implementation
curry-η g = representation-unique (curried-representation (evaluate e g)) (record { term = g; evaluation = id₌ (evaluate e 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) 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 parallel functors \(g,h\colon T\to \Fun (C,D)\), the induced functor \[ (g= h)\longrightarrow (g^u= h^u) \] is an equivalence. Indeed, represent \(g,h\) by points of \(\Map (T,\Fun (C,D))\), apply Lemma 1.3.10 to \(\mathit {u}_T\), and use Construction 1.4.1 at both ends.
Agda The equivalence on identification animae
evaluation-action-isEquiv
Derivation, checked
evaluation-action-isEquiv : IsEquiv (evaluation-forward e T) → (f g : MAP T F) → IsEquiv (evaluation-action e f g)
Proof / implementation
evaluation-action-isEquiv universal f g = endpoint-change-preserves-isEquiv (specialize⁼-functor (evaluation-forward e T) f g) (evaluation-action e f g) (evaluation-specialize e T f) (evaluation-specialize e T g) (replace-edges₌ (comp-unitʳ (specialize⁼-functor (evaluation-forward e T) f g)) (id₌ (evaluation-action e f g)) (evaluation-specialize-inputs (id (Equal f g)))) (specialize⁼-isEquiv (evaluation-forward e T) universal 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.Section07.EvaluationRepresentation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) (T : 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.
Notation 1.7.4. In term notation, an expression \(x:T,y:C\vdash f(x,y):D\) may therefore be curried to \(x:T\vdash (y\mapsto f(x,y)):\Fun (C,D)\). Conversely, evaluation of \(x:T\vdash F(x):\Fun (C,D)\) and \(x:T\vdash c(x):C\) is formed by pairing, giving \(x:T\vdash F(x)(c(x)):D\). These conventions also apply to identifications of the whole functors, with the beta and eta comparisons above.
Agda Currying in term notation
curry
Definition, checked
curry : {T : CAT Γ} → MAP (T × C) D → MAP T F
Proof / implementation
curry f = SpecializationFactorization.factor (chosen-factor 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) 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 Beta and eta for the whole functors
curry-β
Derivation, checked
curry-β : {T : CAT Γ} (f : MAP (T × C) D) → evaluate e (curry f) =₁ f
Proof / implementation
curry-β {T} f = SpecializationFactorization.triangle (chosen-factor f) ∙ (evaluation-specialize e T (curry 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) wherecurry-η
Derivation, checked
curry-η : {T : CAT Γ} (g : MAP T F) → curry (evaluate e g) =₁ g
Proof / implementation
curry-η g = representation-unique (curried-representation (evaluate e g)) (record { term = g; evaluation = id₌ (evaluate e 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.Section07.Currying where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (universal : IsFunctorCategory e) whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.
Remark 1.7.5. By considering the terminal category, we observe that absolute objects \(*\to \Fun (C,D)\) correspond to functors \(C\simeq *\times C\to D\), justifying the notation and terminology of \(\Fun (C,D)\).
Agda Functors as absolute objects
funName
Derivation, checked
funName : {C D : CAT Γ} → MAP C D → MAP One (Fun 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.Section07.CoreOfFun where
module _ {Γ : Context} wherefunName-β
Derivation, checked
funName-β : {C D : CAT Γ} (g : MAP C D) → funUncurry {C = C} {D = D} (funName g) =₁ (g ∘ pr₂ {C = One} {D = 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.Section07.CoreOfFun where
module _ {Γ : Context} whereAbout this correspondence
The current links show the chosen point representing an ordinary functor and its evaluation comparison. They do not constitute a separate formalized equivalence of Agda types of absolute objects.
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.7.6 (Evaluation functor). Given categories \(C\) and \(D\), and \(x \colon *\to C\), the evaluation functor at \(x\) is defined as the composite \[ \ev _x\colon \Fun (C,D) \simeq \Fun (C,D) \times * \xrightarrow {\id \times x} \Fun (C,D) \times C \xrightarrow {\ev } D. \]
Agda Evaluation at an absolute object
evaluate
Definition, checked
evaluate : {T : CAT Γ} → MAP T F → MAP (T × 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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) whereAbout this correspondence
Evaluation at an absolute object is obtained by specializing this evaluation operation to a point with source One. The current formalization keeps the general evaluation operation instead of a separate evalAt abbreviation.
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 functoriality of the product naturally provides functoriality for the functor categories:
Construction 1.7.7 (Functoriality of functor categories). Given a functor \(g\colon D \to D'\), we define the functor \(g \circ -\colon \Fun (C,D) \to \Fun (C,D')\) as the currying of the composite \[ \Fun (C, D) \times C \xrightarrow {\ev } D \xrightarrow {g} D'. \] By assumption we obtain a commutative square as follows:
Agda Postcomposition on functor categories
funPost
Definition, checked
funPost : {C D E : CAT Γ} → MAP D E → MAP (Fun C D) (Fun C E)
Proof / implementation
funPost {C} {D} {E} f = funCurry {C = C} {D = E} (f ∘ funEval {C = C} {D = 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.Section07.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 Postcomposition and evaluation
funPost-β
Derivation, checked
funPost-β : {C D E : CAT Γ} (f : MAP D E) → funUncurry {C = C} {D = E} (funPost {C = C} f) =₁ (f ∘ funEval {C = C} {D = D})
Proof / implementation
funPost-β {C} {D} {E} f = funCurry-β {C = C} {D = E} (f ∘ funEval {C = C} {D = 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.Section07.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.
Similarly, given a functor \(f\colon C' \to C\), we define the functor \(- \circ f\colon \Fun (C,D) \to \Fun (C',D)\) as the currying of the composite \[ \Fun (C,D) \times C' \xrightarrow {\id \times f} \Fun (C,D) \times C \xrightarrow {\ev } D. \] It satisfies the property that it makes the following square commute:
Agda Precomposition on functor categories
funPre
Definition, checked
funPre : {B C D : CAT Γ} → MAP B C → MAP (Fun C D) (Fun B D)
Proof / implementation
funPre {B} {C} {D} k = funCurry {C = B} {D = D} (funEval {C = C} {D = D} ∘ productMap (id (Fun C D)) 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.Section07.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 and evaluation
funPre-β
Derivation, checked
funPre-β : {B C D : CAT Γ} (k : MAP B C) → funUncurry {C = B} {D = D} (funPre {D = D} k) =₁ (funEval {C = C} {D = D} ∘ productMap (id (Fun C D)) k)
Proof / implementation
funPre-β {B} {C} {D} k = funCurry-β {C = B} {D = D} (funEval {C = C} {D = D} ∘ productMap (id (Fun C D)) 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.Section07.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.
In a completely analogous way, every identification \(\beta \colon g = g'\) of functors \(D \to D'\) induces an identification \((\beta \circ -) \colon (g \circ -) = (g' \circ -)\) of functors \(\Fun (C,D) \to \Fun (C, D')\), and similarly for the construction \(- \circ f\).
Agda Composition acts on identifications
funPost-cong
Derivation, checked
funPost-cong : {C D E : CAT Γ} {f g : MAP D E} → f =₁ g → funPost {C = C} f =₁ funPost {C = C} 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.Section07.Functoriality where
module _ {Γ : Context} wherefunPre-cong
Derivation, checked
funPre-cong : {B C D : CAT Γ} {k l : MAP B C} → k =₁ l → funPre {D = D} k =₁ funPre {D = D} l
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.Section07.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.
Exercise 1.7.8 (Exercise 1.9.6 (outside selection)). Formulate and prove that the assignments \(g \mapsto (g \circ -)\) and \(f \mapsto (- \circ f)\) are functorial, in the sense that they respect identity functors and composition of functors.
Agda Identity and composition laws
funPost-id
Derivation, checked
funPost-id : (C D : CAT Γ) → funPost {C = C} (id D) =₁ id (Fun C D)
Proof / implementation
funPost-id C D = reflect (funEval {C = C} {D = D}) (funUniversal C D) _ _ ((evaluate-id (funEval {C = C} {D = D})) ⁻¹ ∙ (comp-unitˡ (funEval {C = C} {D = D}) ∙ funPost-β {C = C} (id 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.Section07.Functoriality where
module _ {Γ : Context} wherefunPre-id
Derivation, checked
funPre-id : (C D : CAT Γ) → funPre {D = D} (id C) =₁ id (Fun C D)
Proof / implementation
funPre-id C D = reflect (funEval {C = C} {D = D}) (funUniversal C D) _ _ ((evaluate-id (funEval {C = C} {D = D})) ⁻¹ ∙ (comp-unitʳ (funEval {C = C} {D = D}) ∙ ((funEval {C = C} {D = D} ◁ productMap-id (Fun C D) C) ∙ funPre-β {D = D} (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.Section07.Functoriality where
module _ {Γ : Context} wherefunPost-comp
Derivation, checked
funPost-comp : {A B C D : CAT Γ} (f : MAP B C) (g : MAP C D) → (funPost {C = A} g ∘ funPost {C = A} f) =₁ funPost {C = A} (g ∘ f)
Proof / implementation
funPost-comp {A} {B} {C} {D} f g = reflect (funEval {C = A} {D = D}) (funUniversal A D) _ _ ((funPost-β {C = A} (g ∘ f)) ⁻¹ ∙ ((comp-assoc (funEval {C = A} {D = B}) f g) ⁻¹ ∙ ((g ◁ funPost-β {C = A} f) ∙ funPost-uncurry g (funPost {C = A} 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.Section07.Functoriality where
module _ {Γ : Context} wherefunPre-comp
Derivation, checked
funPre-comp : {A B C D : CAT Γ} (f : MAP A B) (g : MAP B C) → (funPre {D = D} f ∘ funPre {D = D} g) =₁ funPre {D = D} (g ∘ f)
Proof / implementation
funPre-comp {A} {B} {C} {D} f g = reflect (funEval {C = A} {D = D}) (funUniversal A D) _ _ ((funPre-β {D = D} (g ∘ f)) ⁻¹ ∙ ((funEval {C = C} {D = D} ◁ (productMap-cong (comp-unitˡ (id (Fun C D))) (id₌ (g ∘ f)) ∙ productMap-comp (id (Fun C D)) (id (Fun C D)) f g)) ∙ (comp-assoc (productMap (id (Fun C D)) f) (productMap (id (Fun C D)) g) (funEval {C = C} {D = D}) ∙ ((funPre-β {D = D} g ▷ productMap (id (Fun C D)) f) ∙ funPre-uncurry f (funPre {D = D} 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.Section07.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.
1.7.1 Properties of functor categories
The universal property of functor categories allows us to deduce their compatibilities with the terminal category, the initial category, products, coproducts and pullbacks from the corresponding properties of mapping animae. We will use Proposition 1.4.11 to test the comparison functors after applying \(\Map (T,-)\).
Lemma 1.7.9. For every category \(C\) the functor category \(\Fun (C,*)\) is contractible.
Agda Functors into the terminal category
funTerminal-isEquiv
Derivation, checked
funTerminal-isEquiv : (C : CAT Γ) → IsEquiv (terminate (Fun C One))
Proof / implementation
funTerminal-isEquiv C = record { inverse = funTerminalPoint C ; left-inverse-law = (reflect (funEval {C = C} {D = One}) (funUniversal C One) (funTerminalPoint C ∘ terminate (Fun C One)) (id (Fun C One)) (terminal-identification _ _)) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.FunctorProperties 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. For every category \(T\), the universal property of the functor category gives \[ \Map (T,\Fun (C,*))\simeq \Map (T\times C,*)\simeq *, \] where the last equivalence is Lemma 1.4.4. Thus \(\Fun (C,*)\to *\) induces an equivalence on mapping animae for every \(T\), and is an equivalence by Proposition 1.4.11. □
Agda Testing the terminal comparison on mapping animae
funTerminal-isEquiv
Derivation, checked
funTerminal-isEquiv : (C : CAT Γ) → IsEquiv (terminate (Fun C One))
Proof / implementation
funTerminal-isEquiv C = record { inverse = funTerminalPoint C ; left-inverse-law = (reflect (funEval {C = C} {D = One}) (funUniversal C One) (funTerminalPoint C ∘ terminate (Fun C One)) (id (Fun C One)) (terminal-identification _ _)) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.FunctorProperties where
module _ {Γ : Context} whereAbout this correspondence
The corresponding result is proved in rebuild2, but its current proof is not identified here with the particular mapping-anima chain in this paragraph. Open the full declaration to inspect the actual argument.
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 Detection of the terminal equivalence
funTerminal-isEquiv
Derivation, checked
funTerminal-isEquiv : (C : CAT Γ) → IsEquiv (terminate (Fun C One))
Proof / implementation
funTerminal-isEquiv C = record { inverse = funTerminalPoint C ; left-inverse-law = (reflect (funEval {C = C} {D = One}) (funUniversal C One) (funTerminalPoint C ∘ terminate (Fun C One)) (id (Fun C One)) (terminal-identification _ _)) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.FunctorProperties 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.
Lemma 1.7.10. Let \(C\), \(D\) and \(E\) be categories. Then the functor \[ (\pr _1 \circ \blank , \pr _2 \circ \blank )\colon \Fun (C, D \times E) \to \Fun (C, D) \times \Fun (C,E) \] is an equivalence.
Agda Functor categories preserve products
forward
Definition, 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.Section07.FunctorProducts where
module ProductComparison {Γ : Context} (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.Section07.FunctorProducts where
module ProductComparison {Γ : Context} (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. For every category \(T\), the universal property of functor categories and Proposition 1.4.5 give equivalences \[ \begin {aligned} \Map (T,\Fun (C,D\times E)) &\simeq \Map (T\times C,D\times E)\\ &\simeq \Map (T\times C,D)\times \Map (T\times C,E)\\ &\simeq \Map (T,\Fun (C,D))\times \Map (T,\Fun (C,E))\\ &\simeq \Map (T,\Fun (C,D)\times \Fun (C,E)). \end {aligned} \] This composite is induced by the functor in the statement: after uncurrying, its two components are postcomposition with \(\pr _1\) and \(\pr _2\), by Lemma 1.7.7. The result follows from Proposition 1.4.11. □
Agda The product comparison on mapping animae
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.Section07.FunctorProducts where
module ProductComparison {Γ : Context} (E C D : CAT Γ) whereAbout this correspondence
The corresponding result is proved in rebuild2, but its current proof is not identified here with the particular mapping-anima chain in this paragraph. Open the full declaration to inspect the actual argument.
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 Identifying the specified product functor
forward
Definition, 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.Section07.FunctorProducts where
module ProductComparison {Γ : Context} (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.
Agda Detecting the product equivalence
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.Section07.FunctorProducts where
module ProductComparison {Γ : Context} (E C D : CAT Γ) whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Lemma 1.7.11. Let \(T\) be a category and let \(f\colon C \to E\) and \(g\colon D \to E\) be functors. Then the functor \[ (\pr _1 \circ \blank , \pr _2 \circ \blank )\colon \Fun (T,C \times _{E} D) \to \Fun (T,C) \times _{\Fun (T,E)} \Fun (T,D) \] induced by the identification \((f \circ \blank ) \circ (\pr _1 \circ \blank ) = (g \circ \blank ) \circ (\pr _2 \circ \blank )\) is an equivalence.
Agda Functor categories preserve pullbacks
fun-preserves-pullback
Derivation, checked
fun-preserves-pullback : (s : Cone f g S) → IsPullback s → IsPullback (mappedCone s)
Proof / implementation
fun-preserves-pullback = Preservation.isPullback
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.FunctorPullbacks where
module _ {Γ : Context} {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (K : CAT Γ) wherecomparison-isEquiv
Derivation, checked
comparison-isEquiv : IsEquiv comparison
Proof / implementation
comparison-isEquiv = fun-preserves-pullback K (pullback-cone f g) (pullback-cone-isPullback 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.Section07.FunctorPullbacks where
module FunctorPullback {Γ : Context} (K : CAT Γ) {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) whereAbout this correspondence
The current proof uses native evaluation and complete cone comparisons. It proves preservation for the specified mapped cone; it does not identify its proof steps with the earlier uncurrying-square implementation.
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.6.3, it suffices to show that the pullback square defining \(C \times _E D\) remains a pullback square after applying \(\Map (S,\Fun (T,-))\) for every category \(S\). Under uncurrying, its four corners are identified with \[ \Map (S\times T,C\times _E D),\quad \Map (S\times T,C),\quad \Map (S\times T,D),\quad \Map (S\times T,E). \] By Lemma 1.7.7, the four functors become postcomposition with the original projections, \(f\), and \(g\). These comparisons respect the specified commutativity identification, as follows by uncurrying its defining postcomposition identification. We conclude that this square agrees with the one obtained by applying \(\Map (S \times T, -)\) to the original pullback square, including its commutativity data. So the resulting square is a pullback by Proposition 1.6.3. □
Agda Testing the mapped pullback square
fun-preserves-pullback
Derivation, checked
fun-preserves-pullback : (s : Cone f g S) → IsPullback s → IsPullback (mappedCone s)
Proof / implementation
fun-preserves-pullback = Preservation.isPullback
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.FunctorPullbacks where
module _ {Γ : Context} {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (K : 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 the four corners
evaluation-forward
Definition, checked
evaluation-forward : MAP (Map T F) (Map (T × C) D)
Proof / implementation
evaluation-forward = mapCurry (map-isAn T F) evaluation-universal
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.Section07.Evaluation where
module _ {Γ : Context} {F C D : CAT Γ} (e : MAP (F × C) D) where
module _ (T : 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 commutes with postcomposition
funPost-uncurry
Derivation, checked
funPost-uncurry : {T C D E : CAT Γ} (f : MAP D E) (g : MAP T (Fun C D)) → funUncurry {C = C} {D = E} (funPost {C = C} f ∘ g) =₁ (f ∘ funUncurry {C = C} {D = D} g)
Proof / implementation
funPost-uncurry {C = C} {D} {E} f g = comp-assoc (productMap g (id C)) (funEval {C = C} {D = D}) f ∙ ((funPost-β {C = C} f ▷ productMap g (id C)) ∙ evaluate-restrict (funEval {C = C} {D = E}) (funPost {C = C} 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.Section07.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 Uncurrying respects the specified matching
match-β
Derivation, checked
match-β : Cone.match (uncurryCone value) =₂ desired
Proof / implementation
match-β = restore-boundaries leftChange rightChange desired (evaluate-cong eE (Cone.match value)) (reflect-β-One eE (funUniversal K E) (F ∘ left) (G ∘ right) rawMatch)
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.Section07.FunctorCones where
module FunctorCones {Γ : Context} (K : CAT Γ) {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) where
module CurriedCone {T : CAT Γ} (s : Cone f g (T × K)) wherecompatible
Derivation, checked
compatible : SquareCell₌ (F ◁ left) (G ◁ right) (const (Cone.match s)) (const (Cone.match t))
Proof / implementation
compatible = Fact.factor matching-factor
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.FunctorCones where
module FunctorCones {Γ : Context} (K : CAT Γ) {C D E : CAT Γ} (f : MAP C E) (g : MAP D E) where
module ReflectedCone {X T : CAT Γ} (s t : Cone F G T)
(Φ : ConeIdentification X (uncurryCone s) (uncurryCone t)) whereuncurryCone-restrict
Derivation, checked
uncurryCone-restrict : (r : MAP R T) (s : Cone (funPost {C = K} f) (funPost {C = K} g) T) → ConeIdentification₁ (FunctorCones.uncurryCone K f g (cone-restrict r s)) (cone-restrict (productMap r (id K)) (FunctorCones.uncurryCone K f g s))
Proof / implementation
uncurryCone-restrict = FunctorConeRestriction.comparison K 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.Section07.FunctorConeRestriction where
module _ {Γ : Context} (K : CAT Γ) {C D E T R : CAT Γ} (f : MAP C E) (g : MAP D E) 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 tested square is a pullback
isPullback
Derivation, checked
isPullback : IsPullback (mappedCone s)
Proof / implementation
isPullback = pullback-recognize (mappedCone s) factor β reflect-cones
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.Section07.FunctorPullbacks where
module _ {Γ : Context} {C D E S : CAT Γ} {f : MAP C E} {g : MAP D E} (K : CAT Γ) where
module Preservation (s : Cone f g S) (universal : IsPullback s) 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.
Lemma 1.7.12. For categories \(C\), \(D\) and \(E\), there is a preferred equivalence \[ \Fun (C,\Fun (D,E)) \iso \Fun (C \times D, E)\, . \]
Agda The exponential law
forward
Definition, 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B 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 the preferred functor as the curried functor of the following composite: \[ \Fun (C,\Fun (D,E)) \times C \times D \xrightarrow {\ev \times \id _{D}} \Fun (D,E) \times D \xrightarrow {\ev } E. \] To construct an inverse, it will by currying suffice to construct a functor \(\Fun (C \times D,E) \times C \to \Fun (D,E)\), which we may take to be the curried functor of the following composite \[ \Fun (C \times D,E) \times C \times D \xrightarrow {\ev } E. \] By construction, these two functors are compatible with the chain of equivalences \begin {align*} \Map (T,\Fun (C,\Fun (D,E))) &\simeq \Map (T\times C,\Fun (D,E))\\ &\simeq \Map ((T\times C)\times D,E)\\ &\simeq \Map (T\times (C\times D),E)\\ &\simeq \Map (T,\Fun (C\times D,E))\, . \end {align*}
Agda The preferred exponential comparison
forwardEvaluation
Definition, checked
forwardEvaluation : MAP (Nested × (A × B)) D
Proof / implementation
forwardEvaluation = doubleEvaluation ∘ Associativity.backward Nested A 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B D : CAT Γ) whereforward
Definition, 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B 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 The twice-curried inverse construction
backwardEvaluation
Definition, checked
backwardEvaluation : MAP ((Flat × A) × B) D
Proof / implementation
backwardEvaluation = eFlat ∘ Associativity.forward Flat A 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B D : CAT Γ) wherebackwardFirstCurry
Definition, checked
backwardFirstCurry : MAP (Flat × A) (Fun B 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B D : CAT Γ) wherebackward
Definition, 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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B 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 Compatibility with the chain of mapping-anima equivalences
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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B D : CAT Γ) whereAbout this correspondence
The corresponding result is proved in rebuild2, but its current proof is not identified here with the particular mapping-anima chain in this paragraph. Open the full declaration to inspect the actual argument.
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 Detecting the exponential equivalence
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.Section07.ExponentialLaw where
module ExponentialLaw {Γ : Context} (A B D : CAT Γ) whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
Checked source correspondences for Chapter 1 Sections 1.1–1.8, Chapter 2 Sections 2.1–2.6, and selected declarations throughout Chapter 3. Contextual inheritance is outside the formalization scope. Passage notes identify partial coverage, proof-route and representation differences.
Lemma 1.7.13. For a category \(C\), the functor \(\ev _{*}\colon \Fun (*,C) \to C\) is an equivalence.
Agda Functors out of the terminal category
funOneEvaluation-isEquiv
Derivation, checked
funOneEvaluation-isEquiv : (D : CAT Γ) → IsEquiv (funOneEvaluation D)
Proof / implementation
funOneEvaluation-isEquiv D = record { inverse = funOneInverse D ; left-inverse-law = (funOneInverse-evaluation D) ⁻¹ ; right-inverse-law = (funOneEvaluation-inverse 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.Section07.FunctorProperties 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 leave it to the reader to verify that an inverse is given by currying the equivalence \(C \times * \iso C\). □
Agda The inverse to evaluation at the terminal point
funOneInverse
Derivation, checked
funOneInverse : (D : CAT Γ) → MAP D (Fun One 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.Section07.FunctorProperties where
module _ {Γ : Context} wherefunOneEvaluation-inverse
Derivation, checked
funOneEvaluation-inverse : (D : CAT Γ) → (funOneEvaluation D ∘ funOneInverse D) =₁ id D
Proof / implementation
funOneEvaluation-inverse D = pair-β₁ (id D) (terminate D) ∙ ((funOneInverse-β D ▷ product-unitʳ-inverse D) ∙ evaluate-terminal (funEval {C = One} {D = D}) (funOneInverse 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.Section07.FunctorProperties where
module _ {Γ : Context} wherefunOneInverse-evaluation
Derivation, checked
funOneInverse-evaluation : (D : CAT Γ) → (funOneInverse D ∘ funOneEvaluation D) =₁ id (Fun One D)
Proof / implementation
funOneInverse-evaluation D = reflect e (funUniversal One D) _ _ ((evaluate-id e) ⁻¹ ∙ (comp-unitʳ e ∙ ((e ◁ product-unitʳ-inverse-pr₁ F) ∙ (comp-assoc pr₁ (product-unitʳ-inverse F) e ∙ (pair-β₁ (funOneEvaluation D ∘ pr₁) (id One ∘ pr₂) ∙ ((funOneInverse-β D ▷ productMap (funOneEvaluation D) (id One)) ∙ evaluate-restrict e (funOneInverse D) (funOneEvaluation D))))))) where F : CAT Γ F = Fun One D e : MAP (F × One) D e = funEval {C = One} {D = 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.Section07.FunctorProperties 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.
Lemma 1.7.14. For a category \(C\), the functor category \(\Fun (\emptyset ,C)\) is contractible, i.e. \(\Fun (\emptyset ,C) \iso *\).
Agda Functors out of the initial category
funInitial-isEquiv
Derivation, checked
funInitial-isEquiv : (D : CAT Γ) → IsEquiv (terminate (Fun Zero D))
Proof / implementation
funInitial-isEquiv D = record { inverse = funInitialPoint D ; left-inverse-law = (funInitial-contraction D) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.InitialDomain 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. For every category \(T\), there are equivalences \[ \Map (T,\Fun (\emptyset ,C)) \simeq \Map (T\times \emptyset ,C) \simeq \Map (\emptyset ,C) \simeq *, \] using Lemma 1.5.1 and the initial-category axiom. Hence \(\Fun (\emptyset ,C)\to *\) induces an equivalence on mapping animae for every \(T\), and Proposition 1.4.11 applies. □
Agda The initial-source comparison on mapping animae
funInitial-isEquiv
Derivation, checked
funInitial-isEquiv : (D : CAT Γ) → IsEquiv (terminate (Fun Zero D))
Proof / implementation
funInitial-isEquiv D = record { inverse = funInitialPoint D ; left-inverse-law = (funInitial-contraction D) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.InitialDomain where
module _ {Γ : Context} whereAbout this correspondence
The corresponding result is proved in rebuild2, but its current proof is not identified here with the particular mapping-anima chain in this paragraph. Open the full declaration to inspect the actual argument.
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 Detecting initial-source contractibility
funInitial-isEquiv
Derivation, checked
funInitial-isEquiv : (D : CAT Γ) → IsEquiv (terminate (Fun Zero D))
Proof / implementation
funInitial-isEquiv D = record { inverse = funInitialPoint D ; left-inverse-law = (funInitial-contraction D) ⁻¹ ; right-inverse-law = terminal-identification _ _ }
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.Section07.InitialDomain 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.
Lemma 1.7.15. For categories \(C\), \(D\) and \(E\), restriction along the inclusions \(i_C\colon C \hookrightarrow C \sqcup D\) and \(i_D\colon D \hookrightarrow C \sqcup D\) induces an equivalence \[ (i_C^*,i_D^*)\colon \Fun (C\sqcup D, E) \iso \Fun (C,E) \times \Fun (D,E). \]
Agda Functors out of a coproduct
forward
Definition, 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.Section07.CoproductDomain where
module CoproductDomain {Γ : Context} (C D E : 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.Section07.CoproductDomain where
module CoproductDomain {Γ : Context} (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.
Proof
Proof. For every category \(T\), there are equivalences \[ \begin {aligned} \Map (T,\Fun (C\sqcup D,E)) &\simeq \Map (T\times (C\sqcup D),E)\\ &\simeq \Map ((T\times C)\sqcup (T\times D),E)\\ &\simeq \Map (T\times C,E)\times \Map (T\times D,E)\\ &\simeq \Map (T,\Fun (C,E))\times \Map (T,\Fun (D,E))\\ &\simeq \Map (T,\Fun (C,E)\times \Fun (D,E)), \end {aligned} \] using distributivity, the coproduct axiom, and Proposition 1.4.5. This composite is induced by \((i_C^*,i_D^*)\): after uncurrying, its components are restriction along \(T\times i_C\) and \(T\times i_D\), which correspond under Corollary 1.6.17 to the two coproduct inclusions. The result follows from Proposition 1.4.11. □
Agda The coproduct comparison on mapping animae
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.Section07.CoproductDomain where
module CoproductDomain {Γ : Context} (C D E : CAT Γ) whereAbout this correspondence
The corresponding result is proved in rebuild2, but its current proof is not identified here with the particular mapping-anima chain in this paragraph. Open the full declaration to inspect the actual argument.
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 Identifying restriction along the two inclusions
forward
Definition, 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.Section07.CoproductDomain where
module CoproductDomain {Γ : Context} (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 Detecting the coproduct-source equivalence
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.Section07.CoproductDomain where
module CoproductDomain {Γ : Context} (C D E : CAT Γ) whereAbout this correspondence
These are the corresponding current results or underlying constructions. Some helpers used by the previous proof were consolidated or replaced; no line-by-line agreement of the two implementations is asserted.
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.7.2 Mapping animae and functor categories
We now compare the mapping anima with the functor category. Currying mapping-anima evaluation defines a canonical functor \[ \imath _{C,D}:=(\ev _{\Map })_c\colon \Map (C,D)\longrightarrow \Fun (C,D). \] The following result identifies \(\Map (C,D)\) with the collection of objects of \(\Fun (C,D)\).
Agda The canonical mapping-anima inclusion
mappingInclusion
Definition, checked
mappingInclusion : (C D : CAT Γ) → MAP (Map C D) (Fun 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.Section07.CoreOfFun 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.
Proposition 1.7.16. For any categories \(C\) and \(D\), there is a preferred equivalence \[ \Map (C,D)\iso \Fun (C,D)^\simeq . \] Under this equivalence, the canonical functor \(\imath _{\Fun (C,D)}\colon \Fun (C,D)^\simeq \to \Fun (C,D)\) is identified with \(\imath _{C,D}\).
Agda The core of a functor category
coreFunComparison
Derivation, checked
coreFunComparison : MAP (Map C D) (Core (Fun C D))
Proof / implementation
coreFunComparison = IsEquiv.inverse coreFunUncurrying-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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (C D : CAT Γ) wherecoreFunComparison-isEquiv
Derivation, checked
coreFunComparison-isEquiv : IsEquiv coreFunComparison
Proof / implementation
coreFunComparison-isEquiv = equiv-inverse coreFunUncurrying-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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (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. The universal property of functor categories gives equivalences \[ \Fun (C,D)^\simeq =\Map (*,\Fun (C,D)) \simeq \Map (*\times C,D) \simeq \Map (C,D). \] The inverse of their composite is the desired equivalence. To check compatibility with the canonical functors, it suffices to uncurry. Both resulting functors \(\Map (C,D)\times C\to D\) are identified with mapping-anima evaluation. □
Agda The equivalence from the core to the mapping anima
coreFunUncurrying-isEquiv
Derivation, checked
coreFunUncurrying-isEquiv : IsEquiv coreFunUncurrying
Proof / implementation
coreFunUncurrying-isEquiv = equiv-compose (evaluation-forward (funEval {C = C} {D = D}) One) (Maps.mapPre (product-unitˡ-inverse C)) (funUniversal C D One) (Maps.mapPre-isEquiv (product-unitˡ-inverse C) (product-unitˡ-inverse-isEquiv C))
Enclosing interface and module parameters
The enclosing headers show supplied parameters. Open the full module for imports and surrounding definitions.
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (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 The inverse is the preferred core comparison
coreFunComparison
Derivation, checked
coreFunComparison : MAP (Map C D) (Core (Fun C D))
Proof / implementation
coreFunComparison = IsEquiv.inverse coreFunUncurrying-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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (C D : CAT Γ) wherecoreFunComparison-isEquiv
Derivation, checked
coreFunComparison-isEquiv : IsEquiv coreFunComparison
Proof / implementation
coreFunComparison-isEquiv = equiv-inverse coreFunUncurrying-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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (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 Compatibility with the canonical inclusions
coreFunComparison-inclusion
Derivation, checked
coreFunComparison-inclusion : (coreInclusion (Fun C D) ∘ coreFunComparison) =₁ mappingInclusion C D
Proof / implementation
coreFunComparison-inclusion = comp-unitʳ (mappingInclusion C D) ∙ ((mappingInclusion C D ◁ (IsEquiv.right-inverse-law coreFunUncurrying-isEquiv) ⁻¹) ∙ (comp-assoc coreFunComparison coreFunUncurrying (mappingInclusion C D) ∙ (mappingInclusion-coreUncurrying ⁻¹ ▷ coreFunComparison)))
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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (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 Both uncurried functors are mapping-anima evaluation
coreFunUncurrying-evaluation
Derivation, checked
coreFunUncurrying-evaluation : uncurry coreFunUncurrying =₁ funUncurry {C = C} {D = D} (coreInclusion (Fun C D))
Proof / implementation
coreFunUncurrying-evaluation = (evaluate-restrict (funEval {C = C} {D = D}) mapEval (product-unitʳ-inverse A)) ⁻¹ ∙ ((evaluate (funEval {C = C} {D = D}) mapEval ◁ terminal-regroup) ∙ (comp-assoc (productMap (id A) (product-unitˡ-inverse C)) (Associativity.backward A One C) (evaluate (funEval {C = C} {D = D}) mapEval) ∙ ((mapCurry-β (map-isAn One (Fun C D)) (evaluation-universal (funEval {C = C} {D = D}) One) ▷ productMap (id A) (product-unitˡ-inverse C)) ∙ Maps.mapPre-uncurry (product-unitˡ-inverse C) (evaluation-forward (funEval {C = C} {D = D}) One))))
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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (C D : CAT Γ) wheremappingInclusion-coreUncurrying
Derivation, checked
mappingInclusion-coreUncurrying : (mappingInclusion C D ∘ coreFunUncurrying) =₁ coreInclusion (Fun C D)
Proof / implementation
mappingInclusion-coreUncurrying = reflect (funEval {C = C} {D = D}) (funUniversal C D) _ _ (coreFunUncurrying-evaluation ∙ ((mappingInclusion-β C D ▷ productMap coreFunUncurrying (id C)) ∙ evaluate-restrict (funEval {C = C} {D = D}) (mappingInclusion C D) coreFunUncurrying))
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.Section07.CoreOfFun where
module _ {Γ : Context} where
module _ (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.
Proposition 1.7.17. For any anima \(X\), postcomposition with \(\imath _{C,D}\) induces an equivalence \[ (\imath _{C,D})_*\colon \Map (X,\Map (C,D))\iso \Map (X,\Fun (C,D)). \]
Agda The comparison on anima parameters
mappingInclusion-on-maps
Derivation, checked
mappingInclusion-on-maps : (T C D : CAT Γ) → isAn T → IsEquiv (Maps.mapPost {C = T} (mappingInclusion C D))
Proof / implementation
mappingInclusion-on-maps T C D tAn = equiv-transport (Maps.mapPost⁼ (coreFunComparison-inclusion C D) ∙ Maps.mapPost-comp (coreFunComparison C D) (coreInclusion (Fun C D))) (equiv-compose (Maps.mapPost {C = T} (coreFunComparison C D)) (Maps.mapPost {C = T} (coreInclusion (Fun C D))) (Maps.mapPost-isEquiv (coreFunComparison C D) (coreFunComparison-isEquiv C D)) (core-universal T (Fun C D) tAn))
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.Section07.FunctorProperties 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. By the preceding proposition, this is the universal property of the groupoid core of \(\Fun (C,D)\) from Corollary 1.4.13. □
Agda Apply the universal property of the core
mappingInclusion-on-maps
Derivation, checked
mappingInclusion-on-maps : (T C D : CAT Γ) → isAn T → IsEquiv (Maps.mapPost {C = T} (mappingInclusion C D))
Proof / implementation
mappingInclusion-on-maps T C D tAn = equiv-transport (Maps.mapPost⁼ (coreFunComparison-inclusion C D) ∙ Maps.mapPost-comp (coreFunComparison C D) (coreInclusion (Fun C D))) (equiv-compose (Maps.mapPost {C = T} (coreFunComparison C D)) (Maps.mapPost {C = T} (coreInclusion (Fun C D))) (Maps.mapPost-isEquiv (coreFunComparison C D) (coreFunComparison-isEquiv C D)) (core-universal T (Fun C D) tAn))
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.Section07.FunctorProperties 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.
Supplementary notes
- Uncurrying and pullback squares AI-generated