Displayed categories

src/Categories/Category/Displayed/Instance/DisplayedCats.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Displayed.Instance.DisplayedCats where
+
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Category.Instance.Cats
+open import Categories.Functor.Displayed
+open import Categories.NaturalTransformation.NaturalIsomorphism.Displayed
+
+DisplayedCats : ∀ o ℓ e o′ ℓ′ e′ → Displayed (Cats o ℓ e) (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′)
+DisplayedCats o ℓ e o′ ℓ′ e′ = record
+  { Obj[_] = λ B → Displayed B o′ ℓ′ e′
+  ; _⇒[_]_ = λ C F D → DisplayedFunctor C D F
+  ; _≈[_]_ = λ F′ F≃G G′ → DisplayedNaturalIsomorphism F′ G′ F≃G
+  ; id′ = id′
+  ; _∘′_ = _∘F′_
+  ; identityˡ′ = unitorˡ′
+  ; identityʳ′ = unitorʳ′
+  ; identity²′ = unitor²′
+  ; assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → associator′ H′ G′ F′
+  ; sym-assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → sym-associator′ H′ G′ F′
+  ; equiv′ = isDisplayedEquivalence
+  ; ∘′-resp-≈[] = _ⓘₕ′_
+  }

src/Categories/Category/Instance/Cats.agda

@@ -9,7 +9,7 @@ open import Level
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
+  using (NaturalIsomorphism; associator; sym-associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
 private
   variable
     o ℓ e : Level
@@ -24,7 +24,7 @@ Cats o ℓ e = record
   ; id        = id
   ; _∘_       = _∘F_
   ; assoc     = λ {_ _ _ _ F G H} → associator F G H
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator F G H
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²

src/Categories/Functor/Displayed/Properties.agda

@@ -7,6 +7,8 @@ open import Categories.Category.Displayed
 open import Categories.Functor
 open import Categories.Functor.Displayed
 open import Categories.Functor.Properties
+open import Categories.Morphism
+open import Categories.Morphism.Displayed
 
 module _
   {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
@@ -24,6 +26,17 @@ module _
   open Definitions
   open Definitions′
 
+  [_]-resp-∘′ : ∀ {X Y Z} {f : Y C.⇒ Z} {g : X C.⇒ Y} {h : X C.⇒ Z} {f∘g≈h : f C.∘ g C.≈ h}
+                  {X′  : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
+                  {f′ : Y′ C′.⇒[ f ] Z′} {g′ : X′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′}
+                → f′ C′.∘′ g′ C′.≈[ f∘g≈h ] h′
+                → F′.₁′ f′ D′.∘′ F′.₁′ g′ D′.≈[ [ F ]-resp-∘ f∘g≈h ] F′.₁′ h′
+  [_]-resp-∘′ {f′ = f′} {g′ = g′} {h′ = h′} eq = begin′
+    F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈˘[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ (f′ C′.∘′ g′)     ≈[]⟨ F′.F′-resp-≈[] eq ⟩
+    F′.₁′ h′                ∎′
+    where open D′.HomReasoning′
+
   [_]-resp-square′ : ∀ {W X Y Z} {f : W C.⇒ X} {g : W C.⇒ Y} {h : X C.⇒ Z} {i : Y C.⇒ Z} {sq : CommutativeSquare C f g h i}
                        {W′ : C′.Obj[ W ]} {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
                        {f′ : W′ C′.⇒[ f ] X′} {g′ : W′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′} {i′ : Y′ C′.⇒[ i ] Z′}
@@ -36,4 +49,19 @@ module _
     F′.₁′ i′ D′.∘′ F′.₁′ g′ ∎′
     where open D′.HomReasoning′
 
-
+  [_]-resp-DisplayedIso : ∀ {X Y} {f : X C.⇒ Y} {g : Y C.⇒ X} {iso : Iso C f g}
+                            {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {f′ : X′ C′.⇒[ f ] Y′} {g′ : Y′ C′.⇒[ g ] X′}
+                          → DisplayedIso C′ f′ g′ iso → DisplayedIso D′ (F′.₁′ f′) (F′.₁′ g′) ([ F ]-resp-Iso iso)
+  [_]-resp-DisplayedIso {f′ = f′} {g′ = g′} diso = record
+    { isoˡ′ = begin′
+      F′.₁′ g′ D′.∘′ F′.₁′ f′ ≈[]⟨ [ isoˡ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    ; isoʳ′ = begin′
+      F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈[]⟨ [ isoʳ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    }
+    where
+      open DisplayedIso diso
+      open D′.HomReasoning′

src/Categories/Morphism/Displayed.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism B
+
+open Category B
+open Displayed C
+
+private
+  variable
+    X Y : Obj
+    X′ : Obj[ X ]
+    Y′ : Obj[ Y ]
+
+record DisplayedIso {from : X ⇒ Y} {to : Y ⇒ X} (from′ : X′ ⇒[ from ] Y′) (to′ : Y′ ⇒[ to ] X′) (iso : Iso from to) : Set e′ where
+  open Iso iso
+  field
+    isoˡ′ : to′ ∘′ from′ ≈[ isoˡ ] id′
+    isoʳ′ : from′ ∘′ to′ ≈[ isoʳ ] id′

src/Categories/Morphism/Displayed/Properties.agda

@@ -0,0 +1,54 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category.Core
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed.Properties {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism B
+open import Categories.Morphism.Displayed C
+open import Categories.Morphism.Displayed.Reasoning C
+open import Categories.Morphism.Properties B
+
+open Category B
+open Displayed C
+open HomReasoning′
+
+private
+  variable
+    X Y : Obj
+    X′ Y′ Z′ : Obj[ X ]
+    f g h i : X ⇒ Y
+    h′ i′ : X′ ⇒[ f ] Y′
+
+module _ {f′ : X′ ⇒[ f ] Y′} {g′ : Y′ ⇒[ g ] X′} {iso : Iso f g} (diso : DisplayedIso f′ g′ iso) where
+
+  open DisplayedIso diso
+
+  DisplayedIso-resp-≈[] : {f≈h : f ≈ h} {g≈i : g ≈ i} → f′ ≈[ f≈h ] h′ → g′ ≈[ g≈i ] i′ → DisplayedIso h′ i′ (Iso-resp-≈ iso f≈h g≈i)
+  DisplayedIso-resp-≈[] {h′ = h′} {i′ = i′} f′≈h′ g′≈i′ = record
+    { isoˡ′ = begin′
+      i′ ∘′ h′ ≈˘[]⟨ g′≈i′ ⟩∘′⟨ f′≈h′ ⟩
+      g′ ∘′ f′ ≈[]⟨ isoˡ′ ⟩
+      id′      ∎′
+    ; isoʳ′ = begin′
+      h′ ∘′ i′ ≈˘[]⟨ f′≈h′ ⟩∘′⟨ g′≈i′ ⟩
+      f′ ∘′ g′ ≈[]⟨ isoʳ′ ⟩
+      id′      ∎′
+    }
+
+DisplayedIso-∘′ : {f′ : X′ ⇒[ f ] Y′} {g′ : Y′ ⇒[ g ] X′} {h′ : Y′ ⇒[ h ] Z′} {i′ : Z′ ⇒[ i ] Y′}
+                → {f≅g : Iso f g} {h≅i : Iso h i}
+                → DisplayedIso f′ g′ f≅g → DisplayedIso h′ i′ h≅i
+                → DisplayedIso (h′ ∘′ f′) (g′ ∘′ i′) (Iso-∘ f≅g h≅i)
+DisplayedIso-∘′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} f′≅g′ h′≅i′ = record
+  { isoˡ′ = begin′
+    (g′ ∘′ i′) ∘′ (h′ ∘′ f′) ≈[]⟨ cancelInner′ (isoˡ′ h′≅i′) ⟩
+    g′ ∘′ f′                 ≈[]⟨ isoˡ′ f′≅g′ ⟩
+    id′                      ∎′
+  ; isoʳ′ = begin′
+    (h′ ∘′ f′) ∘′ (g′ ∘′ i′) ≈[]⟨ cancelInner′ (isoʳ′ f′≅g′) ⟩
+    h′ ∘′ i′                 ≈[]⟨ isoʳ′ h′≅i′ ⟩
+    id′                      ∎′
+  }
+  where open DisplayedIso

src/Categories/Morphism/Displayed/Reasoning.agda

@@ -86,3 +86,22 @@ sym-glue′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} {j′ = j′
   h′ ∘′ (f′ ∘′ j′) ≈[]⟨ pullˡ′ sq₁′ ⟩
   (i′ ∘′ g′) ∘′ j′ ≈[]⟨ extendˡ′ sq₂′ ⟩
   (i′ ∘′ l′) ∘′ k′ ∎′
+
+module Cancellers′ {inv : h ∘ i ≈ id} (inv′ : h′ ∘′ i′ ≈[ inv ] id′) where
+
+  cancelʳ′ : (f′ ∘′ h′) ∘′ i′ ≈[ cancelʳ inv ] f′
+  cancelʳ′ {f′ = f′} = begin′
+    (f′ ∘′ h′) ∘′ i′ ≈[]⟨ pullʳ′ inv′ ⟩
+    f′ ∘′ id′        ≈[]⟨ identityʳ′ ⟩
+    f′               ∎′
+
+  cancelˡ′ : h′ ∘′ (i′ ∘′ f′) ≈[ cancelˡ inv ] f′
+  cancelˡ′ {f′ = f′} = begin′
+    h′ ∘′ (i′ ∘′ f′) ≈[]⟨ pullˡ′ inv′ ⟩
+    id′ ∘′ f′        ≈[]⟨ identityˡ′ ⟩
+    f′               ∎′
+
+  cancelInner′ : (f′ ∘′ h′) ∘′ (i′ ∘′ g′) ≈[ cancelInner inv ] f′ ∘′ g′
+  cancelInner′ = pullˡ′ cancelʳ′
+
+open Cancellers′ public

src/Categories/NaturalTransformation/Displayed.agda

@@ -7,16 +7,17 @@ open import Level
 open import Categories.Category.Core
 open import Categories.Category.Displayed
 open import Categories.Functor hiding (id)
-open import Categories.Functor.Displayed hiding (id′)
+open import Categories.Functor.Displayed renaming (id′ to idF′)
 open import Categories.Functor.Displayed.Properties
-import Categories.Morphism.Displayed.Reasoning as DPR
+import Categories.Morphism.Displayed.Reasoning as DMR
 open import Categories.NaturalTransformation
 
 private
   variable
     o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level
     C D E : Category o ℓ e
     F G H : Functor C D
+    C′ D′ : Displayed C o ℓ e
 
 record DisplayedNaturalTransformation
   {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D}
@@ -52,7 +53,7 @@ id′ {D′ = D′} = record
   }
   where
     module D′ = Displayed D′
-    open DPR D′
+    open DMR D′
 
 _∘′ᵥ_ : ∀ {S : NaturalTransformation G H} {T : NaturalTransformation F G}
           {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴}
@@ -68,7 +69,7 @@ _∘′ᵥ_ {D′ = D′} S′ T′ = record
     module D′ = Displayed D′
     module S′ = DisplayedNaturalTransformation S′
     module T′ = DisplayedNaturalTransformation T′
-    open DPR D′
+    open DMR D′
 
 _∘′ₕ_ : ∀ {F G : Functor C D} {H I : Functor D E}
           {S : NaturalTransformation H I} {T : NaturalTransformation F G}
@@ -82,11 +83,41 @@ _∘′ₕ_ {E′ = E′} {F′ = F′} {I′ = I′} S′ T′ = record
   { η′ = λ X → I′.₁′ (T′.η′ X) E′.∘′ S′.η′ (F′.₀′ X)
   ; commute′ = λ f → glue′ ([ I′ ]-resp-square′ (T′.commute′ f)) (S′.commute′ (F′.₁′ f))
   ; sym-commute′ = λ f → sym-glue′ ([ I′ ]-resp-square′ (T′.sym-commute′ f)) (S′.sym-commute′ (F′.₁′ f)) 
-  }
+  } 
   where
     module S′ = DisplayedNaturalTransformation S′
     module T′ = DisplayedNaturalTransformation T′
     module E′ = Displayed E′
     module F′ = DisplayedFunctor F′
     module I′ = DisplayedFunctor I′
-    open DPR E′
+    open DMR E′
+
+id′∘id′⇒id′ : ∀ {C′ : Displayed C o ℓ e} → DisplayedNaturalTransformation {C′ = C′} {D′ = C′} (idF′ ∘F′ idF′) idF′ id∘id⇒id
+id′∘id′⇒id′ {C′ = C′} = record
+  { η′ = λ _ → Displayed.id′ C′
+  ; commute′ = λ _ → DMR.id′-comm-sym C′
+  ; sym-commute′ = λ _ → DMR.id′-comm C′
+  }
+
+id′⇒id′∘id′ : ∀ {C′ : Displayed C o ℓ e} → DisplayedNaturalTransformation {C′ = C′} {D′ = C′} idF′ (idF′ ∘F′ idF′) id⇒id∘id
+id′⇒id′∘id′ {C′ = C′} = record
+  { η′ = λ _ → Displayed.id′ C′
+  ; commute′ = λ _ → DMR.id′-comm-sym C′
+  ; sym-commute′ = λ _ → DMR.id′-comm C′
+  }
+
+module _ {F′ : DisplayedFunctor C′ D′ F} where
+  open DMR D′
+  private module D′ = Displayed D′
+
+  F′⇒F′∘id′ : DisplayedNaturalTransformation F′ (F′ ∘F′ idF′) F⇒F∘id
+  F′⇒F′∘id′ = record { η′ = λ _ → D′.id′; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  F′⇒id′∘F′ : DisplayedNaturalTransformation F′ (idF′ ∘F′ F′) F⇒id∘F
+  F′⇒id′∘F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  F′∘id′⇒F′ : DisplayedNaturalTransformation (F′ ∘F′ idF′) F′ F∘id⇒F
+  F′∘id′⇒F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }
+
+  id′∘F′⇒F′ : DisplayedNaturalTransformation (idF′ ∘F′ F′) F′ id∘F⇒F
+  id′∘F′⇒F′ = record { η′ = λ _ → D′.id′ ; commute′ = λ _ → id′-comm-sym ; sym-commute′ = λ _ → id′-comm }

src/Categories/NaturalTransformation/NaturalIsomorphism.agda

@@ -245,10 +245,10 @@ module _ (F : Functor B C) (G : Functor C D) (H : Functor D E) where
   private
     -- components of α
     assocʳ : NaturalTransformation ((H ∘F G) ∘F F) (H ∘F (G ∘F F))
-    assocʳ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E  }
+    assocʳ = record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E ; sym-commute = λ _ → MR.id-comm E }
 
     assocˡ : NaturalTransformation (H ∘F (G ∘F F)) ((H ∘F G) ∘F F)
-    assocˡ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E }
+    assocˡ = record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E ; sym-commute = λ _ → MR.id-comm E }
 
   associator : (H ∘F G) ∘F F ≃ H ∘F (G ∘F F)
   associator = record { F⇒G = assocʳ ; F⇐G = assocˡ ; iso = iso-id-id }