intro for reindex and reindex'

maxsnew · Mar 17, 2024 · bf19765 · bf19765
1 parent 6d79c61
commit bf19765
Show file tree

Hide file tree

Showing 2 changed files with 120 additions and 30 deletions.
diff --git 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,60 +59,103 @@ 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
 
 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
     module R = HomᴰReasoning Dᴰ
     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
@@ -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ᴰ)