implement an Eq-based Functorᴰ reindexing

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

Hide file tree

Showing 3 changed files with 99 additions and 14 deletions.
diff --git 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
@@ -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,16 +27,19 @@ 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
   private
     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
@@ -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