proposition: Lemma diamond_symm (a : A) (b : B) : diamond_v_sq a a 1 = diamond_h_sq b b 1.
proof: Proof. unfold diamond_v_sq, diamond_h_sq, diamond_v, diamond_h. symmetry; apply ap, concat_pV. Defined.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core