From 6d79c61db680c5603a00dacaac52b016dd01d8be Mon Sep 17 00:00:00 2001 From: Max New Date: Fri, 15 Mar 2024 15:47:07 -0400 Subject: [PATCH] =?UTF-8?q?implement=20an=20Eq-based=20Functor=E1=B4=B0=20?= =?UTF-8?q?reindexing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Categories/Displayed/Functor/More.agda | 89 +++++++++++++++++-- Cubical/Categories/Displayed/Magmoid.agda | 23 +++-- .../Profunctor/FunctorComprehension.agda | 1 + 3 files changed, 99 insertions(+), 14 deletions(-) diff --git a/Cubical/Categories/Displayed/Functor/More.agda b/Cubical/Categories/Displayed/Functor/More.agda index 70bf60de..97c804aa 100644 --- a/Cubical/Categories/Displayed/Functor/More.agda +++ b/Cubical/Categories/Displayed/Functor/More.agda @@ -7,28 +7,105 @@ open import Cubical.Foundations.Prelude open import Cubical.Categories.Category.Base open import Cubical.Categories.Functor +import Cubical.Data.Equality as Eq open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Base.More open import Cubical.Categories.Displayed.Properties open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Constructions.Weaken +import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning private variable - ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' : Level + ℓ ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' : Level + +-- TODO: move to Equality.Base or something + +HEq : {A0 A1 : Type ℓ}(Aeq : A0 Eq.≡ A1) (a0 : A0)(a1 : A1) → Type _ +HEq Aeq a0 a1 = Eq.transport (λ A → A) Aeq a0 Eq.≡ a1 + +singlP' : {A0 A1 : Type ℓ}(Aeq : A0 Eq.≡ A1) (a : A0) → Type _ +singlP' {A1 = A1} Aeq a = Σ[ x ∈ A1 ] HEq Aeq a x + +singl' : {A : Type ℓ}(a : A) → Type _ +singl' {A = A} a = singlP' Eq.refl a + module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}{Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} - {F G : Functor C D} + {F : Functor C D} where + open Functor open Functorᴰ - -- Pro tip: never use this - reindF : (H : F ≡ G) → Functorᴰ F Cᴰ Dᴰ → Functorᴰ G Cᴰ Dᴰ + -- Only use this if H is not refl on ob/hom, otherwise use reindF' below + reindF : ∀ {G}(H : F ≡ G) → Functorᴰ F Cᴰ Dᴰ → Functorᴰ G Cᴰ Dᴰ reindF H = subst (λ F → Functorᴰ F Cᴰ Dᴰ) H + private + module C = Category C + module D = Category D + module Cᴰ = Categoryᴰ Cᴰ + module Dᴰ = Categoryᴰ Dᴰ + module R = HomᴰReasoning Dᴰ + + GF-ob-ty = singl' (F .F-ob) + GF-hom-ty : GF-ob-ty → Type _ + GF-hom-ty GF-ob = singlP' + (Eq.ap (λ G-ob → ∀ {x}{y} → C [ x , y ] → D [ G-ob x , G-ob y ]) + (GF-ob .snd)) + (F .F-hom) -- Pro tip: always use this - -- reindF' : Functorᴰ F Cᴰ Dᴰ → Functorᴰ G Cᴰ Dᴰ + module _ (Fᴰ : Functorᴰ F Cᴰ Dᴰ) where + open Functor + reindF'-ob : (GF-ob : GF-ob-ty) → ∀ {x} → Cᴰ.ob[ x ] → Dᴰ.ob[ GF-ob .fst x ] + reindF'-ob (_ , Eq.refl) = Fᴰ .F-obᴰ + + reindF'-hom : (GF-ob : GF-ob-ty) (GF-hom : GF-hom-ty GF-ob) + → ∀ {x y}{f : C [ x , y ]}{xᴰ}{yᴰ} + → Cᴰ [ f ][ xᴰ , yᴰ ] + → Dᴰ [ GF-hom .fst f + ][ reindF'-ob GF-ob xᴰ + , reindF'-ob GF-ob yᴰ ] + reindF'-hom (_ , Eq.refl) (_ , Eq.refl) = Fᴰ .F-homᴰ + + reindF'-id : (GF-ob : GF-ob-ty) (GF-hom : GF-hom-ty GF-ob) + (GF-id : ∀ {x} → GF-hom .fst (C.id {x}) ≡ D.id) + → ∀ {x}{xᴰ : Cᴰ.ob[ x ]} + → reindF'-hom GF-ob GF-hom (Cᴰ.idᴰ {x}{xᴰ}) Dᴰ.≡[ GF-id ] Dᴰ.idᴰ + reindF'-id (_ , Eq.refl) (_ , Eq.refl) GF-id = R.≡[]-rectify (Fᴰ .F-idᴰ) + + reindF'-seq : (GF-ob : GF-ob-ty) (GF-hom : GF-hom-ty GF-ob) + (GF-seq : ∀ {x}{y}{z}(f : C [ x , y ])(g : C [ y , z ]) + → GF-hom .fst (f C.⋆ g) ≡ (GF-hom .fst f) D.⋆ GF-hom .fst g) + → ∀ {x}{y}{z}{f : C [ x , y ]}{g : C [ y , z ]}{xᴰ}{yᴰ}{zᴰ} + → (fᴰ : Cᴰ [ f ][ xᴰ , yᴰ ]) (gᴰ : Cᴰ [ g ][ yᴰ , zᴰ ]) → + reindF'-hom GF-ob GF-hom + (fᴰ Cᴰ.⋆ᴰ gᴰ) Dᴰ.≡[ GF-seq f g ] + reindF'-hom GF-ob GF-hom fᴰ Dᴰ.⋆ᴰ reindF'-hom GF-ob GF-hom gᴰ + reindF'-seq (_ , Eq.refl) (_ , Eq.refl) GF-seq fᴰ gᴰ = + R.≡[]-rectify (Fᴰ .F-seqᴰ fᴰ gᴰ) + + open Functor + reindF' : (G : Functor C D) + (GF-ob≡FF-ob : F .F-ob Eq.≡ G .F-ob) + (GF-hom≡FF-hom : + HEq (Eq.ap (λ F-ob₁ → ∀ {x} {y} + → C [ x , y ] → D [ F-ob₁ x , F-ob₁ y ]) + GF-ob≡FF-ob) + (F .F-hom) + (G .F-hom)) + → Functorᴰ F Cᴰ Dᴰ + → Functorᴰ G Cᴰ Dᴰ + reindF' G GF-ob≡FF-ob GF-hom≡FF-hom Fᴰ = record + { F-obᴰ = reindF'-ob Fᴰ GF-ob + ; F-homᴰ = reindF'-hom Fᴰ GF-ob GF-hom + ; F-idᴰ = reindF'-id Fᴰ GF-ob GF-hom (G .F-id) + ; F-seqᴰ = reindF'-seq Fᴰ GF-ob GF-hom (G .F-seq) + } where + GF-ob : GF-ob-ty + GF-ob = _ , GF-ob≡FF-ob - -- notation reindF'' + GF-hom : GF-hom-ty GF-ob + GF-hom = _ , GF-hom≡FF-hom diff --git a/Cubical/Categories/Displayed/Magmoid.agda b/Cubical/Categories/Displayed/Magmoid.agda index a7645b01..c3a61632 100644 --- a/Cubical/Categories/Displayed/Magmoid.agda +++ b/Cubical/Categories/Displayed/Magmoid.agda @@ -15,7 +15,8 @@ private ℓC ℓC' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level -- Displayed categories with hom-sets -record Magmoidᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' : Type (ℓ-suc (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓCᴰ ℓCᴰ'))) where +record Magmoidᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' + : Type (ℓ-suc (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓCᴰ ℓCᴰ'))) where no-eta-equality open Category C field @@ -26,7 +27,6 @@ record Magmoidᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' : Type (ℓ-suc ( → Hom[ f ][ xᴰ , yᴰ ] → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ] infixr 9 _⋆ᴰ_ - -- infixr 9 _∘ᴰ_ module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where @@ -34,8 +34,12 @@ module _ {C : Category ℓC ℓC'} module C = Category C module Cᴰ = Categoryᴰ Cᴰ - module _ (idᴰ' : singl {A = ∀ {x} {p : Cᴰ.ob[ x ]} → Cᴰ.Hom[ C.id ][ p , p ]} Cᴰ.idᴰ) - (⋆ᴰ' : singl {A = ∀ {x y z} {f : C.Hom[ x , y ]} {g : C.Hom[ y , z ]} {xᴰ yᴰ zᴰ} → Cᴰ.Hom[ f ][ xᴰ , yᴰ ] → Cᴰ.Hom[ g ][ yᴰ , zᴰ ] → Cᴰ.Hom[ f C.⋆ g ][ xᴰ , zᴰ ]} Cᴰ._⋆ᴰ_) + module _ (idᴰ' : singl {A = ∀ {x} {p : Cᴰ.ob[ x ]} → Cᴰ.Hom[ C.id ][ p , p ]} + Cᴰ.idᴰ) + (⋆ᴰ' : singl {A = ∀ {x y z} {f : C.Hom[ x , y ]} {g : C.Hom[ y , z ]} + {xᴰ yᴰ zᴰ} → Cᴰ.Hom[ f ][ xᴰ , yᴰ ] → Cᴰ.Hom[ g ][ yᴰ , zᴰ ] + → Cᴰ.Hom[ f C.⋆ g ][ xᴰ , zᴰ ]} + Cᴰ._⋆ᴰ_) where private import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning @@ -47,16 +51,19 @@ module _ {C : Category ℓC ℓC'} redefine-id⋆ .Categoryᴰ.isSetHomᴰ = Cᴰ.isSetHomᴰ redefine-id⋆ .Categoryᴰ.idᴰ = idᴰ' .fst redefine-id⋆ .Categoryᴰ._⋆ᴰ_ = ⋆ᴰ' .fst - redefine-id⋆ .Categoryᴰ.⋆IdLᴰ {f = f}{xᴰ = xᴰ}{yᴰ = yᴰ} fᴰ = - subst (λ gᴰ → PathP (λ i → Cᴰ.Hom[ C .Category.⋆IdL f i ][ xᴰ , yᴰ ]) gᴰ fᴰ ) + redefine-id⋆ .Categoryᴰ.⋆IdLᴰ {f = f}{xᴰ = xᴰ}{yᴰ = yᴰ} fᴰ = + subst (λ gᴰ → PathP (λ i → Cᴰ.Hom[ C .Category.⋆IdL f i ][ xᴰ , yᴰ ]) + gᴰ fᴰ ) -- todo: couldn't get congP₂ to work (R.≡[]-rectify λ i → ⋆ᴰ' .snd i (idᴰ' .snd i) fᴰ) (Cᴰ.⋆IdLᴰ fᴰ) redefine-id⋆ .Categoryᴰ.⋆IdRᴰ {f = f}{xᴰ}{yᴰ} fᴰ = - subst (λ gᴰ → PathP (λ i → Cᴰ.Hom[ C .Category.⋆IdR f i ][ xᴰ , yᴰ ]) gᴰ fᴰ) + subst (λ gᴰ → PathP (λ i → Cᴰ.Hom[ C .Category.⋆IdR f i ][ xᴰ , yᴰ ]) + gᴰ fᴰ) (R.≡[]-rectify λ i → ⋆ᴰ' .snd i fᴰ (idᴰ' .snd i)) (Cᴰ.⋆IdRᴰ fᴰ) - redefine-id⋆ .Categoryᴰ.⋆Assocᴰ {x}{y}{z}{w}{f}{g}{h}{xᴰ}{yᴰ}{zᴰ}{wᴰ} fᴰ gᴰ hᴰ = + redefine-id⋆ .Categoryᴰ.⋆Assocᴰ {x}{y}{z}{w}{f}{g}{h}{xᴰ}{yᴰ}{zᴰ}{wᴰ} + fᴰ gᴰ hᴰ = subst2 (PathP (λ i → Cᴰ.Hom[ C .Category.⋆Assoc f g h i ][ xᴰ , wᴰ ])) (R.≡[]-rectify (λ i → ⋆ᴰ' .snd i (⋆ᴰ' .snd i fᴰ gᴰ) hᴰ)) (R.≡[]-rectify (λ i → ⋆ᴰ' .snd i fᴰ (⋆ᴰ' .snd i gᴰ hᴰ))) diff --git a/Cubical/Categories/Profunctor/FunctorComprehension.agda b/Cubical/Categories/Profunctor/FunctorComprehension.agda index dd19b853..f6497363 100644 --- a/Cubical/Categories/Profunctor/FunctorComprehension.agda +++ b/Cubical/Categories/Profunctor/FunctorComprehension.agda @@ -54,6 +54,7 @@ open import Cubical.Categories.Instances.Functors.More open import Cubical.Categories.Displayed.Functor open import Cubical.Categories.Displayed.Constructions.Comma open import Cubical.Categories.Displayed.Constructions.Graph +open import Cubical.Categories.Displayed.Constructions.Weaken open import Cubical.Categories.Displayed.Base open import Cubical.Categories.Displayed.Base.More as Disp open import Cubical.Categories.Displayed.Base.HLevel1Homs