(A B P : Type) : ZeroGpd := Build_ZeroGpd (JoinRecData A B P) _ _ _. Global Instance is0functor_joinrecdata_fun {A B P Q : Type} (g : P -> Q) : Is0Functor (@joinrecdata_fun A B P Q g). Proof. apply Build_Is0Functor. intros f1 f2 h. snrapply Build_JoinRecPath; intros; cbn. - exact (ap g (hl h a)). - exact (ap g (hr h b)). - square_ind f2 h a b. by interval_ind f1 a b. Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare. Require Import NullHomotopy. Require Import Extensions. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.Connectedness. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core.