Displayed Bicategories

src/Cat/Bi/Base.lagda.md

@@ -190,6 +190,8 @@ naturally isomorphic to the identity functor.
         (compose-assocˡ {H = Hom} compose)
         (compose-assocʳ {H = Hom} compose)
 
+  module unitor-l {a} {b} = Cr._≅_ _ (unitor-l {a} {b})
+  module unitor-r {a} {b} = Cr._≅_ _ (unitor-r {a} {b})
   module associator {a} {b} {c} {d} = Cr._≅_ _ (associator {a} {b} {c} {d})
 ```
 

src/Cat/Bi/Instances/Displayed.lagda.md

@@ -106,8 +106,8 @@ as in the nondisplayed case.
       module D' {x} = Cat (Fibre D x) using (_∘_ ; idl ; idr ; elimr ; pushl ; introl)
 
       ni : make-natural-iso {D = Vf _ _} _ _
-      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) }
-      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] D) }
+      ni .eta _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] D }
+      ni .inv _ = record { η' = λ x' → D.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] D }
       ni .eta∘inv _ = ext λ _ → D'.idl _
       ni .inv∘eta _ = ext λ _ → D'.idl _
       ni .natural x y f = ext λ _ → D'.idr _ ∙∙ D'.pushl (F-∘↓ (y .fst)) ∙∙ D'.introl refl
@@ -127,8 +127,8 @@ the structural isomorphisms being identities.
   Disp[] .unitor-l {B = B} = to-natural-iso ni where
     module B = Displayed B
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B }
     ni .eta∘inv _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .inv∘eta _ = ext λ _ → Cat.idl (Fibre B _) _
     ni .natural x y f = ext λ _ → Cat.elimr (Fibre B _) refl ∙ Cat.id-comm (Fibre B _)
@@ -137,8 +137,8 @@ the structural isomorphisms being identities.
     module B' {x} = Cat (Fibre B x) using (_∘_ ; idl ; elimr)
 
     ni : make-natural-iso {D = Vf _ _} _ _
-    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) }
-    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → to-pathp (Disp.id-comm[] B) }
+    ni .eta _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B }
+    ni .inv _ = record { η' = λ x' → B.id' ; is-natural' = λ x y f → Disp.id-comm-sym[] B }
     ni .eta∘inv _ = ext λ _ → B'.idl _
     ni .inv∘eta _ = ext λ _ → B'.idl _
     ni .natural x y f = ext λ _ → B'.elimr refl ∙ ap₂ B'._∘_ (y .F-id') refl

src/Cat/Displayed/Functor.lagda.md

@@ -123,8 +123,26 @@ module
     → (q1 : ∀ {x y x' y'} {f : A.Hom x y} → (f' : ℰ.Hom[ f ] x' y')
             → PathP (λ i → ℱ.Hom[ p i .F₁ f ] (q0 x' i) (q0 y' i)) (F' .F₁' f') (G' .F₁' f'))
     → PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G'
-  Displayed-functor-pathp {F = F} {G = G} {F' = F'} {G' = G'} p q0 q1 =
-    injectiveP (λ _ → eqv) ((λ i x' → q0 x' i) ,ₚ (λ i f' → q1 f' i) ,ₚ prop!)
+  Displayed-functor-pathp {F = F} {F' = F'} {G' = G'} p q0 q1 = dfn where
+    -- We need to define this directly to get nice definitional behavior on the projections
+    dfn : PathP (λ i → Displayed-functor (p i) ℰ ℱ) F' G'
+    dfn i .F₀' x' = q0 x' i
+    dfn i .F₁' f' = q1 f' i
+    dfn i .F-id' {x' = x'} j = 
+      is-set→squarep (λ i j → ℱ.Hom[ F-id (p i) j ]-set (q0 x' i) (q0 x' i)) 
+        (q1 ℰ.id') (F-id' F') (F-id' G') (λ _ → ℱ.id') i j
+    dfn i .F-∘' {f = f} {g = g} {a' = a'} {c' = c'} {f' = f'} {g' = g'} j = 
+      is-set→squarep (λ i j → ℱ.Hom[ F-∘ (p i) f g j ]-set (q0 a' i) (q0 c' i))
+        (q1 (f' ℰ.∘' g')) (F-∘' F') (F-∘' G') (λ k → q1 f' k ℱ.∘' q1 g' k) i j
+
+  Displayed-functor-is-set : {F : Functor A B} → (∀ x → is-set ℱ.Ob[ x ]) → is-set (Displayed-functor F ℰ ℱ)
+  Displayed-functor-is-set fibre-set = Iso→is-hlevel! 2 eqv where instance
+    ℱOb[] : ∀ {x} → H-Level (ℱ.Ob[ x ]) 2
+    ℱOb[] = hlevel-instance (fibre-set _)
+
+  instance
+    Funlike-displayed-functor : ∀ {F : Functor A B} {x} → Funlike (Displayed-functor F ℰ ℱ) (⌞ ℰ.Ob[ x ] ⌟) λ _ → ⌞ ℱ.Ob[ F .F₀ x ] ⌟
+    Funlike-displayed-functor = record { _·_ = λ F x → F .F₀' x }
 ```
 -->
 
@@ -395,6 +413,9 @@ module
             → PathP (λ i → ℱ.Hom[ f ] (p0 x' i) (p0 y' i)) (F .F₁' f') (G .F₁' f'))
     → F ≡ G
   Vertical-functor-path = Displayed-functor-pathp refl
+
+  Vertical-functor-is-set : (∀ x → is-set ℱ.Ob[ x ]) → is-set (Vertical-functor ℰ ℱ)
+  Vertical-functor-is-set fibre-set = Displayed-functor-is-set fibre-set
 ```
 -->
 
@@ -458,6 +479,7 @@ module
     (G' : Displayed-functor G ℰ ℱ)
     : Type lvl
     where
+    constructor NT'
     no-eta-equality
 
     field
@@ -467,6 +489,80 @@ module
         → η' y' ℱ.∘' F' .F₁' f' ℱ.≡[ α .is-natural x y f ] G' .F₁' f' ℱ.∘' η' x'
 ```
 
+<!--
+```agda
+{-# INLINE NT' #-}
+
+unquoteDecl H-Level-=[]=> = declare-record-hlevel 2 H-Level-=[]=> (quote _=[_]=>_)
+
+module _
+  {oa ℓa ob ℓb od ℓd oe ℓe}
+  {A : Precategory oa ℓa} {B : Precategory ob ℓb}
+  {D : Displayed A od ℓd} {E : Displayed B oe ℓe}
+  where
+  private 
+    module A = Precategory A
+    module B = Precategory B
+    module D = Displayed D
+    module E = DR E
+
+  open _=>_
+  open _=[_]=>_
+  open Displayed-functor
+
+  Nat'-pathp : {F₁ F₂ G₁ G₂ : Functor A B} 
+             → {F₁' : Displayed-functor F₁ D E} 
+             → {G₁' : Displayed-functor G₁ D E}
+             → {F₂' : Displayed-functor F₂ D E}
+             → {G₂' : Displayed-functor G₂ D E}
+             → {α : F₁ => G₁} {β : F₂ => G₂}
+             → {α' : F₁' =[ α ]=> G₁'} {β' : F₂' =[ β ]=> G₂'}
+             → (p : F₁ ≡ F₂) (q : G₁ ≡ G₂) 
+             → (r : PathP (λ i → p i => q i) α β)
+             → (p' : PathP (λ i → Displayed-functor (p i) D E) F₁' F₂')
+             → (q' : PathP (λ i → Displayed-functor (q i) D E) G₁' G₂')
+             → (∀ {x} (x' : D.Ob[ x ]) → PathP (λ i → E.Hom[ (r i .η x) ] (p' i .F₀' x') (q' i .F₀' x')) (α' .η' x') (β' .η' x'))
+             → PathP (λ i → (p' i) =[ r i ]=> (q' i)) α' β'
+  Nat'-pathp p q r p' q' w i .η' x' = w x' i
+  Nat'-pathp {α' = α'} {β' = β'} p q r p' q' w i .is-natural' {x = x} {y} {f} x' y' f' j = 
+    is-set→squarep {A = λ i j → E.Hom[ r i .is-natural x y f j ] (F₀' (p' i) x') (F₀' (q' i) y')} (λ _ _ → hlevel 2)
+      (λ i → w y' i E.∘' F₁' (p' i) f') (λ j → is-natural' α' x' y' f' j) (λ j → is-natural' β' x' y' f' j) (λ i → F₁' (q' i) f' E.∘' w x' i) i j
+
+  Nat'-path : {F G : Functor A B} {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+           → {α β : F => G} {α' : F' =[ α ]=> G'} {β' : F' =[ β ]=> G'} 
+           → {p : α ≡ β}
+           → (∀ {x} (x' : D.Ob[ x ]) → α' .η' x' E.≡[ p ηₚ x ] β' .η' x')
+           → PathP (λ i → F' =[ p i ]=> G') α' β'
+  Nat'-path = Nat'-pathp refl refl _ refl refl
+```
+-->
+We can define displayed versions of the indentity natural transformation and 
+composition of natural transformations.
+```agda 
+  idnt' : ∀ {F : Functor A B} {F' : Displayed-functor F D E} → F' =[ idnt ]=> F'
+  idnt' .η' x' = E.id'
+  idnt' .is-natural' x' y' f' = E.id-comm-sym[]
+
+  _∘nt'_ : ∀ {F G H : Functor A B} 
+          → {F' : Displayed-functor F D E} 
+          → {G' : Displayed-functor G D E} 
+          → {H' : Displayed-functor H D E} 
+          → {β : G => H} {α : F => G}
+          → G' =[ β ]=> H' → F' =[ α ]=> G' → F' =[ β ∘nt α ]=> H'
+  (β' ∘nt' α') .η' x' = β' .η' x' E.∘' α' .η' x'
+  _∘nt'_ {F' = F'} {G'} {H'} β' α' .is-natural' x' y' f' = E.cast[] $ 
+    (β'.η' y' E.∘' α'.η' y') E.∘' F'.F₁' f'  E.≡[]⟨ E.pullr[] _ (α'.is-natural' _ _ _) ⟩
+      β'.η' y' E.∘' G'.F₁' f' E.∘' α'.η' x'  E.≡[]⟨ E.pulll[] _ (β'.is-natural' _ _ _) ⟩
+    (H'.F₁' f' E.∘' β'.η' x') E.∘' α'.η' x'  E.≡[]˘⟨ E.assoc' _ _ _ ⟩
+      H'.F₁' f' E.∘' β'.η' x' E.∘' α'.η' x'   ∎
+    where
+      module β' = _=[_]=>_ β'
+      module α' = _=[_]=>_ α'
+      module F' = Displayed-functor F'
+      module G' = Displayed-functor G'
+      module H' = Displayed-functor H'
+```
+
 ::: {.definition #vertical-natural-transformation}
 Let $F, G : \cE \to \cF$ be two vertical functors. A displayed natural
 transformation between $F$ and $G$ is called a **vertical natural
@@ -522,14 +618,11 @@ module _
     Extensional-=>↓ {F' = F'} {G' = G'}  ⦃ e ⦄  = injection→extensional! {f = _=>↓_.η'}
       (λ p → Iso.injective eqv (Σ-prop-path! p)) e
 
-    H-Level-=>↓ : ∀ {F' G'} {n} → H-Level (F' =>↓ G') (2 + n)
-    H-Level-=>↓ = basic-instance 2 (Iso→is-hlevel 2 eqv (hlevel 2))
-
   open _=>↓_
 
   idnt↓ : ∀ {F} → F =>↓ F
   idnt↓ .η' x' = ℱ.id'
-  idnt↓ .is-natural' x' y' f' = to-pathp (DR.id-comm[] ℱ)
+  idnt↓ .is-natural' x' y' f' = DR.id-comm-sym[] ℱ
 
   _∘nt↓_ : ∀ {F G H} → G =>↓ H → F =>↓ G → F =>↓ H
   (f ∘nt↓ g) .η' x' = f .η' _ ℱ↓.∘ g .η' x'

src/Cat/Displayed/Functor/Naturality.lagda.md

@@ -0,0 +1,99 @@
+<!--
+```agda
+open import Cat.Displayed.Instances.DisplayedFunctor
+open import Cat.Functor.Naturality
+open import Cat.Displayed.Functor
+open import Cat.Displayed.Base
+open import Cat.Morphism
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning as DR
+import Cat.Displayed.Morphism as DM
+```
+-->
+```agda
+module Cat.Displayed.Functor.Naturality where
+```
+# Natural isomorhisms of displayed functors
+
+We define displayed versions of our functor naturality tech.
+
+<!--
+```agda
+module _ 
+  {ob ℓb oc ℓc od ℓd oe ℓe} 
+  {B : Precategory ob ℓb} {C : Precategory oc ℓc}
+  {D : Displayed B od ℓd} {E : Displayed C oe ℓe}
+  where
+  private
+    module B = Precategory B
+    module C = Precategory C
+    module DE where
+      open DR Disp[ D , E ] public 
+      open DM Disp[ D , E ] public
+    module D = DR D public
+    module E = DR E public
+
+  open Functor
+  open _=>_
+  open Displayed-functor
+  open _=[_]=>_
+```
+-->
+```agda
+
+  _≅[_]ⁿ_ : {F G : Functor B C} → Displayed-functor F D E → F ≅ⁿ G → Displayed-functor G D E → Type _
+  F ≅[ i ]ⁿ G = F DE.≅[ i ] G
+
+
+  is-natural-transformation' 
+    : {F G : Functor B C} (F' : Displayed-functor F D E) (G' : Displayed-functor G D E)
+    → (α : F => G)
+    → (η' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ α .η x ] (F' .F₀' x') (G' .F₀' x'))
+    → Type _
+  is-natural-transformation' F' G' α η' = 
+    ∀ {x y f} (x' : D.Ob[ x ]) (y' : D.Ob[ y ]) (f' : D.Hom[ f ] x' y')
+        → η' y' E.∘' F' .F₁' f' E.≡[ α .is-natural x y f ] G' .F₁' f' E.∘' η' x'
+
+  inverse-is-natural'
+    : ∀ {F G : Functor B C} (iso : F ≅ⁿ G) {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+    → (α' : F' =[ iso .to ]=> G')
+    → (β' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .from .η x ] (G' .F₀' x') (F' .F₀' x'))
+    → (∀ {x} (x' : D.Ob[ x ]) → α' .η' x' E.∘' β' x' E.≡[ iso .invl ηₚ x ] E.id')
+    → (∀ {x} (x' : D.Ob[ x ]) → β' x' E.∘' α' .η' x' E.≡[ iso .invr ηₚ x ] E.id')
+    → is-natural-transformation' G' F' (iso .from) β'
+  inverse-is-natural' i {F'} {G'} α' β' invl' invr' x' y' f' = E.cast[] $ 
+    β' y' E.∘' G' .F₁' f'                           E.≡[]⟨ E.refl⟩∘'⟨ E.intror[] _ (invl' x') ⟩ 
+    β' y' E.∘' G' .F₁' f' E.∘' α' .η' x' E.∘' β' x' E.≡[]⟨ E.refl⟩∘'⟨ E.extendl[] _ (symP (α' .is-natural' _ _ _)) ⟩
+    β' y' E.∘' α' .η' y' E.∘' F' .F₁' f' E.∘' β' x' E.≡[]⟨ E.cancell[] _ (invr' _) ⟩
+    F' .F₁' f' E.∘' β' x'                           ∎
+
+
+  record make-natural-iso[_] {F G : Functor B C} (iso : F ≅ⁿ G) (F' : Displayed-functor F D E) (G' : Displayed-functor G D E) : Type (ob ⊔ ℓb ⊔ od ⊔ ℓd ⊔ ℓe) where
+    no-eta-equality
+    field
+      eta' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .to .η x   ] (F' .F₀' x') (G' .F₀' x')
+      inv' : ∀ {x} (x' : D.Ob[ x ]) → E.Hom[ iso .from .η x ] (G' .F₀' x') (F' .F₀' x')
+      eta∘inv' : ∀ {x} (x' : D.Ob[ x ]) → eta' x' E.∘' inv' x' E.≡[ (λ i → iso .invl i .η x) ] E.id'
+      inv∘eta' : ∀ {x} (x' : D.Ob[ x ]) → inv' x' E.∘' eta' x' E.≡[ (λ i → iso .invr i .η x) ] E.id'
+      natural' : ∀ {x y} x' y' {f : B.Hom x y} (f' : D.Hom[ f ] x' y')
+               →  eta' y' E.∘' F' .F₁' f' E.≡[ (λ i → iso .to .is-natural x y f i) ]  G' .F₁' f' E.∘' eta' x'
+
+
+  open make-natural-iso[_]
+
+  to-natural-iso' : {F G : Functor B C} {iso : F ≅ⁿ G} {F' : Displayed-functor F D E} {G' : Displayed-functor G D E}
+                  → make-natural-iso[ iso ] F' G' → F' ≅[ iso ]ⁿ G'
+  to-natural-iso' {iso = i} mk = 
+    let to' = record { η' = mk .eta' ; is-natural' = λ {x} {y} {f} x' y' → mk .natural' x' y' } in
+    record 
+      { to' = to'
+      ; from' = record { η' = mk .inv' ; is-natural' = inverse-is-natural' i to' (mk .inv') (mk .eta∘inv') (mk .inv∘eta') } 
+      ; inverses' = record { invl' = Nat'-path (mk .eta∘inv') ; invr' = Nat'-path (mk .inv∘eta') } 
+      }
+```
+<!--
+```agda
+  {-# INLINE to-natural-iso' #-}
+```
+-->