A : Join Empty A <~> A := equiv_join_empty_right _ oE equiv_join_sym _ _. Global Instance join_right_unitor : RightUnitor Join Empty. Proof. snrapply Build_NatEquiv. - apply equiv_join_empty_right. - snrapply Build_Is1Natural. intros A B f. cbn -[equiv_join_empty_right]. snrapply Join_ind_FlFr. + intro a. reflexivity. + intros []. + intros a []. 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.