Library UniMath.CategoryTheory.limits.graphs.terminal

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.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.terminal.

Local Open Scope cat.

Section def_terminal.

Context {C : precategory}.

Definition empty_graph : graph.
Proof.
  ∃ empty.
  exact (λ _ _, empty).
Defined.

Definition termDiagram : diagram empty_graph C.
Proof.
∃ fromempty.
intros u; induction u.
Defined.

Definition termCone (c : C) : cone termDiagram c.
Proof.
use make_cone; intro v; induction v.
Defined.

Definition isTerminal (a : C) :=
  isLimCone termDiagram a (termCone a).

Definition make_isTerminal (b : C) (H : ∏ (a : C), iscontr (a --> b)) :
  isTerminal b.
Proof.
intros a ca.
use tpair.
- ∃ (pr1 (H a)); intro v; induction v.
- intro t.
  apply subtypePath; simpl;
    [ intro f; apply impred; intro v; induction v|].
  apply (pr2 (H a)).
Defined.

Definition Terminal : UU := LimCone termDiagram.

Definition make_Terminal (b : C) (H : isTerminal b) : Terminal.
Proof.
use (make_LimCone _ b (termCone b)).
apply make_isTerminal.
intro a.
set (x := H a (termCone a)).
use tpair.
- apply (pr1 x).
- simpl; intro f; apply path_to_ctr; intro v; induction v.
Defined.

Definition TerminalObject (T : Terminal) : C := lim T.

Definition TerminalArrow (T : Terminal) (b : C) : C⟦b,TerminalObject T⟧ :=
  limArrow _ _ (termCone b).

Lemma TerminalArrowUnique (T : Terminal) (b : C)
  (f : C⟦b,TerminalObject T⟧) : f = TerminalArrow T _.
Proof.
now apply limArrowUnique; intro v; induction v.
Defined.

Lemma ArrowsToTerminal (T : Terminal) (b : C) (f g : C⟦b,TerminalObject T⟧) : f = g.
Proof.
eapply pathscomp0.
apply TerminalArrowUnique.
now apply pathsinv0, TerminalArrowUnique.
Qed.

Lemma TerminalEndo_is_identity (T : Terminal) (f : C⟦TerminalObject T,TerminalObject T⟧) :
  identity (TerminalObject T) = f.
Proof.
now apply ArrowsToTerminal.
Qed.

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

Definition iso_Terminals (T T' : Terminal) : iso (TerminalObject T) (TerminalObject T') :=
   tpair _ (TerminalArrow T' (TerminalObject T)) (isiso_from_Terminal_to_Terminal T' T) .

Definition hasTerminal := ishinh Terminal.





Definition isTerminal_Terminal (T : Terminal) :
  isTerminal (TerminalObject T).
Proof.
  use make_isTerminal.
  intros a.
  use tpair.
  - exact (TerminalArrow T a).
  - intros t. use (TerminalArrowUnique T a).
Qed.

Lemma equiv_isTerminal1 (c : C) :
  limits.terminal.isTerminal C c → isTerminal c.
Proof.
  intros X.
  use make_isTerminal.
  intros b.
  apply (X b).
Qed.

Lemma equiv_isTerminal2 (c : C) :
  limits.terminal.isTerminal C c <- isTerminal c.
Proof.
  intros X.
  set (XT := make_Terminal c X).
  intros b.
  use tpair.
  - exact (TerminalArrow XT b).
  - intros t. use (TerminalArrowUnique XT b).
Qed.

Definition equiv_Terminal1 :
  limits.terminal.Terminal C → Terminal.
Proof.
  intros T.
  exact (make_Terminal T (equiv_isTerminal1 _ (pr2 T))).
Defined.

Definition equiv_Terminal2 :
  limits.terminal.Terminal C <- Terminal.
Proof.
  intros T.
  exact (limits.terminal.make_Terminal
           (TerminalObject T)
           (equiv_isTerminal2 _ (isTerminal_Terminal T))).
Defined.

End def_terminal.

Arguments Terminal : clear implicits.
Arguments isTerminal : clear implicits.

Lemma Terminal_from_Lims (C : precategory) :
  Lims_of_shape empty_graph C → Terminal C.
Proof.
now intros H; apply H.
Defined.