Library UniMath.CategoryTheory.Limits.Terminal
- A proof that the terminal object is a property in a (saturated/univalent) category (isaprop_Terminal)
- Construction of the terminal object from the empty product (terminal_from_empty_product)
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.
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.
Lemma TerminalEndo_is_identity {T : Terminal} (f : T --> T) : f = identity T.
Show proof.
Lemma TerminalArrowEq {T : Terminal} {a : C} (f g : a --> T) : f = g.
Show proof.
Definition make_Terminal (b : C) (H : isTerminal b) : Terminal.
Show proof.
Definition make_isTerminal (b : C) (H : ∏ (a : C), iscontr (a --> b)) :
isTerminal b.
Show proof.
Lemma isziso_from_Terminal_to_Terminal (T T' : Terminal) :
is_z_isomorphism (TerminalArrow T T').
Show proof.
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.
End Terminal_Unique.
Section Terminal_and_EmptyProd.
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.
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.
Lemma TerminalEndo_is_identity {T : Terminal} (f : T --> T) : f = identity T.
Show proof.
Lemma TerminalArrowEq {T : Terminal} {a : C} (f g : a --> T) : f = g.
Show proof.
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.
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.
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 ∅ C fromempty -> Terminal C.
Show proof.
Section TerminalToProduct.
Context {C : category}.
Context (T : Terminal C).
Context {I : UU}.
Context (c : I → C).
Context (φ : I → ∅).
Definition terminal_product_object
: C
:= T.
Definition terminal_product_projection
(i : I)
: C⟦terminal_product_object, c i⟧.
Show proof.
Section Arrow.
Context (c' : C).
Context (cone' : ∏ i, C⟦c', c i⟧).
Definition terminal_product_arrow
: C⟦c', terminal_product_object⟧
:= TerminalArrow T c'.
Lemma terminal_product_arrow_commutes
(i : I)
: terminal_product_arrow · terminal_product_projection i = cone' i.
Show proof.
Lemma terminal_product_arrow_unique
(t : ∑ k, ∏ i : I, k · terminal_product_projection i = cone' i)
: t = terminal_product_arrow ,, terminal_product_arrow_commutes.
Show proof.
End Arrow.
Definition terminal_is_product
: isProduct _ _ _ terminal_product_object terminal_product_projection.
Show proof.
Definition Terminal_is_empty_product
: Product I C c.
Show proof.
End TerminalToProduct.
End Terminal_and_EmptyProd.
Product ∅ C fromempty -> Terminal C.
Show proof.
intros X.
use (make_Terminal (ProductObject _ C X)).
use make_isTerminal.
intros a.
assert (H : ∏ i : ∅, 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)).
use (make_Terminal (ProductObject _ C X)).
use make_isTerminal.
intros a.
assert (H : ∏ i : ∅, 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)).
Section TerminalToProduct.
Context {C : category}.
Context (T : Terminal C).
Context {I : UU}.
Context (c : I → C).
Context (φ : I → ∅).
Definition terminal_product_object
: C
:= T.
Definition terminal_product_projection
(i : I)
: C⟦terminal_product_object, c i⟧.
Show proof.
Section Arrow.
Context (c' : C).
Context (cone' : ∏ i, C⟦c', c i⟧).
Definition terminal_product_arrow
: C⟦c', terminal_product_object⟧
:= TerminalArrow T c'.
Lemma terminal_product_arrow_commutes
(i : I)
: terminal_product_arrow · terminal_product_projection i = cone' i.
Show proof.
Lemma terminal_product_arrow_unique
(t : ∑ k, ∏ i : I, k · terminal_product_projection i = cone' i)
: t = terminal_product_arrow ,, terminal_product_arrow_commutes.
Show proof.
use subtypePairEquality.
{
intro i.
apply impred_isaprop.
intro.
apply homset_property.
}
apply TerminalArrowUnique.
{
intro i.
apply impred_isaprop.
intro.
apply homset_property.
}
apply TerminalArrowUnique.
End Arrow.
Definition terminal_is_product
: isProduct _ _ _ terminal_product_object terminal_product_projection.
Show proof.
use (make_isProduct _ _ (homset_property C)).
intros c' cone'.
use make_iscontr.
- use tpair.
+ exact (terminal_product_arrow c').
+ exact (terminal_product_arrow_commutes c' cone').
- exact (terminal_product_arrow_unique c' cone').
intros c' cone'.
use make_iscontr.
- use tpair.
+ exact (terminal_product_arrow c').
+ exact (terminal_product_arrow_commutes c' cone').
- exact (terminal_product_arrow_unique c' cone').
Definition Terminal_is_empty_product
: Product I C c.
Show proof.
use make_Product.
- exact terminal_product_object.
- exact terminal_product_projection.
- exact terminal_is_product.
- exact terminal_product_object.
- exact terminal_product_projection.
- exact terminal_is_product.
End TerminalToProduct.
End Terminal_and_EmptyProd.
Section TerminalFunctorCat.
Context (C D : category) (ID : Terminal D).
Definition Terminal_functor_precat : Terminal [C,D].
Show proof.
End 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).
- 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.
End monics_terminal.
Definition iso_to_Terminal
{C : category}
(T : Terminal C)
(x : C)
(i : z_iso T x)
: isTerminal C x.
Show proof.
Context {C : category} (TC : Terminal C).
Lemma from_terminal_isMonic (a : C) (f : TC --> a) : isMonic f.
Show proof.
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).
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).