Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal
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.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment.
Require Import UniMath.CategoryTheory.limits.terminal.
Import MonoidalNotations.
Local Open Scope cat.
Local Open Scope moncat.
Section EnrichedTerminal.
Context {V : monoidal_cat}
{C : category}
(E : enrichment C V).
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment.
Require Import UniMath.CategoryTheory.limits.terminal.
Import MonoidalNotations.
Local Open Scope cat.
Local Open Scope moncat.
Section EnrichedTerminal.
Context {V : monoidal_cat}
{C : category}
(E : enrichment C V).
1. Terminal objects in an enriched category
Definition is_terminal_enriched
(x : C)
: UU
:= ∏ (y : C), isTerminal V (E ⦃ y, x ⦄).
Definition terminal_enriched
: UU
:= ∑ (x : C), is_terminal_enriched x.
Coercion terminal_enriched_to_ob
(x : terminal_enriched)
: C
:= pr1 x.
Coercion terminal_enriched_to_is_terminal
(x : terminal_enriched)
: is_terminal_enriched x
:= pr2 x.
(x : C)
: UU
:= ∏ (y : C), isTerminal V (E ⦃ y, x ⦄).
Definition terminal_enriched
: UU
:= ∑ (x : C), is_terminal_enriched x.
Coercion terminal_enriched_to_ob
(x : terminal_enriched)
: C
:= pr1 x.
Coercion terminal_enriched_to_is_terminal
(x : terminal_enriched)
: is_terminal_enriched x
:= pr2 x.
2. Being terminal is a proposition
3. Accessors for terminal objects
Section Accessors.
Context {x : C}
(Hx : is_terminal_enriched x).
Definition is_terminal_enriched_arrow
(y : C)
: I_{V} --> E ⦃ y , x ⦄
:= TerminalArrow (_ ,, Hx y) I_{V}.
Definition is_terminal_enriched_eq
{y : C}
(f g : I_{V} --> E ⦃ y , x ⦄)
: f = g.
Show proof.
Definition terminal_underlying
: Terminal C.
Show proof.
Context {x : C}
(Hx : is_terminal_enriched x).
Definition is_terminal_enriched_arrow
(y : C)
: I_{V} --> E ⦃ y , x ⦄
:= TerminalArrow (_ ,, Hx y) I_{V}.
Definition is_terminal_enriched_eq
{y : C}
(f g : I_{V} --> E ⦃ y , x ⦄)
: f = g.
Show proof.
Definition terminal_underlying
: Terminal C.
Show proof.
refine (x ,, _).
intros y.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros f g ;
refine (!(enriched_to_from_arr E f) @ _ @ enriched_to_from_arr E g) ;
apply maponpaths ;
apply is_terminal_enriched_eq).
- exact (enriched_to_arr E (is_terminal_enriched_arrow y)).
End Accessors.intros y.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros f g ;
refine (!(enriched_to_from_arr E f) @ _ @ enriched_to_from_arr E g) ;
apply maponpaths ;
apply is_terminal_enriched_eq).
- exact (enriched_to_arr E (is_terminal_enriched_arrow y)).
4. Builders for terminal objects
Definition make_is_terminal_enriched
(x : C)
(f : ∏ (w : V) (y : C), w --> E ⦃ y , x ⦄)
(p : ∏ (w : V) (y : C) (f g : w --> E ⦃ y , x ⦄), f = g)
: is_terminal_enriched x.
Show proof.
Definition make_is_terminal_enriched_from_iso
(TV : Terminal V)
(x : C)
(Hx : ∏ (y : C),
is_z_isomorphism (TerminalArrow TV (E ⦃ y, x ⦄)))
: is_terminal_enriched x.
Show proof.
Definition terminal_enriched_from_underlying
(TC : Terminal C)
(TV : Terminal V)
(HV : conservative_moncat V)
: is_terminal_enriched TC.
Show proof.
(x : C)
(f : ∏ (w : V) (y : C), w --> E ⦃ y , x ⦄)
(p : ∏ (w : V) (y : C) (f g : w --> E ⦃ y , x ⦄), f = g)
: is_terminal_enriched x.
Show proof.
intros y w.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
apply p).
- apply f.
use iscontraprop1.
- abstract
(use invproofirrelevance ;
intros φ₁ φ₂ ;
apply p).
- apply f.
Definition make_is_terminal_enriched_from_iso
(TV : Terminal V)
(x : C)
(Hx : ∏ (y : C),
is_z_isomorphism (TerminalArrow TV (E ⦃ y, x ⦄)))
: is_terminal_enriched x.
Show proof.
Definition terminal_enriched_from_underlying
(TC : Terminal C)
(TV : Terminal V)
(HV : conservative_moncat V)
: is_terminal_enriched TC.
Show proof.
use (make_is_terminal_enriched_from_iso TV).
intro y.
use HV.
use isweq_iso.
- intro f.
apply enriched_from_arr.
apply (TerminalArrow TC).
- abstract
(intros f ; cbn ;
refine (_ @ enriched_from_to_arr E f) ;
apply maponpaths ;
apply TerminalArrowEq).
- abstract
(intros f ; cbn ;
apply TerminalArrowEq).
intro y.
use HV.
use isweq_iso.
- intro f.
apply enriched_from_arr.
apply (TerminalArrow TC).
- abstract
(intros f ; cbn ;
refine (_ @ enriched_from_to_arr E f) ;
apply maponpaths ;
apply TerminalArrowEq).
- abstract
(intros f ; cbn ;
apply TerminalArrowEq).
5. Being terminal is closed under iso
Definition terminal_enriched_from_iso
{x y : C}
(Hx : is_terminal_enriched x)
(f : z_iso x y)
: is_terminal_enriched y.
Show proof.
{x y : C}
(Hx : is_terminal_enriched x)
(f : z_iso x y)
: is_terminal_enriched y.
Show proof.
6. Terminal objects are isomorphic
Definition iso_between_terminal_enriched
{x y : C}
(Hx : is_terminal_enriched x)
(Hy : is_terminal_enriched y)
: z_iso x y.
Show proof.
Definition isaprop_terminal_enriched
(HC : is_univalent C)
: isaprop terminal_enriched.
Show proof.
{x y : C}
(Hx : is_terminal_enriched x)
(Hy : is_terminal_enriched y)
: z_iso x y.
Show proof.
use make_z_iso.
- exact (enriched_to_arr E (is_terminal_enriched_arrow Hy x)).
- exact (enriched_to_arr E (is_terminal_enriched_arrow Hx y)).
- split.
+ abstract
(refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ;
apply maponpaths ;
apply (is_terminal_enriched_eq Hx)).
+ abstract
(refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ;
apply maponpaths ;
apply (is_terminal_enriched_eq Hy)).
- exact (enriched_to_arr E (is_terminal_enriched_arrow Hy x)).
- exact (enriched_to_arr E (is_terminal_enriched_arrow Hx y)).
- split.
+ abstract
(refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ;
apply maponpaths ;
apply (is_terminal_enriched_eq Hx)).
+ abstract
(refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ;
apply maponpaths ;
apply (is_terminal_enriched_eq Hy)).
Definition isaprop_terminal_enriched
(HC : is_univalent C)
: isaprop terminal_enriched.
Show proof.
use invproofirrelevance.
intros φ₁ φ₂.
use subtypePath.
{
intro.
apply isaprop_is_terminal_enriched.
}
use (isotoid _ HC).
use iso_between_terminal_enriched.
- exact (pr2 φ₁).
- exact (pr2 φ₂).
End EnrichedTerminal.intros φ₁ φ₂.
use subtypePath.
{
intro.
apply isaprop_is_terminal_enriched.
}
use (isotoid _ HC).
use iso_between_terminal_enriched.
- exact (pr2 φ₁).
- exact (pr2 φ₂).
7. Enriched categories with a terminal object
Definition cat_with_enrichment_terminal
(V : monoidal_cat)
: UU
:= ∑ (C : cat_with_enrichment V), terminal_enriched C.
Coercion cat_with_enrichment_terminal_to_cat_with_enrichment
{V : monoidal_cat}
(C : cat_with_enrichment_terminal V)
: cat_with_enrichment V
:= pr1 C.
Definition terminal_of_cat_with_enrichment
{V : monoidal_cat}
(C : cat_with_enrichment_terminal V)
: terminal_enriched C
:= pr2 C.
(V : monoidal_cat)
: UU
:= ∑ (C : cat_with_enrichment V), terminal_enriched C.
Coercion cat_with_enrichment_terminal_to_cat_with_enrichment
{V : monoidal_cat}
(C : cat_with_enrichment_terminal V)
: cat_with_enrichment V
:= pr1 C.
Definition terminal_of_cat_with_enrichment
{V : monoidal_cat}
(C : cat_with_enrichment_terminal V)
: terminal_enriched C
:= pr2 C.