Library UniMath.Bicategories.Core.Examples.Initial

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
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.

Section Initial_Bicategory.
  Definition initial_1_id_comp_cells : prebicat_1_id_comp_cells
    := tpair (λ C : precategory_data, prebicat_2cell_struct C)
             empty_category
             (λ (a b : empty_category) (f g : a --> b), ∅).

  Definition initial_2_id_comp_struct
    : prebicat_2_id_comp_struct initial_1_id_comp_cells.
  Show proof.

  Definition initial_prebicat_data : prebicat_data
    := initial_1_id_comp_cells,, initial_2_id_comp_struct.

  Lemma initial_bicat_laws : prebicat_laws initial_prebicat_data.
  Show proof.

  Definition initial_prebicat : prebicat
    := initial_prebicat_data,, initial_bicat_laws.

  Definition cellset_initial_prebicat
    : isaset_cells initial_prebicat
    := λ u : ∅, fromempty u.

  Definition initial_bicat : bicat
    := initial_prebicat,, cellset_initial_prebicat.

  Definition initial_bicat_invertible_2cell
             {x y : initial_bicat}
             {f g : x --> y}
             (α : f ==> g)
    : is_invertible_2cell α.
  Show proof.

  Definition initial_bicat_adjoint_equivalence
             {x y : initial_bicat}
             (f : x --> y)
    : left_adjoint_equivalence f.
  Show proof.

  Definition initial_bicat_is_univalent_2_1
    : is_univalent_2_1 initial_bicat.
  Show proof.

  Definition initial_bicat_is_univalent_2_0
    : is_univalent_2_0 initial_bicat.
  Show proof.

  Definition initial_bicat_is_univalent_2
    : is_univalent_2 initial_bicat.
  Show proof.

End Initial_Bicategory.