defn: opposite fibrations

src/1Lab/Equiv.lagda.md

@@ -29,8 +29,8 @@ The key issue is that any [[identity system]] is equipped with a [[path
 induction]] principle, which, if extended to the type of isomorphisms,
 would let us conclude that *being an isomorphism* is a [[proposition]]:
 but this is [provably not the case]. The result of formulating
-univalence using isomorphisms is sometimes caled [[isovalence]] --- that
-page has a formalisation of its failure.
+univalence using isomorphisms is sometimes called [[isovalence]] ---
+that page has a formalisation of its failure.
 
 [provably not the case]: 1Lab.Counterexamples.IsIso.html
 

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

@@ -45,7 +45,7 @@ private
 ```
 -->
 
-# Reindexing for cartesian fibrations
+# Reindexing for cartesian fibrations {defines="base-change"}
 
 A [[cartesian fibration]] can be thought of as a [[displayed category]]
 $\cE$ whose [[fibre categories]] $\cE^*(b)$ depend

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

@@ -0,0 +1,371 @@
+<!--
+```agda
+{-# OPTIONS -vtc.decl:5 --lossy-unification #-}
+open import Cat.Displayed.Cartesian
+open import Cat.Functor.Naturality
+open import Cat.Displayed.Fibre
+open import Cat.Displayed.Base
+open import Cat.Prelude
+
+import Cat.Displayed.Cartesian.Indexing as Ix
+import Cat.Displayed.Fibre.Reasoning as Fib
+import Cat.Displayed.Reasoning as Disp
+import Cat.Functor.Reasoning as Fr
+import Cat.Reasoning as Cat
+```
+-->
+
+```agda
+module Cat.Displayed.Instances.Opposite
+  {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ')
+  (cart : Cartesian-fibration E)
+  where
+```
+
+# The opposite of a fibration
+
+<!--
+```agda
+open Cartesian-fibration cart
+open Displayed E
+open Ix E cart
+open Cat B
+open _=>_
+
+private
+  module rebase {x} {y} {f : Hom x y} = Fr (base-change f)
+  module D = Displayed
+  module E = Disp E
+  module F = Fib E
+  open F renaming (_∘_ to infixr 25 _∘v_) using ()
+
+  _^*_ : ∀ {a b} (f : Hom a b) → Ob[ b ] → Ob[ a ]
+  f ^* x = has-lift.x' f x
+
+  π : ∀ {a b} {f : Hom a b} {x : Ob[ b ]} → Hom[ f ] (f ^* x) x
+  π = has-lift.lifting _ _
+
+  γ← = ^*-comp-from
+  γ→ = ^*-comp-to
+  ι← = ^*-id-from
+  ι→ = ^*-id-to
+  _[_] = rebase
+  infix 30 _[_]
+```
+-->
+
+Since the theory of [[fibrations]] over $\cB$ behaves like ordinary
+category theory over $\Sets$, we expect to find $\cB$-indexed analogues
+of basic constructions such as functor categories, product categories,
+and, what concerns us here, *opposite* categories. Working at the level
+of [[displayed categories]], fix a fibration $\cE \liesover \cB$; we
+want to construct the fibration classifies[^catcore]
+
+$$
+\cB\op \xto{\cE^*(-)} \Cat \xto{(-)\op} \Cat\text{,}
+$$
+
+[^catcore]:
+    Note that, strictly speaking, the construction of opposite
+    categories can not be extended to a pseudofunctor $\Cat \to \Cat$: While
+    the opposite of a functor goes in the same direction as the original
+    (i.e.  $F : \cC \to \cD$ is taken to $F\op : \cC\op \to \cD$), the
+    opposite of a *natural transformation* has reversed direction.
+    Therefore, the "opposite category functor" would be typed $\Cat \to
+    \Cat^{\rm{co}}$, landing instead in the *2-cell dual* of $\Cat$.
+
+    However, because the domain $\cB\op$ is [[locally discrete|locally
+    discrete bicategory]], all of its 2-cells are isomorphisms.
+    Therefore, the pseudofunctor classified by a given fibration factors
+    through the *homwise [[core]]* of $\Cat$ --- and the construction of
+    opposite categories restricts to a map $\Cat^{\rm{core}} \to
+    \Cat^{\rm{core}}$.
+
+in other words, the fibration whose [[fibre categories]] are the
+opposites of those of $\cE$. Note that this is still a category over
+$\cB$, unlike in the case of the [[total opposite]], which results in a
+category over $\cB\op$ --- which, generally, will not be a fibration.
+The construction of the fibred opposite proceeds using $\cE$'s
+[[base change]] functors. A morphism $h : y \to\op_f x$, lying over a map
+$f : a \to b$, is defined to be a map $f^*y \to_{\id} x$, as indicated
+(in red) in the diagram below.
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  x \&\& {f^*y} \&\& y \\
+  \\
+  a \&\& a \&\& b
+  \arrow["\pi", from=1-3, to=1-5]
+  \arrow[lies over, from=1-5, to=3-5]
+  \arrow[lies over, from=1-3, to=3-3]
+  \arrow["f"', from=3-3, to=3-5]
+  \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=3-5]
+	\arrow["h"', color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1]
+  \arrow[Rightarrow, no head, from=3-1, to=3-3]
+  \arrow[lies over, from=1-1, to=3-1]
+\end{tikzcd}\]
+~~~
+
+At the level of vertical maps, this says that a morphism $x \to\op y$ is
+determined by a morphism $\id^*y \to x$, hence by a morphism $y \to x$;
+this correspondence trivially extends to an [[isomorphism of
+precategories]] between $\cE^*(x)\op$ and $\cE^*_{\rm{op}}(x)$. If we
+have maps $h : f^*z \to y$ and $h': g^*y \to x$, then their composite
+$fg^*z \to x$ is computed as the composite
+
+$$
+fg^*z \xto{\gamma} g^*f^*z \xto{f^*h} g^*y \xto{h'} x\text{,}
+$$
+
+where the map $\gamma$ is one of the structural morphisms expressing
+[[pseudofunctoriality|pseudofunctor]] of $\cE^*(-)$.
+
+```agda
+_∘,_
+  : ∀ {a b c} {x y z} {f : Hom b c} {g : Hom a b}
+  → (f' : Hom[ id ] (f ^* z) y) (g' : Hom[ id ] (g ^* y) x)
+  → Hom[ id {x = a} ] ((f ∘ g) ^* z) x
+_∘,_ {g = g} f' g' = g' ∘v g [ f' ] ∘v γ→
+```
+
+## The coherence problem
+
+Having done the mathematics behind the fibred opposite, we turn to
+teaching Agda about the construction. Recall that the algebraic laws
+(associativity, unitality) of a displayed category $\cE \liesover \cB$
+are *dependent paths* over the corresponding laws in $\cB$. Ordinarily,
+this dependence is strictly at the level of morphisms depending on
+morphisms, with the domain and codomain staying fixed --- and we have an
+extensive toolkit of combinators for dealing with this indexing.
+
+However, the fibred opposite mixes levels in a complicated way. For
+concreteness, let's focus on the right identity law. We want to
+construct a path between some $h : f^*y \to x$ and the composite
+
+$$
+(f\id)^*y \xto{\gamma} {\id}^*f^*y \xto{{\id}^*h} {\id}^*x \xto{\pi} x\text{,}
+$$
+
+but note that, while these are both vertical maps, they have different
+*domains*! While the path we're trying to construct *is* allowed to
+depend on the witness that $f\id = f$ in $\cB$, introducing this
+dependency on the domain *object* actually complicates things even
+further. Our toolkit does not include very many tools for working with
+dependent identifications between maps whose source and target vary.
+
+The solution is to reify the dependency of the identifications into a
+*morphism*, which we can then calculate with at the level of fibre
+categories. Given a path $p : f = f'$, we obtain a vertical map $f'^*x
+\to f^*x$, which we call the `adjust`{.Agda}ment induced by $p$. The
+explicit definition below is identical to transporting the identity map
+$f^*x \to f^*x$ along $p$, but computes better:
+
+```agda
+private
+  adjust
+    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]}
+    → (p : f ≡ f')
+    → Hom[ id ] (f' ^* x) (f ^* x)
+  adjust p = has-lift.universal' _ _ (idr _ ∙ p) (has-lift.lifting _ _)
+```
+
+<!--
+```agda
+private abstract
+  π-adjust
+    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]} (p : f ≡ f')
+    → π {a} {b} {f} {x} ∘' adjust p ≡[ refl ∙ idr f ∙ p ] π
+  π-adjust p = has-lift.commutes _ _ _ _ ∙[] to-pathp⁻ refl
+
+  adjust-refl
+    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
+    → adjust {x = x} (λ i → f) ≡ id'
+  adjust-refl = has-lift.uniquep₂ _ _ (idr _) refl (idr _) (adjust refl) id'
+    (to-pathp (ap E.hom[] (has-lift.commutes _ _ _ _) ·· E.hom[]-∙ _ _ ·· E.liberate _))
+    (idr' _)
+```
+-->
+
+The point of introducing `adjust`{.Agda} is the following theorem, which
+connects transport in the domain of a vertical morphism with
+postcomposition along `adjust`{.Agda}. The proof is by path induction:
+it suffices to cover the case where the domain varies trivially, which
+leads to a correspondingly trivial adjustment.
+
+```agda
+  transp-lift
+    : ∀ {a b} {f f' : Hom a b} {x : Ob[ b ]} {y : Ob[ a ]} {h : Hom[ id ] (f ^* x) y}
+    → (p : f ≡ f')
+    → transport (λ i → Hom[ id ] (p i ^* x) y) h ≡ h ∘v adjust p
+  transp-lift {f = f} {x = x} {y} {h} =
+    J (λ f' p → transport (λ i → Hom[ id ] (p i ^* x) y) h ≡ E.hom[ idl id ] (h ∘' adjust p))
+      ( transport-refl _
+      ∙ sym (ap E.hom[] (ap₂ _∘'_ refl adjust-refl)
+      ∙ ap E.hom[] (from-pathp⁻ (idr' h)) ∙ E.hom[]-∙ _ _ ∙ E.liberate _))
+```
+
+To finish, we'll need to connect the `adjust`{.Agda}ment induced by the
+algebraic laws of $\cB$ with the pseudofunctoriality witnesses of $\cE$.
+
+```agda
+  adjust-idr
+    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
+    → adjust {x = x} (idr f) ≡ γ← ∘v ι←
+
+  adjust-idl
+    : ∀ {a b} {f : Hom a b} {x : Ob[ b ]}
+    → adjust {x = x} (idl f) ≡ γ← ∘v f [ ι← ]
+
+  adjust-assoc
+    : ∀ {a b c d} {f : Hom c d} {g : Hom b c} {h : Hom a b} {x : Ob[ d ]}
+    → adjust {x = x} (assoc f g h) ≡ γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→
+```
+
+<details>
+<summary>The proofs here are nothing more than calculations at the level
+of the underlying displayed category. They're not informative; it's fine
+to take the three theorems above as given.</summary>
+
+```agda
+  adjust-idr {f = f} {x} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (idr f))
+    (   F.pulllf (has-lift.commutesv (f ∘ id) x (π ∘' π))
+    ∙[] E.pullr[] (idr id) (has-lift.commutesp id (f ^* x) (idr id) id')
+    ∙[] idr' π)
+
+  adjust-idl {f = f} {x} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (idl f))
+    (   F.pulllf (has-lift.commutesv (id ∘ f) x (π ∘' π))
+    ∙[] E.pullr[] _ (has-lift.commutesp f (id ^* x) id-comm (ι← ∘' π))
+    ∙[] E.pulll[] _ (has-lift.commutesp id x (idr id) id') ∙[] idl' π)
+
+  adjust-assoc {f = f} {g} {h} = has-lift.uniquep₂ _ _ _ _ _ _ _ (π-adjust (assoc f g h))
+    (F.pulllf (has-lift.commutesv (f ∘ g ∘ h) _ _) ∙[] E.pullr[] _ (F.pulllf (has-lift.commutesp (g ∘ h) _ (idr (g ∘ h)) _))
+    ∙[] (E.refl⟩∘'⟨ E.pullr[] (id-comm ∙ sym (idr (id ∘ h))) (F.pulllf (has-lift.commutesp _ _ _ _)))
+    ∙[] (E.refl⟩∘'⟨ E.pulll[] _ (E.pulll[] (idr g) (has-lift.commutesp _ _ _ _)))
+    ∙[] E.pulll[] _ (E.pulll[] _ (has-lift.commutes _ _ _ _))
+    ∙[] E.pullr[] (idr h) (has-lift.commutesp _ _ _ _)
+    ∙[] has-lift.commutes _ _ _ _)
+```
+
+</details>
+
+## The construction
+
+Using `adjust`{.Agda}, and the three theorems above, we can tackle each
+of the three laws in turn. Having boiled the proofs down to reasoning
+about coherence morphisms in a pseudofunctor, the proofs are... no more
+than reasoning about coherence morphisms in a pseudofunctor --- which is
+to say, boring algebra. Let us make concrete note of the *data* of the
+fibrewise opposite before tackling the properties:
+
+```agda
+_^op' : Displayed B o' ℓ'
+_^op' .D.Ob[_] = Ob[_]
+_^op' .D.Hom[_]     f x y = Hom[ id ] (f ^* y) x
+_^op' .D.Hom[_]-set f x y = Hom[_]-set _ _ _
+_^op' .D.id'  = π
+_^op' .D._∘'_ = _∘,_
+```
+
+We can look at the case of left identity as a representative example.
+Note that, after applying the generic `transp-lift`{.Agda} and the
+specific lemma --- in this case, `adjust-idl`{.Agda} --- we're reasoning
+entirely in the fibres of $\cE$. This lets us side-step most of the
+indexed nonsense that otherwise haunts working with fibrations.
+
+```agda
+_^op' .D.idl' {x = x} {y} {f = f} f' = to-pathp $
+  transport (λ i → Hom[ id ] (idl f i ^* y) x) _  ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-idl ⟩
+  (f' ∘v f [ π ] ∘v γ→) ∘v γ← ∘v f [ ι← ]         ≡⟨ F.pullr (F.pullr refl) ⟩
+  f' ∘v f [ π ] ∘v γ→ ∘v (γ← ∘v f [ ι← ])         ≡⟨ ap₂ _∘v_ refl (ap₂ _∘v_ refl (F.cancell (^*-comp .F.invl))) ⟩
+  f' ∘v f [ π ] ∘v f [ ι← ]                       ≡⟨ F.elimr (rebase.annihilate (E.cancel _ _ (has-lift.commutesv _ _ _))) ⟩
+  f'                                              ∎
+```
+
+The next two cases are very similar, so we'll present them without
+further comment.
+
+```agda
+_^op' .D.idr' {x = x} {y} {f} f' = to-pathp $
+  transport (λ i → Hom[ id ] (idr f i ^* y) x) _  ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-idr ⟩
+  (π ∘v id [ f' ] ∘v γ→) ∘v γ← ∘v ι←              ≡⟨ F.pullr (F.pullr (F.cancell (^*-comp .F.invl))) ⟩
+  π ∘v id [ f' ] ∘v ι←                            ≡⟨ ap (π ∘v_) (sym (base-change-id .Isoⁿ.from .is-natural _ _ _)) ⟩
+  π ∘v ι← ∘v f'                                   ≡⟨ F.cancell (base-change-id .Isoⁿ.invl ηₚ _) ⟩
+  f'                                              ∎
+
+_^op' .D.assoc' {x = x} {y} {z} {f} {g} {h} f' g' h' = to-pathp $
+  transport (λ i → Hom[ id ] (assoc f g h i ^* _) _) (f' ∘, (g' ∘, h'))           ≡⟨ transp-lift _ ∙ ap₂ _∘v_ refl adjust-assoc ⟩
+  ((h' ∘v h [ g' ] ∘v γ→) ∘v (g ∘ h) [ f' ] ∘v γ→) ∘v γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→  ≡⟨ sym (F.assoc _ _ _) ∙ F.pullr (F.pullr (ap (γ→ ∘v_) (F.pullr refl))) ⟩
+  h' ∘v h [ g' ] ∘v γ→ ∘v (g ∘ h) [ f' ] ∘v ⌜ γ→ ∘v γ← ∘v γ← ∘v h [ γ→ ] ∘v γ→ ⌝  ≡⟨ ap (λ e → h' ∘v h [ g' ] ∘v γ→ ∘v (g ∘ h) [ f' ] ∘v e) (F.cancell (^*-comp .F.invl))  ⟩
+  h' ∘v h [ g' ] ∘v ⌜ γ→ ∘v (g ∘ h) [ f' ] ∘v γ← ∘v h [ γ→ ] ∘v γ→ ⌝              ≡⟨ ap (λ e → h' ∘v h [ g' ] ∘v e) (F.extendl (sym (^*-comp-to-natural _))) ⟩
+  h' ∘v h [ g' ] ∘v h [ g [ f' ] ] ∘v γ→ ∘v γ← ∘v h [ γ→ ] ∘v γ→                  ≡⟨ ap₂ _∘v_ refl (F.pulll (sym (rebase.F-∘ _ _)) ∙ ap₂ _∘v_ refl (F.cancell (^*-comp .F.invl))) ⟩
+  h' ∘v h [ g' ∘v g [ f' ] ] ∘v h [ γ→ ] ∘v γ→                                    ≡⟨ ap (h' ∘v_) (rebase.pulll (F.pullr refl)) ⟩
+  h' ∘v h [ g' ∘v g [ f' ] ∘v γ→ ] ∘v γ→                                          ∎
+```
+
+Having defined the fibration, we can prove the comparison theorem
+mentioned in the introductory paragraph, showing that passing from $\cE$
+to $\cE\op$ inverts *each fibre*.
+
+```agda
+opposite-map : ∀ {a} {x y : Ob[ a ]} → Fib.Hom E y x ≃ Fib.Hom _^op' x y
+opposite-map .fst f = f ∘v π
+opposite-map .snd = is-iso→is-equiv $ iso
+  (λ f → f ∘v has-lift.universalv id _ id')
+  (λ x → F.cancelr (base-change-id .Isoⁿ.invr ηₚ _))
+  (λ x → F.cancelr (base-change-id .Isoⁿ.invl ηₚ _))
+```
+
+## Cartesian lifts
+
+<!--
+```agda
+abstract
+  ∘,-idl
+    : ∀ {a b c} {x y} {f : Hom b c} {g : Hom a b} (f' : Hom[ id ] (g ^* (f ^* x)) y)
+    → id' ∘, f' ≡ f' ∘v γ→
+  ∘,-idl {f = f} {g} f' =
+    f' ∘v g [ id' ] ∘v γ→ ≡⟨ ap (f' ∘v_) (F.eliml (base-change g .Functor.F-id)) ⟩
+    f' ∘v γ→              ∎
+
+private module Cf = Cartesian-fibration
+```
+-->
+
+Since we defined the displayed morphism spaces directly in terms of
+$\cE$'s base change, it's not surprising that $\cE_{\rm{op}}$ is itself
+a [[fibration]]. Indeed, if we have $f : a \to b$ and $y \liesover b$, a
+Cartesian lift of $y$ along $f$, *in the opposite*, boils down to asking
+for something to fit into the question mark in the diagram
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  {f^*y} \&\& {f^*y} \&\& y \\
+  \\
+  a \&\& a \&\& {b\text{.}}
+  \arrow["\pi", from=1-3, to=1-5]
+  \arrow[from=1-5, to=3-5]
+  \arrow[from=1-3, to=3-3]
+  \arrow["f"', from=3-3, to=3-5]
+  \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=3-5]
+  \arrow["?"', color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1]
+  \arrow[Rightarrow, no head, from=3-1, to=3-3]
+  \arrow[from=1-1, to=3-1]
+  \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-90}, draw=none, from=1-3, to=3-1]
+\end{tikzcd}\]
+~~~
+
+It's no coincidence that the boundary of the question mark is precisely
+that of the identity morphism. A mercifully short calculation
+establishes that this choice *does* furnish a Cartesian lift.
+
+```agda
+Opposite-cartesian : Cartesian-fibration _^op'
+Opposite-cartesian .Cf.has-lift f y' = record
+  { lifting   = id'
+  ; cartesian = record
+    { universal = λ m h → h ∘v γ←
+    ; commutes  = λ m h → ∘,-idl (h ∘v γ←) ∙ F.cancelr (^*-comp .F.invr)
+    ; unique    = λ m h → sym (F.cancelr (^*-comp .F.invl)) ∙ ap (_∘v γ←) (sym (∘,-idl m) ∙ h)
+    }
+  }
+```