open import Cat.Displayed.Cartesian
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Univalence.Reasoning
import Cat.Displayed.Univalence
import Cat.Displayed.Reasoning as Dr
import Cat.Displayed.Morphism
import Cat.Reasoning as Cr

module Cat.Displayed.Cartesian.Identity
{o β o' β'} {B : Precategory o β} (E : Displayed B o' β')
where


# Identity of cartesian liftsπ

In this module, we prove that Cartesian morphisms are unique up to vertical isomorphism, which, if the displayed category is univalent (regardless of univalence of the base), can be strengthened to show that the type of Cartesian lifts for a given βcornerβ is a proposition.

private
module B = Cr B

open Cat.Displayed.Univalence.Reasoning E
open Cat.Displayed.Univalence E
open Cat.Displayed.Morphism E
open Displayed E
open Dr E
open _β[_]_


Weβll first observe that if we have two witnesses that is a Cartesian morphism over then the fact that both provide unique solutions to factorisation problems imply that these must be the same solution. Therefore, since the other components are paths, a morphism can be Cartesian in at most one way.

module _ {a b a' b'} (f : B.Hom a b) {f' : Hom[ f ] a' b'}
(cβ cβ : is-cartesian E f f')
where

private
module c1 = is-cartesian cβ
module c2 = is-cartesian cβ

open is-cartesian

private
univ : β {u u'} (m : B.Hom u a) (h' : Hom[ f B.β m ] u' b')
β c1.universal m h' β‘ c2.universal m h'
univ m h' = c2.unique (c1.universal m h') (c1.commutes m h')

Cartesian-is-prop : cβ β‘ cβ
Cartesian-is-prop i .universal m h' = univ m h' i
Cartesian-is-prop i .commutes m h' =
is-propβpathp (Ξ» i β Hom[ f B.β m ]-set _ b' (f' β' univ m h' i) h')
(c1.commutes m h')
(c2.commutes m h') i
Cartesian-is-prop i .unique {h' = h'} m' p =
is-propβpathp (Ξ» i β Hom[ _ ]-set _ a' m' (univ _ h' i))
(c1.unique m' p) (c2.unique m' p) i


Unsurprisingly, thatβs the easier half of the proof. Another quarter of the proof is cartesian-domain-unique, which is in another castle defined in another module. By the construction there, the isomorphism sends to

module _ {a b aβ' aβ' b'} (f : B.Hom a b) {fβ' : Hom[ f ] aβ' b'}
{fβ' : Hom[ f ] aβ' b'} (cβ : is-cartesian E f fβ') (cβ : is-cartesian E f fβ')
where
private
module c1 = is-cartesian cβ
module c2 = is-cartesian cβ

  cartesian-map-uniquep
: (p : f B.β B.id β‘ f) β fβ' β' cartesian-domain-unique E cβ cβ .from' β‘[ p ] fβ'
cartesian-map-uniquep p = to-pathpβ» \$
c1.commutes B.id _ β reindex (sym (B.idr f)) (sym p)

module _ {a b b'} (f : B.Hom a b) (l1 l2 : Cartesian-lift E f b') where
open Cartesian-lift

private
module l1 = Cartesian-lift l1
module l2 = Cartesian-lift l2


Having established that being Cartesian is a property of a morphism, that any pair of Cartesian lifts for the same and have isomorphic domains, and that this isomorphism sends the first morphism to the second, all that remains is putting this together into a tidy proof: If is univalent, the space of Cartesian lifts for is a proposition.

  Cartesian-lift-is-prop : is-category-displayed β l1 β‘ l2
Cartesian-lift-is-prop e-cat = p where
im = cartesian-domain-unique E l1.cartesian l2.cartesian

obp : l1.x' β‘ l2.x'
obp = ββ-identity-system e-cat .to-path im

pres : PathP (Ξ» i β Hom[ f ] (obp i) b') l1.lifting l2.lifting
pres = Hom[]-pathp-refll-iso e-cat (B.idr f) im l1.lifting l2.lifting
(cartesian-map-uniquep f l1.cartesian l2.cartesian (B.idr f))

p : l1 β‘ l2
p i .x'        = obp i
p i .lifting   = pres i
p i .cartesian =
is-propβpathp (Ξ» i β Cartesian-is-prop {a' = obp i} f {f' = pres i})
l1.cartesian l2.cartesian i