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