(a a' : A) {b b' : B} (p : b = b') : jglue a b @ (jglue a' b)^ = jglue a b' @ (jglue a' b')^. Proof. by destruct p. 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.