Library UniMath.Induction.M.Core

M-types

The M-type associated to (A, B) is the final coalgebra of the associated polynomial functor.

We can't use (1) the definition of Terminal, because we can't use (2) that (co)algebras and their morphisms form a precategory, because this is only true when the base category has homsets, which UU doesn't. Therefore, we must redefine what it means to be a final coalgebra here without categorical language.

(Definition 4 in Ahrens, Capriotti, and Spadotti) (IsFinal in HoTT/M-types)

Author: Langston Barrett (@siddharthist)

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).
Show proof.

    apply impred.
    intro.
    apply isapropiscontr.

  Lemma is_prefinal_to_is_final (X : coalgebra F) :
    is_prefinal X -> (∏ Y, isaprop (coalgebra_homo F Y X)) -> is_final X.
  Show proof.

exact (λ is_pre is_prop Y, iscontraprop1 (is_prop Y) (is_pre Y)).

  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 {_ _} _.