Library UniMath.Induction.M.Core
M-types
Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.FunctorCoalgebras.
Require Import UniMath.Induction.PolynomialFunctors.
Section M.
Context {A : UU} (B : A → UU).
Local Notation F := (polynomial_functor A B).
Definition is_prefinal (X : coalgebra F) :=
∏ (Y : coalgebra F), coalgebra_homo F Y X.
Definition is_final (X : coalgebra F) :=
∏ (Y : coalgebra F), iscontr (coalgebra_homo F Y X).
prop-IsFinal in HoTT/M-types
Definition isaprop_is_final (X : coalgebra F) : isaprop (is_final X).
Proof.
apply impred.
intro.
apply isapropiscontr.
Defined.
Lemma is_prefinal_to_is_final (X : coalgebra F) :
is_prefinal X → (∏ Y, isaprop (coalgebra_homo F Y X)) → is_final X.
Proof.
exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)).
Defined.
Definition M := ∑ (X : coalgebra F), is_final X.
Definition M_coalgebra : M → coalgebra F := pr1.
Definition M_is_final : ∏ (m : M), is_final (pr1 m) := pr2.
Coercion M_coalgebra : M >-> coalgebra.
End M.
Arguments isaprop_is_final {_ _} _.
Arguments is_prefinal {_ _} _.
Arguments is_final {_ _} _.
Proof.
apply impred.
intro.
apply isapropiscontr.
Defined.
Lemma is_prefinal_to_is_final (X : coalgebra F) :
is_prefinal X → (∏ Y, isaprop (coalgebra_homo F Y X)) → is_final X.
Proof.
exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)).
Defined.
Definition M := ∑ (X : coalgebra F), is_final X.
Definition M_coalgebra : M → coalgebra F := pr1.
Definition M_is_final : ∏ (m : M), is_final (pr1 m) := pr2.
Coercion M_coalgebra : M >-> coalgebra.
End M.
Arguments isaprop_is_final {_ _} _.
Arguments is_prefinal {_ _} _.
Arguments is_final {_ _} _.