Displayed functor cleanup

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

@@ -122,7 +122,7 @@ the structural isomorphisms being identities.
   Disp[] : Prebicategory (o ⊔ ℓ ⊔ lsuc (o' ⊔ ℓ')) (o ⊔ ℓ ⊔ o' ⊔ ℓ') (o ⊔ ℓ ⊔ o' ⊔ ℓ')
   Disp[] .Ob = Displayed B o' ℓ'
   Disp[] .Hom = Vertical-functors
-  Disp[] .id = Displayed-functor→Vertical-functor Id'
+  Disp[] .id = Id'
   Disp[] .compose = ∘V-functor
   Disp[] .unitor-l {B = B} = to-natural-iso ni where
     module B = Displayed B

src/Cat/Displayed/Adjoint.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+open import Cat.Functor.Adjoint.Compose
 open import Cat.Functor.Equivalence
 open import Cat.Displayed.Functor
 open import Cat.Instances.Functor
@@ -64,9 +65,9 @@ module _
 
 ```agda
   record _⊣[_]_
-    (L' : Displayed-functor ℰ ℱ L)
+    (L' : Displayed-functor L ℰ ℱ)
     (adj : L ⊣ R)
-    (R' : Displayed-functor ℱ ℰ R )
+    (R' : Displayed-functor R ℱ ℰ)
     : Type lvl where
     no-eta-equality
     open _⊣_ adj
@@ -91,6 +92,11 @@ that a pair of vertical [[fibred functors]] $L : \cE \to \cF$, $R : \cF
 \to cF$ are **fibred adjoint functors** if they are displayed adjoint
 functors, and the unit and counit are vertical natural transformations.
 
+Unlike vertical functors and vertical natural transformations, we have to
+define fibred adjunctions as a separate type: general displayed adjunctions
+use composition of displayed functors for the unit and counit, whereas fibred
+adjunctions use vertical composition instead.
+
 <!--
 ```agda
 module _
@@ -103,7 +109,7 @@ module _
     open Precategory B
     module ℰ = Displayed ℰ
     module ℱ = Displayed ℱ
-    open Vertical-fibred-functor
+    open Vertical-functor
 
     lvl : Level
     lvl = ob ⊔ ℓb ⊔ oe ⊔ ℓe ⊔ of ⊔ ℓf
@@ -114,13 +120,13 @@ module _
 
 ```agda
   record _⊣↓_
-    (L : Vertical-fibred-functor ℰ ℱ)
-    (R : Vertical-fibred-functor ℱ ℰ)
+    (L : Vertical-functor ℰ ℱ)
+    (R : Vertical-functor ℱ ℰ)
     : Type lvl where
     no-eta-equality
     field
-      unit' : IdVf =>f↓ R ∘Vf L
-      counit' : L ∘Vf R =>f↓ IdVf
+      unit' : Id' =>↓ R ∘V L
+      counit' : L ∘V R =>↓ Id'
 
     module unit' = _=>↓_ unit'
     module counit' = _=>↓_ counit' renaming (η' to ε')

src/Cat/Displayed/Cartesian/Discrete.lagda.md

@@ -410,7 +410,7 @@ map $a'' \to_f b$ --- so we can take the canonical $f' : a' \to_f b$ and
 transport it over the given $a'' = a'$.
 
 ```agda
-    pieces : Displayed-functor (∫ B (discrete→presheaf P p-disc)) P Id
+    pieces : Vertical-functor (∫ B (discrete→presheaf P p-disc)) P
     pieces .F₀' x = x
     pieces .F₁' {f = f} {a'} {b'} x =
       subst (λ e → Hom[ f ] e b') x $ cart-lift f b' .centre .snd

src/Cat/Displayed/Cartesian/Right.lagda.md

@@ -22,13 +22,19 @@ module Cat.Displayed.Cartesian.Right
   {ℬ : Precategory o ℓ}
   (ℰ : Displayed ℬ o' ℓ')
   where
+```
+
+<!--
+```agda
 
 open Cat.Reasoning ℬ
 open Displayed ℰ
 open Cat.Displayed.Cartesian ℰ
 open Cat.Displayed.Morphism ℰ
 open Cat.Displayed.Reasoning ℰ
+open is-fibred-functor
 ```
+-->
 
 # Right fibrations
 
@@ -137,13 +143,12 @@ functor+right-fibration→fibred
   → {ℱ : Displayed 𝒟 o₂' ℓ₂'}
   → {F : Functor 𝒟 ℬ}
   → Right-fibration
-  → (F' : Displayed-functor ℱ ℰ F)
-  → Fibred-functor ℱ ℰ F
-functor+right-fibration→fibred rfib F' .Fibred-functor.disp =
-  F'
-functor+right-fibration→fibred rfib F' .Fibred-functor.F-cartesian f' _ =
+  → (F' : Displayed-functor F ℱ ℰ)
+  → is-fibred-functor F'
+functor+right-fibration→fibred rfib F' .F-cartesian {f' = f'} _ =
   Right-fibration.cartesian rfib (F₁' f')
-  where open Displayed-functor F'
+  where
+    open Displayed-functor F'
 ```
 
 Specifically, this implies that all displayed functors into a discrete
@@ -157,8 +162,8 @@ functor+discrete→fibred
   → {ℱ : Displayed 𝒟 o₂' ℓ₂'}
   → {F : Functor 𝒟 ℬ}
   → is-discrete-cartesian-fibration ℰ
-  → (F' : Displayed-functor ℱ ℰ F)
-  → Fibred-functor ℱ ℰ F
+  → (F' : Displayed-functor F ℱ ℰ)
+  → is-fibred-functor F'
 functor+discrete→fibred disc F' =
   functor+right-fibration→fibred (discrete→right-fibration disc) F'
 ```

src/Cat/Displayed/Composition.lagda.md

@@ -68,7 +68,7 @@ that projects out the data of $\cE$ from the composite.
 πᵈ : ∀ {o ℓ o' ℓ' o'' ℓ''}
     → {ℬ : Precategory o ℓ}
     → {ℰ : Displayed ℬ o' ℓ'} {ℱ : Displayed (∫ ℰ) o'' ℓ''}
-    → Displayed-functor (ℰ D∘ ℱ) ℰ Id
+    → Displayed-functor Id (ℰ D∘ ℱ) ℰ
 πᵈ .Displayed-functor.F₀' = fst
 πᵈ .Displayed-functor.F₁' = fst
 πᵈ .Displayed-functor.F-id' = refl

src/Cat/Displayed/Comprehension.lagda.md

@@ -111,8 +111,11 @@ We call such a [[fibred functor]] a **comprehension structure** on $\cE$[^1].
 but this is a bit of a misnomer, as they are structures on fibrations!
 
 ```agda
-Comprehension : Type _
-Comprehension = Vertical-fibred-functor E (Slices B)
+record Comprehension-structure : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
+  no-eta-equality
+  field
+    Comprehend : Vertical-functor E (Slices B)
+    Comprehend-is-fibred : is-fibred-functor Comprehend
 ```
 
 Now, let's make all that earlier intuition formal. Let $\cE$ be a fibration,
@@ -121,17 +124,22 @@ context extensions, along with their associated projections.
 
 
 ```agda
-module Comprehension (fib : Cartesian-fibration E) (P : Comprehension) where opaque
-  open Vertical-fibred-functor P
-  open Cartesian-fibration E fib
+module Comprehension
+  (E-fib : Cartesian-fibration E)
+  (P : Comprehension-structure)
+  where opaque
+  open Comprehension-structure P
+  open is-fibred-functor Comprehend-is-fibred
+  open Vertical-functor Comprehend
+  open Cartesian-fibration E E-fib
 
   _⨾_ : ∀ Γ → Ob[ Γ ] → Ob
   Γ ⨾ x = F₀' x .domain
 
   infixl 5 _⨾_
 
   _[_] : ∀ {Γ Δ} → Ob[ Δ ] → Hom Γ Δ → Ob[ Γ ]
-  x [ σ ] =  base-change E fib σ .F₀ x
+  x [ σ ] = σ ^* x
 
   πᶜ : ∀ {Γ x} → Hom (Γ ⨾ x) Γ
   πᶜ {x = x} = F₀' x .map
@@ -177,7 +185,7 @@ Crucially, when $f$ is cartesian, then the above square is a pullback.
     : ∀ {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
     → is-cartesian E σ f
     → is-pullback B πᶜ σ (σ ⨾ˢ f) πᶜ
-  sub-pullback {f = f} cart = cartesian→pullback B (F-cartesian f cart)
+  sub-pullback {f = f} cart = cartesian→pullback B (F-cartesian cart)
 
   module sub-pullback
     {Γ Δ x y} {σ : Hom Γ Δ} {f : Hom[ σ ] x y}
@@ -429,7 +437,7 @@ comonads.
 ```agda
 Comprehension→comonad
   : Cartesian-fibration E
-  → Comprehension
+  → Comprehension-structure
   → Comprehension-comonad
 Comprehension→comonad fib P = comp-comonad where
   open Cartesian-fibration E fib
@@ -495,7 +503,7 @@ We also show that comprehension comonads yield comprehension structures.
 Comonad→comprehension
   : Cartesian-fibration E
   → Comprehension-comonad
-  → Comprehension
+  → Comprehension-structure
 ```
 
 We begin by constructing a [vertical functor] $\cE \to B^{\to}$ that maps
@@ -507,6 +515,8 @@ $\eps : W(\Gamma, X) \to (\Gamma, X)$.
 ```agda
 Comonad→comprehension fib comp-comonad = comprehension where
   open Comprehension-comonad comp-comonad
+  open Comprehension-structure
+  open is-fibred-functor
   open Vertical-functor
   open is-pullback
 
@@ -527,14 +537,14 @@ square in $\cB$. As the comonad is a comprehension comonad, counit is
 cartesian, which finishes off the proof.
 
 ```agda
-  fibred : is-vertical-fibred vert
-  fibred {f = σ} f cart =
+  fibred : is-fibred-functor vert
+  fibred .F-cartesian {f = σ} {f' = f'} cart =
     pullback→cartesian B $
     cartesian+total-pullback→pullback E fib
       counit-cartesian counit-cartesian
       (cartesian-pullback cart)
 
-  comprehension : Comprehension
-  comprehension .Vertical-fibred-functor.vert = vert
-  comprehension .Vertical-fibred-functor.F-cartesian = fibred
+  comprehension : Comprehension-structure
+  comprehension .Comprehend = vert
+  comprehension .Comprehend-is-fibred = fibred
 ```

src/Cat/Displayed/Comprehension/Coproduct.lagda.md

@@ -19,7 +19,7 @@ module Cat.Displayed.Comprehension.Coproduct
   {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
   {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
   (D-fib : Cartesian-fibration D) (E-fib : Cartesian-fibration E)
-  (P : Comprehension E)
+  (P : Comprehension-structure E)
   where
 ```
 

src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md

@@ -54,7 +54,7 @@ module _
   {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
   {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
   {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
-  (P : Comprehension D) {Q : Comprehension E}
+  (P : Comprehension-structure D) {Q : Comprehension-structure E}
   (coprods : has-comprehension-coproducts D-fib E-fib Q)
   where
   private
@@ -122,7 +122,7 @@ module strong-comprehension-coproducts
   {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
   {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
   {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
-  (P : Comprehension D) {Q : Comprehension E}
+  (P : Comprehension-structure D) {Q : Comprehension-structure E}
   (coprods : has-comprehension-coproducts D-fib E-fib Q)
   (strong : strong-comprehension-coproducts P coprods)
   where

src/Cat/Displayed/Comprehension/Coproduct/VeryStrong.lagda.md

@@ -45,7 +45,7 @@ module _
   {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
   {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
   {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
-  (P : Comprehension D) {Q : Comprehension E}
+  (P : Comprehension-structure D) {Q : Comprehension-structure E}
   (coprods : has-comprehension-coproducts D-fib E-fib Q)
   where
   private
@@ -71,7 +71,7 @@ module very-strong-comprehension-coproducts
   {ob ℓb od ℓd oe ℓe} {B : Precategory ob ℓb}
   {D : Displayed B od ℓd} {E : Displayed B oe ℓe}
   {D-fib : Cartesian-fibration D} {E-fib : Cartesian-fibration E}
-  (P : Comprehension D) {Q : Comprehension E}
+  (P : Comprehension-structure D) {Q : Comprehension-structure E}
   (coprods : has-comprehension-coproducts D-fib E-fib Q)
   (vstrong : very-strong-comprehension-coproducts P coprods)
   where
@@ -162,7 +162,7 @@ module _
   {ob ℓb oe ℓe} {B : Precategory ob ℓb}
   {E : Displayed B oe ℓe}
   {E-fib : Cartesian-fibration E}
-  {P : Comprehension E}
+  {P : Comprehension-structure E}
   (coprods : has-comprehension-coproducts E-fib E-fib P)
   where
 ```