module Cat.Displayed.Cartesian.Identity
  {o β„“ o' β„“'} {B : Precategory o β„“} (E : Displayed B o' β„“')

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.

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')

    module c1 = is-cartesian c₁
    module c2 = is-cartesian cβ‚‚

  open is-cartesian

    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

    : (p : f B.∘ ≑ f) β†’ f₁' ∘' cartesian-domain-unique E c₁ cβ‚‚ .from' ≑[ p ] fβ‚‚'
  cartesian-map-uniquep p = to-pathp⁻ $
    c1.commutes _ βˆ™ reindex (sym (B.idr f)) (sym p)

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