Library UniMath.Bicategories.Morphisms.ExtensionsAndLiftings

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.Bicategories.Core.Bicat.
Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.OpMorBicat.
Require Import UniMath.Bicategories.Core.Examples.OpCellBicat.

Local Open Scope cat.

Section LeftExtension.
  Context {B : bicat}
          {x y z : B}
          (f : x --> z)
          (g : x --> y).

  Definition is_left_extension
             {h : y --> z}
             (τ : f ==> g · h)
    : UU
    := ∏ (k : y --> z), isweq (λ (θ : h ==> k), τ • (g ◃ θ)).

  Section Projections.
    Context {h : y --> z}
            {τ : f ==> g · h}
            (Hτ : is_left_extension τ).

    Definition is_left_extension_extend
               {k : y --> z}
               (θ : f ==> g · k)
      : h ==> k
      := invmap (make_weq _ (Hτ k)) θ.

    Proposition is_left_extension_extend_left
                {k : y --> z}
                (θ : h ==> k)
      : is_left_extension_extend (τ • (g ◃ θ)) = θ.
    Show proof.

    Proposition is_left_extension_extend_right
                {k : y --> z}
                (θ : f ==> g · k)
      : τ • (g ◃ is_left_extension_extend θ) = θ.
    Show proof.
  End Projections.

  Proposition make_is_left_extension
              {h : y --> z}
              (τ : f ==> g · h)
              (F : ∏ (k : y --> z) (θ : f ==> g · k), h ==> k)
              (HF₁ : ∏ (k : y --> z) (θ : h ==> k), F k (τ • (g ◃ θ)) = θ)
              (HF₂ : ∏ (k : y --> z) (θ : f ==> g · k), τ • (g ◃ F k θ) = θ)
    : is_left_extension τ.
  Show proof.

  Proposition isaprop_is_left_extension
              {h : y --> z}
              (τ : f ==> g · h)
    : isaprop (is_left_extension τ).
  Show proof.

  Definition left_extension
    : UU
    := ∑ (h : y --> z)
         (τ : f ==> g · h),
       is_left_extension τ.

  Coercion mor_of_left_extension
           (h : left_extension)
    : y --> z
    := pr1 h.

  Definition cell_of_left_extension
             (h : left_extension)
    : f ==> g · h
    := pr12 h.

  Coercion left_extension_is_left_extension
           (h : left_extension)
    : is_left_extension (cell_of_left_extension h)
    := pr22 h.
End LeftExtension.

Definition preserves_is_left_extension
           {B : bicat}
           {x y z a : B}
           {f : x --> z}
           {g : x --> y}
           (k : z --> a)
           {h : y --> z}
           {τ : f ==> g · h}
           (Hτ : is_left_extension f g τ)
  : UU
  := is_left_extension (f · k) g ((τ ▹ k) • rassociator _ _ _).

Proposition isaprop_preserves_is_left_extension
            {B : bicat}
            {x y z a : B}
            {f : x --> z}
            {g : x --> y}
            (k : z --> a)
            {h : y --> z}
            {τ : f ==> g · h}
            (Hτ : is_left_extension f g τ)
  : isaprop (preserves_is_left_extension k Hτ).
Show proof.

Definition is_absolute_left_extension
           {B : bicat}
           {x y z : B}
           {f : x --> z}
           {g : x --> y}
           {h : y --> z}
           {τ : f ==> g · h}
           (Hτ : is_left_extension f g τ)
  : UU
  := ∏ (a : B)
       (k : z --> a),
     preserves_is_left_extension k Hτ.

Proposition isaprop_is_absolute_left_extension
            {B : bicat}
            {x y z : B}
            {f : x --> z}
            {g : x --> y}
            {h : y --> z}
            {τ : f ==> g · h}
            (Hτ : is_left_extension f g τ)
  : isaprop (is_absolute_left_extension Hτ).
Show proof.

Section LeftLifting.
  Context {B : bicat}
          {x y z : B}
          (f : z --> x)
          (g : y --> x).

  Definition is_left_lifting
             {h : z --> y}
             (τ : f ==> h · g)
    : UU
    := ∏ (k : z --> y), isweq (λ (θ : h ==> k), τ • (θ ▹ g)).

  Section Projections.
    Context {h : z --> y}
            {τ : f ==> h · g}
            (Hτ : is_left_lifting τ).

    Definition is_left_lifting_lift
               {k : z --> y}
               (θ : f ==> k · g)
      : h ==> k
      := invmap (make_weq _ (Hτ k)) θ.

    Proposition is_left_lifting_lift_left
                {k : z --> y}
                (θ : h ==> k)
      : is_left_lifting_lift (τ • (θ ▹ g)) = θ.
    Show proof.

    Proposition is_left_lifting_lift_right
                {k : z --> y}
                (θ : f ==> k · g)
      : τ • (is_left_lifting_lift θ ▹ g) = θ.
    Show proof.
  End Projections.

  Proposition make_is_left_lifting
              {h : z --> y}
              (τ : f ==> h · g)
              (F : ∏ (k : z --> y) (θ : f ==> k · g), h ==> k)
              (HF₁ : ∏ (k : z --> y) (θ : h ==> k), F k (τ • (θ ▹ g)) = θ)
              (HF₂ : ∏ (k : z --> y) (θ : f ==> k · g), τ • (F k θ ▹ g) = θ)
    : is_left_lifting τ.
  Show proof.

  Proposition isaprop_is_left_lifting
              {h : z --> y}
              (τ : f ==> h · g)
    : isaprop (is_left_lifting τ).
  Show proof.

  Definition left_lifting
    : UU
    := ∑ (h : z --> y)
         (τ : f ==> h · g),
       is_left_lifting τ.

  Coercion mor_of_left_lifting
           (h : left_lifting)
    : z --> y
    := pr1 h.

  Definition cell_of_left_lifting
             (h : left_lifting)
    : f ==> h · g
    := pr12 h.

  Coercion left_lifting_is_left_lifting
           (h : left_lifting)
    : is_left_lifting (cell_of_left_lifting h)
    := pr22 h.
End LeftLifting.

Definition preserves_is_left_lifting
           {B : bicat}
           {x y z a : B}
           {f : z --> x}
           {g : y --> x}
           (k : a --> z)
           {h : z --> y}
           {τ : f ==> h · g}
           (Hτ : is_left_lifting f g τ)
  : UU
  := is_left_lifting (k · f) g ((k ◃ τ) • lassociator _ _ _).

Proposition isaprop_preserves_is_left_lifting
            {B : bicat}
            {x y z a : B}
            {f : z --> x}
            {g : y --> x}
            (k : a --> z)
            {h : z --> y}
            {τ : f ==> h · g}
            (Hτ : is_left_lifting f g τ)
  : isaprop (preserves_is_left_lifting k Hτ).
Show proof.

Definition is_absolute_left_lifting
           {B : bicat}
           {x y z : B}
           {f : z --> x}
           {g : y --> x}
           {h : z --> y}
           {τ : f ==> h · g}
           (Hτ : is_left_lifting f g τ)
  : UU
  := ∏ (a : B)
       (k : a --> z),
     preserves_is_left_lifting k Hτ.

Proposition isaprop_is_absolute_left_lifting
            {B : bicat}
            {x y z : B}
            {f : z --> x}
            {g : y --> x}
            {h : z --> y}
            {τ : f ==> h · g}
            (Hτ : is_left_lifting f g τ)
  : isaprop (is_absolute_left_lifting Hτ).
Show proof.

Definition is_left_extension_weq_is_left_lifting_op
           {B : bicat}
           {x y z : B}
           (f : z --> x)
           (g : y --> x)
           {h : z --> y}
           (τ : f ==> h · g)
  : is_left_lifting _ _ τ
    ≃
    @is_left_extension (op1_bicat B) x y z f g h τ.
Show proof.

Definition preserves_is_left_extension_weq_preserves_is_left_lifting_op
           {B : bicat}
           {x y z a : B}
           {f : z --> x}
           {g : y --> x}
           (k : a --> z)
           {h : z --> y}
           {τ : f ==> h · g}
           (Hτ : is_left_lifting f g τ)
  : preserves_is_left_lifting k Hτ
    ≃
    @preserves_is_left_extension (op1_bicat B) _ _ _ _ _ _ k _ _ Hτ.
Show proof.

Definition is_absolute_left_extension_weq_is_absolute_left_lifting_op
           {B : bicat}
           {x y z : B}
           {f : z --> x}
           {g : y --> x}
           {h : z --> y}
           {τ : f ==> h · g}
           (Hτ : is_left_lifting f g τ)
  : is_absolute_left_lifting Hτ
    ≃
    @is_absolute_left_extension (op1_bicat B) _ _ _ _ _ _ _ Hτ.
Show proof.

Section RightExtension.
  Context {B : bicat}
          {x y z : B}
          (f : x --> z)
          (g : x --> y).

  Definition is_right_extension
             {h : y --> z}
             (τ : g · h ==> f)
    : UU
    := ∏ (k : y --> z), isweq (λ (θ : k ==> h), (g ◃ θ) • τ).

  Section Projections.
    Context {h : y --> z}
            {τ : g · h ==> f}
            (Hτ : is_right_extension τ).

    Definition is_right_extension_extend
               {k : y --> z}
               (θ : g · k ==> f)
      : k ==> h
      := invmap (make_weq _ (Hτ k)) θ.

    Proposition is_right_extension_extend_left
                {k : y --> z}
                (θ : k ==> h)
      : is_right_extension_extend ((g ◃ θ) • τ) = θ.
    Show proof.

    Proposition is_right_extension_extend_right
                {k : y --> z}
                (θ : g · k ==> f)
      : (g ◃ is_right_extension_extend θ) • τ = θ.
    Show proof.
  End Projections.

  Proposition make_is_right_extension
              {h : y --> z}
              (τ : g · h ==> f)
              (F : ∏ (k : y --> z) (θ : g · k ==> f), k ==> h)
              (HF₁ : ∏ (k : y --> z) (θ : k ==> h), F k ((g ◃ θ) • τ) = θ)
              (HF₂ : ∏ (k : y --> z) (θ : g · k ==> f), (g ◃ F k θ) • τ = θ)
    : is_right_extension τ.
  Show proof.

  Proposition isaprop_is_right_extension
              {h : y --> z}
              (τ : g · h ==> f)
    : isaprop (is_right_extension τ).
  Show proof.

  Definition right_extension
    : UU
    := ∑ (h : y --> z)
         (τ : g · h ==> f),
       is_right_extension τ.

  Coercion mor_of_right_extension
           (h : right_extension)
    : y --> z
    := pr1 h.

  Definition cell_of_right_extension
             (h : right_extension)
    : g · h ==> f
    := pr12 h.

  Coercion right_extension_is_right_extension
           (h : right_extension)
    : is_right_extension (cell_of_right_extension h)
    := pr22 h.
End RightExtension.

Definition preserves_is_right_extension
           {B : bicat}
           {x y z a : B}
           {f : x --> z}
           {g : x --> y}
           (k : z --> a)
           {h : y --> z}
           {τ : g · h ==> f}
           (Hτ : is_right_extension f g τ)
  : UU
  := is_right_extension (f · k) g (lassociator _ _ _ • (τ ▹ k)).

Proposition isaprop_preserves_is_right_extension
            {B : bicat}
            {x y z a : B}
            {f : x --> z}
            {g : x --> y}
            (k : z --> a)
            {h : y --> z}
            {τ : g · h ==> f}
            (Hτ : is_right_extension f g τ)
  : isaprop (preserves_is_right_extension k Hτ).
Show proof.

Definition is_absolute_right_extension
           {B : bicat}
           {x y z : B}
           {f : x --> z}
           {g : x --> y}
           {h : y --> z}
           {τ : g · h ==> f}
           (Hτ : is_right_extension f g τ)
  : UU
  := ∏ (a : B)
       (k : z --> a),
     preserves_is_right_extension k Hτ.

Proposition isaprop_is_absolute_right_extension
            {B : bicat}
            {x y z : B}
            {f : x --> z}
            {g : x --> y}
            {h : y --> z}
            {τ : g · h ==> f}
            (Hτ : is_right_extension f g τ)
  : isaprop (is_absolute_right_extension Hτ).
Show proof.

Definition is_left_extension_weq_is_right_extension_co
           {B : bicat}
           {x y z : B}
           (f : x --> z)
           (g : x --> y)
           {h : y --> z}
           (τ : g · h ==> f)
  : is_right_extension f g τ
    ≃
    @is_left_extension (op2_bicat B) x y z f g h τ.
Show proof.

Definition preserves_is_left_extension_weq_preserves_is_right_extension_co
           {B : bicat}
           {x y z a : B}
           {f : x --> z}
           {g : x --> y}
           (k : z --> a)
           {h : y --> z}
           {τ : g · h ==> f}
           (Hτ : is_right_extension f g τ)
  : preserves_is_right_extension k Hτ
    ≃
    @preserves_is_left_extension (op2_bicat B) _ _ _ _ _ _ k _ _ Hτ.
Show proof.

Definition is_absolute_left_extension_weq_is_absolute_right_extension_op
           {B : bicat}
           {x y z : B}
           {f : x --> z}
           {g : x --> y}
           {h : y --> z}
           {τ : g · h ==> f}
           (Hτ : is_right_extension f g τ)
  : is_absolute_right_extension Hτ
    ≃
    @is_absolute_left_extension (op2_bicat B) _ _ _ _ _ _ _ Hτ.
Show proof.

Section RightLifting.
  Context {B : bicat}
          {x y z : B}
          (f : z --> x)
          (g : y --> x).

  Definition is_right_lifting
             {h : z --> y}
             (τ : h · g ==> f)
    : UU
    := ∏ (k : z --> y), isweq (λ (θ : k ==> h), (θ ▹ g) • τ).

  Section Projections.
    Context {h : z --> y}
            {τ : h · g ==> f}
            (Hτ : is_right_lifting τ).

    Definition is_right_lifting_lift
               {k : z --> y}
               (θ : k · g ==> f)
      : k ==> h
      := invmap (make_weq _ (Hτ k)) θ.

    Proposition is_right_lifting_lift_left
                {k : z --> y}
                (θ : k ==> h)
      : is_right_lifting_lift ((θ ▹ g) • τ) = θ.
    Show proof.

    Proposition is_right_lifting_lift_right
                {k : z --> y}
                (θ : k · g ==> f)
      : (is_right_lifting_lift θ ▹ g) • τ = θ.
    Show proof.
  End Projections.

  Proposition make_is_right_lifting
              {h : z --> y}
              (τ : h · g ==> f)
              (F : ∏ (k : z --> y) (θ : k · g ==> f), k ==> h)
              (HF₁ : ∏ (k : z --> y) (θ : k ==> h), F k ((θ ▹ g) • τ) = θ)
              (HF₂ : ∏ (k : z --> y) (θ : k · g ==> f), (F k θ ▹ g) • τ = θ)
    : is_right_lifting τ.
  Show proof.

  Proposition isaprop_is_right_lifting
              {h : z --> y}
              (τ : h · g ==> f)
    : isaprop (is_right_lifting τ).
  Show proof.

  Definition right_lifting
    : UU
    := ∑ (h : z --> y)
         (τ : h · g ==> f),
       is_right_lifting τ.

  Coercion mor_of_right_lifting
           (h : right_lifting)
    : z --> y
    := pr1 h.

  Definition cell_of_right_lifting
             (h : right_lifting)
    : h · g ==> f
    := pr12 h.

  Coercion right_lifting_is_left_lifting
           (h : right_lifting)
    : is_right_lifting (cell_of_right_lifting h)
    := pr22 h.
End RightLifting.

Definition preserves_is_right_lifting
           {B : bicat}
           {x y z a : B}
           {f : z --> x}
           {g : y --> x}
           (k : a --> z)
           {h : z --> y}
           {τ : h · g ==> f}
           (Hτ : is_right_lifting f g τ)
  : UU
  := is_right_lifting (k · f) g (rassociator _ _ _ • (k ◃ τ)).

Proposition isaprop_preserves_is_right_lifting
            {B : bicat}
            {x y z a : B}
            {f : z --> x}
            {g : y --> x}
            (k : a --> z)
            {h : z --> y}
            {τ : h · g ==> f}
            (Hτ : is_right_lifting f g τ)
  : isaprop (preserves_is_right_lifting k Hτ).
Show proof.

Definition is_absolute_right_lifting
           {B : bicat}
           {x y z : B}
           {f : z --> x}
           {g : y --> x}
           {h : z --> y}
           {τ : h · g ==> f}
           (Hτ : is_right_lifting f g τ)
  : UU
  := ∏ (a : B)
       (k : a --> z),
     preserves_is_right_lifting k Hτ.

Proposition isaprop_is_absolute_right_lifting
            {B : bicat}
            {x y z : B}
            {f : z --> x}
            {g : y --> x}
            {h : z --> y}
            {τ : h · g ==> f}
            (Hτ : is_right_lifting f g τ)
  : isaprop (is_absolute_right_lifting Hτ).
Show proof.

Definition is_left_extension_weq_is_right_lifting_coop
           {B : bicat}
           {x y z : B}
           (f : z --> x)
           (g : y --> x)
           {h : z --> y}
           (τ : h · g ==> f)
  : is_right_lifting f g τ
    ≃
    @is_left_extension (op2_bicat (op1_bicat B)) x y z f g h τ.
Show proof.

Definition preserves_is_left_extension_weq_preserves_is_right_lifting_coop
           {B : bicat}
           {x y z a : B}
           {f : z --> x}
           {g : y --> x}
           (k : a --> z)
           {h : z --> y}
           {τ : h · g ==> f}
           (Hτ : is_right_lifting f g τ)
  : preserves_is_right_lifting k Hτ
    ≃
    @preserves_is_left_extension (op2_bicat (op1_bicat B)) _ _ _ _ _ _ k _ _ Hτ.
Show proof.

Definition is_absolute_left_extension_weq_is_absolute_right_lifting_coop
           {B : bicat}
           {x y z : B}
           {f : z --> x}
           {g : y --> x}
           {h : z --> y}
           {τ : h · g ==> f}
           (Hτ : is_right_lifting f g τ)
  : is_absolute_right_lifting Hτ
    ≃
    @is_absolute_left_extension (op2_bicat (op1_bicat B)) _ _ _ _ _ _ _ Hτ.
Show proof.