Library UniMath.CategoryTheory.limits.terminal

Direct definition of terminal object together with:
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

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

Lemma isaprop_isTerminal (b : C)
  : isaprop (isTerminal b).
Show proof.
  apply impred_isaprop
  ; intro
  ; apply isapropiscontr.

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.
apply proofirrelevancecontr, (pr2 T T).

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

Definition make_Terminal (b : C) (H : isTerminal b) : Terminal.
Show proof.
  exists b; exact H.

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

Lemma isziso_from_Terminal_to_Terminal (T T' : Terminal) :
   is_z_isomorphism (TerminalArrow T T').
Show proof.
 exists (TerminalArrow T' T).
 now split; apply TerminalEndo_is_identity.

Definition z_iso_Terminals (T T' : Terminal) : z_iso T T' :=
  TerminalArrow T' T,,isziso_from_Terminal_to_Terminal T' T.

Definition hasTerminal := ishinh Terminal.

End def_terminal.

Arguments Terminal : clear implicits.
Arguments isTerminal : clear implicits.
Arguments TerminalObject {_} _.
Arguments TerminalArrow {_} _ _.
Arguments TerminalArrowUnique {_} _ _ _.
Arguments make_isTerminal {_} _ _ _.
Arguments make_Terminal {_} _ _.

Section Terminal_Unique.

Context (C : category) (H : is_univalent C).

Lemma isaprop_Terminal : isaprop (Terminal C).
Show proof.
  apply invproofirrelevance.
  intros T T'.
  apply (total2_paths_f (isotoid _ H (z_iso_Terminals T T')) ).
  apply isaprop_isTerminal.

End Terminal_Unique.

Section Terminal_and_EmptyProd.

Construct Terminal from empty arbitrary product.
  Definition terminal_from_empty_product (C : category) :
    Product empty C fromempty -> Terminal C.
  Show proof.
    intros X.
    use (make_Terminal (ProductObject _ C X)).
    use make_isTerminal.
    intros a.
    assert (H : ∏ i : empty, C⟦a, fromempty i⟧) by
        (intros i; apply (fromempty i)).
    apply (make_iscontr (ProductArrow _ _ X H)).
    abstract (intros t; apply ProductArrowUnique; intros i; apply (fromempty i)).

End Terminal_and_EmptyProd.










Construction of terminal object in a functor category

Section TerminalFunctorCat.

Context (C D : category) (ID : Terminal D).

Definition Terminal_functor_precat : Terminal [C,D].
Show proof.
use make_Terminal.
- exact (constant_functor _ _ ID).
- intros F.
  use tpair.
  + use make_nat_trans.
    * intro a; apply TerminalArrow.
    * abstract (intros a b f; apply TerminalArrowEq).
  + abstract (intros α; apply (nat_trans_eq D); intro a; apply TerminalArrowUnique).

End TerminalFunctorCat.

Morphisms from the terminal object are monic
Section monics_terminal.

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

Lemma from_terminal_isMonic (a : C) (f : TC --> a) : isMonic f.
Show proof.
apply make_isMonic; intros b g h H.
now apply TerminalArrowEq.

End monics_terminal.

Definition iso_to_Terminal
           {C : category}
           (T : Terminal C)
           (x : C)
           (i : z_iso T x)
  : isTerminal C x.
Show proof.
  intros w.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ₁ φ₂ ;
       refine (!(id_right _) @ _ @ id_right _) ;
       rewrite <- !(z_iso_after_z_iso_inv i) ;
       rewrite !assoc ;
       apply maponpaths_2 ;
       apply TerminalArrowEq).
  - exact (TerminalArrow T w · i).