From 44363cc916acdc8e1d3afbc2276d27ff57864484 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 9 Jan 2024 13:46:53 +0100 Subject: [PATCH 1/8] First shot of other adjoint functor --- src/Categories/Functor/Slice.agda | 63 ++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/src/Categories/Functor/Slice.agda b/src/Categories/Functor/Slice.agda index 6121dd816..9661b754a 100644 --- a/src/Categories/Functor/Slice.agda +++ b/src/Categories/Functor/Slice.agda @@ -4,16 +4,22 @@ open import Categories.Category using (Category) module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where -open import Function using () renaming (id to id→) +open import Function.Base using (_$_) renaming (id to id→) +open import Categories.Category.BinaryProducts +open import Categories.Category.Cartesian +open import Categories.Category.CartesianClosed C open import Categories.Diagram.Pullback C using (Pullback; unglue; Pullback-resp-≈) open import Categories.Functor using (Functor) open import Categories.Functor.Properties using ([_]-resp-∘) open import Categories.Morphism.Reasoning C +open import Categories.Object.Exponential C open import Categories.Object.Product C +open import Categories.Object.Terminal C import Categories.Category.Slice as S import Categories.Category.Construction.Pullbacks as Pbs +import Categories.Object.Product.Construction as ×C open Category C open HomReasoning @@ -96,3 +102,58 @@ module _ {A : Obj} where ; F-resp-≈ = λ f≈g → ⟨⟩-cong₂ refl (∘-resp-≈ˡ f≈g) } + -- This can and probably should be restricted + -- e.g. we only need exponential objects with A as domain + -- I don't think we need all products but I don't have a clear idea of what products we do need + module _ (ccc : CartesianClosed) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where + + open CartesianClosed ccc + open Cartesian cartesian + open Terminal terminal + open BinaryProducts products + + -- Needs better name! + Coforgetful : Functor (Slice A) C + Coforgetful = record + { F₀ = p.P + ; F₁ = λ f → p.universal _ (F₁-lemma f) + ; identity = λ {X} → sym $ p.unique X (sym (!-unique _)) $ begin + p.p₂ X ∘ id ≈⟨ identityʳ ⟩ + p.p₂ X ≈˘⟨ η-exp′ ⟩ + λg (eval′ ∘ first (p.p₂ X)) ≈˘⟨ λ-cong (pullˡ identityˡ) ⟩ + λg (id ∘ eval′ ∘ first (p.p₂ X)) ∎ + ; homomorphism = λ {S} {T} {U} {f} {g} → sym $ p.unique U (sym (!-unique _)) $ begin + p.p₂ U ∘ p.universal U (F₁-lemma g) ∘ p.universal T (F₁-lemma f) ≈⟨ pullˡ (p.p₂∘universal≈h₂ U) ⟩ + λg (h g ∘ eval′ ∘ first (p.p₂ T)) ∘ p.universal T (F₁-lemma f) ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩ + λg (h g ∘ eval′) ∘ p.p₂ T ∘ p.universal T (F₁-lemma f) ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ T ⟩ + λg (h g ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S)) ≈⟨ subst ⟩ + λg ((h g ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S)))) ≈⟨ λ-cong (pullʳ β′) ⟩ + λg (h g ∘ (h f ∘ eval′ ∘ first (p.p₂ S))) ≈⟨ λ-cong sym-assoc ⟩ + λg ((h g ∘ h f) ∘ eval′ ∘ first (p.p₂ S)) ∎ + ; F-resp-≈ = λ f≈g → p.universal-resp-≈ _ refl (λ-cong (∘-resp-≈ˡ f≈g)) + } + where + p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′)) + p X = pullback (λg π₂) (λg (arr X ∘ eval′)) + module p X = Pullback (p X) + + abstract + F₁-lemma : ∀ {S} {T} (f : Slice⇒ S T) → λg π₂ ∘ ! ≈ λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S)) + F₁-lemma {S} {T} f = λ-unique₂′ $ begin + eval′ ∘ first (λg π₂ ∘ !) ≈˘⟨ refl⟩∘⟨ first∘first ⟩ + eval′ ∘ first (λg π₂) ∘ first ! ≈⟨ pullˡ β′ ⟩ + π₂ ∘ first ! ≈⟨ π₂∘⁂ ○ identityˡ ⟩ + π₂ ≈⟨ λ-inj lemma ⟩ + arr S ∘ eval′ ∘ first (p.p₂ S) ≈˘⟨ pullˡ (△ f) ⟩ + arr T ∘ h f ∘ eval′ ∘ first (p.p₂ S) ≈˘⟨ pullʳ β′ ⟩ + (arr T ∘ eval′) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ≈˘⟨ pullˡ β′ ⟩ + eval′ ∘ first (λg (arr T ∘ eval′)) ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ≈⟨ refl⟩∘⟨ first∘first ⟩ + eval′ ∘ first (λg (arr T ∘ eval′) ∘ λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∎ + where + lemma : λg π₂ ≈ λg (arr S ∘ eval′ ∘ first (p.p₂ S)) + lemma = begin + λg π₂ ≈˘⟨ λ-cong (π₂∘⁂ ○ identityˡ) ⟩ + λg (π₂ ∘ first (p.p₁ S)) ≈˘⟨ subst ⟩ + λg π₂ ∘ p.p₁ S ≈⟨ p.commute S ⟩ + λg (arr S ∘ eval′) ∘ p.p₂ S ≈⟨ subst ○ λ-cong assoc ⟩ + λg (arr S ∘ eval′ ∘ first (p.p₂ S)) ∎ From 56f4a35dcb2c86eeea3e5a1dce9f0c0ea6703f35 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 10 Jan 2024 13:52:16 +0100 Subject: [PATCH 2/8] Define adjoint --- src/Categories/Adjoint/Instance/Slice.agda | 103 ++++++++++++++++++++- 1 file changed, 101 insertions(+), 2 deletions(-) diff --git a/src/Categories/Adjoint/Instance/Slice.agda b/src/Categories/Adjoint/Instance/Slice.agda index 1f425c510..d88e2f115 100644 --- a/src/Categories/Adjoint/Instance/Slice.agda +++ b/src/Categories/Adjoint/Instance/Slice.agda @@ -5,10 +5,18 @@ open import Categories.Category using (Category) module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where open import Categories.Adjoint using (_⊣_) -open import Categories.Category.Slice C using (SliceObj; Slice⇒; slicearr) -open import Categories.Functor.Slice C using (Forgetful; Free) +open import Categories.Category.BinaryProducts C +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.CartesianClosed using (CartesianClosed) +open import Categories.Category.Slice C using (SliceObj; sliceobj; Slice⇒; slicearr) +open import Categories.Functor.Slice C using (Forgetful; Free; Coforgetful) +open import Categories.Morphism.Reasoning C open import Categories.NaturalTransformation using (ntHelper) +open import Categories.Diagram.Pullback C hiding (swap) open import Categories.Object.Product C +open import Categories.Object.Terminal C + +open import Function.Base using (_$_) open Category C open HomReasoning @@ -44,3 +52,94 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where ⟨ π₁ , π₂ ⟩ ≈⟨ η ⟩ id ∎ } + +module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where + + open CartesianClosed ccc + open Cartesian cartesian + open Terminal terminal + open BinaryProducts products + + Free⊣Coforgetful : Free {A = A} product ⊣ Coforgetful ccc pullback + Free⊣Coforgetful = record + { unit = ntHelper record + { η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X)) + ; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin + p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ f ≈⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩ + λg swap ∘ f ≈⟨ subst ⟩ + λg (swap ∘ first f) ≈⟨ λ-cong swap∘⁂ ⟩ + λg (second f ∘ swap) ≈˘⟨ λ-cong (∘-resp-≈ʳ β′) ⟩ + λg (second f ∘ eval′ ∘ first (λg swap)) ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl))) ⟩ + λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _)) ≈˘⟨ λ-cong (pull-last first∘first) ⟩ + λg ((second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ first (p.universal (sliceobj π₁) _)) ≈˘⟨ subst ⟩ + λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩ + p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ∘ p.universal (sliceobj π₁) _ ∎ + } + ; counit = ntHelper record + { η = λ X → slicearr (counit-△ X) + ; commute = λ {S} {T} f → begin + (eval′ ∘ first (p.p₂ T) ∘ swap) ∘ second (p.universal T _) ≈⟨ pull-last swap∘⁂ ⟩ + eval′ ∘ first (p.p₂ T) ∘ first (p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩ + eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ T) Equiv.refl ⟩∘⟨refl ⟩ + eval′ ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∘ swap ≈⟨ pullˡ β′ ⟩ + (h f ∘ eval′ ∘ first (p.p₂ S)) ∘ swap ≈⟨ assoc²' ⟩ + h f ∘ eval′ ∘ first (p.p₂ S) ∘ swap ∎ + } + ; zig = λ {X} → begin + (eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap) ∘ second (p.universal (sliceobj π₁) _) ≈⟨ assoc²' ⟩ + eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap ∘ second (p.universal (sliceobj π₁) _) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘⁂ ⟩ + eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ first (p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩ + eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl ⟩∘⟨refl ⟩ + eval′ ∘ first (λg swap) ∘ swap ≈⟨ pullˡ β′ ⟩ + swap ∘ swap ≈⟨ swap∘swap ⟩ + id ∎ + ; zag = λ {X} → p.unique-diagram X !-unique₂ $ begin + p.p₂ X ∘ p.universal X _ ∘ p.universal (sliceobj π₁) _ ≈⟨ pullˡ (p.p₂∘universal≈h₂ X) ⟩ + λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (subst ○ λ-cong assoc) ⟩ + λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩ + λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap ≈⟨ subst ⟩ + λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap)) ≈⟨ λ-cong (pullʳ β′) ⟩ + λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pull-last swap∘swap) ⟩ + λg (eval′ ∘ first (p.p₂ X) ∘ id) ≈⟨ λ-cong (∘-resp-≈ʳ identityʳ) ⟩ + λg (eval′ ∘ first (p.p₂ X)) ≈⟨ η-exp′ ⟩ + p.p₂ X ≈˘⟨ identityʳ ⟩ + p.p₂ X ∘ id ∎ + } + where + p : (X : SliceObj A) → Pullback {X = ⊤} {Z = A ^ A} {Y = Y X ^ A} (λg π₂) (λg (arr X ∘ eval′)) + p X = pullback (λg π₂) (λg (arr X ∘ eval′)) + module p X = Pullback (p X) + + abstract + unit-pb : ∀ (X : Obj) → eval′ ∘ first {A = X} {C = A} (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap) + unit-pb X = begin + eval′ ∘ first (λg π₂ ∘ !) ≈˘⟨ refl⟩∘⟨ first∘first ⟩ + eval′ ∘ first (λg π₂) ∘ first ! ≈⟨ pullˡ β′ ⟩ + π₂ ∘ first ! ≈⟨ π₂∘⁂ ○ identityˡ ⟩ + π₂ ≈˘⟨ project₁ ⟩ + π₁ ∘ swap ≈˘⟨ refl⟩∘⟨ β′ ⟩ + π₁ ∘ eval′ ∘ first (λg swap) ≈˘⟨ extendʳ β′ ⟩ + eval′ ∘ first (λg (π₁ ∘ eval′)) ∘ first (λg swap) ≈⟨ refl⟩∘⟨ first∘first ⟩ + eval′ ∘ first (λg (π₁ ∘ eval′) ∘ λg swap) ∎ + -- A good chunk of the above, maybe all if you squint, is duplicated with F₁-lemma + -- eval′ ∘ first (λg π₂ ∘ !) ≈ eval′ ∘ first (λg (f ∘ eval′) ∘ first (λg g) + -- With f : X ⇒ Y and g : Z × Y ⇒ X. Not sure what conditions f and g need to have + + -- Would it be better if Free used π₂ rather than π₁? + -- It would mean we could avoid this swap + counit-△ : ∀ X → arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈ π₁ + counit-△ X = begin + arr X ∘ eval′ ∘ first (p.p₂ X) ∘ swap ≈˘⟨ assoc² ⟩ + ((arr X ∘ eval′) ∘ first (p.p₂ X)) ∘ swap ≈⟨ lemma ⟩∘⟨refl ⟩ + (π₂ ∘ first (p.p₁ X)) ∘ swap ≈⟨ (π₂∘⁂ ○ identityˡ) ⟩∘⟨refl ⟩ + π₂ ∘ swap ≈⟨ project₂ ⟩ + π₁ ∎ + where + lemma : (arr X ∘ eval′) ∘ first (p.p₂ X) ≈ π₂ ∘ first (p.p₁ X) + lemma = λ-inj $ begin + λg ((arr X ∘ eval′) ∘ first (p.p₂ X)) ≈˘⟨ subst ⟩ + λg (arr X ∘ eval′) ∘ p.p₂ X ≈˘⟨ p.commute X ⟩ + λg π₂ ∘ p.p₁ X ≈⟨ subst ⟩ + λg (π₂ ∘ first (p.p₁ X)) ∎ + + From 5559e746e54380cbac7ad5b18e880ee1029eecba Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 09:19:49 +0100 Subject: [PATCH 3/8] Use cancel-r --- src/Categories/Adjoint/Instance/Slice.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Categories/Adjoint/Instance/Slice.agda b/src/Categories/Adjoint/Instance/Slice.agda index d88e2f115..3a46fb80a 100644 --- a/src/Categories/Adjoint/Instance/Slice.agda +++ b/src/Categories/Adjoint/Instance/Slice.agda @@ -99,8 +99,7 @@ module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _ ≈⟨ refl⟩∘⟨ p.p₂∘universal≈h₂ (sliceobj π₁) ⟩ λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ λg swap ≈⟨ subst ⟩ λg (((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ eval′) ∘ first (λg swap)) ≈⟨ λ-cong (pullʳ β′) ⟩ - λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pull-last swap∘swap) ⟩ - λg (eval′ ∘ first (p.p₂ X) ∘ id) ≈⟨ λ-cong (∘-resp-≈ʳ identityʳ) ⟩ + λg ((eval′ ∘ first (p.p₂ X) ∘ swap) ∘ swap) ≈⟨ λ-cong (pullʳ (cancelʳ swap∘swap)) ⟩ λg (eval′ ∘ first (p.p₂ X)) ≈⟨ η-exp′ ⟩ p.p₂ X ≈˘⟨ identityʳ ⟩ p.p₂ X ∘ id ∎ From 0322606b760c890e91e1a8912b8b720442aa70fa Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 24 Jan 2024 09:20:04 +0100 Subject: [PATCH 4/8] Define first-cong and second-cong, use throughout --- src/Categories/Adjoint/Instance/Slice.agda | 6 +++--- src/Categories/Category/BinaryProducts.agda | 6 ++++++ src/Categories/Category/CartesianClosed.agda | 4 ++-- .../Properties/Presheaves/FromCartesianCCC.agda | 6 +++--- .../Object/NaturalNumbers/Properties/Parametrized.agda | 4 ++-- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/Categories/Adjoint/Instance/Slice.agda b/src/Categories/Adjoint/Instance/Slice.agda index 3a46fb80a..f1e6a13fa 100644 --- a/src/Categories/Adjoint/Instance/Slice.agda +++ b/src/Categories/Adjoint/Instance/Slice.agda @@ -69,7 +69,7 @@ module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X λg swap ∘ f ≈⟨ subst ⟩ λg (swap ∘ first f) ≈⟨ λ-cong swap∘⁂ ⟩ λg (second f ∘ swap) ≈˘⟨ λ-cong (∘-resp-≈ʳ β′) ⟩ - λg (second f ∘ eval′ ∘ first (λg swap)) ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl))) ⟩ + λg (second f ∘ eval′ ∘ first (λg swap)) ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (first-cong (p.p₂∘universal≈h₂ (sliceobj π₁))))) ⟩ λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _)) ≈˘⟨ λ-cong (pull-last first∘first) ⟩ λg ((second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ first (p.universal (sliceobj π₁) _)) ≈˘⟨ subst ⟩ λg (second f ∘ eval′ ∘ first (p.p₂ (sliceobj π₁))) ∘ p.universal (sliceobj π₁) _ ≈˘⟨ pullˡ (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩ @@ -80,7 +80,7 @@ module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X ; commute = λ {S} {T} f → begin (eval′ ∘ first (p.p₂ T) ∘ swap) ∘ second (p.universal T _) ≈⟨ pull-last swap∘⁂ ⟩ eval′ ∘ first (p.p₂ T) ∘ first (p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩ - eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ T) Equiv.refl ⟩∘⟨refl ⟩ + eval′ ∘ first (p.p₂ T ∘ p.universal T _) ∘ swap ≈⟨ refl⟩∘⟨ first-cong (p.p₂∘universal≈h₂ T) ⟩∘⟨refl ⟩ eval′ ∘ first (λg (h f ∘ eval′ ∘ first (p.p₂ S))) ∘ swap ≈⟨ pullˡ β′ ⟩ (h f ∘ eval′ ∘ first (p.p₂ S)) ∘ swap ≈⟨ assoc²' ⟩ h f ∘ eval′ ∘ first (p.p₂ S) ∘ swap ∎ @@ -89,7 +89,7 @@ module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X (eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap) ∘ second (p.universal (sliceobj π₁) _) ≈⟨ assoc²' ⟩ eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ swap ∘ second (p.universal (sliceobj π₁) _) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ swap∘⁂ ⟩ eval′ ∘ first (p.p₂ (sliceobj π₁)) ∘ first (p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ pullˡ first∘first ⟩ - eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ ⁂-cong₂ (p.p₂∘universal≈h₂ (sliceobj π₁)) Equiv.refl ⟩∘⟨refl ⟩ + eval′ ∘ first (p.p₂ (sliceobj π₁) ∘ p.universal (sliceobj π₁) _) ∘ swap ≈⟨ refl⟩∘⟨ first-cong (p.p₂∘universal≈h₂ (sliceobj π₁)) ⟩∘⟨refl ⟩ eval′ ∘ first (λg swap) ∘ swap ≈⟨ pullˡ β′ ⟩ swap ∘ swap ≈⟨ swap∘swap ⟩ id ∎ diff --git a/src/Categories/Category/BinaryProducts.agda b/src/Categories/Category/BinaryProducts.agda index 1b0cc33b3..3f5907a74 100644 --- a/src/Categories/Category/BinaryProducts.agda +++ b/src/Categories/Category/BinaryProducts.agda @@ -94,6 +94,12 @@ record BinaryProducts : Set (levelOfTerm 𝒞) where ⁂-cong₂ : f ≈ g → h ≈ i → f ⁂ h ≈ g ⁂ i ⁂-cong₂ = [ product ⇒ product ]×-cong₂ + first-cong : f ≈ g → f ⁂ h ≈ g ⁂ h + first-cong f≈g = ⁂-cong₂ f≈g Equiv.refl + + second-cong : g ≈ h → f ⁂ g ≈ f ⁂ h + second-cong g≈h = ⁂-cong₂ Equiv.refl g≈h + ⁂∘⟨⟩ : (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g ∘ g′ ⟩ ⁂∘⟨⟩ = [ product ⇒ product ]×∘⟨⟩ diff --git a/src/Categories/Category/CartesianClosed.agda b/src/Categories/Category/CartesianClosed.agda index 8f35da80f..6eae77356 100644 --- a/src/Categories/Category/CartesianClosed.agda +++ b/src/Categories/Category/CartesianClosed.agda @@ -56,7 +56,7 @@ record CartesianClosed : Set (levelOfTerm 𝒞) where open CartesianMonoidal cartesian using (A×⊤≅A) open BinaryProducts cartesian.products using (_×_; product; π₁; π₂; ⟨_,_⟩; project₁; project₂; η; ⟨⟩-cong₂; ⟨⟩∘; _⁂_; ⟨⟩-congˡ; ⟨⟩-congʳ; - first∘first; firstid; first; second; first↔second; second∘second; ⁂-cong₂; -×_) + first∘first; firstid; first; second; first↔second; second∘second; second-cong; -×_) open Terminal cartesian.terminal using (⊤; !; !-unique₂; ⊤-id) B^A×A : ∀ B A → Product (B ^ A) A @@ -194,7 +194,7 @@ record CartesianClosed : Set (levelOfTerm 𝒞) where ; identity = λ-cong (identityˡ ○ (elimʳ (id×id product))) ○ η-id′ ; homomorphism = λ-unique₂′ helper ; F-resp-≈ = λ where - (eq₁ , eq₂) → λ-cong (∘-resp-≈ eq₂ (∘-resp-≈ʳ (⁂-cong₂ refl eq₁))) + (eq₁ , eq₂) → λ-cong (∘-resp-≈ eq₂ (∘-resp-≈ʳ (second-cong eq₁))) } where helper : eval′ ∘ first (λg ((g ∘ f) ∘ eval′ ∘ second (h ∘ i))) ≈ eval′ ∘ first (λg (g ∘ eval′ ∘ second i) ∘ λg (f ∘ eval′ ∘ second h)) diff --git a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda index fbc127f04..4492be0af 100644 --- a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda +++ b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda @@ -55,7 +55,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi in begin F.₁ (second (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ second∘second ⟩ F.₁ (second g) ⟨$⟩ (F.₁ (second f) ⟨$⟩ x) ∎ - ; F-resp-≈ = λ {Y Z} {f g} eq → F.F-resp-≈ (⁂-cong₂ C.Equiv.refl eq) + ; F-resp-≈ = λ {Y Z} {f g} eq → F.F-resp-≈ (second-cong eq) } where module F = Functor F @@ -79,7 +79,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi in begin F₁ (first (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ first∘first ⟩ F₁ (first g) ⟨$⟩ (F₁ (first f) ⟨$⟩ x) ∎ - ; F-resp-≈ = λ {A B} {f g} eq → F-resp-≈ (⁂-cong₂ eq C.Equiv.refl) + ; F-resp-≈ = λ {A B} {f g} eq → F-resp-≈ (first-cong eq) } where open Functor F @@ -113,7 +113,7 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi F.₁ C.id ⟨$⟩ (α.η Y ⟨$⟩ x) ≈⟨ F.identity ⟩ α.η Y ⟨$⟩ x ∎ ; homomorphism = λ {X Y Z} → Setoid.sym (F.₀ (Z × _)) ([ F ]-resp-∘ first∘first) - ; F-resp-≈ = λ eq → F.F-resp-≈ (⁂-cong₂ eq C.Equiv.refl) + ; F-resp-≈ = λ eq → F.F-resp-≈ (first-cong eq) } module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where diff --git a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda index 639ad1db3..13828d57c 100644 --- a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda +++ b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda @@ -59,7 +59,7 @@ NNO×CCC⇒PNNO nno = record commute₂' {A} {X} {f} {g} = begin g ∘ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ pullˡ (pullˡ (⟺ β′)) ⟩ ((eval′ ∘ (λg (g ∘ eval′) ⁂ id)) ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ (pullʳ ⁂∘⁂) ⟩∘⟨refl ⟩ - (eval′ ∘ (λg (g ∘ eval′) ∘ universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⁂-cong₂ s-commute refl)) ⟩∘⟨refl ⟩ + (eval′ ∘ (λg (g ∘ eval′) ∘ universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (first-cong s-commute)) ⟩∘⟨refl ⟩ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ∘ s ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⟺ ⁂∘⁂)) ⟩∘⟨refl ⟩ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ (s ⁂ id)) ∘ swap ≈⟨ pullʳ (pullʳ (⟺ swap∘⁂)) ⟩ eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ swap ∘ (id ⁂ s) ≈⟨ sym-assoc ○ sym-assoc ⟩ @@ -71,7 +71,7 @@ NNO×CCC⇒PNNO nno = record λg (u ∘ swap) ≈⟨ nno-unique (⟺ (λ-unique′ (begin - eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id) ≈⟨ refl⟩∘⟨ ⟺ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ + eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id) ≈⟨ refl⟩∘⟨ ⟺ (⁂∘⁂ ○ second-cong identity²) ⟩ eval′ ∘ (λg (u ∘ swap) ⁂ id) ∘ (z ⁂ id) ≈⟨ pullˡ β′ ⟩ (u ∘ swap) ∘ (z ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ u ∘ (id ⁂ z) ∘ swap ≈⟨ pushʳ (bp-unique′ From 11dddb7a93d9bc382ff29bdcb5e10cf0df71ffe6 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 27 Jan 2024 19:48:34 +0100 Subject: [PATCH 5/8] Make pullback-functorial less forgetful I also fiddled with pbarr a bit to make its equality argument abstract --- .../Category/Construction/Pullbacks.agda | 14 ++-- src/Categories/Functor/Slice.agda | 81 ++++++++++++------- 2 files changed, 63 insertions(+), 32 deletions(-) diff --git a/src/Categories/Category/Construction/Pullbacks.agda b/src/Categories/Category/Construction/Pullbacks.agda index 54138bdc6..212aee570 100644 --- a/src/Categories/Category/Construction/Pullbacks.agda +++ b/src/Categories/Category/Construction/Pullbacks.agda @@ -33,12 +33,16 @@ record Pullback⇒ W (X Y : PullbackObj W) : Set (o ⊔ ℓ ⊔ e) where commute₁ : Y.arr₁ ∘ mor₁ ≈ X.arr₁ commute₂ : Y.arr₂ ∘ mor₂ ≈ X.arr₂ + private abstract + pbarrlemma : Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈ Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ + pbarrlemma = begin + Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈⟨ pullˡ commute₁ ⟩ + X.arr₁ ∘ X.pullback.p₁ ≈⟨ X.pullback.commute ⟩ + X.arr₂ ∘ X.pullback.p₂ ≈˘⟨ pullˡ commute₂ ⟩ + Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ ∎ + pbarr : X.pullback.P ⇒ Y.pullback.P - pbarr = Y.pullback.universal $ begin - Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈⟨ pullˡ commute₁ ⟩ - X.arr₁ ∘ X.pullback.p₁ ≈⟨ X.pullback.commute ⟩ - X.arr₂ ∘ X.pullback.p₂ ≈˘⟨ pullˡ commute₂ ⟩ - Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ ∎ + pbarr = Y.pullback.universal pbarrlemma open Pullback⇒ diff --git a/src/Categories/Functor/Slice.agda b/src/Categories/Functor/Slice.agda index 9661b754a..99e7b6fa2 100644 --- a/src/Categories/Functor/Slice.agda +++ b/src/Categories/Functor/Slice.agda @@ -56,35 +56,62 @@ module _ {A : Obj} where module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i) open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁) - pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C + pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B) pullback-functorial f = record - { F₀ = λ X → p.P X - ; F₁ = λ f → p⇒ _ _ f - ; identity = λ {X} → sym (p.unique X id-comm id-comm) - ; homomorphism = λ {_ Y Z} → - p.unique-diagram Z (p.p₁∘universal≈h₁ Z ○ ⟺ identityˡ ○ ⟺ (pullʳ (p.p₁∘universal≈h₁ Y)) ○ ⟺ (pullˡ (p.p₁∘universal≈h₁ Z))) - (p.p₂∘universal≈h₂ Z ○ assoc ○ ⟺ (pullʳ (p.p₂∘universal≈h₂ Y)) ○ ⟺ (pullˡ (p.p₂∘universal≈h₂ Z))) - ; F-resp-≈ = λ {_ B} {h i} eq → - p.unique-diagram B (p.p₁∘universal≈h₁ B ○ ⟺ (p.p₁∘universal≈h₁ B)) - (p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B)) + { F₀ = λ X → S.sliceobj (p.p₁ X) + ; F₁ = λ f → S.slicearr {h = p⇒.pbarr _ _ f} (p.p₁∘universal≈h₁ _ ○ identityˡ) + ; identity = sym $ p.unique _ id-comm id-comm + ; homomorphism = p.unique-diagram _ homomorphism-lemmaˡ homomorphism-lemmaʳ + ; F-resp-≈ = λ {_ B} {h i} eq → p.unique-diagram B F-resp-≈-lemmaˡ (F-resp-≈-lemmaʳ eq) } - where p : ∀ X → Pullback f (arr X) - p X = pullback f (arr X) - module p X = Pullback (p X) - - p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y - p⇒ X Y g = Pbs.Pullback⇒.pbarr pX⇒pY - where pX : Pbs.PullbackObj C A - pX = record { pullback = p X } - pY : Pbs.PullbackObj C A - pY = record { pullback = p Y } - pX⇒pY : Pbs.Pullback⇒ C A pX pY - pX⇒pY = record - { mor₁ = Category.id C - ; mor₂ = h g - ; commute₁ = identityʳ - ; commute₂ = △ g - } + where + p : ∀ X → Pullback f (arr X) + p X = pullback f (arr X) + module p X = Pullback (p X) + + p⇒ : ∀ X Y (g : Slice⇒ X Y) → Pbs.Pullback⇒ C A _ _ + p⇒ X Y g = pX⇒pY + where + pX : Pbs.PullbackObj C A + pX = record { pullback = p X } + pY : Pbs.PullbackObj C A + pY = record { pullback = p Y } + pX⇒pY : Pbs.Pullback⇒ C A pX pY + pX⇒pY = record + { mor₁ = Category.id C + ; mor₂ = h g + ; commute₁ = identityʳ + ; commute₂ = △ g + } + + module p⇒ X Y g = Pbs.Pullback⇒ (p⇒ X Y g) + + homomorphism-lemmaˡ : ∀ {X Y Z α β} → p.p₁ Z ∘ p⇒.pbarr X Z _ ≈ p.p₁ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α + homomorphism-lemmaˡ {X} {Y} {Z} {α} {β} = begin + p.p₁ Z ∘ p⇒.pbarr X Z _ ≈⟨ p.p₁∘universal≈h₁ Z ⟩ + id ∘ p.p₁ X ≈˘⟨ identityˡ ⟩ + id ∘ id ∘ p.p₁ X ≈˘⟨ pullʳ (p.p₁∘universal≈h₁ Y) ⟩ + (id ∘ p.p₁ Y) ∘ p⇒.pbarr X Y α ≈˘⟨ pullˡ (p.p₁∘universal≈h₁ Z) ⟩ + p.p₁ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α ∎ + + homomorphism-lemmaʳ : ∀ {X Y Z α β} → p.p₂ Z ∘ p⇒.pbarr X Z _ ≈ p.p₂ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α + homomorphism-lemmaʳ {X} {Y} {Z} {α} {β} = begin + p.p₂ Z ∘ p⇒.pbarr X Z _ ≈⟨ p.p₂∘universal≈h₂ Z ⟩ + (h β ∘ h α) ∘ p.p₂ X ≈˘⟨ glue′ (p.p₂∘universal≈h₂ Z) (p.p₂∘universal≈h₂ Y) ⟩ + p.p₂ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α ∎ + + F-resp-≈-lemmaˡ : ∀ {A B} {α β : Slice⇒ A B} → p.p₁ B ∘ p⇒.pbarr A B α ≈ p.p₁ B ∘ p⇒.pbarr A B β + F-resp-≈-lemmaˡ {A} {B} {α} {β} = begin + p.p₁ B ∘ p⇒.pbarr A B α ≈⟨ p.p₁∘universal≈h₁ B ⟩ + id ∘ p.p₁ A ≈˘⟨ p.p₁∘universal≈h₁ B ⟩ + p.p₁ B ∘ p⇒.pbarr A B β ∎ + + F-resp-≈-lemmaʳ : ∀ {A B} {α β : Slice⇒ A B} → h α ≈ h β → p.p₂ B ∘ p⇒.pbarr A B α ≈ p.p₂ B ∘ p⇒.pbarr A B β + F-resp-≈-lemmaʳ {A} {B} {α} {β} eq = begin + p.p₂ B ∘ p⇒.pbarr A B α ≈⟨ p.p₂∘universal≈h₂ B ⟩ + h α ∘ p.p₂ A ≈⟨ eq ⟩∘⟨refl ⟩ + h β ∘ p.p₂ A ≈˘⟨ p.p₂∘universal≈h₂ B ⟩ + p.p₂ B ∘ p⇒.pbarr A B β ∎ module _ (product : {X : Obj} → Product A X) where From bf07868e8cf19da7b81637b0c8bcb1a00d138aba Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 27 Jan 2024 20:52:34 +0100 Subject: [PATCH 6/8] Rename slice functors --- src/Categories/Adjoint/Instance/BaseChange.agda | 4 ++-- src/Categories/Adjoint/Instance/Slice.agda | 10 +++++----- src/Categories/Functor/Slice.agda | 17 ++++++++--------- src/Categories/Functor/Slice/BaseChange.agda | 6 +++--- 4 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/Categories/Adjoint/Instance/BaseChange.agda b/src/Categories/Adjoint/Instance/BaseChange.agda index 937f1042c..1441646c7 100644 --- a/src/Categories/Adjoint/Instance/BaseChange.agda +++ b/src/Categories/Adjoint/Instance/BaseChange.agda @@ -6,7 +6,7 @@ module Categories.Adjoint.Instance.BaseChange {o ℓ e} (C : Category o ℓ e) w open import Categories.Adjoint using (_⊣_) open import Categories.Adjoint.Compose using (_∘⊣_) -open import Categories.Adjoint.Instance.Slice using (Forgetful⊣Free) +open import Categories.Adjoint.Instance.Slice using (TotalSpace⊣ConstantFamily) open import Categories.Category.Slice C using (Slice) open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice≃slice) open import Categories.Category.Equivalence.Properties using (module C≅D) @@ -18,4 +18,4 @@ open Category C module _ {A B : Obj} (f : B ⇒ A) (pullback : ∀ {C} {h : C ⇒ A} → Pullback f h) where !⊣* : BaseChange! f ⊣ BaseChange* f pullback - !⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ Forgetful⊣Free (Slice A) (pullback⇒product pullback) + !⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ TotalSpace⊣ConstantFamily (Slice A) (pullback⇒product pullback) diff --git a/src/Categories/Adjoint/Instance/Slice.agda b/src/Categories/Adjoint/Instance/Slice.agda index f1e6a13fa..195ad871e 100644 --- a/src/Categories/Adjoint/Instance/Slice.agda +++ b/src/Categories/Adjoint/Instance/Slice.agda @@ -9,7 +9,7 @@ open import Categories.Category.BinaryProducts C open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.CartesianClosed using (CartesianClosed) open import Categories.Category.Slice C using (SliceObj; sliceobj; Slice⇒; slicearr) -open import Categories.Functor.Slice C using (Forgetful; Free; Coforgetful) +open import Categories.Functor.Slice C using (TotalSpace; ConstantFamily; InternalSections) open import Categories.Morphism.Reasoning C open import Categories.NaturalTransformation using (ntHelper) open import Categories.Diagram.Pullback C hiding (swap) @@ -30,8 +30,8 @@ module _ {A : Obj} (product : ∀ {X} → Product A X) where module product {X} = Product (product {X}) open product - Forgetful⊣Free : Forgetful ⊣ Free product - Forgetful⊣Free = record + TotalSpace⊣ConstantFamily : TotalSpace ⊣ ConstantFamily product + TotalSpace⊣ConstantFamily = record { unit = ntHelper record { η = λ _ → slicearr project₁ ; commute = λ {X} {Y} f → begin @@ -60,8 +60,8 @@ module _ {A : Obj} (ccc : CartesianClosed C) (pullback : ∀ {X} {Y} {Z} (h : X open Terminal terminal open BinaryProducts products - Free⊣Coforgetful : Free {A = A} product ⊣ Coforgetful ccc pullback - Free⊣Coforgetful = record + ConstantFamily⊣InternalSections : ConstantFamily {A = A} product ⊣ InternalSections ccc pullback + ConstantFamily⊣InternalSections = record { unit = ntHelper record { η = λ X → p.universal (sliceobj π₁) (λ-unique₂′ (unit-pb X)) ; commute = λ {S} {T} f → p.unique-diagram (sliceobj π₁) !-unique₂ $ begin diff --git a/src/Categories/Functor/Slice.agda b/src/Categories/Functor/Slice.agda index 99e7b6fa2..bfd717d5c 100644 --- a/src/Categories/Functor/Slice.agda +++ b/src/Categories/Functor/Slice.agda @@ -42,8 +42,8 @@ module _ {A : Obj} where open S C - Forgetful : Functor (Slice A) C - Forgetful = record + TotalSpace : Functor (Slice A) C + TotalSpace = record { F₀ = Y ; F₁ = h ; identity = refl @@ -56,8 +56,8 @@ module _ {A : Obj} where module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i) open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁) - pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B) - pullback-functorial f = record + BaseChange : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B) + BaseChange f = record { F₀ = λ X → S.sliceobj (p.p₁ X) ; F₁ = λ f → S.slicearr {h = p⇒.pbarr _ _ f} (p.p₁∘universal≈h₁ _ ○ identityˡ) ; identity = sym $ p.unique _ id-comm id-comm @@ -120,8 +120,8 @@ module _ {A : Obj} where open product -- this is adapted from proposition 1.33 of Aspects of Topoi (Freyd, 1972) - Free : Functor C (Slice A) - Free = record + ConstantFamily : Functor C (Slice A) + ConstantFamily = record { F₀ = λ _ → sliceobj π₁ ; F₁ = λ f → slicearr ([ product ⇒ product ]π₁∘× ○ identityˡ) ; identity = id×id product @@ -139,9 +139,8 @@ module _ {A : Obj} where open Terminal terminal open BinaryProducts products - -- Needs better name! - Coforgetful : Functor (Slice A) C - Coforgetful = record + InternalSections : Functor (Slice A) C + InternalSections = record { F₀ = p.P ; F₁ = λ f → p.universal _ (F₁-lemma f) ; identity = λ {X} → sym $ p.unique X (sym (!-unique _)) $ begin diff --git a/src/Categories/Functor/Slice/BaseChange.agda b/src/Categories/Functor/Slice/BaseChange.agda index 84ab8d87b..20d8174d9 100644 --- a/src/Categories/Functor/Slice/BaseChange.agda +++ b/src/Categories/Functor/Slice/BaseChange.agda @@ -7,7 +7,7 @@ module Categories.Functor.Slice.BaseChange {o ℓ e} (C : Category o ℓ e) wher open import Categories.Category.Slice C using (Slice) open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice⇒slice; slice⇒slice-slice) open import Categories.Functor using (Functor; _∘F_) -open import Categories.Functor.Slice using (Forgetful; Free) +open import Categories.Functor.Slice using (TotalSpace; ConstantFamily; BaseChange) open import Categories.Diagram.Pullback C using (Pullback) open Category C @@ -16,9 +16,9 @@ module _ {A B : Obj} (f : B ⇒ A) where -- Any morphism induces a functor between slices. BaseChange! : Functor (Slice B) (Slice A) - BaseChange! = Forgetful (Slice A) ∘F slice⇒slice-slice f + BaseChange! = TotalSpace (Slice A) ∘F slice⇒slice-slice f -- Any morphism which admits pullbacks induces a functor the other way between slices. -- This is adjoint to BaseChange!: see Categories.Adjoint.Instance.BaseChange. BaseChange* : (∀ {C} {h : C ⇒ A} → Pullback f h) → Functor (Slice A) (Slice B) - BaseChange* pullback = slice-slice⇒slice f ∘F Free (Slice A) (pullback⇒product pullback) + BaseChange* pullback = slice-slice⇒slice f ∘F ConstantFamily (Slice A) (pullback⇒product pullback) From 723fe77d883d18c8464e37a342d17cba852a424d Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 27 Jan 2024 20:53:14 +0100 Subject: [PATCH 7/8] Remove Functor.Slice.BaseChange It was pretty much exactly the same as Functor.Slice.BaseChange.BaseChange* --- src/Categories/Functor/Slice.agda | 62 ------------------------------- 1 file changed, 62 deletions(-) diff --git a/src/Categories/Functor/Slice.agda b/src/Categories/Functor/Slice.agda index bfd717d5c..06d098270 100644 --- a/src/Categories/Functor/Slice.agda +++ b/src/Categories/Functor/Slice.agda @@ -51,68 +51,6 @@ module _ {A : Obj} where ; F-resp-≈ = id→ } - module _ (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where - private - module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i) - open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁) - - BaseChange : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B) - BaseChange f = record - { F₀ = λ X → S.sliceobj (p.p₁ X) - ; F₁ = λ f → S.slicearr {h = p⇒.pbarr _ _ f} (p.p₁∘universal≈h₁ _ ○ identityˡ) - ; identity = sym $ p.unique _ id-comm id-comm - ; homomorphism = p.unique-diagram _ homomorphism-lemmaˡ homomorphism-lemmaʳ - ; F-resp-≈ = λ {_ B} {h i} eq → p.unique-diagram B F-resp-≈-lemmaˡ (F-resp-≈-lemmaʳ eq) - } - where - p : ∀ X → Pullback f (arr X) - p X = pullback f (arr X) - module p X = Pullback (p X) - - p⇒ : ∀ X Y (g : Slice⇒ X Y) → Pbs.Pullback⇒ C A _ _ - p⇒ X Y g = pX⇒pY - where - pX : Pbs.PullbackObj C A - pX = record { pullback = p X } - pY : Pbs.PullbackObj C A - pY = record { pullback = p Y } - pX⇒pY : Pbs.Pullback⇒ C A pX pY - pX⇒pY = record - { mor₁ = Category.id C - ; mor₂ = h g - ; commute₁ = identityʳ - ; commute₂ = △ g - } - - module p⇒ X Y g = Pbs.Pullback⇒ (p⇒ X Y g) - - homomorphism-lemmaˡ : ∀ {X Y Z α β} → p.p₁ Z ∘ p⇒.pbarr X Z _ ≈ p.p₁ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α - homomorphism-lemmaˡ {X} {Y} {Z} {α} {β} = begin - p.p₁ Z ∘ p⇒.pbarr X Z _ ≈⟨ p.p₁∘universal≈h₁ Z ⟩ - id ∘ p.p₁ X ≈˘⟨ identityˡ ⟩ - id ∘ id ∘ p.p₁ X ≈˘⟨ pullʳ (p.p₁∘universal≈h₁ Y) ⟩ - (id ∘ p.p₁ Y) ∘ p⇒.pbarr X Y α ≈˘⟨ pullˡ (p.p₁∘universal≈h₁ Z) ⟩ - p.p₁ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α ∎ - - homomorphism-lemmaʳ : ∀ {X Y Z α β} → p.p₂ Z ∘ p⇒.pbarr X Z _ ≈ p.p₂ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α - homomorphism-lemmaʳ {X} {Y} {Z} {α} {β} = begin - p.p₂ Z ∘ p⇒.pbarr X Z _ ≈⟨ p.p₂∘universal≈h₂ Z ⟩ - (h β ∘ h α) ∘ p.p₂ X ≈˘⟨ glue′ (p.p₂∘universal≈h₂ Z) (p.p₂∘universal≈h₂ Y) ⟩ - p.p₂ Z ∘ p⇒.pbarr Y Z β ∘ p⇒.pbarr X Y α ∎ - - F-resp-≈-lemmaˡ : ∀ {A B} {α β : Slice⇒ A B} → p.p₁ B ∘ p⇒.pbarr A B α ≈ p.p₁ B ∘ p⇒.pbarr A B β - F-resp-≈-lemmaˡ {A} {B} {α} {β} = begin - p.p₁ B ∘ p⇒.pbarr A B α ≈⟨ p.p₁∘universal≈h₁ B ⟩ - id ∘ p.p₁ A ≈˘⟨ p.p₁∘universal≈h₁ B ⟩ - p.p₁ B ∘ p⇒.pbarr A B β ∎ - - F-resp-≈-lemmaʳ : ∀ {A B} {α β : Slice⇒ A B} → h α ≈ h β → p.p₂ B ∘ p⇒.pbarr A B α ≈ p.p₂ B ∘ p⇒.pbarr A B β - F-resp-≈-lemmaʳ {A} {B} {α} {β} eq = begin - p.p₂ B ∘ p⇒.pbarr A B α ≈⟨ p.p₂∘universal≈h₂ B ⟩ - h α ∘ p.p₂ A ≈⟨ eq ⟩∘⟨refl ⟩ - h β ∘ p.p₂ A ≈˘⟨ p.p₂∘universal≈h₂ B ⟩ - p.p₂ B ∘ p⇒.pbarr A B β ∎ - module _ (product : {X : Obj} → Product A X) where private From ce4a5180afd917c12ffc254bc413544051bd41e9 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 27 Jan 2024 21:30:13 +0100 Subject: [PATCH 8/8] Remove accidentally added import --- src/Categories/Functor/Slice/BaseChange.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Categories/Functor/Slice/BaseChange.agda b/src/Categories/Functor/Slice/BaseChange.agda index 20d8174d9..937502e51 100644 --- a/src/Categories/Functor/Slice/BaseChange.agda +++ b/src/Categories/Functor/Slice/BaseChange.agda @@ -7,7 +7,7 @@ module Categories.Functor.Slice.BaseChange {o ℓ e} (C : Category o ℓ e) wher open import Categories.Category.Slice C using (Slice) open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice⇒slice; slice⇒slice-slice) open import Categories.Functor using (Functor; _∘F_) -open import Categories.Functor.Slice using (TotalSpace; ConstantFamily; BaseChange) +open import Categories.Functor.Slice using (TotalSpace; ConstantFamily) open import Categories.Diagram.Pullback C using (Pullback) open Category C