(** ** 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.Induction.FunctorCoalgebras_legacy.
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). (* can be coerced to a function *)
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)
*)
(* We use "refine (x @ _)" instead of "rewrite" for more predictable proof terms. *)
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 : forall {X Y : UU} {F : UU → UU} {f : X → F X} {g : Y → F Y}
(p : X = Y),
(forall (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 :
forall {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 : forall 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.