Library UniMath.CategoryTheory.limits.graphs.terminal

Terminal object defined as a limit

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 : category}.

Definition empty_graph : graph.
Show proof.
  exists empty.
  exact (λ _ _, empty).

Definition termDiagram : diagram empty_graph C.
Show proof.
exists fromempty.
intros u; induction u.

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

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

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

Definition Terminal : UU := LimCone termDiagram.

Definition make_Terminal (b : C) (H : isTerminal b) : Terminal.
Show 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.

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 _.
Show proof.
now apply limArrowUnique; intro v; induction v.

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

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

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

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).
Show proof.
  use make_isTerminal.
  intros a.
  use tpair.
  - exact (TerminalArrow T a).
  - intros t. use (TerminalArrowUnique T a).

Maps between terminal as a special limit and direct definition

Lemma equiv_isTerminal1 (c : C) :
  limits.terminal.isTerminal C c -> isTerminal c.
Show proof.
  intros X.
  use make_isTerminal.
  intros b.
  apply (X b).

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

Definition equiv_Terminal1 :
  limits.terminal.Terminal C -> Terminal.
Show proof.
  intros T.
  exact (make_Terminal T (equiv_isTerminal1 _ (pr2 T))).

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

End def_terminal.

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

Lemma Terminal_from_Lims (C : category) :
  Lims_of_shape empty_graph C -> Terminal C.
Show proof.
now intros H; apply H.