{A B C D} (f : A <~> C) (g : B <~> D) : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _. Global Instance is0bifunctor_join : Is0Bifunctor Join. Proof. snrapply Build_Is0Bifunctor'. 1,2: exact _. apply Build_Is0Functor. intros A B [f g]. exact (functor_join f g). 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.