Library UniMath.Induction.M.Uniqueness

Uniqueness of M-types

M-types are unique up to propositional equality.
Author: Langston Barrett (@siddharthist)

Require Import UniMath.Foundations.PartD.
Require Import UniMath.MoreFoundations.Univalence.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCoalgebras.
Require Import UniMath.CategoryTheory.categories.Type.Core.
Require Import UniMath.Induction.PolynomialFunctors.
Require Import UniMath.Induction.M.Core.

Section Uniqueness.

  Local Open Scope functions.
  Local Open Scope cat.

  Context (A : UU).
  Context (B : A → UU).

Following the paper, we have X ⇒ Y = Hom(X, Y)
  Local Notation F := (polynomial_functor A B).   Local Notation "F*" := (polynomial_functor_arr A B).
  Local Notation "X ⇒ Y" := (coalgebra_homo F X Y).

Since we can't use the standard categorical proof, we must re-prove that final coalgebras are unique up to isomorphism.
(Lemma 5 in Ahrens, Capriotti, and Spadotti)
We prove that their carriers (first projections) are isomorphic, and hence equal (by univalence).
This is standard categorical reasoning: each has exactly one arrow to the other, which, composing, gives an endormorphism. However, each has exactly one endomorphism, the identity map. Therefore, they are isomorphic.

  Lemma M_carriers_iso : ∏ X Y : M B, (coalgebra_ob _ X) ≃
                                      (coalgebra_ob _ Y).
  Proof.
    intros X Y.

Get the coalgebra morphisms X → Y and Y → X via finality
    pose (X_mor_Y := iscontrpr1 (pr2 Y X)).
    pose (Y_mor_X := iscontrpr1 (pr2 X Y)).

    apply (weq_iso
             (mor_from_coalgebra_homo _ _ _ X_mor_Y)
             (mor_from_coalgebra_homo _ _ _ Y_mor_X)).
    - intro x.
      apply (@eqtohomot _ _ (Y_mor_X ∘ X_mor_Y) (idfun _)).
      refine (base_paths (coalgebra_homo_comp _ _ _ _ X_mor_Y Y_mor_X)
                         (coalgebra_homo_id F X) _).
      apply (proofirrelevancecontr (pr2 X X)).
    - intro y.
      apply (@eqtohomot _ _ (X_mor_Y ∘ Y_mor_X) (idfun _)).
      refine (base_paths (coalgebra_homo_comp _ _ _ _ Y_mor_X X_mor_Y)
                         (coalgebra_homo_id F Y) _).
      apply (proofirrelevancecontr (pr2 Y Y)).
  Defined.

Note the crucial use of univalence
  Lemma M_carriers_eq : ∏ X Y : M B, (coalgebra_ob _ X) = (coalgebra_ob _ Y).
  Proof.
    exact (fun X Y ⇒ weqtopaths (M_carriers_iso X Y)).
  Defined.

Now we must prove that the coalgebra morphisms, when transported along the path M_carriers_eq, will be equal.
(≅⇒≡ in HoTT/M-types)

  Lemma M_coalg_eq : ∏ X Y : M B, M_coalgebra B X = M_coalgebra B Y.
  Proof.
    intros X Y.
    pose (π1eq := (M_carriers_eq X Y)).
    pose (f := pr1 ((pr2 Y) (M_coalgebra B X))).
    apply (total2_paths_f π1eq).

Some shorthands for items we'll use
    pose (is_final_X := pr2 X).
    pose (is_final_Y := pr2 Y).
    pose (θ := pr2 (pr1 X)).
    pose (ψ := pr2 (pr1 Y)).

substⁱ-lemma in HoTT/M-types
    assert (trans_fun : ∀ {X Y : UU} {F : UU → UU} {f : X → F X} {g : Y → F Y}
                          (p : X = Y),
               (∀ (x : X), transportf F p (f x) = g (transportf (idfun UU) p x)) →
               transportf (λ X, X → F X) p f = g).
    {
      intros ? ? ? ? ? p H.
      induction p.
      unfold transportf.
      apply funextfun.
      exact H.
    }

    apply trans_fun.
    intro x.

imap-subst in HoTT/M-types
    assert (arr_transport :
              ∀ {X Y : UU} (p : X = Y),
                F× (transportf (idfun _) p) = transportf F p).
    {
      intros ? ? p.
      induction p.
      reflexivity.
    }

    
In HoTT/M-types: lemma₁ : ∀ i x → subst (λ Z → Z i) π₁≡ x ≡ proj₁ f i x
    assert (lemma1 : ∀ x : pr1 (pr1 X), transportf (idfun UU) π1eq x = (pr1 f) x).
    {
      intro.
      refine (toforallpaths _ _ _ _ x0).
      refine ((weqpath_transport (M_carriers_iso _ Y)) @ _).
      reflexivity.
    }

    
lemma₂ in HoTT/M-types
    assert (lemma2 : transportf F π1eq = F× (pr1 f)).
    {
      refine (!(arr_transport _ _ π1eq) @ _).
      apply maponpaths.
      unfold π1eq, M_carriers_eq.
      refine ((weqpath_transport (M_carriers_iso _ _)) @ _).
      reflexivity.
    }

    refine (_ @ !(maponpaths ψ (lemma1 x))).
    refine (toforallpaths _ (transportf F π1eq) (F× (pr1 f)) lemma2 (θ x) @ _).

Now our goal is simply the condition that f is a coalgebra morphism
    apply (toforallpaths _ (F× (pr1 f) ∘ θ) (ψ ∘ pr1 f)).
    exact (pr2 f).
  Defined.

  Lemma isaprop_M : isaprop (M B).
    apply invproofirrelevance.
    intros X Y.
    apply subtypePath.
    - exact isaprop_is_final.
    - exact (M_coalg_eq X Y).
  Defined.
End Uniqueness.