From 20c8d196566842fbbea13914545312437976d693 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 16 Jan 2025 15:09:46 -0500 Subject: [PATCH 1/5] refactor: improve proofs/notation for discrete fibrations --- src/Cat/Displayed/Cartesian/Discrete.lagda.md | 370 +++++++++++------- src/Cat/Displayed/Cartesian/Right.lagda.md | 6 +- src/Cat/Displayed/Instances/Identity.lagda.md | 6 +- 3 files changed, 239 insertions(+), 143 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md index 4c37fe499..2408a4192 100644 --- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md +++ b/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,17 @@ 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 +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} @@ -60,8 +62,9 @@ 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 ``` @@ -69,139 +72,241 @@ module _ {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where --> ```agda - record Discrete-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where + record is-discrete-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 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') ``` -So suppose we have an open diagram +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 + ^*-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 + opaque + ^*-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 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') +``` + +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 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'$. - -```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 +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'$. -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-fibration → Cartesian-fibration E + discrete→cartesian disc = r where + open is-discrete-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 +324,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-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-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 +355,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-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-fibration (∫ B P) + discrete .is-discrete-fibration.fibre-set X = P.₀ X .is-tr - discrete .Discrete-fibration.lifts f P[Y] = + discrete .is-discrete-fibration.cart-lift f P[Y] = contr (P.₁ f P[Y] , refl) Singleton-is-contr ``` @@ -299,7 +395,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-fibration p-disc open Displayed-functor open Displayed P ``` @@ -308,7 +404,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 +413,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 +423,24 @@ _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' = from-pathp (ap snd (cart-lift _ _ .paths _)) 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 _)) + (cart-lift _ _ .centre .snd)) (fibre-set _ _ _ _ _) + ∙ from-pathp (ap snd (cart-lift _ _ .paths _)) ``` 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-fibration) hl : ∀ x → is-prop _ hl x = Iso→is-hlevel! 1 eqv ``` diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md index e0b19d966..7c9c04628 100644 --- a/src/Cat/Displayed/Cartesian/Right.lagda.md +++ b/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-fibration ℰ → Right-fibration discrete→right-fibration dfib = vertical-invertible+fibration→right-fibration (discrete→cartesian ℰ dfib) - (discrete→vertical-invertible ℰ dfib) + (is-discrete-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-fibration ℰ → (F' : Displayed-functor ℱ ℰ F) → Fibred-functor ℱ ℰ F functor+discrete→fibred disc F' = diff --git a/src/Cat/Displayed/Instances/Identity.lagda.md b/src/Cat/Displayed/Instances/Identity.lagda.md index 0960a9397..ba6fbc329 100644 --- a/src/Cat/Displayed/Instances/Identity.lagda.md +++ b/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-fibration IdD +IdD-discrete-fibration .is-discrete-fibration.fibre-set _ = hlevel 2 +IdD-discrete-fibration .is-discrete-fibration.cart-lift _ _ = hlevel 0 ``` Every morphism in the identity fibration is trivially cartesian and From 3f58cc73ee4f2e4db5b258fac158ef1c5335c580 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 16 Jan 2025 15:14:26 -0500 Subject: [PATCH 2/5] chore: rename discrete fibrations to discrete cartesian fibrations This makes the terminology around discrete cocartesian fibrations much cleaner. --- src/Cat/Displayed/Cartesian/Discrete.lagda.md | 74 +++++++++---------- src/Cat/Displayed/Cartesian/Right.lagda.md | 6 +- src/Cat/Displayed/Instances/Identity.lagda.md | 6 +- 3 files changed, 43 insertions(+), 43 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md index 2408a4192..a6e8c7033 100644 --- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md +++ b/src/Cat/Displayed/Cartesian/Discrete.lagda.md @@ -42,6 +42,7 @@ over $\cB$, i.e., a functor $\cB\op\to\Sets$. Here, we identify a purely fibrati property that picks out the discrete fibrations among the displayed categories, without talking about the fibres directly. +:::{.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 @@ -56,9 +57,9 @@ 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 - record is-discrete-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where + record is-discrete-cartesian-fibration : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where field fibre-set : ∀ x → is-set E.Ob[ x ] cart-lift @@ -93,7 +93,7 @@ $$ π* f y' = cart-lift f y' .centre .snd ``` -## Basic properties of discrete fibrations +## Basic properties of discrete cartesian fibrations Every hom set of a discrete fibration is a [[proposition]]. @@ -117,20 +117,20 @@ We can improve the previous result by noticing that morphisms $f' : x' \to_{f} y'$ give rise to proofs that $f^*(y') = x'$. ```agda - ^*-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') + 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 - opaque ^*-hom : ∀ {x y x' y'} → (f : B.Hom x y) @@ -140,20 +140,21 @@ $f^{*}(y') = x'$ and morphisms $x' \to y'$. 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 _ _ _ _ _) + ^*-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 functorial. +The (necessarily unique) choice of lifts in a discrete fibration are +contravariantly functorial. ```agda ^*-id @@ -177,7 +178,7 @@ the identity morphism, and the latter by composition of lifts! ^*-∘ f g z' = ^*-lift (f B.∘ g) (π* f z' ∘' π* g (f ^* z')) ``` -## Invertible maps in discrete fibrations +## 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 @@ -293,9 +294,9 @@ _fibrations_, we prove that any discrete fibration is a [[Cartesian fibration]]. ```agda - discrete→cartesian : is-discrete-fibration → Cartesian-fibration E + discrete→cartesian : is-discrete-cartesian-fibration → Cartesian-fibration E discrete→cartesian disc = r where - open is-discrete-fibration disc + open is-discrete-cartesian-fibration disc r : Cartesian-fibration E ``` @@ -326,11 +327,11 @@ module _ {o ℓ} (B : Precategory o ℓ) where ```agda discrete→presheaf : ∀ {o' ℓ'} (E : Displayed B o' ℓ') - → is-discrete-fibration E + → is-discrete-cartesian-fibration E → Functor (B ^op) (Sets o') discrete→presheaf {o' = o'} E disc = psh where module E = Displayed E - open is-discrete-fibration disc + open is-discrete-cartesian-fibration disc ``` For each object in $X : \cB$, we take the set of objects $E$ that @@ -357,14 +358,14 @@ from the contractibilty of singletons. ```agda presheaf→discrete : ∀ {κ} → Functor (B ^op) (Sets κ) - → Σ[ E ∈ Displayed B κ κ ] is-discrete-fibration E + → Σ[ E ∈ Displayed B κ κ ] is-discrete-cartesian-fibration E presheaf→discrete {κ = κ} P = ∫ B P , discrete where module P = Functor P - discrete : is-discrete-fibration (∫ B P) - discrete .is-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 .is-discrete-fibration.cart-lift f P[Y] = + discrete .is-discrete-cartesian-fibration.cart-lift f P[Y] = contr (P.₁ f P[Y] , refl) Singleton-is-contr ``` @@ -395,7 +396,7 @@ objects, and an invertible action on morphisms. ```agda presheaf≃discrete .rinv (P , p-disc) = Σ-prop-path hl ∫≡dx where - open is-discrete-fibration p-disc + open is-discrete-cartesian-fibration p-disc open Displayed-functor open Displayed P ``` @@ -423,11 +424,10 @@ _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 (cart-lift _ _ .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 - (cart-lift _ _ .centre .snd)) (fibre-set _ _ _ _ _) - ∙ from-pathp (ap snd (cart-lift _ _ .paths _)) + is-prop→pathp (λ _ → Hom[]-is-prop) _ _ ``` It remains to show that, given a map $a'' \to b$ (and the rest of the @@ -450,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 is-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 ``` diff --git a/src/Cat/Displayed/Cartesian/Right.lagda.md b/src/Cat/Displayed/Cartesian/Right.lagda.md index 7c9c04628..60d2cd5b6 100644 --- a/src/Cat/Displayed/Cartesian/Right.lagda.md +++ b/src/Cat/Displayed/Cartesian/Right.lagda.md @@ -125,12 +125,12 @@ Intuitively, this is true, as sets are 0-groupoids. ```agda discrete→right-fibration - : is-discrete-fibration ℰ + : is-discrete-cartesian-fibration ℰ → Right-fibration discrete→right-fibration dfib = vertical-invertible+fibration→right-fibration (discrete→cartesian ℰ dfib) - (is-discrete-fibration.all-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 𝒟 ℬ} - → is-discrete-fibration ℰ + → is-discrete-cartesian-fibration ℰ → (F' : Displayed-functor ℱ ℰ F) → Fibred-functor ℱ ℰ F functor+discrete→fibred disc F' = diff --git a/src/Cat/Displayed/Instances/Identity.lagda.md b/src/Cat/Displayed/Instances/Identity.lagda.md index ba6fbc329..226edda4c 100644 --- a/src/Cat/Displayed/Instances/Identity.lagda.md +++ b/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 : is-discrete-fibration IdD -IdD-discrete-fibration .is-discrete-fibration.fibre-set _ = hlevel 2 -IdD-discrete-fibration .is-discrete-fibration.cart-lift _ _ = 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 From cfceae89645cbb6527376fb0975cfedc7785f7fd Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 16 Jan 2025 18:16:11 -0500 Subject: [PATCH 3/5] def: discrete cocartesian fibrations --- .../Displayed/Cocartesian/Discrete.lagda.md | 282 ++++++++++++++++++ 1 file changed, 282 insertions(+) create mode 100644 src/Cat/Displayed/Cocartesian/Discrete.lagda.md diff --git a/src/Cat/Displayed/Cocartesian/Discrete.lagda.md b/src/Cat/Displayed/Cocartesian/Discrete.lagda.md new file mode 100644 index 000000000..7762fc6a4 --- /dev/null +++ b/src/Cat/Displayed/Cocartesian/Discrete.lagda.md @@ -0,0 +1,282 @@ +--- +description: | + Discrete cocartesian fibrations. +--- + +```agda +module Cat.Displayed.Cocartesian.Discrete where +``` + + + +# Discrete cocartesian fibrations + +:::{.definition #discrete-cocartesian-fibration alias="discrete-fibration"} +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 + 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) +``` + +
+The proofs are formally dual to the cartesian case, so we omit +the details. + + +```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 _ _ _ _ _) +``` +
+ +## 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' +``` + +
+The proof is essentially identical to the [cartesian case], +so we omit the details. + + +[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) _ _ +``` +
+ +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 _ _ +``` + +
+The argument is almost identical to the proof that [all morphisms +in discrete cartesian fibrations are cartesian], so we suppress the details. + + +[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' ∎ +``` +
+ +## 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') +``` From 243143c72ab8065114f0f45fc973db5190fdeecf Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 17 Jan 2025 09:48:17 -0500 Subject: [PATCH 4/5] prose: forgot an "op" --- src/Cat/Displayed/Cocartesian/Discrete.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Displayed/Cocartesian/Discrete.lagda.md b/src/Cat/Displayed/Cocartesian/Discrete.lagda.md index 7762fc6a4..ad6e97cbb 100644 --- a/src/Cat/Displayed/Cocartesian/Discrete.lagda.md +++ b/src/Cat/Displayed/Cocartesian/Discrete.lagda.md @@ -31,7 +31,7 @@ open is-cocartesian # Discrete cocartesian fibrations -:::{.definition #discrete-cocartesian-fibration alias="discrete-fibration"} +:::{.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 From 3c4923dcd6612073179a03c9059ea2c6317f4563 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Fri, 17 Jan 2025 11:22:32 -0500 Subject: [PATCH 5/5] prose: prose fixes --- src/Cat/Displayed/Cartesian/Discrete.lagda.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Cat/Displayed/Cartesian/Discrete.lagda.md b/src/Cat/Displayed/Cartesian/Discrete.lagda.md index a6e8c7033..f4fc2d48f 100644 --- a/src/Cat/Displayed/Cartesian/Discrete.lagda.md +++ b/src/Cat/Displayed/Cartesian/Discrete.lagda.md @@ -195,7 +195,7 @@ also invertible. 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'$. +$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 @@ -300,7 +300,7 @@ fibration]]. r : Cartesian-fibration E ``` -Luckily for us, the sea has already risen to meet us.: by assumption, +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. @@ -337,7 +337,7 @@ module _ {o ℓ} (B : Precategory o ℓ) where 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 cart-lift. +uniqueness of the lifts. ```agda psh : Functor (B ^op) (Sets o') @@ -405,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 cart-lift $(a', f')$. Our functor must, given objects +space of Cartesian lifts $(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'$. @@ -432,7 +432,7 @@ conclude that we've put together a functor. 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, cart-lift are unique, so this +that $a''$ is the chosen lift $a'$. But again, lifts are unique, so this is immediate. ```agda