Discrete cocartesian fibrations

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

@@ -14,7 +14,9 @@ open import Cat.Displayed.Base
 open import Cat.Displayed.Path
 open import Cat.Prelude
 
+import Cat.Displayed.Reasoning
 import Cat.Displayed.Morphism
+import Cat.Reasoning
 ```
 -->
 
@@ -30,17 +32,18 @@ open is-cartesian
 ```
 -->
 
-# Discrete fibrations
+# Discrete cartesian fibrations
 
-A **discrete fibration** is a [[displayed category]] whose [[fibre
-categories]] are all _discrete categories_: thin, univalent groupoids.
-Since thin, univalent groupoids are sets, a discrete fibration over
-$\cB$ is an alternate way of encoding a presheaf over $\cB$, i.e., a
-functor $\cB\op\to\Sets$. Here, we identify a purely fibrational
+A **discrete cartesian fibration** or **discrete fibration** is a
+[[displayed category]] whose [[fibre categories]] are all _discrete categories_:
+thin, univalent groupoids. Since thin, univalent groupoids are sets, a
+discrete fibration over $\cB$ is an alternate way of encoding a presheaf
+over $\cB$, i.e., a functor $\cB\op\to\Sets$. Here, we identify a purely fibrational
 property that picks out the discrete fibrations among the displayed
 categories, without talking about the fibres directly.
 
-A discrete fibration is a displayed category such that each type of
+:::{.definition #discrete-cartesian-fibration alias="discrete-fibration"}
+A discrete cartesian fibration is a displayed category such that each type of
 displayed objects is a set, and such that, for each right corner
 
 ~~~{.quiver}
@@ -54,154 +57,257 @@ displayed objects is a set, and such that, for each right corner
 
 there is a contractible space of objects $x'$ over $x$ equipped with
 maps $x' \to_f y'$.
+:::
 
 <!--
-
 ```agda
 module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
   private
-    module B = Precategory B
+    module B = Cat.Reasoning B
     module E = Displayed E
+    open Cat.Displayed.Reasoning E
     open Cat.Displayed.Morphism E
     open Displayed E
 ```
-
 -->
 
 ```agda
-  record Discrete-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
+  record is-discrete-cartesian-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
     field
       fibre-set : ∀ x → is-set E.Ob[ x ]
-      lifts
+      cart-lift
         : ∀ {x y} (f : B.Hom x y) (y' : E.Ob[ y ])
         → is-contr (Σ[ x' ∈ E.Ob[ x ] ] E.Hom[ f ] x' y')
 ```
 
-## Discrete fibrations are cartesian
+We will denote the canonical lift of $f$ to $y'$ as
+$$
+\pi_{f, y'}^{*} : f^{*}(y') \to_{f} y'
+$$
 
-To prove that discrete fibrations deserve the name discrete
-_fibrations_, we prove that any discrete fibration is a [[Cartesian
-fibration]]. By assumption, every right corner has a unique lift, which
-is in particular a lift: we just have to show that the lift is
-Cartesian.
+```agda
+    _^*_ : ∀ {x y} → (f : B.Hom x y) (y' : E.Ob[ y ]) → E.Ob[ x ]
+    f ^* y' = cart-lift f y' .centre .fst
+
+    π* : ∀ {x y} → (f : B.Hom x y) (y' : E.Ob[ y ]) → E.Hom[ f ] (f ^* y') y'
+    π* f y' = cart-lift f y' .centre .snd
+```
+
+## Basic properties of discrete cartesian fibrations
+
+Every hom set of a discrete fibration is a [[proposition]].
 
 ```agda
-  discrete→cartesian : Discrete-fibration → Cartesian-fibration E
-  discrete→cartesian disc = r where
-    open Discrete-fibration disc
-    r : Cartesian-fibration E
-    r .has-lift f y' .x' = lifts f y' .centre .fst
-    r .has-lift f y' .lifting = lifts f y' .centre .snd
+    Hom[]-is-prop : ∀ {x y x' y'} {f : B.Hom x y} → is-prop (Hom[ f ] x' y')
+```
+
+Let $f', f'' : x' \to_{f} y'$ be a pair of morphisms in $\cE$. Both
+$(x', f')$ and $(x' , f'')$ are candidates for lifts of $y'$ along
+$f$, so contractibility of lifts ensures that $(x', f') = (x' , f'')$.
+Moreover, the type of objects in $\cE$ forms a [[set]], so we can
+conclude that $f' = f''$.
+
+```agda
+    Hom[]-is-prop {x' = x'} {y' = y'} {f = f} f' f'' =
+      Σ-inj-set (fibre-set _) $
+      is-contr→is-prop (cart-lift f y') (x' , f') (x' , f'')
+```
+
+We can improve the previous result by noticing that morphisms
+$f' : x' \to_{f} y'$ give rise to proofs that $f^*(y') = x'$.
+
+```agda
+    opaque
+      ^*-lift
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → Hom[ f ] x' y'
+        → f ^* y' ≡ x'
+      ^*-lift {x' = x'} {y' = y'} f f' =
+        ap fst $ cart-lift f y' .paths (x' , f')
+```
+
+We can further improve this to an equivalence between paths
+$f^{*}(y') = x'$ and morphisms $x' \to y'$.
+
+```agda
+      ^*-hom
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → f ^* y' ≡ x'
+        → Hom[ f ] x' y'
+      ^*-hom {x' = x'} {y' = y'} f p =
+        hom[ B.idr f ] $
+          π* f y' ∘' subst (λ y' → Hom[ B.id ] x' y') (sym p) id'
+
+      ^*-hom-is-equiv
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → is-equiv (^*-hom {x' = x'} {y' = y'} f)
+      ^*-hom-is-equiv f =
+        is-iso→is-equiv $
+        iso (^*-lift f)
+          (λ _ → Hom[]-is-prop _ _)
+          (λ _ → fibre-set _ _ _ _ _)
+```
+
+## Functoriality of lifts
+
+The (necessarily unique) choice of lifts in a discrete fibration are
+contravariantly functorial.
+
+```agda
+    ^*-id
+      : ∀ {x} (x' : Ob[ x ])
+      → B.id ^* x' ≡ x'
+
+    ^*-∘
+      : ∀ {x y z}
+      → (f : B.Hom y z) (g : B.Hom x y) (z' : Ob[ z ])
+      → (f B.∘ g) ^* z' ≡ g ^* (f ^* z')
 ```
 
-So suppose we have an open diagram
+The proof here is rather slick. As noted earlier morphisms $x' \to_{f} y'$
+in a discrete fibration correspond to proofs that $f^{*}(y') = x'$, so
+it suffices to construct morphisms $x' \to_{id} x'$ and
+$g^{*}(f^{*}(z')) \to_{f \circ g} z'$, resp. The former is given by
+the identity morphism, and the latter by composition of lifts!
+
+```agda
+    ^*-id x' = ^*-lift B.id id'
+    ^*-∘ f g z' = ^*-lift (f B.∘ g) (π* f z' ∘' π* g (f ^* z'))
+```
+
+## Invertible maps in discrete cartesian fibrations
+
+Let $f : x \to y$ be an [[invertible]] morphism of $\cB$. If $\cE$
+is a discrete fibration, then every morphism displayed over $f$ is
+also invertible.
+
+```agda
+    all-invertible[]
+      : ∀ {x y x' y'} {f : B.Hom x y}
+      → (f' : Hom[ f ] x' y')
+      → (f⁻¹ : B.is-invertible f)
+      → is-invertible[ f⁻¹ ] f'
+```
+
+Let $f : x \to y$ be an invertible morphism, and $f' : x' \to_{f} y'$
+be a morphism lying over $f$. Every hom set of $\cE$ is a proposition,
+so constructing an inverse only requires us to exhibit a map
+$y' \to_{f^{-1}} x'$, which in turn is given by a proof that $f^{-1}(x') = y'$.
+This is easy enough to prove with a bit of algebra.
+
+```agda
+    all-invertible[] {x' = x'} {y' = y'} {f = f} f' f⁻¹ = f'⁻¹ where
+      module f⁻¹ = B.is-invertible f⁻¹
+      open is-invertible[_]
+
+      f'⁻¹ : is-invertible[ f⁻¹ ] f'
+      f'⁻¹ .inv' =
+        ^*-hom f⁻¹.inv $
+          f⁻¹.inv ^* x'         ≡˘⟨ ap (f⁻¹.inv ^*_) (^*-lift f f') ⟩
+          f⁻¹.inv ^* (f ^* y')  ≡˘⟨ ^*-∘ f f⁻¹.inv y' ⟩
+          (f B.∘ f⁻¹.inv) ^* y' ≡⟨ ap (_^* y') f⁻¹.invl ⟩
+          B.id ^* y'            ≡⟨ ^*-id y' ⟩
+          y'                    ∎
+      f'⁻¹ .inverses' .Inverses[_].invl' =
+        is-prop→pathp (λ _ → Hom[]-is-prop) _ _
+      f'⁻¹ .inverses' .Inverses[_].invr' =
+        is-prop→pathp (λ _ → Hom[]-is-prop) _ _
+```
+
+As an easy corollary, we get that all vertical maps in a discrete
+fibration are invertible.
+
+```agda
+    all-invertible↓
+      : ∀ {x x' y'}
+      → (f' : Hom[ B.id {x} ] x' y')
+      → is-invertible↓ f'
+    all-invertible↓ f' = all-invertible[] f' B.id-invertible
+```
+
+
+## Cartesian maps in discrete fibrations
+
+Every morphism in a discrete fibration is [[cartesian|cartesian-morphism]].
+Every hom set in a discrete fibration is propositional, so we just
+need to establish the existence portion of the universal property.
+
+```agda
+    all-cartesian
+      : ∀ {x y x' y'} {f : B.Hom x y}
+      → (f' : Hom[ f ] x' y')
+      → is-cartesian E f f'
+    all-cartesian f' .commutes _ _ = Hom[]-is-prop _ _
+    all-cartesian f' .unique _ _ = Hom[]-is-prop _ _
+```
+
+Suppose we have an open diagram
 
 ~~~{.quiver}
 \[\begin{tikzcd}
   {u'} \\
-  & {a'} && {b'} \\
+  & {x'} && {y'} \\
   u \\
-  & a && {b,}
+  & x && {y,}
   \arrow["{f'}"', from=2-2, to=2-4]
   \arrow["f", from=4-2, to=4-4]
   \arrow[lies over, from=2-2, to=4-2]
   \arrow[lies over, from=2-4, to=4-4]
-  \arrow["m"', from=3-1, to=4-2]
+  \arrow["g"', from=3-1, to=4-2]
   \arrow[lies over, from=1-1, to=3-1]
   \arrow["{h'}", curve={height=-12pt}, from=1-1, to=2-4]
 \end{tikzcd}\]
 ~~~
 
-where $f' : a' \to b'$ is the unique lift of $f$ along $b'$. We need to
-find a map $u' \to_m a'$. Observe that we have a right corner (with
-vertices $u$ and $a'$ over $a$), so that we an object $u_2$ over $u$ and
-map $l : u_2 \to_m a'$. Initially, this looks like it might not help,
-but observe that $u' \xto{h'}_{f \circ m} b'$ and $u_2 \xto{l}_{u} a'
-\xto{f'}_f b'$ are lifts of the right corner with base given by $u \to a
-\to b$, so that by uniqueness, $u2 = u'$: thus, we can use $l$ as our
-map $u' \to a'$.
+where $f' : x' \to_{f} y'$ is the unique lift of $f$ along $y'$. We need to
+find a map $u' \to_{g} x'$. By the usual yoga, it suffices to show that
+$g^{*}(x') = u'$.
 
-```agda
-    r .has-lift f y' .cartesian .universal {u} {u'} m h' =
-      subst (λ x → E.Hom[ m ] x (lifts f y' .centre .fst))
-        (ap fst $ is-contr→is-prop (lifts (f B.∘ m) y')
-          (_ , lifts f y' .centre .snd E.∘' lifts m _ .centre .snd)
-          (u' , h'))
-        (lifts m (lifts f y' .centre .fst) .centre .snd)
-    r .has-lift f y' .cartesian .commutes m h' =
-      Σ-inj-set (fibre-set _) $ is-contr→is-prop (lifts (f B.∘ m) y') _ _
-    r .has-lift f y' .cartesian .unique {u} {u'} {m} m' x =
-      Σ-inj-set (fibre-set u) $ is-contr→is-prop (lifts m _) (u' , m') (u' , _)
-```
-
-## Fibres of discrete fibrations
-
-Let $x$ be an object of $\cB$. Let us ponder the fibre $\cE^*(x)$:
-we know that it is strict, since by assumption there is a _set_ of
-objects over $x$. Let us show also that it is thin: imagine that we have
-two parallel, vertical arrows $f, g : a \to_{\id} b$. These assemble
-into a diagram like
-
-~~~{.quiver}
-\[\begin{tikzcd}
-  {a'} && {b'} && {a'} \\
-  \\
-  x && x && {x\text{,}}
-  \arrow["f", from=1-1, to=1-3]
-  \arrow["g"', from=1-5, to=1-3]
-  \arrow[lies over, from=1-1, to=3-1]
-  \arrow[lies over, from=1-3, to=3-3]
-  \arrow[lies over, from=1-5, to=3-5]
-  \arrow["{\mathrm{id}}"{description}, from=3-1, to=3-3]
-  \arrow["{\mathrm{id}}"{description}, from=3-5, to=3-3]
-  \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3]
-  \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-90}, draw=none, from=1-5, to=3-3]
-\end{tikzcd}\]
-~~~
+Note that we can transform $f' : x' \to_{f} y'$ into a proof that $f^{*}(y') = x'$,
+and $h'$ into a proof that $(f \circ g)^{*}(y') = u'$. Moreover,
+$(f \circ g)^{*}(y') = g^{*}(f^{*}(y'))$. Putting this all together, we get:
 
-whence we see that $(a', f)$ and $(a', g)$ are both lifts for the lower
-corner given by lifting the identity map along $b'$ --- so, since lifts
-are unique, we have $f = g$.
+$$
+\begin{align*}
+g^{*}(x') &= g^{*}(f^{*}(y')) \\
+          &= (f \circ g)^{*}(y') \\
+          &= u'
+\end{align*}
+$$
 
 ```agda
-  discrete→thin-fibres
-    : ∀ x → Discrete-fibration → ∀ {a b} → is-prop (Fibre E x .Precategory.Hom a b)
-  discrete→thin-fibres x disc {a} {b} f g =
-    Σ-inj-set (fibre-set x) $
-      is-contr→is-prop (lifts B.id b) (a , f) (a , g)
-    where open Discrete-fibration disc
+    all-cartesian {x' = x'} {y' = y'} {f = f} f' .universal {u' = u'} g h' =
+      ^*-hom g $
+        g ^* x'          ≡˘⟨ ap (g ^*_) (^*-lift f f') ⟩
+        (g ^* (f ^* y')) ≡˘⟨ ^*-∘ f g y' ⟩
+        (f B.∘ g) ^* y'  ≡⟨ ^*-lift (f B.∘ g) h' ⟩
+        u'               ∎
 ```
 
-## Morphisms in discrete fibrations
+## Discrete fibrations are cartesian
 
-If $\cE$ is a discrete fibration, then the only vertical morphisms
-are identities. This follows directly from lifts being contractible.
+To prove that discrete fibrations deserve the name discrete
+_fibrations_, we prove that any discrete fibration is a [[Cartesian
+fibration]].
 
 ```agda
-  discrete→vertical-id
-    : Discrete-fibration
-    → ∀ {x} {x'' : E.Ob[ x ]} (f' : Σ[ x' ∈ E.Ob[ x ] ] (E.Hom[ B.id ] x' x''))
-    → (x'' , E.id') ≡ f'
-  discrete→vertical-id disc {x'' = x''} f' =
-    sym (lifts B.id _ .paths (x'' , E.id')) ∙ lifts B.id x'' .paths f'
-    where open Discrete-fibration disc
+  discrete→cartesian : is-discrete-cartesian-fibration → Cartesian-fibration E
+  discrete→cartesian disc = r where
+    open is-discrete-cartesian-fibration disc
+    r : Cartesian-fibration E
 ```
 
-We can use this fact in conjunction with the fact that all fibres are thin to show
-that every vertical morphism in a discrete fibration is invertible.
+Luckily for us, the sea has already risen to meet us.: by assumption,
+every right corner has a unique lift, and every morphism in a discrete
+fibration is cartesian.
 
 ```agda
-  discrete→vertical-invertible
-    : Discrete-fibration
-    → ∀ {x} {x' x'' : E.Ob[ x ]} → (f' : E.Hom[ B.id ] x' x'') → is-invertible↓ f'
-  discrete→vertical-invertible disc {x' = x'} {x'' = x''} f' =
-    make-invertible↓
-      (subst (λ x' → E.Hom[ B.id ] x'' x') x''≡x' E.id')
-      (to-pathp (discrete→thin-fibres _ disc _ _))
-      (to-pathp (discrete→thin-fibres _ disc _ _))
-    where
-      x''≡x' : x'' ≡ x'
-      x''≡x' = ap fst (discrete→vertical-id disc (x' , f'))
+    r .has-lift f y' .x' = f ^* y'
+    r .has-lift f y' .lifting = π* f y'
+    r .has-lift f y' .cartesian = all-cartesian (π* f y')
 ```
 
 ## Discrete fibrations are presheaves
@@ -219,36 +325,26 @@ module _ {o ℓ} (B : Precategory o ℓ)  where
 -->
 
 ```agda
-  discrete→presheaf : ∀ {o' ℓ'} (E : Displayed B o' ℓ') → Discrete-fibration E
-                    → Functor (B ^op) (Sets o')
+  discrete→presheaf
+    : ∀ {o' ℓ'} (E : Displayed B o' ℓ')
+    → is-discrete-cartesian-fibration E
+    → Functor (B ^op) (Sets o')
   discrete→presheaf {o' = o'} E disc = psh where
     module E = Displayed E
-    open Discrete-fibration disc
+    open is-discrete-cartesian-fibration disc
 ```
 
 For each object in $X : \cB$, we take the set of objects $E$ that
 lie over $X$. The functorial action of `f : Hom X Y` is then constructed
 by taking the domain of the lift of `f`. Functoriality follows by
-uniqueness of the lifts.
+uniqueness of the cart-lift.
 
 ```agda
     psh : Functor (B ^op) (Sets o')
     psh .Functor.F₀ X = el E.Ob[ X ] (fibre-set X)
-    psh .Functor.F₁ f X' = lifts f X' .centre .fst
-    psh .Functor.F-id = funext λ X' → ap fst (lifts B.id X' .paths (X' , E.id'))
-    psh .Functor.F-∘ {X} {Y} {Z} f g = funext λ X' →
-      let Y' : E.Ob[ Y ]
-          Y' = lifts g X' .centre .fst
-
-          g' : E.Hom[ g ] Y' X'
-          g' = lifts g X' .centre .snd
-
-          Z' : E.Ob[ Z ]
-          Z' = lifts f Y' .centre .fst
-
-          f' : E.Hom[ f ] Z' Y'
-          f' = lifts f Y' .centre .snd
-      in ap fst (lifts (g B.∘ f) X' .paths (Z' , (g' E.∘' f' )))
+    psh .Functor.F₁ f X' = f ^* X'
+    psh .Functor.F-id = funext λ X' → ^*-id X'
+    psh .Functor.F-∘ {X} {Y} {Z} f g = funext λ X' → ^*-∘ g f X'
 ```
 
 To construct a discrete fibration from a presheaf $P$, we take the
@@ -260,15 +356,16 @@ from the contractibilty of singletons.
 [(displayed) category of elements]: Cat.Displayed.Instances.Elements.html
 
 ```agda
-  presheaf→discrete : ∀ {κ} → Functor (B ^op) (Sets κ)
-                    → Σ[ E ∈ Displayed B κ κ ] Discrete-fibration E
+  presheaf→discrete
+    : ∀ {κ} → Functor (B ^op) (Sets κ)
+    → Σ[ E ∈ Displayed B κ κ ] is-discrete-cartesian-fibration E
   presheaf→discrete {κ = κ} P = ∫ B P , discrete where
     module P = Functor P
 
-    discrete : Discrete-fibration (∫ B P)
-    discrete .Discrete-fibration.fibre-set X =
+    discrete : is-discrete-cartesian-fibration (∫ B P)
+    discrete .is-discrete-cartesian-fibration.fibre-set X =
       P.₀ X .is-tr
-    discrete .Discrete-fibration.lifts f P[Y] =
+    discrete .is-discrete-cartesian-fibration.cart-lift f P[Y] =
       contr (P.₁ f P[Y] , refl) Singleton-is-contr
 ```
 
@@ -299,7 +396,7 @@ objects, and an invertible action on morphisms.
 
 ```agda
   presheaf≃discrete .rinv (P , p-disc) = Σ-prop-path hl ∫≡dx where
-    open Discrete-fibration p-disc
+    open is-discrete-cartesian-fibration p-disc
     open Displayed-functor
     open Displayed P
 ```
@@ -308,7 +405,7 @@ The functor will send an object $c \liesover x$ to that same object $c$;
 This is readily seen to be invertible. But the action on morphisms is
 slightly more complicated. Recall that, since $P$ is a discrete
 fibration, every span $b' \liesover b \xot{f} a$ has a contractible
-space of Cartesian lifts $(a', f')$. Our functor must, given objects
+space of Cartesian cart-lift $(a', f')$. Our functor must, given objects
 $a'', b'$, a map $f : a \to b$, and a proof that $a'' = a'$, produce a
 map $a'' \to_f b$ --- so we can take the canonical $f' : a' \to_f b$ and
 transport it over the given $a'' = a'$.
@@ -317,7 +414,7 @@ transport it over the given $a'' = a'$.
     pieces : Displayed-functor (∫ B (discrete→presheaf P p-disc)) P Id
     pieces .F₀' x = x
     pieces .F₁' {f = f} {a'} {b'} x =
-      subst (λ e → Hom[ f ] e b') x $ lifts f b' .centre .snd
+      subst (λ e → Hom[ f ] e b') x $ cart-lift f b' .centre .snd
 ```
 
 This transport _threatens_ to throw a spanner in the works, since it is
@@ -327,24 +424,23 @@ _can't_ ruin our day. Directly from the uniqueness of $(a', f')$ we
 conclude that we've put together a functor.
 
 ```agda
-    pieces .F-id' = from-pathp (ap snd (lifts _ _ .paths _))
+    pieces .F-id' =
+      is-prop→pathp (λ _ → Hom[]-is-prop) _ _
     pieces .F-∘' {f = f} {g} {a'} {b'} {c'} {f'} {g'} =
-      ap (λ e → subst (λ e → Hom[ f B.∘ g ] e c') e
-            (lifts _ _ .centre .snd)) (fibre-set _ _ _ _ _)
-      ∙ from-pathp (ap snd (lifts _ _ .paths _))
+      is-prop→pathp (λ _ → Hom[]-is-prop) _ _
 ```
 
 It remains to show that, given a map $a'' \to b$ (and the rest of the
 data $a$, $b$, $f : a \to b$, $b' \liesover b$), we can recover a proof
-that $a''$ is the chosen lift $a'$. But again, lifts are unique, so this
+that $a''$ is the chosen lift $a'$. But again, cart-lift are unique, so this
 is immediate.
 
 ```agda
     ∫≡dx : ∫ B (discrete→presheaf P p-disc) ≡ P
     ∫≡dx = Displayed-path pieces (λ _ → id-equiv) (is-iso→is-equiv p) where
       p : ∀ {a b} {f : B.Hom a b} {a'} {b'} → is-iso (pieces .F₁' {f = f} {a'} {b'})
-      p .inv f  = ap fst $ lifts _ _ .paths (_ , f)
-      p .rinv p = from-pathp (ap snd (lifts _ _ .paths _))
+      p .inv f  = ap fst $ cart-lift _ _ .paths (_ , f)
+      p .rinv p = from-pathp (ap snd (cart-lift _ _ .paths _))
       p .linv p = fibre-set _ _ _ _ _
 ```
 
@@ -354,7 +450,7 @@ this witness lives in a proposition (it is a pair of propositions), so
 it survives automatically.
 
 ```agda
-    private unquoteDecl eqv = declare-record-iso eqv (quote Discrete-fibration)
+    private unquoteDecl eqv = declare-record-iso eqv (quote is-discrete-cartesian-fibration)
     hl : ∀ x → is-prop _
     hl x = Iso→is-hlevel! 1 eqv
 ```

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

@@ -125,12 +125,12 @@ Intuitively, this is true, as sets are 0-groupoids.
 
 ```agda
 discrete→right-fibration
-  : Discrete-fibration ℰ
+  : is-discrete-cartesian-fibration ℰ
   → Right-fibration
 discrete→right-fibration dfib =
   vertical-invertible+fibration→right-fibration
     (discrete→cartesian ℰ dfib)
-    (discrete→vertical-invertible ℰ dfib)
+    (is-discrete-cartesian-fibration.all-invertible↓ dfib)
 ```
 
 ## Fibred functors and right fibrations
@@ -164,7 +164,7 @@ functor+discrete→fibred
   → {𝒟 : Precategory o₂ ℓ₂}
   → {ℱ : Displayed 𝒟 o₂' ℓ₂'}
   → {F : Functor 𝒟 ℬ}
-  → Discrete-fibration ℰ
+  → is-discrete-cartesian-fibration ℰ
   → (F' : Displayed-functor ℱ ℰ F)
   → Fibred-functor ℱ ℰ F
 functor+discrete→fibred disc F' =

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

@@ -0,0 +1,282 @@
+---
+description: |
+  Discrete cocartesian fibrations.
+---
+<!--
+```agda
+open import Cat.Displayed.Cocartesian
+open import Cat.Displayed.Functor
+open import Cat.Instances.Functor
+open import Cat.Displayed.Fibre
+open import Cat.Displayed.Base
+open import Cat.Displayed.Path
+open import Cat.Prelude
+
+import Cat.Displayed.Reasoning
+import Cat.Displayed.Morphism
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Displayed.Cocartesian.Discrete where
+```
+
+<!--
+```agda
+open Cocartesian-fibration
+open Cocartesian-lift
+open is-cocartesian
+```
+-->
+
+# Discrete cocartesian fibrations
+
+:::{.definition #discrete-cocartesian-fibration alias="discrete-opfibration"}
+A **discrete cocartesian fibration** or **discrete opfibration** is a
+[[displayed category]] that satisfies the dual lifting property of a
+[[discrete cartesian fibration]]. Explicitly, a displayed category
+$\cE \liesover \cB$ is a discrete cocartesian fibration if:
+
+- Every type of displayed objects is a set.
+- For each left corner
+
+~~~{.quiver}
+\[\begin{tikzcd}
+  {x'} & \\
+  x & {y\text{,}}
+  \arrow[lies over, from=1-1, to=2-1]
+  \arrow["f"', from=2-1, to=2-2]
+\end{tikzcd}\]
+~~~
+
+there is a contractible space of objects $y'$ equipped with
+maps $x' \to_{f} y'$.
+
+:::
+
+
+<!--
+```agda
+module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
+  private
+    module B = Cat.Reasoning B
+    module E = Displayed E
+    open Cat.Displayed.Reasoning E
+    open Cat.Displayed.Morphism E
+    open Displayed E
+```
+-->
+
+```agda
+  record is-discrete-cocartesian-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
+    field
+      fibre-set : ∀ x → is-set E.Ob[ x ]
+      cocart-lift
+        : ∀ {x y} (f : B.Hom x y) (x' : E.Ob[ x ])
+        → is-contr (Σ[ y' ∈ E.Ob[ y ] ] E.Hom[ f ] x' y')
+```
+
+
+We will denote the canonical lift of $f$ to $y'$ as
+$$
+\iota_{f, x'}^{*} : x' \to_{f} f_{!}(x')
+$$
+
+```agda
+    _^!_ : ∀ {x y} → (f : B.Hom x y) → (x' : E.Ob[ x ]) → E.Ob[ y ]
+    f ^! x' = cocart-lift f x' .centre .fst
+
+    ι! : ∀ {x y} → (f : B.Hom x y) → (x' : E.Ob[ x ]) → E.Hom[ f ] x' (f ^! x')
+    ι! f x' = cocart-lift f x' .centre .snd
+```
+
+## Basic properties of discrete cocartesian fibrations
+
+Discrete cocartesian fibrations are formally dual to discrete cartesian
+fibrations, so they enjoy many of the same basic properties.
+Many of the proofs are functionally identical, so we will only provide
+brief commentary, and direct interested readers to the
+[corresponding section] in the page for discrete cartesian fibrations
+for details.
+
+[corresponding section]: Cat.Displayed.Cartesian.Discrete.html#basic-properties-of-discrete-cartesian-fibrations
+
+First, note that the type of morphisms in a discrete cocartesian fibration
+is always a [[proposition]].
+
+```agda
+    Hom[]-is-prop : ∀ {x y x' y'} {f : B.Hom x y} → is-prop (Hom[ f ] x' y')
+    Hom[]-is-prop {x' = x'} {y' = y'} {f = f} f' f'' =
+      Σ-inj-set (fibre-set _) $
+      is-contr→is-prop (cocart-lift f x') (y' , f') (y' , f'')
+```
+
+Additionally, morphisms $x' \to_{f} y'$ in a discrete cocartesian fibration
+are equivalent to proofs that $f_{!}(x') = y'$.
+
+```agda
+    opaque
+      ^!-lift
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → Hom[ f ] x' y'
+        → f ^! x' ≡ y'
+
+      ^!-hom
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → f ^! x' ≡ y'
+        → Hom[ f ] x' y'
+
+      ^!-hom-is-equiv
+        : ∀ {x y x' y'}
+        → (f : B.Hom x y)
+        → is-equiv (^!-hom {x' = x'} {y' = y'} f)
+```
+
+<details>
+<summary>The proofs are formally dual to the cartesian case, so we omit
+the details.
+</summary>
+
+```agda
+
+      ^!-lift {x' = x'} {y' = y'} f f' =
+        ap fst $ cocart-lift f x' .paths (y' , f')
+
+      ^!-hom {x' = x'} {y' = y'} f p =
+        hom[ B.idl f ] $
+          subst (λ x' → Hom[ B.id ] x' y') (sym p) id' ∘' ι! f x'
+
+      ^!-hom-is-equiv f =
+        is-iso→is-equiv $
+        iso (^!-lift f)
+          (λ _ → Hom[]-is-prop _ _)
+          (λ _ → fibre-set _ _ _ _ _)
+```
+</details>
+
+## Functoriality of lifts
+
+The (necessarily unique) choice of lifts in a discrete cocartesian fibration
+are functorial. Unlike the cartesian case, discrete cartesian fibrations
+are *covariantly* functorial; this asymmetry is an artifact of duality.
+
+```agda
+    ^!-id
+      : ∀ {x} (x' : Ob[ x ])
+      → B.id ^! x' ≡ x'
+    ^!-id x' = ^!-lift B.id id'
+
+    ^!-∘
+      : ∀ {x y z}
+      → (f : B.Hom y z) (g : B.Hom x y) (x' : Ob[ x ])
+      → (f B.∘ g) ^! x' ≡ f ^! (g ^! x')
+    ^!-∘ f g x' = ^!-lift (f B.∘ g) (ι! f (g ^! x') ∘' ι! g x')
+```
+
+## Invertible maps in discrete cocartesian fibrations
+
+Let $f : x \to y$ be an [[invertible]] morphism of $\cB$. If $\cE$
+is a discrete cocartesian fibration, then every morphism displayed over
+$f$ is also invertible.
+
+```agda
+    all-invertible[]
+      : ∀ {x y x' y'} {f : B.Hom x y}
+      → (f' : Hom[ f ] x' y')
+      → (f⁻¹ : B.is-invertible f)
+      → is-invertible[ f⁻¹ ] f'
+```
+
+<details>
+<summary>The proof is essentially identical to the [cartesian case],
+so we omit the details.
+</summary>
+
+[cartesian case]: Cat.Displayed.Cartesian.Discrete.html#invertible-maps-in-discrete-cartesian-fibrations
+
+```agda
+    all-invertible[] {x' = x'} {y' = y'} {f = f} f' f⁻¹ = f'⁻¹ where
+      module f⁻¹ = B.is-invertible f⁻¹
+      open is-invertible[_]
+
+      f'⁻¹ : is-invertible[ f⁻¹ ] f'
+      f'⁻¹ .inv' =
+        ^!-hom f⁻¹.inv $
+          f⁻¹.inv ^! y'         ≡˘⟨ ap (f⁻¹.inv ^!_) (^!-lift f f') ⟩
+          f⁻¹.inv ^! (f ^! x')  ≡˘⟨ ^!-∘ f⁻¹.inv f x' ⟩
+          (f⁻¹.inv B.∘ f) ^! x' ≡⟨ ap (_^! x') f⁻¹.invr ⟩
+          B.id ^! x'            ≡⟨ ^!-id x' ⟩
+          x'                    ∎
+      f'⁻¹ .inverses' .Inverses[_].invl' =
+        is-prop→pathp (λ _ → Hom[]-is-prop) _ _
+      f'⁻¹ .inverses' .Inverses[_].invr' =
+        is-prop→pathp (λ _ → Hom[]-is-prop) _ _
+```
+</details>
+
+As an easy corollary, we get that all vertical maps in a discrete
+fibration are invertible.
+
+```agda
+    all-invertible↓
+      : ∀ {x x' y'}
+      → (f' : Hom[ B.id {x} ] x' y')
+      → is-invertible↓ f'
+    all-invertible↓ f' = all-invertible[] f' B.id-invertible
+```
+
+## Cocartesian maps in discrete cocartesian fibrations
+
+As the name suggests, every morphism in a discrete cocartesian fibration
+is [[cocartesian|cocartesian-morphism]]. Note that as every hom set in a
+discrete cocartesian fibration is propositional, so we just
+need to establish the existence portion of the universal property.
+
+```agda
+    all-cocartesian
+      : ∀ {x y x' y'} {f : B.Hom x y}
+      → (f' : Hom[ f ] x' y')
+      → is-cocartesian E f f'
+    all-cocartesian f' .commutes _ _ = Hom[]-is-prop _ _
+    all-cocartesian f' .unique _ _ = Hom[]-is-prop _ _
+```
+
+<details>
+<summary>The argument is almost identical to the proof that [all morphisms
+in discrete cartesian fibrations are cartesian], so we suppress the details.
+</summary>
+
+[all morphisms in discrete cartesian fibrations are cartesian]: Cat.Displayed.Cartesian.Discrete.html#cartesian-maps-in-discrete-fibrations
+
+```agda
+    all-cocartesian {x' = x'} {y' = y'} {f = f} f' .universal {u' = u'} g h' =
+      ^!-hom g $
+        g ^! y'         ≡˘⟨ ap (g ^!_) (^!-lift f f') ⟩
+        g ^! (f ^! x')  ≡˘⟨ ^!-∘ g f x' ⟩
+        (g B.∘ f) ^! x' ≡⟨ ^!-lift (g B.∘ f) h' ⟩
+        u'              ∎
+```
+</details>
+
+## Discrete cocartesian fibrations are cocartesian
+
+To prove that discrete cocartesian fibrations deserve the name
+_fibration_, we prove that any discrete fibration is a [[cocartesian
+fibration]]. Luckily, we already have all the pieces at hand: every morphism
+in $\cE$ is cocartesian, so all we need to is to exhibit a lift, and
+by our assumption, all such lifts exist!
+
+```agda
+  discrete→cocartesian
+    : is-discrete-cocartesian-fibration
+    → Cocartesian-fibration E
+  discrete→cocartesian dfib = cocart-fib where
+    open is-discrete-cocartesian-fibration dfib
+
+    cocart-fib : Cocartesian-fibration E
+    cocart-fib .has-lift f x' .y' = f ^! x'
+    cocart-fib .has-lift f x' .lifting = ι! f x'
+    cocart-fib .has-lift f x' .cocartesian = all-cocartesian (ι! f x')
+```

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

@@ -46,9 +46,9 @@ This fibration is obviously a discrete fibration; in fact, it's about as
 discrete as you can get!
 
 ```agda
-IdD-discrete-fibration : Discrete-fibration IdD
-IdD-discrete-fibration .Discrete-fibration.fibre-set _ = hlevel 2
-IdD-discrete-fibration .Discrete-fibration.lifts _ _ = hlevel 0
+IdD-discrete-fibration : is-discrete-cartesian-fibration IdD
+IdD-discrete-fibration .is-discrete-cartesian-fibration.fibre-set _ = hlevel 2
+IdD-discrete-fibration .is-discrete-cartesian-fibration.cart-lift _ _ = hlevel 0
 ```
 
 Every morphism in the identity fibration is trivially cartesian and