Library UniMath.CategoryTheory.limits.terminal

Direct definition of terminal object together with:

A proof that the terminal object is a property in a (saturated/univalent) category (isaprop_Terminal)
Construction of the terminal object from the empty product (terminal_from_empty_product)

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.Monics.

Local Open Scope cat.

Section def_terminal.

Context {C : precategory}.

Definition isTerminal (b : C) : UU := ∏ a : C, iscontr (a --> b).

Definition Terminal : UU := ∑ a, isTerminal a.

Definition TerminalObject (T : Terminal) : C := pr1 T.
Coercion TerminalObject : Terminal >-> ob.

Definition TerminalArrow (T : Terminal) (b : C) : b --> T := pr1 (pr2 T b).

Lemma TerminalArrowUnique {T : Terminal} {a : C} (f : C⟦a,TerminalObject T⟧) :
f = TerminalArrow T _.
Show proof.

exact (pr2 (pr2 T _ ) _ ).

Lemma TerminalEndo_is_identity {T : Terminal} (f : T --> T) : f = identity T.
Show proof.

now apply proofirrelevance, isapropifcontr, (pr2 T T).

Lemma TerminalArrowEq {T : Terminal} {a : C} (f g : a --> T) : f = g.
Show proof.

now rewrite (TerminalArrowUnique f), (TerminalArrowUnique g).

Definition mk_Terminal (b : C) (H : isTerminal b) : Terminal.
Show proof.

exists b; exact H.

Definition mk_isTerminal (b : C) (H : ∏ (a : C), iscontr (a --> b)) :
isTerminal b.
Show proof.

exact H.

Lemma isiso_from_Terminal_to_Terminal (T T' : Terminal) :
is_iso (TerminalArrow T T').
Show proof.

apply (is_iso_qinv _ (TerminalArrow T' T)).
now split; apply TerminalEndo_is_identity.

Definition iso_Terminals (T T' : Terminal) : iso T T' :=
(TerminalArrow T' T,,isiso_from_Terminal_to_Terminal T' T) .

Definition hasTerminal := ishinh Terminal.

Section Terminal_Unique.

Hypothesis H : is_univalent C.

Lemma isaprop_Terminal : isaprop Terminal.
Show proof.

  apply invproofirrelevance.
  intros T T'.
  apply (total2_paths_f (isotoid _ H (iso_Terminals T T')) ).
  apply proofirrelevance.
  unfold isTerminal.
  apply impred.
  intro t ; apply isapropiscontr.

End Terminal_Unique.

End def_terminal.

Arguments Terminal : clear implicits.
Arguments isTerminal : clear implicits.
Arguments TerminalObject {_} _.
Arguments TerminalArrow {_} _ _.
Arguments TerminalArrowUnique {_} _ _ _.
Arguments mk_isTerminal {_} _ _ _.
Arguments mk_Terminal {_} _ _.

Section Terminal_and_EmptyProd.

Construct Terminal from empty arbitrary product.

  Definition terminal_from_empty_product (C : precategory) :
    Product empty C fromempty -> Terminal C.
  Show proof.

    intros X.
    use (mk_Terminal (ProductObject _ C X)).
    use mk_isTerminal.
    intros a.
    assert (H : ∏ i : empty, C⟦a, fromempty i⟧) by
        (intros i; apply (fromempty i)).
    apply (iscontrpair (ProductArrow _ _ X H)); intros t.
    apply ProductArrowUnique; intros i; apply (fromempty i).

End Terminal_and_EmptyProd.

Construction of terminal object in a functor category

Section TerminalFunctorCat.

Variables (C D : precategory) (ID : Terminal D) (hsD : has_homsets D).

Definition Terminal_functor_precat : Terminal [C,D,hsD].
Show proof.

use mk_Terminal.
- use mk_functor.
  + use tpair.
    * intros c; apply (TerminalObject ID).
    * simpl; intros a b f; apply (TerminalArrow ID).
  + split.
    * intro a; apply TerminalEndo_is_identity.
    * intros a b c f g; apply pathsinv0, TerminalArrowUnique.
- intros F.
  use tpair.
  + use mk_nat_trans; simpl.
    * intro a; apply TerminalArrow.
    * intros a b f; simpl.
      rewrite (TerminalEndo_is_identity (TerminalArrow ID ID)), id_right.
      apply TerminalArrowUnique.
  + abstract (intros α; apply (nat_trans_eq hsD); intro a; apply TerminalArrowUnique).

End TerminalFunctorCat.

Morphisms from the terminal object are monic

Section monics_terminal.

Context {C : precategory} (TC : Terminal C).

Lemma from_terminal_isMonic (a : C) (f : C⟦TC,a⟧) : isMonic f.
Show proof.

apply mk_isMonic; intros b g h H.
now apply TerminalArrowEq.

End monics_terminal.