Library UniMath.CategoryTheory.Bicategories.Bicategories.Examples.Final
Final bicategory and proof that it's univalent.
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.categories.StandardCategories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Bicat. Import Bicat.Notations.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Univalence.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Adjunctions.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.EquivToAdjequiv.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.AdjointUnique.
Local Open Scope cat.
Local Open Scope bicategory_scope.
Section Final_Bicategory.
Definition final_1_id_comp_cells : prebicat_1_id_comp_cells
:= tpair (λ C : precategory_data, prebicat_2cell_struct C)
unit_category
(λ (a b : unit_category) (f g : a --> b), unit).
Definition final_2_id_comp_struct
: prebicat_2_id_comp_struct final_1_id_comp_cells.
Proof.
repeat split; exact tounit.
Defined.
Definition final_prebicat_data : prebicat_data
:= final_1_id_comp_cells,, final_2_id_comp_struct.
Lemma final_bicat_laws : prebicat_laws final_prebicat_data.
Proof.
repeat apply dirprodpair; intros; apply isProofIrrelevantUnit.
Qed.
Definition final_prebicat : prebicat
:= final_prebicat_data,, final_bicat_laws.
Definition cellset_final_prebicat
: isaset_cells final_prebicat.
Proof.
red. cbn. intros. exact isasetunit.
Qed.
Definition final_bicat : bicat
:= final_prebicat,, cellset_final_prebicat.
Definition final_bicat_invertible_2cell
{x y : final_bicat}
{f g : x --> y}
(α : f ==> g)
: is_invertible_2cell α.
Proof.
refine (tt ,, (_ ,, _)) ; reflexivity.
Defined.
Definition final_bicat_adjoint_equivalence
{x y : final_bicat}
(f : x --> y)
: left_adjoint_equivalence f.
Proof.
use tpair.
- use tpair.
+ exact (!f).
+ exact (tt ,, tt).
- split ; split ; cbn.
+ reflexivity.
+ reflexivity.
+ apply final_bicat_invertible_2cell.
+ apply final_bicat_invertible_2cell.
Defined.
It is univalent
Definition final_bicat_is_univalent_2_1
: is_univalent_2_1 final_bicat.
Proof.
intros x y p q.
use isweqimplimpl.
- intros.
apply isasetaprop.
apply isapropunit.
- apply isasetaprop.
apply isasetaprop.
exact isapropunit.
- simple refine (isaprop_total2 (_ ,, _) (λ η , _ ,, _)).
+ exact isapropunit.
+ apply isaprop_is_invertible_2cell.
Defined.
Definition final_bicat_is_univalent_2_0
: is_univalent_2_0 final_bicat.
Proof.
intros x y.
apply isweqimplimpl.
- intros.
induction x, y.
reflexivity.
- apply isasetaprop.
exact isapropunit.
- simple refine (isaprop_total2 (_ ,, _) (λ η , _ ,, _)).
+ apply isasetaprop.
exact isapropunit.
+ apply isaprop_left_adjoint_equivalence.
exact final_bicat_is_univalent_2_1.
Defined.
End Final_Bicategory.
: is_univalent_2_1 final_bicat.
Proof.
intros x y p q.
use isweqimplimpl.
- intros.
apply isasetaprop.
apply isapropunit.
- apply isasetaprop.
apply isasetaprop.
exact isapropunit.
- simple refine (isaprop_total2 (_ ,, _) (λ η , _ ,, _)).
+ exact isapropunit.
+ apply isaprop_is_invertible_2cell.
Defined.
Definition final_bicat_is_univalent_2_0
: is_univalent_2_0 final_bicat.
Proof.
intros x y.
apply isweqimplimpl.
- intros.
induction x, y.
reflexivity.
- apply isasetaprop.
exact isapropunit.
- simple refine (isaprop_total2 (_ ,, _) (λ η , _ ,, _)).
+ apply isasetaprop.
exact isapropunit.
+ apply isaprop_left_adjoint_equivalence.
exact final_bicat_is_univalent_2_1.
Defined.
End Final_Bicategory.