Equivalence between two presentations of the suspension

Susp-Join.agda

open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import 1Lab.Type
open import 1Lab.Equiv

data Susp {ℓ} (A : Type ℓ) : Type ℓ where
  N S   : Susp A
  merid : A → N ≡ S

data Join {ℓ₁ ℓ₂} (A : Type ℓ₁) (B : Type ℓ₂) : Type (ℓ₁ ⊔ ℓ₂) where
  inl  : A → Join A B
  inr  : B → Join A B
  join : (a : A) → (b : B) → inl a ≡ inr b

Susp-Join : ∀ {ℓ} {A : Type ℓ} → Susp A ≃ Join Bool A
Susp-Join {ℓ} {A} = Iso→Equiv (to , iso from to-from from-to) where
  to : Susp A → Join Bool A
  to N = inl true
  to S = inl false
  to (merid a i) = (join true a ∙ sym (join false a)) i

  from : Join Bool A → Susp A
  from (inl true) = N
  from (inl false) = S
  from (inr _) = S
  from (join true a i) = merid a i
  from (join false a i) = S

  to-from : (x : Join Bool A) → to (from x) ≡ x
  to-from (inl true) = refl
  to-from (inl false) = refl
  to-from (inr a) = join false a
  to-from (join true a i) j = ∙-filler (join true a) (sym (join false a)) (~ j) i
  to-from (join false a i) j = join false a (i ∧ j)

  from-to : (x : Susp A) → from (to x) ≡ x
  from-to N = refl
  from-to S = refl
  from-to (merid a i) j = (ap-comp-path from (join true a) (sym (join false a)) ∙ ∙-id-r _) j i