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.
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.