{A B} : functor_join idmap idmap == (idmap : Join A B -> Join A B). Proof. snrapply Join_ind_FlFr. 1,2: reflexivity. intros a b. simpl. apply equiv_p1_1q. lhs nrapply functor_join_beta_jglue. symmetry; apply ap_idmap. 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.