(A B : Type) {P Q : Type} (g : P -> Q) (f : JoinRecData A B P) : join_rec (joinrecdata_fun g f) $== g o join_rec f. Proof. exact (isnat (join_rec_natequiv A B) g f). 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.