From bf19765a6f29392e3c9f8963107eac6ec1e2b607 Mon Sep 17 00:00:00 2001 From: Max New Date: Fri, 15 Mar 2024 09:32:46 -0400 Subject: [PATCH] intro for reindex and reindex' --- .../Displayed/Constructions/Reindex.agda | 122 +++++++++++++----- Cubical/Categories/Displayed/Magmoid.agda | 28 +++- 2 files changed, 120 insertions(+), 30 deletions(-) diff --git a/Cubical/Categories/Displayed/Constructions/Reindex.agda b/Cubical/Categories/Displayed/Constructions/Reindex.agda index 971e600e..9bbd75f7 100644 --- a/Cubical/Categories/Displayed/Constructions/Reindex.agda +++ b/Cubical/Categories/Displayed/Constructions/Reindex.agda @@ -9,8 +9,8 @@ module Cubical.Categories.Displayed.Constructions.Reindex where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma -import Cubical.Data.Equality as Equality -import Cubical.Data.Equality.Conversion as Equality +import Cubical.Data.Equality as Eq +import Cubical.Data.Equality.Conversion as Eq open import Cubical.Categories.Category.Base open import Cubical.Categories.Constructions.BinProduct @@ -26,7 +26,28 @@ open import Cubical.Categories.Displayed.Magmoid private variable - ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level + ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level + +module _ + {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} + {F : Functor C D} + {B : Category ℓB ℓB'} {Bᴰ : Categoryᴰ B ℓBᴰ ℓBᴰ'} + (G : Functor B C) + (FGᴰ : Functorᴰ (F ∘F G) Bᴰ Dᴰ) + where + private + module Dᴰ = Categoryᴰ Dᴰ + module F*Dᴰ = Categoryᴰ (reindex Dᴰ F) + module R = HomᴰReasoning Dᴰ + open Functor + open Functorᴰ + intro : Functorᴰ G Bᴰ (reindex Dᴰ F) + intro .F-obᴰ = FGᴰ .F-obᴰ + intro .F-homᴰ = FGᴰ .F-homᴰ + intro .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-idᴰ) (R.reind-filler _ _)) + intro .F-seqᴰ fᴰ gᴰ = + R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-seqᴰ fᴰ gᴰ) (R.reind-filler _ _)) module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') @@ -38,29 +59,32 @@ module _ -- todo: generalize upstream somewhere to Data.Equality? isPropEqHom : ∀ {a b : C.ob} {f g : C [ a , b ]} - → isProp (f Equality.≡ g) + → isProp (f Eq.≡ g) isPropEqHom {f = f}{g} = - subst isProp (Equality.PathPathEq {x = f}{y = g}) (C.isSetHom f g) + subst isProp (Eq.PathPathEq {x = f}{y = g}) (C.isSetHom f g) open Categoryᴰ Cᴰ - reind' : {a b : C.ob} {f g : C [ a , b ]} (p : f Equality.≡ g) + reind' : {a b : C.ob} {f g : C [ a , b ]} (p : f Eq.≡ g) {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} → Hom[ f ][ aᴰ , bᴰ ] → Hom[ g ][ aᴰ , bᴰ ] - reind' p = Equality.transport Hom[_][ _ , _ ] p + reind' p = Eq.transport Hom[_][ _ , _ ] p reind≡reind' : ∀ {a b : C.ob} {f g : C [ a , b ]} - {p : f ≡ g} {e : f Equality.≡ g} + {p : f ≡ g} {e : f Eq.≡ g} {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} → (fᴰ : Hom[ f ][ aᴰ , bᴰ ]) → R.reind p fᴰ ≡ reind' e fᴰ - reind≡reind' {p = p}{e} fᴰ = subst {x = Equality.pathToEq p} (λ e → R.reind p fᴰ ≡ reind' e fᴰ) - (isPropEqHom _ _) - lem + reind≡reind' {p = p}{e} fᴰ = + subst {x = Eq.pathToEq p} + (λ e → R.reind p fᴰ ≡ reind' e fᴰ) + (isPropEqHom _ _) + lem where - lem : R.reind p fᴰ ≡ reind' (Equality.pathToEq p) fᴰ - lem = sym (Equality.eqToPath ((Equality.transportPathToEq→transportPath Hom[_][ _ , _ ]) p fᴰ)) - + lem : R.reind p fᴰ ≡ reind' (Eq.pathToEq p) fᴰ + lem = sym (Eq.eqToPath + ((Eq.transportPathToEq→transportPath Hom[_][ _ , _ ]) p fᴰ)) + open Category open Functor @@ -68,9 +92,9 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') (F : Functor C D) - (F-id' : {x : C .ob} → D .id {x = F .F-ob x} Equality.≡ F .F-hom (C .id)) + (F-id' : {x : C .ob} → D .id {x = F .F-ob x} Eq.≡ F .F-hom (C .id)) (F-seq' : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ]) - → (F .F-hom f) ⋆⟨ D ⟩ (F .F-hom g) Equality.≡ F .F-hom (f ⋆⟨ C ⟩ g)) + → (F .F-hom f) ⋆⟨ D ⟩ (F .F-hom g) Eq.≡ F .F-hom (f ⋆⟨ C ⟩ g)) where private @@ -78,20 +102,60 @@ module _ module C = Category C module D = Category D module Dᴰ = Categoryᴰ Dᴰ - open Functor F - -- I admonish you to use this definition only when F-id' and F-seq' - -- above are Equality.refl - reindex' : Categoryᴰ C ℓDᴰ ℓDᴰ' - reindex' = redefine-id⋆ (reindex Dᴰ F) - (reind' Dᴰ F-id' Dᴰ.idᴰ , implicitFunExt (λ {x} → implicitFunExt (λ {xᴰ} → + singId : singl {A = {x : C .ob} {p : Dᴰ .Categoryᴰ.ob[_] (F .F-ob x)} → + Dᴰ .Categoryᴰ.Hom[_][_,_] {F .F-ob x} {F .F-ob x} + (F .F-hom {x} {x} (C .id {x})) p p} + (R.reind (λ i → F .F-id (~ i)) (Dᴰ.idᴰ)) + singId = (reind' Dᴰ F-id' Dᴰ.idᴰ , + implicitFunExt (λ {x} → implicitFunExt (λ {xᴰ} → reind≡reind' Dᴰ Dᴰ.idᴰ))) - ((λ fᴰ gᴰ → reind' Dᴰ (F-seq' _ _) (Dᴰ._⋆ᴰ_ fᴰ gᴰ)) - , implicitFunExt (λ {x} → implicitFunExt (λ {y} → implicitFunExt (λ {z} → + + + singSeq : singl + {A = ∀ {x y z} {f : C .Hom[_,_] x y} {g : C .Hom[_,_] y z}{xᴰ}{yᴰ}{zᴰ} + → Dᴰ.Hom[ F .F-hom f ][ xᴰ , yᴰ ] + → Dᴰ.Hom[ F .F-hom g ][ yᴰ , zᴰ ] + → Dᴰ.Hom[ F .F-hom (f C.⋆ g)][ xᴰ , zᴰ ]} + (λ {x}{y}{z}{f}{g} fᴰ gᴰ → R.reind (sym (F .F-seq f g)) (fᴰ Dᴰ.⋆ᴰ gᴰ)) + singSeq = (λ fᴰ gᴰ → reind' Dᴰ (F-seq' _ _) (Dᴰ._⋆ᴰ_ fᴰ gᴰ)) , + implicitFunExt (λ {x} → implicitFunExt (λ {y} → implicitFunExt (λ {z} → implicitFunExt (λ {f} → implicitFunExt (λ {g} → implicitFunExt (λ {xᴰ} → - implicitFunExt (λ {yᴰ} → implicitFunExt (λ {zᴰ} → funExt (λ fᴰ → funExt λ gᴰ → - reind≡reind' Dᴰ (fᴰ Dᴰ.⋆ᴰ gᴰ))))))))))) + implicitFunExt (λ {yᴰ} → implicitFunExt (λ {zᴰ} → + funExt (λ fᴰ → funExt λ gᴰ → reind≡reind' Dᴰ (fᴰ Dᴰ.⋆ᴰ gᴰ)))))))))) + + -- This definition is preferable to reindex when F-id' and F-seq' + -- are given by Eq.refl. + reindex' : Categoryᴰ C ℓDᴰ ℓDᴰ' + reindex' = redefine-id⋆ (reindex Dᴰ F) singId singSeq + + + -- TODO: it would be really nice to have a macro reindexRefl! that + -- worked like the following: See + -- Cubical.Categories.Constructions.Quotient.More for an example + -- reindexRefl! Cᴰ F = reindex' Cᴰ F Eq.refl (λ _ _ → Eq.refl) + + -- TODO + -- π-reindex : Functorᴰ F reindex' Dᴰ + module _ {B : Category ℓB ℓB'} {Bᴰ : Categoryᴰ B ℓBᴰ ℓBᴰ'} + (G : Functor B C) + (FGᴰ : Functorᴰ (F ∘F G) Bᴰ Dᴰ) + where + reindex-intro' : Functorᴰ G Bᴰ reindex' + reindex-intro' = redefine-id⋆F (reindex Dᴰ F) singId singSeq (intro G FGᴰ) + +module _ + {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} + {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} + {F : Functor C D} + {F-id' : {x : C .ob} → D .id {x = F .F-ob x} Eq.≡ F .F-hom (C .id)} + {F-seq' : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ]) + → (F .F-hom f) ⋆⟨ D ⟩ (F .F-hom g) Eq.≡ F .F-hom (f ⋆⟨ C ⟩ g)} + {B : Category ℓB ℓB'} {Bᴰ : Categoryᴰ B ℓBᴰ ℓBᴰ'} + (G : Functor B C) + (FGᴰ : Functorᴰ (F ∘F G) Bᴰ Dᴰ) + where - -- TODO: it would be really nice to have a macro reindexRefl! that worked like the following: - -- See Cubical.Categories.Constructions.Quotient.More for an example - -- reindexRefl! Cᴰ F = reindex' Cᴰ F Equality.refl (λ _ _ → Equality.refl) + open Functorᴰ + intro' : Functorᴰ G Bᴰ (reindex' Dᴰ F F-id' F-seq') + intro' = reindex-intro' Dᴰ F F-id' F-seq' G FGᴰ diff --git a/Cubical/Categories/Displayed/Magmoid.agda b/Cubical/Categories/Displayed/Magmoid.agda index c3a61632..8fd9062f 100644 --- a/Cubical/Categories/Displayed/Magmoid.agda +++ b/Cubical/Categories/Displayed/Magmoid.agda @@ -8,11 +8,13 @@ open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels open import Cubical.Data.Sigma open import Cubical.Categories.Category.Base +open import Cubical.Categories.Functor open import Cubical.Categories.Displayed.Base +open import Cubical.Categories.Displayed.Functor private variable - ℓC ℓC' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' : Level + ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level -- Displayed categories with hom-sets record Magmoidᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' @@ -68,3 +70,27 @@ module _ {C : Category ℓC ℓC'} (R.≡[]-rectify (λ i → ⋆ᴰ' .snd i (⋆ᴰ' .snd i fᴰ gᴰ) hᴰ)) (R.≡[]-rectify (λ i → ⋆ᴰ' .snd i fᴰ (⋆ᴰ' .snd i gᴰ hᴰ))) (Cᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ) + + module _ {D : Category ℓD ℓD'}{Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'} + {F : Functor D C} + (Fᴰ : Functorᴰ F Dᴰ Cᴰ) + where + open Functorᴰ + open Functor + private + module Dᴰ = Categoryᴰ Dᴰ + module RID = Categoryᴰ redefine-id⋆ + redefine-id⋆F : Functorᴰ F Dᴰ redefine-id⋆ + redefine-id⋆F .F-obᴰ = Fᴰ .F-obᴰ + redefine-id⋆F .F-homᴰ = Fᴰ .F-homᴰ + redefine-id⋆F .F-idᴰ {x}{xᴰ} = + subst (λ idᴰ → (Fᴰ .F-homᴰ (Dᴰ .Categoryᴰ.idᴰ)) RID.≡[ F .F-id ] idᴰ) + (λ i → idᴰ' .snd i) + (Fᴰ .F-idᴰ) + redefine-id⋆F .F-seqᴰ {x} {y} {z} {f} {g} {xᴰ} {yᴰ} {zᴰ} fᴰ gᴰ = + subst (λ _⋆ᴰ_ → + Fᴰ .F-homᴰ (fᴰ Dᴰ.⋆ᴰ gᴰ) + RID.≡[ F .F-seq f g ] + Fᴰ .F-homᴰ fᴰ ⋆ᴰ Fᴰ .F-homᴰ gᴰ) + (λ i → ⋆ᴰ' .snd i) + (Fᴰ .F-seqᴰ fᴰ gᴰ)