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.
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 _ _ _)).
Defined.
Lemma pointed_one_type_bicat_laws
: prebicat_laws pointed_one_type_bicat_data.
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.
Qed.
Definition pointed_one_types
: bicat.
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).
Defined.