Library UniMath.Bicategories.Core.Examples.PointedOneTypesBicat

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.OneTypes.
Require Import UniMath.Bicategories.Morphisms.Adjunctions.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.

Local Open Scope cat.

The bicategory

Definition pointed_one_type_bicat_data
: prebicat_data.
Show proof.

  use build_prebicat_data.
  - exact (∑ (X : one_type ), X).
  - exact (λ X Y , ∑ (f : pr1 X → pr1 Y ), f (pr2 X) = pr2 Y).
  - exact (λ X Y f g , ∑ (h : pr1 f = pr1 g ),
           transportf (λ φ , φ (pr2 X) = pr2 Y) h (pr2 f) = pr2 g).
  - exact (λ X , (λ x , x ) ,, idpath _).
  - exact (λ X Y Z f g , (λ x ,pr1 g(pr1 f x)) ,, maponpaths (pr1 g) (pr2 f) @ pr2 g).
  - exact (λ X Y f , idpath _ ,, idpath _).
  - refine (λ X Y f g h p q , (pr1 p @ pr1 q ) ,, _) ; cbn in *.
    exact (!(transport_f_f _ _ _ _) @ maponpaths _ (pr2 p) @ pr2 q).
  - refine (λ X Y Z f g h p , (maponpaths (λ φ x , φ (pr1 f x)) (pr1 p)) ,, _) ; cbn in *.
    induction g as [g1 g2], h as [h1 h2], p as [p1 p2] ; cbn in *.
    induction p1, p2 ; cbn.
    apply idpath.
  - refine (λ X Y Z f g h p , (maponpaths (λ φ x , pr1 h (φ x)) (pr1 p)) ,, _) ; cbn in *.
    induction g as [g1 g2], h as [h1 h2], p as [p1 p2] ; cbn in *.
    induction p1, p2 ; cbn.
    apply idpath.
  - exact (λ X Y f , idpath _ ,, idpath _).
  - exact (λ X Y f , idpath _ ,, idpath _).
  - refine (λ X Y f , idpath _ ,, _) ; cbn in *.
    exact (pathscomp0rid _ @ maponpathsidfun _).
  - refine (λ X Y f , idpath _ ,, _) ; cbn in *.
    exact (!(pathscomp0rid _ @ maponpathsidfun _)).
  - refine (λ W X Y Z f g h , idpath _ ,, _) ; cbn in *.
    refine (path_assoc _ _ _ @ _).
    apply maponpaths_2.
    refine (_ @ !(maponpathscomp0 _ _ _)).
    apply maponpaths_2.
    exact (!(maponpathscomp _ _ _)).
  - refine (λ W X Y Z f g h , idpath _ ,, ! _) ; cbn in *.
    refine (path_assoc _ _ _ @ _).
    apply maponpaths_2.
    refine (_ @ !(maponpathscomp0 _ _ _)).
    apply maponpaths_2.
    exact (!(maponpathscomp _ _ _)).

Lemma pointed_one_type_bicat_laws
: prebicat_laws pointed_one_type_bicat_data.
Show proof.

  repeat (use tpair).
  - intros X Y f g p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], p as [p1 p2] ; cbn in *.
    induction p1 ; cbn.
    apply idpath.
  - intros X Y f g p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], p as [p1 p2] ; cbn in *.
    induction p1, p2 ; cbn.
    apply idpath.
  - intros X Y f g h k p q r ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], k as [k1 k2].
    induction p as [p1 p2], q as [q1 q2], r as [r1 r2] ; cbn in *.
    induction p1, p2, q1, q2, r1, r2.
    apply idpath.
  - intros; apply idpath.
  - intros; apply idpath.
  - intros X Y Z f g h i p q ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2], q as [q1 q2] ; cbn in *.
    induction p1, p2, q1, q2 ; cbn.
    apply idpath.
  - intros X Y Z f g h i p q ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2], q as [q1 q2] ; cbn in *.
    induction p1, p2, q1, q2 ; cbn.
    apply idpath.
  - intros X Y f g p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], p as [p1 p2] ; cbn in *.
    induction p1, p2 ; cbn.
    apply idpath.
  - intros X Y f g p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], p as [p1 p2] ; cbn in *.
    induction p1, p2, f2 ; cbn.
    apply idpath.
  - intros W X Y Z f g h i p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2] ; cbn in *.
    induction p1, p2, f2, g2, h2 ; cbn.
    apply idpath.
  - intros W X Y Z f g h i p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2] ; cbn in *.
    induction p1, p2, f2, g2 ; cbn.
    apply idpath.
  - intros W X Y Z f g h i p ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2] ; cbn in *.
    induction p1, p2, f2, h2 ; cbn.
    apply idpath.
  - intros X Y Z f g h i p q ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2].
    induction p as [p1 p2], q as [q1 q2] ; cbn in *.
    induction p1, p2, q1, q2, f2, h2 ; cbn.
    apply idpath.
  - intros; apply idpath.
  - intros; apply idpath.
  - intros X Y p ; cbn in *.
    induction p as [p1 p2].
    induction p2 ; cbn.
    apply idpath.
  - intros X Y p ; cbn in *.
    induction p as [p1 p2].
    induction p2 ; cbn.
    apply idpath.
  - intros W X Y Z f g h ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2] ; cbn in *.
    induction f2, g2, h2 ; cbn.
    apply idpath.
  - intros W X Y Z f g h ; cbn in *.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2] ; cbn in *.
    induction f2, g2, h2 ; cbn.
    apply idpath.
  - intros X Y Z f g ; cbn in *.
    induction f as [f1 f2], g as [g1 g2] ; cbn in *.
    induction f2, g2 ; cbn.
    apply idpath.
  - intros V W X Y Z f g h i.
    induction f as [f1 f2], g as [g1 g2], h as [h1 h2], i as [i1 i2] ; cbn in *.
    induction f2, g2, h2, i2 ; cbn.
    apply idpath.

Definition pointed_one_types
: bicat.
Show proof.

  use build_bicategory.
  - exact pointed_one_type_bicat_data.
  - exact pointed_one_type_bicat_laws.
  - intros X Y f g ; cbn in *.
    use isaset_total2.
    + exact (impredfun 3 (pr1 X) (pr1 Y) (pr21 Y) (pr1 f) (pr1 g)).
    + intro ; cbn.
      repeat intro.
      apply hlevelntosn.
      apply (pr21 Y).