# Library UniMath.CategoryTheory.limits.terminal

Direct definition of terminal object together with:
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.

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 : Ca,TerminalObject T) :
f = TerminalArrow T _.
Proof.
exact (pr2 (pr2 T _ ) _ ).
Defined.

Lemma TerminalEndo_is_identity {T : Terminal} (f : T --> T) : f = identity T.
Proof.
now apply proofirrelevance, isapropifcontr, (pr2 T T).
Qed.

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

Definition make_Terminal (b : C) (H : isTerminal b) : Terminal.
Proof.
b; exact H.
Defined.

Definition make_isTerminal (b : C) (H : (a : C), iscontr (a --> b)) :
isTerminal b.
Proof.
exact H.
Defined.

Lemma isiso_from_Terminal_to_Terminal (T T' : Terminal) :
is_iso (TerminalArrow T T').
Proof.
apply (is_iso_qinv _ (TerminalArrow T' T)).
now split; apply TerminalEndo_is_identity.
Defined.

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

End Terminal_Unique.

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

Construct Terminal from empty arbitrary product.
Definition terminal_from_empty_product (C : precategory) :
Product empty C fromempty Terminal C.
Proof.
intros X.
use (make_Terminal (ProductObject _ C X)).
use make_isTerminal.
intros a.
assert (H : i : empty, Ca, fromempty i) by
(intros i; apply (fromempty i)).
apply (make_iscontr (ProductArrow _ _ X H)); intros t.
apply ProductArrowUnique; intros i; apply (fromempty i).
Defined.

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].
Proof.
use make_Terminal.
- use make_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 make_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).
Defined.

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 : CTC,a) : isMonic f.
Proof.
apply make_isMonic; intros b g h H.
now apply TerminalArrowEq.
Qed.

End monics_terminal.