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.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
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 _.
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 mk_Terminal (b : C) (H : isTerminal b) : Terminal.
Proof.
  ∃ b; exact H.
Defined.

Definition mk_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 mk_isTerminal {_} _ _ _.
Arguments mk_Terminal {_} _ _.

Section Terminal_and_EmptyProd.

  Definition terminal_from_empty_product (C : precategory) :
    Product empty C fromempty → Terminal C.
  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).
  Defined.

End Terminal_and_EmptyProd.

Section TerminalFunctorCat.

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

Definition Terminal_functor_precat : Terminal [C,D,hsD].
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).
Defined.

End TerminalFunctorCat.

Section monics_terminal.

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

Lemma from_terminal_isMonic (a : C) (f : C⟦TC,a⟧) : isMonic f.
Proof.
apply mk_isMonic; intros b g h H.
now apply TerminalArrowEq.
Qed.

End monics_terminal.