open import Cat.Instances.Shape.Interval
open import Cat.Morphism.Class
open import Cat.Prelude

import Cat.Reasoning
module Cat.Morphism.Lifts where

Lifting properties of morphismsπŸ”—

private module Impl {o β„“} {C : Precategory o β„“} where
  open Precategory C
  private
    variable
      a b c d x y : ⌞ C ⌟
      f g h u v : Hom a b

Let be a square of morphisms fitting into a commutative square like so:

A lifting of such a square is a morphism such that and 

  Lifting
    : (f : Hom a b) (g : Hom x y) (u : Hom a x) (v : Hom b y)
    β†’ Type _
  Lifting {a} {b} {x} {y} f g u v = Ξ£[ w ∈ Hom b x ] w ∘ f ≑ u Γ— g ∘ w ≑ v

Let be two morphisms of We say that left lifts against and right lifts against if for every commutative square

there merely exists a lifting

We can also talk about objects with left or right lifting properties. An object left lifts against a morphism if for every cospan there merely exists a map with

Similarly, an object right lifts against a morphism if for every span there merely exists a map with

Finally, we say that a class of morphisms lifts against another class of morphisms when every lifts against every Note that we can also consider liftings of objects/morphisms against classes of morphisms, but we will leave the reader to fill in the definitions.

Note

In the formalisation, we will write Lifts to denote all of the aforementioned lifting properties.

  record Lifts-against
    {β„“l β„“r}
    (L : Type β„“l) (R : Type β„“r)
    (β„“p : Level)
    : Type (β„“l βŠ” β„“r βŠ” (lsuc β„“p)) where
    field
      lifts-prop : L β†’ R β†’ Type β„“p
      orthogonal-prop : L β†’ R β†’ Type β„“p

  open Lifts-against

  Lifts
    : βˆ€ {β„“l β„“r β„“p} {L : Type β„“l} {R : Type β„“r}
    β†’ L β†’ R β†’ ⦃ _ :  Lifts-against L R β„“p ⦄ β†’ Type _
  Lifts l r ⦃ Lifts ⦄ = Lifts .lifts-prop l r

  Orthogonal
    : βˆ€ {β„“l β„“r β„“p} {L : Type β„“l} {R : Type β„“r}
    β†’ L β†’ R β†’ ⦃ _ :  Lifts-against L R β„“p ⦄ β†’ Type _
  Orthogonal l r ⦃ Lifts ⦄ = Lifts .orthogonal-prop l r

  instance
    Lifts-against-hom-hom : βˆ€ {a b x y} β†’ Lifts-against (Hom a b) (Hom x y) β„“
    Lifts-against-hom-hom .lifts-prop f g = βˆ€ u v β†’ v ∘ f ≑ g ∘ u β†’ βˆ₯ Lifting f g u v βˆ₯
    Lifts-against-hom-hom .orthogonal-prop f g = βˆ€ u v β†’ v ∘ f ≑ g ∘ u β†’ is-contr (Lifting f g u v)

    Lifts-against-ob-hom : βˆ€ {x y} β†’ Lifts-against Ob (Hom x y) β„“
    Lifts-against-ob-hom {x} {y} .lifts-prop a f = βˆ€ (u : Hom a y) β†’ βˆ₯ Ξ£[ h ∈ Hom a x ] f ∘ h ≑ u βˆ₯
    Lifts-against-ob-hom {x} {y} .orthogonal-prop a f = βˆ€ (u : Hom a y) β†’ is-contr (Ξ£[ h ∈ Hom a x ] f ∘ h ≑ u)

    Lifts-against-hom-ob : βˆ€ {a b} β†’ Lifts-against (Hom a b) Ob β„“
    Lifts-against-hom-ob {a} {b} .lifts-prop f x = βˆ€ (u : Hom a x) β†’ βˆ₯ Ξ£[ h ∈ Hom b x ] h ∘ f ≑ u βˆ₯
    Lifts-against-hom-ob {a} {b} .orthogonal-prop f x = βˆ€ (u : Hom a x) β†’ is-contr (Ξ£[ h ∈ Hom b x ] h ∘ f ≑ u)

    -- We need an INCOHERENT here to avoid competing instances for
    -- 'Lifts L R' when 'L, R : Arrows C'. We prefer to use the left instance first, as that
    -- will lay out our arguments left-to-right.
    Lifts-against-arrows-left
      : βˆ€ {β„“r β„“p ΞΊ} {R : Type β„“r}
      β†’ ⦃ _ : βˆ€ {a b} β†’ Lifts-against (Hom a b) R β„“p ⦄
      β†’ Lifts-against (Arrows C ΞΊ) R (o βŠ” β„“ βŠ” β„“p βŠ” ΞΊ)
    Lifts-against-arrows-left .lifts-prop L r = βˆ€ {a b} β†’ (f : Hom a b) β†’ f ∈ L β†’ Lifts f r
    Lifts-against-arrows-left .orthogonal-prop L r = βˆ€ {a b} β†’ (f : Hom a b) β†’ f ∈ L β†’ Orthogonal f r

    Lifts-against-arrows-right
      : βˆ€ {β„“l β„“p ΞΊ} {L : Type β„“l}
      β†’ ⦃ _ : βˆ€ {x y} β†’ Lifts-against L (Hom x y) β„“p ⦄
      β†’ Lifts-against L (Arrows C ΞΊ) (o βŠ” β„“ βŠ” β„“p βŠ” ΞΊ)
    Lifts-against-arrows-right .lifts-prop l R = βˆ€ {x y} β†’ (f : Hom x y) β†’ f ∈ R β†’ Lifts l f
    Lifts-against-arrows-right .orthogonal-prop l R = βˆ€ {x y} β†’ (f : Hom x y) β†’ f ∈ R β†’ Orthogonal l f
    {-# INCOHERENT Lifts-against-arrows-right #-}

open Impl hiding (Lifts; Orthogonal; Lifting) public
module _ {o β„“} (C : Precategory o β„“) where open Impl {C = C} using (Lifts ; Orthogonal ; Lifting) public

module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C
  private
    module Arr = Cat.Reasoning (Arr C)
    variable
      a b c d x y : ⌞ C ⌟
      f g h u v : Hom a b

Basic properties of liftingsπŸ”—

Invertible morphisms have left and right liftings against all morphisms.

  invertible-left-lifts : Lifts C Isos g
  invertible-right-lifts : Lifts C f Isos

Consider a square like the one below with invertible.

The composite fits perfectly along the diagonal, and some short calculations show that both triangles commute.

  invertible-left-lifts f f-inv u v vf=gu =
    pure (u ∘ f.inv , cancelr f.invr , pulll (sym vf=gu) βˆ™ cancelr f.invl)
    where module f = is-invertible f-inv
The proof for right lifts is formally dual. 
  invertible-right-lifts g g-inv u v vf=gu =
    pure (g.inv ∘ v , pullr vf=gu βˆ™ cancell g.invr , cancell g.invl)
    where module g = is-invertible g-inv

If both and left lift against some then so does 

  ∘l-lifts-against : Lifts C f h β†’ Lifts C g h β†’ Lifts C (f ∘ g) h

Showing that lifts against amounts to finding a diagonal for the rectangle

under the assumption that Our first move is to re-orient the square and use lifting property to find a map with and

The bottom triangle of the above diagram can be arranged as a square with on the right and on the left, which lets us use lifting property to find a map

If we place along the diagonal of our original square, we can see that and 

  ∘l-lifts-against {f = f} f-lifts g-lifts u v vfg=hu = do
    (w , wg=u , hw=vf) ← g-lifts u (v ∘ f) (reassocl.from vfg=hu)
    (t , tf=w , ht=v)  ← f-lifts w v (sym hw=vf)
    pure (t , pulll tf=w βˆ™ wg=u , ht=v)

Dually, if and both right lift against a morphism then so does 

  ∘r-lifts-against : Lifts C f g β†’ Lifts C f h β†’ Lifts C f (g ∘ h)
The proof follows the exact same trajectory as the left case, so we will spare the reader the details. 
  ∘r-lifts-against {h = h} f-lifts g-lifts u v ve=fgu = do
    (w , we=gu , fw=v) ← f-lifts (h ∘ u) v (reassocr.to ve=fgu)
    (t , te=u , gt=w)  ← g-lifts u w we=gu
    pure (t , te=u , pullr gt=w βˆ™ fw=v)

For the next few lemmas, consider a square of the following form, where and are both lifts of the outer square

  ∘l-lifts-class : βˆ€ {ΞΊ} (R : Arrows C ΞΊ) β†’ Lifts C f R β†’ Lifts C g R β†’ Lifts C (f ∘ g) R
  ∘l-lifts-class R f-lifts g-lifts r r∈R = ∘l-lifts-against (f-lifts r r∈R) (g-lifts r r∈R)

  ∘r-lifts-class : βˆ€ {ΞΊ} (L : Arrows C ΞΊ) β†’ Lifts C L f β†’ Lifts C L g β†’ Lifts C L (f ∘ g)
  ∘r-lifts-class L f-lifts g-lifts l l∈L = ∘r-lifts-against (f-lifts l l∈L) (g-lifts l l∈L)

If is an epimorphism, then In more succinct terms, the type of lifts of such a square is a proposition.

  left-epic→lift-is-prop
    : is-epic f β†’ v ∘ f ≑ g ∘ u β†’ is-prop (Lifting C f g u v)
  left-epic→lift-is-prop f-epi vf=gu (l , lf=u , _) (k , kf=u , _) = Σ-prop-path! $
    f-epi l k (lf=u βˆ™ sym kf=u)

Dually, if is a monomorphism, then we the type of lifts is also a proposition.

  right-monic→lift-is-prop
    : is-monic g β†’ v ∘ f ≑ g ∘ u β†’ is-prop (Lifting C f g u v)
  right-monic→lift-is-prop g-mono vf=gu (l , _ , gl=v) (k , _ , gk=v) =
    Ξ£-prop-path! (g-mono l k (gl=v βˆ™ sym gk=v))