Library UniMath.Bicategories.Core.Examples.Final

Final bicategory and proof that it's univalent.

Note: UniMath.CategoryTheory.categories.StandardCategories has the definition of final 1-category (unit_category).

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.categories.StandardCategories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.EquivToAdjequiv.
Require Import UniMath.Bicategories.Core.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.
  Show proof.
    repeat split; exact tounit.

  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.
  Show proof.
    repeat apply make_dirprod; intros; apply isProofIrrelevantUnit.

  Definition final_prebicat : prebicat
    := final_prebicat_data,, final_bicat_laws.

  Lemma cellset_final_prebicat
    : isaset_cells final_prebicat.
  Show proof.
    red. cbn. intros. exact isasetunit.

  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 α.
  Show proof.
    refine (tt ,, (_ ,, _)) ; reflexivity.

  Definition final_bicat_adjoint_equivalence
             {x y : final_bicat}
             (f : x --> y)
    : left_adjoint_equivalence f.
  Show 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.

It is univalent
  Definition final_bicat_is_univalent_2_1
    : is_univalent_2_1 final_bicat.
  Show 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.

  Definition final_bicat_is_univalent_2_0
    : is_univalent_2_0 final_bicat.
  Show 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.

  Definition final_bicat_is_univalent_2
    : is_univalent_2 final_bicat.
  Show proof.
    split.
    - exact final_bicat_is_univalent_2_0.
    - exact final_bicat_is_univalent_2_1.

End Final_Bicategory.