text:
open import Data.Nat using (ℕ; suc ; zero; _+_; _≤′_; _<′_; _<_; _≤_;
    z≤n; s≤s; ≤′-refl; ≤′-step; _≟_) renaming (_⊔_ to max)
open import Data.Nat.Properties
  using (n≤0⇒n≡0; ≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; ≤-step; ⊔-mono-≤;
         +-mono-≤; +-mono-≤-<; +-mono-<-≤; +-comm; +-assoc; n≤1+n;
         ≤-pred; m≤m+n; n≤m+n; ≤-reflexive; ≤′⇒≤; ≤⇒≤′; +-suc)
open Data.Nat.Properties.≤-Reasoning using (begin_; _≤⟨_⟩_; _∎)
open import Data.Bool  using (Bool) renaming (_≟_ to _=?_)
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Empty using (⊥-elim) renaming (⊥ to Bot)
open import Data.Unit using (⊤; tt)
open import Data.Maybe
open import Data.List using (List ; _∷_ ; []; _++_)
open import Relation.Nullary using (¬_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning renaming (begin_ to start_; _∎ to _□)

module extra.Value where

data Base : Set where
  Nat : Base
  𝔹 : Base

data Prim : Set where
  base : Base → Prim
  _⇒_ : Base → Prim → Prim

base-rep : Base → Set
base-rep Nat = ℕ
base-rep 𝔹 = Bool

rep : Prim → Set
rep (base b) = base-rep b
rep (b ⇒ p) = base-rep b → rep p

base-eq? : (B : Base) → (B' : Base) → Dec (B ≡ B')
base-eq? Nat Nat = yes refl
base-eq? Nat 𝔹 = no (λ ())
base-eq? 𝔹 Nat = no (λ ())
base-eq? 𝔹 𝔹 = yes refl

base-rep-eq? : ∀{B} → (k : base-rep B) (k′ : base-rep B) → Dec (k ≡ k′)
base-rep-eq? {Nat} k k′ = k ≟ k′
base-rep-eq? {𝔹} k k′ = k =? k′

infixr 7 _↦_
infixl 6 _⊔_

data Value : Set

data Value where
  ⊥ : Value
  const : {b : Base} → base-rep b → Value
  _↦_ : Value → Value → Value
  _⊔_ : (u : Value) → (v : Value) → Value

infix 5 _∈_

_∈_ : Value → Value → Set
u ∈ ⊥ = u ≡ ⊥
u ∈ const {B} k = u ≡ const {B} k
u ∈ v ↦ w = u ≡ v ↦ w
u ∈ (v ⊔ w) = u ∈ v ⊎ u ∈ w

infix 5 _⊆_

_⊆_ : Value → Value → Set
v ⊆ w = ∀{u} → u ∈ v → u ∈ w

AllFun : (u : Value) → Set
AllFun ⊥ = Bot
AllFun (const x) = Bot
AllFun (v ↦ w) = ⊤
AllFun (u ⊔ v) = AllFun u × AllFun v

dom : (u : Value) → Value
dom ⊥ = ⊥
dom (const k) = ⊥
dom (v ↦ w) = v
dom (u ⊔ v) = dom u ⊔ dom v

cod : (u : Value) → Value
cod ⊥  = ⊥
cod (const k) = ⊥
cod (v ↦ w) = w
cod (u ⊔ v) = cod u ⊔ cod v

infix 4 _⊑_

data _⊑_ : Value → Value → Set where

  ⊑-⊥ : ∀ {v} → ⊥ ⊑ v

  ⊑-const : ∀ {B}{k} → const {B} k ⊑ const {B} k

  ⊑-conj-L : ∀ {u v w}
        → v ⊑ u
        → w ⊑ u
          -----------
        → v ⊔ w ⊑ u

  ⊑-conj-R1 : ∀ {u v w}
       → u ⊑ v
         ------------------
       → u ⊑ v ⊔ w

  ⊑-conj-R2 : ∀ {u v w}
       → u ⊑ w
         -----------
       → u ⊑ v ⊔ w

  ⊑-fun : ∀ {u u′ v w}
       → u′ ⊆ u
       → AllFun u′
       → dom u′ ⊑ v
       → w ⊑ cod u′
         -------------------
       → v ↦ w ⊑ u

⊑-refl : ∀{v} → v ⊑ v
⊑-refl {⊥} = ⊑-⊥
⊑-refl {const k} = ⊑-const
⊑-refl {v ↦ w} = ⊑-fun{v ↦ w}{v ↦ w} (λ {u} z → z) tt (⊑-refl{v}) ⊑-refl
⊑-refl {v₁ ⊔ v₂} = ⊑-conj-L (⊑-conj-R1 ⊑-refl) (⊑-conj-R2 ⊑-refl)

factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set
factor u u′ v w = AllFun u′ × u′ ⊆ u × dom u′ ⊑ v × w ⊑ cod u′

⊑-fun-inv : ∀{u₁ u₂ v w}
      → u₁ ⊑ u₂
      → v ↦ w ∈ u₁
      → Σ[ u₃ ∈ Value ] factor u₂ u₃ v w
⊑-fun-inv {.⊥} {u₂} {v} {w} ⊑-⊥ ()
⊑-fun-inv {.(const _)} {.(const _)} {v} {w} ⊑-const ()
⊑-fun-inv {u11 ⊔ u12} {u₂} {v} {w} (⊑-conj-L u₁⊑u₂ u₁⊑u₃) (inj₁ x) =
    ⊑-fun-inv u₁⊑u₂ x
⊑-fun-inv {u11 ⊔ u12} {u₂} {v} {w} (⊑-conj-L u₁⊑u₂ u₁⊑u₃) (inj₂ y) =
    ⊑-fun-inv u₁⊑u₃ y
⊑-fun-inv {u₁} {u21 ⊔ u22} {v} {w} (⊑-conj-R1 u₁⊑u₂) v↦w∈u₁
    with ⊑-fun-inv {u₁} {u21} {v} {w} u₁⊑u₂ v↦w∈u₁
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u3⊆u₁ , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
    ⟨ u₃ , ⟨ afu₃ , ⟨ (λ {x} x₁ → inj₁ (u3⊆u₁ x₁)) , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩
⊑-fun-inv {u₁} {u21 ⊔ u22} {v} {w} (⊑-conj-R2 u₁⊑u₂) v↦w∈u₁
    with ⊑-fun-inv {u₁} {u22} {v} {w} u₁⊑u₂ v↦w∈u₁
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u3⊆u₁ , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩ =
    ⟨ u₃ , ⟨ afu₃ , ⟨ (λ {x} x₁ → inj₂ (u3⊆u₁ x₁)) , ⟨ du₃⊑v , w⊑codu₃ ⟩ ⟩ ⟩ ⟩
⊑-fun-inv {u11 ↦ u21} {u₂} {v} {w} (⊑-fun{u′ = u′} u′⊆u₂ afu′ du′⊑u11 u21⊑cu′)
    refl =
      ⟨ u′ , ⟨ afu′ , ⟨ u′⊆u₂ , ⟨ du′⊑u11 , u21⊑cu′ ⟩ ⟩ ⟩ ⟩

sub-inv-trans : ∀{u′ u₂ u : Value}
    → AllFun u′  →  u′ ⊆ u
    → (∀{v′ w′} → v′ ↦ w′ ∈ u′ → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′)
      ---------------------------------------------------------------
    → Σ[ u₃ ∈ Value ] factor u₂ u₃ (dom u′) (cod u′)
sub-inv-trans {⊥} {u₂} {u} () u′⊆u IH
sub-inv-trans {const k} {u₂} {u} () u′⊆u IH
sub-inv-trans {u₁′ ↦ u₂′} {u₂} {u} fu′ u′⊆u IH = IH refl
sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} ⟨ afu₁′ , afu₂′ ⟩ u′⊆u IH
    with sub-inv-trans {u₁′} {u₂} {u} afu₁′
               (λ {u₁} z → u′⊆u (inj₁ z)) (λ {v′} {w′} z → IH (inj₁ z))
    | sub-inv-trans {u₂′} {u₂} {u} afu₂′
               (λ {u₁} z → u′⊆u (inj₂ z)) (λ {v′} {w′} z → IH (inj₂ z))
... | ⟨ u₃ , ⟨ afu₃ , ⟨ u₃⊆ , ⟨ du₃⊑ , ⊑cu₃ ⟩ ⟩ ⟩ ⟩
    | ⟨ u₄ , ⟨ afu₄ , ⟨ u₄⊆ , ⟨ du₄⊑ , ⊑cu₄ ⟩ ⟩ ⟩ ⟩ =

      ⟨ (u₃ ⊔ u₄) , ⟨ ⟨ afu₃ , afu₄ ⟩ , ⟨ G , ⟨ H , I ⟩ ⟩ ⟩ ⟩
    where
    G : ∀ {u₁} → u₁ ∈ u₃ ⊎ u₁ ∈ u₄ → u₁ ∈ u₂
    G {u₁} (inj₁ x) = u₃⊆ x
    G {u₁} (inj₂ y) = u₄⊆ y

    H : dom u₃ ⊔ dom u₄ ⊑ dom u₁′ ⊔ dom u₂′
    H = ⊑-conj-L (⊑-conj-R1 du₃⊑) (⊑-conj-R2 du₄⊑)

    I : cod u₁′ ⊔ cod u₂′ ⊑ cod u₃ ⊔ cod u₄
    I = ⊑-conj-L (⊑-conj-R1 ⊑cu₃) (⊑-conj-R2 ⊑cu₄)

⊔⊑R : ∀{B C A}
    → B ⊔ C ⊑ A
    → B ⊑ A
⊔⊑R (⊑-conj-L B⊔C⊑A B⊔C⊑A₁) = B⊔C⊑A
⊔⊑R (⊑-conj-R1 B⊔C⊑A) = ⊑-conj-R1 (⊔⊑R B⊔C⊑A)
⊔⊑R (⊑-conj-R2 B⊔C⊑A) = ⊑-conj-R2 (⊔⊑R B⊔C⊑A)

⊔⊑L : ∀{B C A}
    → B ⊔ C ⊑ A
    → C ⊑ A
⊔⊑L (⊑-conj-L B⊔C⊑A B⊔C⊑A₁) = B⊔C⊑A₁
⊔⊑L (⊑-conj-R1 B⊔C⊑A) = ⊑-conj-R1 (⊔⊑L B⊔C⊑A)
⊔⊑L (⊑-conj-R2 B⊔C⊑A) = ⊑-conj-R2 (⊔⊑L B⊔C⊑A)

u∈v⊑w→u⊑w : ∀{B A C} → C ∈ B → B ⊑ A → C ⊑ A
u∈v⊑w→u⊑w {⊥} C∈B B⊑A  rewrite C∈B = B⊑A
u∈v⊑w→u⊑w {const k} C∈B B⊑A rewrite C∈B = B⊑A
u∈v⊑w→u⊑w {B₁ ↦ B₂} C∈B B⊑A rewrite C∈B = B⊑A
u∈v⊑w→u⊑w {B₁ ⊔ B₂}{A}{C} (inj₁ C∈B₁) B⊑A = u∈v⊑w→u⊑w {B₁}{A}{C} C∈B₁ (⊔⊑R B⊑A)
u∈v⊑w→u⊑w {B₁ ⊔ B₂}{A}{C} (inj₂ C∈B₂) B⊑A = u∈v⊑w→u⊑w {B₂}{A}{C} C∈B₂ (⊔⊑L B⊑A)

u⊆v⊑w→u⊑w : ∀{u v w} → u ⊆ v → v ⊑ w → u ⊑ w
u⊆v⊑w→u⊑w {⊥} {v} {w} u⊆v v⊑w = ⊑-⊥
u⊆v⊑w→u⊑w {const k} {v} {w} u⊆v v⊑w
    with u⊆v refl
... | k∈v = u∈v⊑w→u⊑w k∈v v⊑w
u⊆v⊑w→u⊑w {u₁ ↦ u₂} {v} {w} u⊆v v⊑w
    with u⊆v refl
... | u₁↦u₂∈v = u∈v⊑w→u⊑w u₁↦u₂∈v v⊑w
u⊆v⊑w→u⊑w {u₁ ⊔ u₂} {v} {w} u⊆v v⊑w =
    ⊑-conj-L (u⊆v⊑w→u⊑w u₁⊆v v⊑w) (u⊆v⊑w→u⊑w u₂⊆v v⊑w)
    where
    u₁⊆v : u₁ ⊆ v
    u₁⊆v {u′} u′∈u₁ = u⊆v (inj₁ u′∈u₁)
    u₂⊆v : u₂ ⊆ v
    u₂⊆v {u′} u′∈u₂ = u⊆v (inj₂ u′∈u₂)

depth : (v : Value) → ℕ
depth ⊥ = zero
depth (const k) = zero
depth (v ↦ w) = suc (max (depth v) (depth w))
depth (v₁ ⊔ v₂) = max (depth v₁) (depth v₂)

size : (v : Value) → ℕ
size ⊥ = zero
size (const k) = zero
size (v ↦ w) = suc (size v + size w)
size (v₁ ⊔ v₂) = suc (size v₁ + size v₂)

∈→depth≤ : ∀{v u : Value} → u ∈ v → depth u ≤ depth v
∈→depth≤ {⊥} {u} u∈v rewrite u∈v = _≤_.z≤n
∈→depth≤ {const x} {u} u∈v rewrite u∈v = _≤_.z≤n
∈→depth≤ {v ↦ w} {u} u∈v rewrite u∈v = ≤-refl
∈→depth≤ {v₁ ⊔ v₂} {u} (inj₁ x) =
    ≤-trans (∈→depth≤ {v₁} {u} x) (m≤m⊔n (depth v₁) (depth v₂))
∈→depth≤ {v₁ ⊔ v₂} {u} (inj₂ y) =
    ≤-trans (∈→depth≤ {v₂} {u} y) (n≤m⊔n (depth v₁) (depth v₂))

max-lub : ∀{x y z : ℕ} → x ≤ z → y ≤ z → max x y ≤ z
max-lub {.0} {y} {z} _≤_.z≤n y≤z = y≤z
max-lub {suc x} {.0} {suc z} (_≤_.s≤s x≤z) _≤_.z≤n = _≤_.s≤s x≤z
max-lub {suc x} {suc y} {suc z} (_≤_.s≤s x≤z) (_≤_.s≤s y≤z) =
  let max-xy≤z = max-lub {x}{y}{z} x≤z y≤z in
  _≤_.s≤s max-xy≤z

⊔⊆-inv : ∀{u v w : Value}
       → (u ⊔ v) ⊆ w
         ---------------
       → u ⊆ w  ×  v ⊆ w
⊔⊆-inv uvw = ⟨ (λ x → uvw (inj₁ x)) , (λ x → uvw (inj₂ x)) ⟩

⊆→depth≤ : ∀{u v : Value} → u ⊆ v → depth u ≤ depth v
⊆→depth≤ {⊥} {v} u⊆v = _≤_.z≤n
⊆→depth≤ {const x} {v} u⊆v = _≤_.z≤n
⊆→depth≤ {u₁ ↦ u₂} {v} u⊆v = ∈→depth≤ (u⊆v refl)
⊆→depth≤ {u₁ ⊔ u₂} {v} u⊆v
    with ⊔⊆-inv u⊆v
... | ⟨ u₁⊆v , u₂⊆v ⟩ =
    let u₁≤v = ⊆→depth≤ u₁⊆v in
    let u₂≤v = ⊆→depth≤ u₂⊆v in
    max-lub u₁≤v u₂≤v

dom-depth-≤ : ∀{u : Value} → depth (dom u) ≤ depth u
dom-depth-≤ {⊥} = _≤_.z≤n
dom-depth-≤ {const k} = _≤_.z≤n
dom-depth-≤ {v ↦ w} = ≤-step (m≤m⊔n (depth v) (depth w))
dom-depth-≤ {u ⊔ v} =
  let ih1 = dom-depth-≤ {u} in
  let ih2 = dom-depth-≤ {v} in
  ⊔-mono-≤ ih1 ih2

cod-depth-≤ : ∀{u : Value} → depth (cod u) ≤ depth u
cod-depth-≤ {⊥} = _≤_.z≤n
cod-depth-≤ {const k} = _≤_.z≤n
cod-depth-≤ {v ↦ w} = ≤-step (n≤m⊔n (depth v) (depth w))
cod-depth-≤ {u ⊔ v} =
  let ih1 = cod-depth-≤ {u} in
  let ih2 = cod-depth-≤ {v} in
  ⊔-mono-≤ ih1 ih2

≤′-trans : ∀{x y z} → x ≤′ y → y ≤′ z → x ≤′ z
≤′-trans x≤′y y≤′z = ≤⇒≤′ (≤-trans (≤′⇒≤ x≤′y) (≤′⇒≤ y≤′z))

data _<<_ : ℕ × ℕ → ℕ × ℕ → Set where
  fst : ∀{x x' y y'} → x <′ x' → ⟨ x , y ⟩ << ⟨ x' , y' ⟩
  snd : ∀{x x' y y'} → x ≤′ x' → y <′ y' → ⟨ x , y ⟩ << ⟨ x' , y' ⟩

<<-nat-wf : (P : ℕ → ℕ → Set) →
         (∀ x y → (∀ {x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → P x' y') → P x y) →
         ∀ x y → P x y
<<-nat-wf P ih x y = ih x y (help x y)
  where help : (x y : ℕ) → ∀{ x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → P x' y'
        help .(suc x') y {x'}{y'} (fst ≤′-refl) =
            ih x' y' (help x' y')
        help .(suc x) y {x'}{y'} (fst (≤′-step {x} q)) =
            help x y {x'}{y'} (fst q)
        help x .(suc y) {x'}{y} (snd x'≤x ≤′-refl) =
            let h : ∀ {x₁} {x₂} → (⟨ x₁ , x₂ ⟩ << ⟨ x , y ⟩) → P x₁ x₂
                h = help x y in
            ih x' y G
            where
            G : ∀ {x'' y'} → ⟨ x'' , y' ⟩ << ⟨ x' , y ⟩ → P x'' y'
            G {x''} {y'} (fst x''<x') =
               help x y (fst {y = y'}{y' = y} (≤′-trans x''<x' x'≤x))
            G {x''} {y'} (snd x''≤x' y'<y) =
               help x y {x''}{y'} (snd (≤′-trans x''≤x' x'≤x) y'<y)
        help x .(suc y) {x'}{y'} (snd x′≤x (≤′-step {y} q)) =
            help x y {x'}{y'} (snd x′≤x q)

⊑-trans-P : ℕ → ℕ → Set
⊑-trans-P d s = ∀{u v w} → d ≡ depth u + depth w → s ≡ size u + size v
                         → u ⊑ v → v ⊑ w → u ⊑ w

⊑-trans-rec : ∀ d s → ⊑-trans-P d s
⊑-trans-rec = <<-nat-wf ⊑-trans-P helper
  where
  helper : ∀ x y
         → (∀ {x' y'} → ⟨ x' , y' ⟩ << ⟨ x , y ⟩ → ⊑-trans-P x' y')
         → ⊑-trans-P x y
  helper d s IH {.⊥} {v} {w} d≡ s≡ ⊑-⊥ v⊑w = ⊑-⊥
  helper d s IH {.(const _)} {.(const _)} {w} d≡ s≡ ⊑-const v⊑w = v⊑w
  helper d s IH {u₁ ⊔ u₂} {v} {w} d≡ s≡ (⊑-conj-L u₁⊑v u₂⊑v) v⊑w
      rewrite d≡ | s≡ =
      let u₁⊑w = IH M1 {u₁}{v}{w} refl refl u₁⊑v v⊑w in
      let u₂⊑w = IH M2 {u₂}{v}{w} refl refl u₂⊑v v⊑w in
      ⊑-conj-L u₁⊑w u₂⊑w
      where
      M1a = begin
               depth u₁ + depth w
             ≤⟨ +-mono-≤ (m≤m⊔n (depth u₁) (depth u₂)) ≤-refl ⟩
               max (depth u₁) (depth u₂) + depth w
            ∎
      M1b = begin
               suc (size u₁ + size v)
            ≤⟨ s≤s (+-mono-≤ ≤-refl (n≤m+n (size u₂) (size v))) ⟩
               suc (size u₁ + (size u₂ + size v))
            ≤⟨ s≤s (≤-reflexive (sym (+-assoc (size u₁) (size u₂) (size v)))) ⟩
               suc (size u₁ + size u₂ + size v)
            ∎
      M1 : ⟨ depth u₁ + depth w , size u₁ + size v ⟩ <<
           ⟨ max (depth u₁) (depth u₂) + depth w ,
             suc (size u₁ + size u₂ + size v) ⟩
      M1 = snd (≤⇒≤′ M1a) (≤⇒≤′ M1b)
      M2a = begin
               depth u₂ + depth w
             ≤⟨ +-mono-≤ (n≤m⊔n (depth u₁) (depth u₂)) ≤-refl ⟩
               max (depth u₁) (depth u₂) + depth w
            ∎
      M2b = begin
               suc (size u₂ + size v)
            ≤⟨ s≤s (+-mono-≤ (n≤m+n (size u₁) (size u₂)) ≤-refl) ⟩
               suc ((size u₁ + size u₂) + size v)
            ∎
      M2 : ⟨ depth u₂ + depth w , size u₂ + size v ⟩ <<
           ⟨ max (depth u₁) (depth u₂) + depth w ,
             suc (size u₁ + size u₂ + size v) ⟩
      M2 = snd (≤⇒≤′ M2a) (≤⇒≤′ M2b)
  helper d s IH {u} {v₁ ⊔ v₂} {w} d≡ s≡ (⊑-conj-R1 u⊑v₁) v₁⊔v₂⊑w
      rewrite d≡ | s≡ =
      let v₁⊑w = ⊔⊑R v₁⊔v₂⊑w in
      IH M {u}{v₁}{w} refl refl u⊑v₁ v₁⊑w
      where
      Ma = begin
              suc (size u + size v₁)
           ≤⟨ ≤-reflexive (sym (+-suc (size u) (size v₁))) ⟩
              size u + suc (size v₁)
           ≤⟨ +-mono-≤ ≤-refl (s≤s (m≤m+n (size v₁) (size v₂))) ⟩
              size u + suc (size v₁ + size v₂)
           ∎
      M : ⟨ depth u + depth w , size u + size v₁ ⟩ <<
          ⟨ depth u + depth w , size u + suc (size v₁ + size v₂) ⟩
      M = snd (≤⇒≤′ ≤-refl) (≤⇒≤′ Ma)
  helper d s IH {u} {v₁ ⊔ v₂} {w} d≡ s≡ (⊑-conj-R2 u⊑v₂) v₁⊔v₂⊑w
      rewrite d≡ | s≡ =
      let v₂⊑w = ⊔⊑L v₁⊔v₂⊑w in
      IH M {u}{v₂}{w} refl refl u⊑v₂ v₂⊑w
      where
      Ma = begin
              suc (size u + size v₂)
           ≤⟨ ≤-reflexive (sym (+-suc (size u) (size v₂))) ⟩
              size u + suc (size v₂)
           ≤⟨ +-mono-≤ ≤-refl (s≤s (n≤m+n (size v₁) (size v₂))) ⟩
              size u + suc (size v₁ + size v₂)
           ∎
      M : ⟨ depth u + depth w , size u + size v₂ ⟩ <<
          ⟨ depth u + depth w , size u + suc (size v₁ + size v₂) ⟩
      M = snd (≤⇒≤′ ≤-refl) (≤⇒≤′ Ma)
  helper d s IH {u₁ ↦ u₂}{v}{w}d≡ s≡ (⊑-fun{u′ = v′}v′⊆v afv′ dv′⊑u₁ u₂⊑cv′) v⊑w
      rewrite d≡ | s≡
      with sub-inv-trans afv′ v′⊆v
                (λ {v₁}{v₂} v₁↦v₂∈v′ → ⊑-fun-inv {v′} {w} (u⊆v⊑w→u⊑w v′⊆v v⊑w)
                                         v₁↦v₂∈v′)
  ... | ⟨ w′ , ⟨ afw′ , ⟨ w′⊆w , ⟨ dw′⊑dv′ , cv′⊑cw′ ⟩ ⟩ ⟩ ⟩ =
        let dw′⊑u₁ = IH M1 {dom w′}{dom v′}{u₁} refl refl dw′⊑dv′ dv′⊑u₁ in
        let u₂⊑cw′ = IH M2 {u₂}{cod v′}{cod w′} refl refl u₂⊑cv′ cv′⊑cw′ in
        ⊑-fun{u′ = w′} w′⊆w afw′ dw′⊑u₁ u₂⊑cw′
      where
      dw′≤w : depth (dom w′) ≤ depth w
      dw′≤w = ≤-trans (dom-depth-≤{w′}) (⊆→depth≤ w′⊆w)
      cw′≤w : depth (cod w′) ≤ depth w
      cw′≤w = ≤-trans (cod-depth-≤{w′}) (⊆→depth≤ w′⊆w)

      M1a = begin
               suc (depth (dom w′) + depth u₁)
            ≤⟨ s≤s (≤-reflexive (+-comm (depth (dom w′)) (depth u₁))) ⟩
               suc (depth u₁ + depth (dom w′))
            ≤⟨ s≤s (+-mono-≤ (m≤m⊔n (depth u₁) (depth u₂)) dw′≤w) ⟩
               suc (max (depth u₁) (depth u₂) + depth w)
            ∎
      M1 : ⟨ depth (dom w′) + depth u₁ , size (dom w′) + size (dom v′) ⟩
        << ⟨ suc (max (depth u₁) (depth u₂) + depth w) ,
             suc (size u₁ + size u₂ + size v) ⟩
      M1 = fst (≤⇒≤′ M1a)
      M2a = begin
               suc (depth u₂ + depth (cod w′))
            ≤⟨ s≤s (+-mono-≤ (n≤m⊔n (depth u₁) (depth u₂)) cw′≤w) ⟩
               suc (max (depth u₁) (depth u₂) + depth w)
            ∎
      M2 : ⟨ depth u₂ + depth (cod w′) ,
             size u₂ + size (cod v′) ⟩
        << ⟨ suc (max (depth u₁) (depth u₂) + depth w) ,
             suc (size u₁ + size u₂ + size v) ⟩
      M2 = fst (≤⇒≤′ M2a)

⊑-trans : ∀{u v w} → u ⊑ v → v ⊑ w → u ⊑ w
⊑-trans {u} {v} {w} u⊑v v⊑w =
    ⊑-trans-rec (depth u + depth w) (size u + size v) refl refl u⊑v v⊑w


text:
-- Andreas, 2012-09-07
-- {-# OPTIONS -v tc.polarity:10 -v tc.conv.irr:20 -v tc.conv.elim:25 -v tc.conv.term:10 #-}
module Issue691 where

open import Common.Equality

data Bool : Set where
  true false : Bool

assert : (A : Set) → A → Bool → Bool
assert _ _ true  = true
assert _ _ false = false

g : Bool -> Bool -> Bool
g x true  = true
g x false = true

unsolved : Bool -> Bool
unsolved y =
  let X : Bool
      X = _
  in  assert (g X y ≡ g true y) refl X
-- X should be left unsolved

istrue : (unsolved false) ≡ true
istrue = refl

ext: agda

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Container combinators
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Container.Combinator where

open import Level using (Level; _⊔_; Lift)
open import Data.Empty using (⊥)
open import Data.Product as P using (_,_; proj₁; proj₂; ∃)
open import Data.Sum.Base as S using ([_,_]′)
open import Data.Unit.Base using (⊤)
import Function as F

open import Data.Container.Core
open import Data.Container.Relation.Unary.Any

------------------------------------------------------------------------
-- Combinators

module _ {s p : Level} where

-- Identity.

  id : Container s p
  id .Shape    = Lift s ⊤
  id .Position = F.const (Lift p ⊤)

-- Constant.

  const : Set s → Container s p
  const X .Shape    = X
  const X .Position = F.const (Lift p ⊥)

-- Composition.

infixr 9 _∘_

_∘_ : ∀ {s₁ s₂ p₁ p₂} → Container s₁ p₁ → Container s₂ p₂ →
      Container (s₁ ⊔ s₂ ⊔ p₁) (p₁ ⊔ p₂)
(C₁ ∘ C₂) .Shape    = ⟦ C₁ ⟧ (Shape C₂)
(C₁ ∘ C₂) .Position = ◇ C₁ (Position C₂)

-- Product. (Note that, up to isomorphism, this is a special case of
-- indexed product.)

infixr 2 _×_

_×_ : ∀ {s₁ s₂ p₁ p₂} → Container s₁ p₁ → Container s₂ p₂ →
      Container (s₁ ⊔ s₂) (p₁ ⊔ p₂)
(C₁ × C₂) .Shape    = Shape C₁ P.× Shape C₂
(C₁ × C₂) .Position = P.uncurry λ s₁ s₂ → (Position C₁ s₁) S.⊎ (Position C₂ s₂)

-- Indexed product.

Π : ∀ {i s p} (I : Set i) → (I → Container s p) → Container (i ⊔ s) (i ⊔ p)
Π I C .Shape    = ∀ i → Shape (C i)
Π I C .Position = λ s → ∃ λ i → Position (C i) (s i)

-- Constant exponentiation. (Note that this is a special case of
-- indexed product.)

infix 0 const[_]⟶_

const[_]⟶_ : ∀ {i s p} → Set i → Container s p → Container (i ⊔ s) (i ⊔ p)
const[ X ]⟶ C = Π X (F.const C)

-- Sum. (Note that, up to isomorphism, this is a special case of
-- indexed sum.)

infixr 1 _⊎_

_⊎_ : ∀ {s₁ s₂ p} → Container s₁ p → Container s₂ p → Container (s₁ ⊔ s₂) p
(C₁ ⊎ C₂) .Shape    = (Shape C₁ S.⊎ Shape C₂)
(C₁ ⊎ C₂) .Position = [ Position C₁ , Position C₂ ]′

-- Indexed sum.

Σ : ∀ {i s p} (I : Set i) → (I → Container s p) → Container (i ⊔ s) p
Σ I C .Shape    = ∃ λ i → Shape (C i)
Σ I C .Position = λ s → Position (C (proj₁ s)) (proj₂ s)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
{-
This file contains:
1. The iso π₃S²≅ℤ
2. A proof that π₃S² is generated by the Hopf map
-}
module Cubical.Homotopy.Group.Pi3S2 where

open import Cubical.Homotopy.Loopspace

open import Cubical.Homotopy.Group.LES
open import Cubical.Homotopy.Group.PinSn
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open Iso
open import Cubical.Foundations.Equiv

open import Cubical.HITs.SetTruncation renaming (elim to sElim)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.S1

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Int

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.Instances.Int

TotalHopf→∙S² : (Σ (S₊ 2) S¹Hopf , north , base) →∙ S₊∙ 2
fst TotalHopf→∙S² = fst
snd TotalHopf→∙S² = refl

IsoTotalSpaceJoin' : Iso (Σ (S₊ 2) S¹Hopf) (S₊ 3)
IsoTotalSpaceJoin' = compIso hopfS¹.IsoTotalSpaceJoin (IsoSphereJoin 1 1)

IsoFiberTotalHopfS¹ : Iso (fiber (fst TotalHopf→∙S²) north) S¹
fun IsoFiberTotalHopfS¹ ((x , y) , z) = subst S¹Hopf z y
inv IsoFiberTotalHopfS¹ x = (north , x) , refl
rightInv IsoFiberTotalHopfS¹ x = refl
leftInv IsoFiberTotalHopfS¹ ((x , y) , z) =
  ΣPathP
    ((ΣPathP
      (sym z , (λ i → transp (λ j → S¹Hopf (z (~ i ∧ j))) i y)))
         , (λ j i → z (i ∨ ~ j)))

IsoFiberTotalHopfS¹∙≡ :
  (fiber (fst TotalHopf→∙S²) north , (north , base) , refl) ≡ S₊∙ 1
IsoFiberTotalHopfS¹∙≡ = ua∙ (isoToEquiv IsoFiberTotalHopfS¹) refl

private
  transportGroupEquiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
      (n : ℕ) (f : A →∙ B)
    → isEquiv (fst (πLES.A→B f n))
    → isEquiv (fst (π'∘∙Hom n f))
  transportGroupEquiv n f iseq =
    transport (λ i → isEquiv (fst (π∘∙A→B-PathP n f i))) iseq

π₃S²≅π₃TotalHopf : GroupEquiv (πGr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                              (πGr 2 (S₊∙ 2))
fst (fst π₃S²≅π₃TotalHopf) = fst (πLES.A→B TotalHopf→∙S² 2)
snd (fst π₃S²≅π₃TotalHopf) =
  SES→isEquiv
    (isContr→≡UnitGroup
      (subst isContr (cong (π 3) (sym IsoFiberTotalHopfS¹∙≡))
        (∣ refl ∣₂ , (sElim (λ _ → isSetPathImplicit)
          (λ p → cong ∣_∣₂
            (isOfHLevelSuc 3 isGroupoidS¹ _ _ _ _ _ _ refl p))))))
    (isContr→≡UnitGroup
      (subst isContr (cong (π 2) (sym IsoFiberTotalHopfS¹∙≡))
        (∣ refl ∣₂ , (sElim (λ _ → isSetPathImplicit) (λ p
                    → cong ∣_∣₂ (isGroupoidS¹ _ _ _ _ refl p))))))
    (πLES.fib→A TotalHopf→∙S² 2)
    (πLES.A→B TotalHopf→∙S² 2)
    (πLES.B→fib TotalHopf→∙S² 1)
    (πLES.Ker-A→B⊂Im-fib→A TotalHopf→∙S² 2)
    (πLES.Ker-B→fib⊂Im-A→B TotalHopf→∙S² 1)
snd π₃S²≅π₃TotalHopf = snd (πLES.A→B TotalHopf→∙S² 2)

π'₃S²≅π'₃TotalHopf : GroupEquiv (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                                (π'Gr 2 (S₊∙ 2))
fst (fst π'₃S²≅π'₃TotalHopf) = fst (π'∘∙Hom 2 TotalHopf→∙S²)
snd (fst π'₃S²≅π'₃TotalHopf) =
  transportGroupEquiv 2 TotalHopf→∙S² (π₃S²≅π₃TotalHopf .fst .snd)
snd π'₃S²≅π'₃TotalHopf = snd (π'∘∙Hom 2 TotalHopf→∙S²)

πS³≅πTotalHopf : (n : ℕ)
  → GroupEquiv (π'Gr n (S₊∙ 3)) (π'Gr n (Σ (S₊ 2) S¹Hopf , north , base))
πS³≅πTotalHopf n =
  π'Iso n
   ((isoToEquiv
     (invIso
      (compIso
       (hopfS¹.IsoTotalSpaceJoin)
       (IsoSphereJoin 1 1))))
  , refl)

π₃S²≅ℤ : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤGroup
π₃S²≅ℤ =
  compGroupEquiv
    (invGroupEquiv
      (compGroupEquiv (πS³≅πTotalHopf 2) π'₃S²≅π'₃TotalHopf))
    (GroupIso→GroupEquiv (πₙ'Sⁿ≅ℤ 2))

-- We prove that the generator is the Hopf map
π₃TotalHopf-gen' : π' 3 (Σ (Susp S¹) S¹Hopf , north , base)
π₃TotalHopf-gen' =
  ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂

πS³≅πTotalHopf-gen :
  fst (fst (πS³≅πTotalHopf 2)) ∣ idfun∙ _ ∣₂ ≡ π₃TotalHopf-gen'
πS³≅πTotalHopf-gen =
  cong ∣_∣₂
    (∘∙-idʳ (inv (compIso (hopfS¹.IsoTotalSpaceJoin)
                 (IsoSphereJoin 1 1)) , refl))

πTotalHopf-gen :
  gen₁-by (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
    ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂
πTotalHopf-gen =
  subst (gen₁-by (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base)))
        πS³≅πTotalHopf-gen
        (Iso-pres-gen₁ (π'Gr 2 (S₊∙ 3))
                       (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                       ∣ idfun∙ _ ∣₂
                       (πₙ'Sⁿ-gen-by-idfun 2)
                       (GroupEquiv→GroupIso (πS³≅πTotalHopf 2)))

πTotalHopf≅πS²-gen :
    fst (fst π'₃S²≅π'₃TotalHopf)
      π₃TotalHopf-gen'
  ≡ ∣ HopfMap' , refl ∣₂
πTotalHopf≅πS²-gen =
  cong ∣_∣₂ (ΣPathP (refl , (sym (rUnit refl))))

π₂S³-gen-by-HopfMap' : gen₁-by (π'Gr 2 (S₊∙ 2)) ∣ HopfMap' , refl ∣₂
π₂S³-gen-by-HopfMap' =
  subst (gen₁-by (π'Gr 2 (S₊∙ 2)))  πTotalHopf≅πS²-gen
    (Iso-pres-gen₁ (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base)) (π'Gr 2 (S₊∙ 2))
      ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂
      πTotalHopf-gen
      (GroupEquiv→GroupIso π'₃S²≅π'₃TotalHopf))

π₂S³-gen-by-HopfMap : gen₁-by (π'Gr 2 (S₊∙ 2)) ∣ HopfMap ∣₂
π₂S³-gen-by-HopfMap =
  subst (gen₁-by (π'Gr 2 (S₊∙ 2)))
        (cong ∣_∣₂ (sym hopfMap≡HopfMap'))
        π₂S³-gen-by-HopfMap'

-- As a consequence, we also get that the Hopf invariant determines
-- an iso π₃S²≅ℤ
hopfInvariantEquiv : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤGroup
fst (fst hopfInvariantEquiv) = HopfInvariant-π' 0
snd (fst hopfInvariantEquiv) =
  GroupEquivℤ-isEquiv (invGroupEquiv π₃S²≅ℤ) ∣ HopfMap ∣₂
                      π₂S³-gen-by-HopfMap (GroupHom-HopfInvariant-π' 0)
                      (abs→⊎ _ _ HopfInvariant-HopfMap)
snd hopfInvariantEquiv = snd (GroupHom-HopfInvariant-π' 0)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2014-01-24, Issue 1411
-- First split might not succeed in the unifier,
-- so try later splits also.

-- {-# OPTIONS -v tc.lhs:10 #-}

open import Common.Prelude
open import Common.Equality

data Fin : Nat → Set where
  fzero : (n : Nat) → Fin (suc n)
  fsuc  : (n : Nat) → (i : Fin n) → Fin (suc n)

data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set where
  refl : a ≅ a

works : ∀ n m (i : Fin n) (j : Fin m) → n ≡ m → fsuc n i ≅ fsuc m j → i ≅ j
works n .n i .i refl refl = refl

fails : ∀ n m (i : Fin n) (j : Fin m) → fsuc n i ≅ fsuc m j → n ≡ m → i ≅ j
fails n .n i .i refl refl = refl

-- Refuse to solve heterogeneous constraint i : Fin n =?= j : Fin m
-- when checking that the pattern refl has type fsuc n i ≅ fsuc m j

-- Should work now.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}

module EnumEquiv where

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; _+_)
open import Data.Fin using (Fin; inject+; raise)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_,_; proj₁; proj₂)

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; module ≡-Reasoning)

open import Equiv using (_≃_; trans≃; _⊎≃_; iseq; module isequiv)
open import FinEquiv using (Fin0-⊥; module Plus)

open Plus using (+≃⊎; ⊎≃+)

------------------------------------------------------------------------------
-- An equivalence between a set 'A' and a finite set 'Fin n' is an
-- enumeration of A.

Enum : ∀ {ℓ} → (A : Set ℓ) → (n : ℕ) →  Set ℓ
Enum A n = A ≃ Fin n

-- We only need some additive equivalences...

0E : Enum ⊥ 0
0E = ⊥-elim , iseq Fin0-⊥ (λ { () }) Fin0-⊥ (λ { () })

_⊕e_ : {A : Set} {B : Set} {n m : ℕ} →
       Enum A n → Enum B m → Enum (A ⊎ B) (n + m)
eA ⊕e eB = trans≃ (eA ⊎≃ eB) ⊎≃+

-- shorthand to select the element indexed by i in the enumeration

select : {A B : Set} (eq : A ≃ B) → (B → A)
select (_ , iseq g _ _ _) = g

-- The enumeration of (A ⊎ B) is an enumeration of A followed by an
-- enumeration of B; in other words if we have an equivalence between
-- (A ⊎ B) and Fin (m + n) and we are given an index i < m then this
-- index selects an element of A.

-- evaluating an ⊕e on the left component

eval-left : {A B : Set} {m n : ℕ} {eA : Enum A m} {eB : Enum B n} (i : Fin m) →
  select (eA ⊕e eB) (inject+ n i) ≡ inj₁ (select eA i)
eval-left {m = m} {n} {eA} {eB} i =
  let (fwd , iseq bwd _ _ bwd∘fwd~id) = ⊎≃+ {m} {n} in
  begin (
    select (eA ⊕e eB) (inject+ n i)
      ≡⟨ refl ⟩ -- β reduce ⊕e, reverse-β Plus.fwd
    select (trans≃ (eA ⊎≃ eB) ⊎≃+) (fwd (inj₁ i))
      ≡⟨ refl ⟩ -- expand qinv.g and trans≃
    select (eA ⊎≃ eB) (select ⊎≃+ (fwd (inj₁ i)))
      ≡⟨ refl ⟩ -- expand rhs
    select (eA ⊎≃ eB) ((bwd ∘ fwd) (inj₁ i))
      ≡⟨ cong (select (eA ⊎≃ eB)) (bwd∘fwd~id (inj₁ i)) ⟩
    select (eA ⊎≃ eB) (inj₁ i)
      ≡⟨ refl ⟩ -- by definition of path⊎
    inj₁ (select eA i) ∎)
  where open ≡-Reasoning

eval-right : {A B : Set} {m n : ℕ} {eA : Enum A m} {eB : Enum B n} →
  (i : Fin n) → select (eA ⊕e eB) (raise m i) ≡ inj₂ (select eB i)
eval-right {eA = eA} {eB} i =
  cong (select (eA ⊎≃ eB)) (isequiv.β (proj₂ ⊎≃+) (inj₂ i))

------------------------------------------------------------------------------
-- We can also do the same for multiplication but it's not needed

-- _⊛e_ : {A B : Set} {n m : ℕ} → Enum A n → Enum B m → Enum (A × B) (n * m)
-- eA ⊛e eB = trans≃ (path× eA eB) Times.fwd-iso
--
-- etc.

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Progress of CBV reductions in Fω with interval kinds
------------------------------------------------------------------------

{-# OPTIONS --safe --without-K #-}

-- This module contains a variant of the "progress" theorem for Fω
-- with interval kinds.  Progress says roughly that well-typed terms
-- do not get stuck.  I.e. a well-typed term is either a value or it
-- can take a call-by-value (CBV) reduction step.  Together with the
-- subject reduction (aka "preservation") theorem from
-- FOmegaInt.Typing.Preservation, progress ensures type safety.  For
-- details, see e.g.
--
--  * B. C. Pierce, TAPL (2002), pp. 95.
--
--  * A. Wright and M. Felleisen, "A Syntactic Approach to Type
--    Soundness" (1994).

module FOmegaInt.Typing.Progress where

open import Data.Product using (_,_; ∃)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary.Negation using (contradiction)

open import FOmegaInt.Syntax
open import FOmegaInt.Typing
open import FOmegaInt.Typing.Inversion
open import FOmegaInt.Reduction.Cbv

open Syntax
open TermCtx
open Substitution using (_[_])
open Typing

-- A canonical forms lemma for universal types: closed values of
-- universal type are type abstractions.
Π-can : ∀ {f k a} → Val f → [] ⊢Tm f ∈ Π k a → ∃ λ k′ →
        ∃ λ a′ → f ≡ Λ k′ a′
Π-can (Λ k a) (∈-∀-i k-kd a∈b)   = k , a , refl
Π-can (Λ k a) (∈-⇑ Λka∈b b<:Πkc) = k , a , refl
Π-can (ƛ a b) (∈-⇑ ƛab∈c c<:Πkd) with Tm∈-gen ƛab∈c
Π-can (ƛ a b) (∈-⇑ ƛab∈c c<:Πkd) | ∈-→-i a∈* b∈e a⇒e<:c =
  contradiction (<:-trans a⇒e<:c c<:Πkd) ⇒-≮:-Π

-- A canonical forms lemma for arrow types: closed values of arrow
-- type are term abstractions.
⇒-can : ∀ {f a b} → Val f → [] ⊢Tm f ∈ a ⇒ b → ∃ λ a′ → ∃ λ b′ → f ≡ ƛ a′ b′
⇒-can (Λ k a) (∈-⇑ Λka∈b b<:c⇒d) with Tm∈-gen Λka∈b
⇒-can (Λ k a) (∈-⇑ Λka∈b b<:c⇒d) | ∈-∀-i k-kd a∈e Πke<:b =
  contradiction (<:-trans Πke<:b b<:c⇒d) Π-≮:-⇒
⇒-can (ƛ a b) (∈-→-i a∈* b∈c c∈*) = a , b , refl
⇒-can (ƛ a b) (∈-⇑ ƛab∈c c<:d⇒e)  = a , b , refl

-- Progress: well-typed terms do not get stuck (under CBV reduction).
prog : ∀ {a b} → [] ⊢Tm a ∈ b → Val a ⊎ (∃ λ a′ → a →v a′)
prog (∈-var () _ _)
prog (∈-∀-i k-kd b∈c)    = inj₁ (Λ _ _)
prog (∈-→-i a∈* b∈c c∈*) = inj₁ (ƛ _ _)
prog (∈-∀-e a∈Πkc b∈k) with prog a∈Πkc
prog (∈-∀-e a∈Πkc b∈k) | inj₁ u with Π-can u a∈Πkc
...| k′ , a′ , refl = inj₂ (_ , cont-⊡ k′ a′ _)
prog (∈-∀-e a∈Πkc b∈k) | inj₂ (a′ , a→a′) = inj₂ (_ , a→a′ ⊡ _)
prog (∈-→-e a∈c⇒d b∈c) with prog a∈c⇒d
prog (∈-→-e a∈c⇒d b∈c) | inj₁ u with prog b∈c
prog (∈-→-e a∈c⇒d b∈c) | inj₁ u | inj₁ v with ⇒-can u a∈c⇒d
...| c′ , a′ , refl = inj₂ (_ , cont-· c′ a′ v)
prog (∈-→-e a∈c⇒d b∈c) | inj₁ u | inj₂ (b′ , b→b′) = inj₂ (_ , u ·₂ b→b′)
prog (∈-→-e a∈c⇒d b∈c) | inj₂ (a′ , a→a′) = inj₂ (_ , a→a′ ·₁ _)
prog (∈-⇑ a∈b b<:c)    = prog a∈b

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
-- Andreas & James, 2016-04-18 pre-AIM XXIII
-- order of clauses should not matter here!

{-# OPTIONS --exact-split #-}

open import Common.Prelude

record R A : Set where
  field out : A

T : (x y : Bool) → Set
T true y     = R Bool
T false true = R Nat
T false false = R String

test : (x y : Bool) → T x y
R.out (test true  y)     = y
R.out (test false true ) = 0
R.out (test false false) = "hallo"

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

module Haskell.Modules.RWS.RustAnyHow where

open import Haskell.Modules.RWS
open import Haskell.Prelude

private
  variable
    Ev Wr St : Set
    A B C    : Set

ok   : A → RWS Ev Wr St (Either B A)
ok   = pure ∘ Right

bail : B → RWS Ev Wr St (Either B A)
bail = pure ∘ Left

infixl 4 _∙?∙_
_∙?∙_ : RWS Ev Wr St (Either C A) → (A → RWS Ev Wr St (Either C B)) → RWS Ev Wr St (Either C B)
_∙?∙_ = RWS-ebind

infixl 4 _∙^∙_
_∙^∙_ : RWS Ev Wr St (Either B A) → (B → B) → RWS Ev Wr St (Either B A)
m ∙^∙ f = do
  x ← m
  either (bail ∘ f) ok x


text:
module STLC.Type where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas using (TermLemmas)

open import Data.Nat using (ℕ; _+_)

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_)

open import Data.Vec using (Vec; []; _∷_; lookup)

open import Relation.Binary.PropositionalEquality as Eq
  using (refl; _≡_; sym; cong₂)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

-- --------------------------------------------------------------------
-- Types
-- --------------------------------------------------------------------
-- Recall that STLC types are defined as:
--  τ ::= α | τ -> τ
-- where α denotes a type variable.

infix 9 `_
infixr 7 _⇒_

data Type (n : ℕ) : Set where
  `_ : Fin n -> Type n
  _⇒_ : Type n -> Type n -> Type n

-- --------------------------------------------------------------------

module Substitution where

  -- This sub module defines application of the subtitution
  module Application₀ { T : ℕ -> Set } ( l : Lift T Type ) where
    open Lift l hiding  (var)

    -- Application of substitution to type
    infixl 8 _/_

    _/_ : ∀ { m n : ℕ } -> Type m -> Sub T m n -> Type n
    ` x / ρ = lift (lookup ρ x)
    (τ₁ ⇒ τ₂) / ρ = (τ₁ / ρ) ⇒ (τ₂ / ρ)

    open Application (record { _/_ = _/_ }) using (_/✶_)

    -- The application of sequences of substitutions is defined
    -- by (_/✶_). We use this to prove some generic lemmas on
    -- the lifting of sets

    ⇒-/✶-lift : ∀ k { m n τ₁ τ₂ } (ρs : Subs T m n) ->
        (τ₁ ⇒ τ₂) /✶ ρs ↑✶ k ≡ (τ₁ /✶ ρs ↑✶ k) ⇒ (τ₂ /✶ ρs ↑✶ k)
    ⇒-/✶-lift k ε = refl
    ⇒-/✶-lift k (ρ ◅ ρs) = cong₂ _/_ (⇒-/✶-lift k ρs) refl

  t = record
    {var = `_
    ; app = Application₀._/_
    }

  open TermSubst t public hiding (var)

  infix 8 _[/_]

  -- Shorthand for single-variable type substitutions
  _[/_] : ∀ { n } → Type (1 + n) → Type n → Type n
  τ₁ [/ τ₂ ] = τ₁ / sub τ₂

module Lemmas where

  module Lemmas₀ { T₁ T₂ } { l₁ : Lift T₁ Type} { l₂ : Lift T₂ Type } where
    open Substitution

    open Lifted l₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
    open Lifted l₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

    /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n)
      -> (∀ k x -> ` x /✶₁ ρs₁ ↑✶₁ k ≡ ` x /✶₂ ρs₂ ↑✶₂ k)
      -> ∀ k τ -> τ /✶₁ ρs₁ ↑✶₁ k ≡ τ /✶₂ ρs₂ ↑✶₂ k
    /✶-↑✶ ρs₁ ρs₂ hyp k (` x) = hyp k x
    /✶-↑✶ ρs₁ ρs₂ hyp k (τ₁ ⇒ τ₂) =
      begin
        (τ₁ ⇒ τ₂) /✶₁ ρs₁ ↑✶₁ k
      ≡⟨ Application₀.⇒-/✶-lift _ k ρs₁ ⟩
        (τ₁ /✶₁ ρs₁ ↑✶₁ k) ⇒ (τ₂ /✶₁ ρs₁ ↑✶₁ k)
      ≡⟨ cong₂ (_⇒_) (/✶-↑✶ ρs₁ ρs₂ hyp k τ₁) (/✶-↑✶ ρs₁ ρs₂ hyp k τ₂) ⟩
        (τ₁ /✶₂ ρs₂ ↑✶₂ k) ⇒ (τ₂ /✶₂ ρs₂ ↑✶₂ k)
      ≡⟨ sym (Application₀.⇒-/✶-lift _ k ρs₂) ⟩
        (τ₁ ⇒ τ₂) /✶₂ ρs₂ ↑✶₂ k
      ∎

  t : TermLemmas Type
  t = record
    { termSubst = Substitution.t
    ; app-var = refl
    ; /✶-↑✶ = Lemmas₀./✶-↑✶
    }

  open TermLemmas t public hiding (var)

module Operators where

  infixr 7 _⇒ⁿ_

  -- n-ary function type
  _⇒ⁿ_ : ∀ { n k } -> Vec (Type n) k -> Type n -> Type n
  [] ⇒ⁿ τ = τ
  (τ ∷ τs) ⇒ⁿ σ = τ ⇒ (τs ⇒ⁿ σ)

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types


text:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category using (Category; _[_≈_])

-- Karoubi Envelopes. These are the free completions of categories under split idempotents
module Categories.Category.Construction.KaroubiEnvelope {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Morphism.Idempotent.Bundles 𝒞
open import Categories.Morphism.Reasoning 𝒞

private
  module 𝒞 = Category 𝒞
  open 𝒞.HomReasoning
  open 𝒞.Equiv

  open Idempotent
  open Idempotent⇒

KaroubiEnvelope : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
KaroubiEnvelope = record
  { Obj = Idempotent
  ; _⇒_ = Idempotent⇒
  ; _≈_ = λ f g → 𝒞 [ Idempotent⇒.hom f ≈ Idempotent⇒.hom g ]
  ; id = id
  ; _∘_ = _∘_
  ; assoc = 𝒞.assoc
  ; sym-assoc = 𝒞.sym-assoc
  ; identityˡ = λ {I} {J} {f} → absorbˡ f
  ; identityʳ = λ {I} {J} {f} → absorbʳ f
  ; identity² = λ {I} → idempotent I
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≈ = 𝒞.∘-resp-≈
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning function extensionality for propositional equality
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Axiom.Extensionality.Propositional where

open import Function
open import Level using (Level; _⊔_; suc; lift)
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core

------------------------------------------------------------------------
-- Function extensionality states that if two functions are
-- propositionally equal for every input, then the functions themselves
-- must be propositionally equal.

Extensionality : (a b : Level) → Set _
Extensionality a b =
  {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) → f ≡ g

------------------------------------------------------------------------
-- Properties

-- If extensionality holds for a given universe level, then it also
-- holds for lower ones.

lower-extensionality : ∀ {a₁ b₁} a₂ b₂ →
                       Extensionality (a₁ ⊔ a₂) (b₁ ⊔ b₂) →
                       Extensionality a₁ b₁
lower-extensionality a₂ b₂ ext f≡g = cong (λ h → Level.lower ∘ h ∘ lift) $
    ext (cong (lift {ℓ = b₂}) ∘ f≡g ∘ Level.lower {ℓ = a₂})

-- Functional extensionality implies a form of extensionality for
-- Π-types.

∀-extensionality : ∀ {a b} → Extensionality a (suc b) →
                   {A : Set a} (B₁ B₂ : A → Set b) →
                   (∀ x → B₁ x ≡ B₂ x) →
                   (∀ x → B₁ x) ≡ (∀ x → B₂ x)
∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
∀-extensionality ext B .B  B₁≡B₂ | refl = refl


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLane1
open import homotopy.EilenbergMacLaneFunctor

module cohomology.CupProduct.OnEM.CommutativityInLowDegrees where

module _ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G

  import cohomology.CupProduct.OnEM.InLowDegrees G H as GH
  import cohomology.CupProduct.OnEM.InLowDegrees H G as HG
  open EMExplicit

  ×-cp₀₀-comm : EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 0 ∘ GH.×-cp₀₀
              ∼ HG.×-cp₀₀ ∘ ×-swap
  ×-cp₀₀-comm (g' , h') =
    (EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 0 $
     emloop $
     (<– (emloop-equiv G.grp) g') G⊗H.⊗ (<– (emloop-equiv H.grp) h'))
      =⟨ EM₁-fmap-emloop-β G⊗H.swap $
         (<– (emloop-equiv G.grp) g') G⊗H.⊗ (<– (emloop-equiv H.grp) h') ⟩
    (emloop $
     GroupHom.f G⊗H.swap $
     (<– (emloop-equiv G.grp) g') G⊗H.⊗ (<– (emloop-equiv H.grp) h'))
      =⟨ ap emloop $ G⊗H.swap-β (<– (emloop-equiv G.grp) g') (<– (emloop-equiv H.grp) h') ⟩
    (emloop $
     (<– (emloop-equiv H.grp) h') H⊗G.⊗ (<– (emloop-equiv G.grp) g')) =∎

  ⊙×-cp₀₀-comm :
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 0 ◃⊙∘
    GH.⊙×-cp₀₀ ◃⊙idf
    =⊙∘
    HG.⊙×-cp₀₀ ◃⊙∘
    ⊙×-swap ◃⊙idf
  ⊙×-cp₀₀-comm =
    ⊙seq-λ= ×-cp₀₀-comm $
    contr-center $ =ₛ-level {n = -2} $ EM-level H⊗G.abgroup 0

module CP₀₁-comm {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G

  import cohomology.CupProduct.OnEM.InLowDegrees G H as GH
  import cohomology.CupProduct.OnEM.InLowDegrees H G as HG

  private
    swap : H⊗G.grp →ᴳ G⊗H.grp
    swap = H⊗G.swap
    module swap = GroupHom swap

  cp₀₁-comm : ∀ g h →
    ap (GH.cp₀₁ g) (emloop h) ==
    ap (EM₁-fmap swap ∘ HG.cp₀₁ h) (emloop g)
  cp₀₁-comm g h =
    ap (GH.cp₀₁ g) (emloop h)
      =⟨ GH.cp₀₁-emloop-β g h ⟩
    emloop (g G⊗H.⊗ h)
      =⟨ ap emloop (! (H⊗G.swap-β h g)) ⟩
    emloop (swap.f (h H⊗G.⊗ g))
      =⟨ ! (EM₁-fmap-emloop-β swap (h H⊗G.⊗ g)) ⟩
    ap (EM₁-fmap swap) (emloop (h H⊗G.⊗ g))
      =⟨ ap (ap (EM₁-fmap swap)) (! (HG.cp₀₁-emloop-β h g)) ⟩
    ap (EM₁-fmap swap) (ap (HG.cp₀₁ h) (emloop g))
      =⟨ ∘-ap (EM₁-fmap swap) (HG.cp₀₁ h) (emloop g) ⟩
    ap (EM₁-fmap swap ∘ HG.cp₀₁ h) (emloop g) =∎

module CP₁₁-comm {i} {j} (G : AbGroup i) (H : AbGroup j) where

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G
    module swap = GroupHom H⊗G.swap

    import cohomology.CupProduct.OnEM.InLowDegrees G H as GH
    import cohomology.CupProduct.OnEM.InLowDegrees H G as HG

    infix 80 _G∪H_
    _G∪H_ : EM₁ G.grp → EM₁ H.grp → EMExplicit.EM G⊗H.abgroup 2
    _G∪H_ = GH.cp₁₁

    infix 80 _H∪G_
    _H∪G_ : EM₁ H.grp → EM₁ G.grp → EMExplicit.EM H⊗G.abgroup 2
    _H∪G_ = HG.cp₁₁

  ⊙−₁ : ⊙EM₁ H⊗G.grp ⊙→ ⊙EM₁ G⊗H.grp
  ⊙−₁ = ⊙EM₁-fmap (inv-hom G⊗H.abgroup) ⊙∘ ⊙EM₁-fmap H⊗G.swap

  −₁ : EM₁ H⊗G.grp → EM₁ G⊗H.grp
  −₁ = fst ⊙−₁

  − : EMExplicit.EM H⊗G.abgroup 2 → EMExplicit.EM G⊗H.abgroup 2
  − = Trunc-fmap (Susp-fmap −₁)

  ⊙− : EMExplicit.⊙EM H⊗G.abgroup 2 ⊙→ EMExplicit.⊙EM G⊗H.abgroup 2
  ⊙− = ⊙Trunc-fmap (⊙Susp-fmap −₁)

  comm-embase-emloop-seq : ∀ h →
    ap (λ y → embase G∪H y) (emloop h) =-=
    ap (λ y → − (y H∪G embase)) (emloop h)
  comm-embase-emloop-seq h =
    ap (λ y → embase G∪H y) (emloop h)
      =⟪idp⟫
    ap (cst [ north ]₂) (emloop h)
      =⟪ ap-cst [ north ]₂ (emloop h) ⟫
    idp
      =⟪idp⟫
    ap − (idp {a = [ north ]})
      =⟪ ! (ap (ap −) (HG.ap-cp₁₁-embase h)) ⟫
    ap − (ap (_H∪G embase) (emloop h))
      =⟪ ∘-ap − (_H∪G embase) (emloop h) ⟫
    ap (λ y → − (y H∪G embase)) (emloop h) ∎∎

  comm-emloop-embase-seq : ∀ g →
    ap (_G∪H embase) (emloop g) =-=
    ap (λ x → − (embase H∪G x)) (emloop g)
  comm-emloop-embase-seq g =
    ap (_G∪H embase) (emloop g)
      =⟪ GH.ap-cp₁₁-embase g ⟫
    idp
      =⟪ ! (ap-cst [ north ]₂ (emloop g)) ⟫
    ap (cst [ north ]₂) (emloop g)
      =⟪idp⟫
    ap (λ x → − (embase H∪G x)) (emloop g) ∎∎

  comm-embase-emloop' : ∀ h →
    ap (embase G∪H_) (emloop h) ==
    ap (λ y → − (y H∪G embase)) (emloop h)
  comm-embase-emloop' h = ↯ (comm-embase-emloop-seq h)

  comm-emloop-embase' : ∀ g →
    ap (λ x → GH.cp₁₁ x embase) (emloop g) ==
    ap (λ x → − (embase H∪G x)) (emloop g)
  comm-emloop-embase' g = ↯ (comm-emloop-embase-seq g)

  abstract

    comm-embase-emloop-comp' : ∀ h₁ h₂ →
      comm-embase-emloop' (H.comp h₁ h₂) ◃∙
      ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂) ◃∎
      =ₛ
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ◃∙
      ap-∙ (embase G∪H_) (emloop h₁) (emloop h₂) ◃∙
      ap2 _∙_ (comm-embase-emloop' h₁) (comm-embase-emloop' h₂) ◃∙
      ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂) ◃∎
    comm-embase-emloop-comp' h₁ h₂ =
      comm-embase-emloop' (H.comp h₁ h₂) ◃∙
      ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂) ◃∎
        =ₛ⟨ 0 & 1 & expand (comm-embase-emloop-seq (H.comp h₁ h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ! (ap (ap −) (HG.ap-cp₁₁-embase (H.comp h₁ h₂))) ◃∙
      ∘-ap − (_H∪G embase) (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂) ◃∎
        =ₛ⟨ 2 & 2 & !ₛ $
            homotopy-naturality (ap − ∘ ap (_H∪G embase))
                                (ap (λ y → − (y H∪G embase)))
                                (∘-ap − (_H∪G embase))
                                (emloop-comp h₁ h₂) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ! (ap (ap −) (HG.ap-cp₁₁-embase (H.comp h₁ h₂))) ◃∙
      ap (ap − ∘ ap (_H∪G embase)) (emloop-comp h₁ h₂) ◃∙
      ∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂) ◃∎
        =ₛ₁⟨ 1 & 1 & !-ap (ap −) (HG.ap-cp₁₁-embase (H.comp h₁ h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (HG.ap-cp₁₁-embase (H.comp h₁ h₂))) ◃∙
      ap (ap − ∘ ap (_H∪G embase)) (emloop-comp h₁ h₂) ◃∙
      ∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂) ◃∎
        =ₛ₁⟨ 2 & 1 & ap-∘ (ap −) (ap (_H∪G embase)) (emloop-comp h₁ h₂) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (HG.ap-cp₁₁-embase (H.comp h₁ h₂))) ◃∙
      ap (ap −) (ap (ap (_H∪G embase)) (emloop-comp h₁ h₂)) ◃∙
      ∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂) ◃∎
        =ₛ⟨ 1 & 2 &
            ap-seq-=ₛ (ap −) $
            post-rotate-seq-in {p = _ ◃∙ _ ◃∎} $
            pre-rotate'-in $
            !ₛ $ HG.ap-cp₁₁-embase-coh h₁ h₂ ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (ap2 _∙_ (HG.ap-cp₁₁-embase h₁) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ap (ap −) (! (ap-∙ (_H∪G embase) (emloop h₁) (emloop h₂))) ◃∙
      ∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂) ◃∎
        =ₛ₁⟨ 2 & 1 & ap-! (ap −) (ap-∙ (_H∪G embase) (emloop h₁) (emloop h₂))⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (ap2 _∙_ (HG.ap-cp₁₁-embase h₁) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ! (ap (ap −) (ap-∙ (_H∪G embase) (emloop h₁) (emloop h₂))) ◃∙
      ∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂) ◃∎
        =ₛ₁⟨ 3 & 1 & ! (!ap-∘=∘-ap − (_H∪G embase) (emloop h₁ ∙ emloop h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (ap2 _∙_ (HG.ap-cp₁₁-embase h₁) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ! (ap (ap −) (ap-∙ (_H∪G embase) (emloop h₁) (emloop h₂))) ◃∙
      ! (ap-∘ − (_H∪G embase) (emloop h₁ ∙ emloop h₂)) ◃∎
        =ₛ⟨ 2 & 2 &
            post-rotate-seq-in {p = _ ◃∙ _ ◃∎} $
            pre-rotate'-seq-in {p = _ ◃∙ _ ◃∎} $
            ap-∘-∙-coh − (_H∪G embase) (emloop h₁) (emloop h₂) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap (ap −) (! (ap2 _∙_ (HG.ap-cp₁₁-embase h₁) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ap-∙ − (ap (_H∪G embase) (emloop h₁)) (ap (_H∪G embase) (emloop h₂)) ◃∙
      ! (ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                 (ap-∘ − (_H∪G embase) (emloop h₂))) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ₁⟨ 1 & 1 &
              ap (ap (ap −)) (!-ap2 _∙_ (HG.ap-cp₁₁-embase h₁) (HG.ap-cp₁₁-embase h₂)) ∙
              ap-ap2 (ap −) _∙_ (! (HG.ap-cp₁₁-embase h₁)) (! (HG.ap-cp₁₁-embase h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap2 (λ p q → ap − (p ∙ q)) (! (HG.ap-cp₁₁-embase h₁)) (! (HG.ap-cp₁₁-embase h₂)) ◃∙
      ap-∙ − (ap (_H∪G embase) (emloop h₁)) (ap (_H∪G embase) (emloop h₂)) ◃∙
      ! (ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                 (ap-∘ − (_H∪G embase) (emloop h₂))) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ⟨ 1 & 2 &
            homotopy-naturality2 (λ p q → ap − (p ∙ q))
                                  (λ p q → ap − p ∙ ap − q)
                                  (λ p q → ap-∙ − p q)
                                  (! (HG.ap-cp₁₁-embase h₁))
                                  (! (HG.ap-cp₁₁-embase h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      idp ◃∙
      ap2 (λ p q → ap − p ∙ ap − q) (! (HG.ap-cp₁₁-embase h₁)) (! (HG.ap-cp₁₁-embase h₂)) ◃∙
      ! (ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                 (ap-∘ − (_H∪G embase) (emloop h₂))) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ⟨ 1 & 1 & expand [] ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap2 (λ p q → ap − p ∙ ap − q) (! (HG.ap-cp₁₁-embase h₁)) (! (HG.ap-cp₁₁-embase h₂)) ◃∙
      ! (ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                 (ap-∘ − (_H∪G embase) (emloop h₂))) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ₁⟨ 1 & 1 &
              ! (ap2-ap-lr _∙_ (ap −) (ap −) (! (HG.ap-cp₁₁-embase h₁)) (! (HG.ap-cp₁₁-embase h₂))) ∙
              ap2 (ap2 _∙_) (ap-! (ap −) (HG.ap-cp₁₁-embase h₁)) (ap-! (ap −) (HG.ap-cp₁₁-embase h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap2 _∙_ (! (ap (ap −) (HG.ap-cp₁₁-embase h₁))) (! (ap (ap −) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ! (ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                 (ap-∘ − (_H∪G embase) (emloop h₂))) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ₁⟨ 2 & 1 &
            !-ap2 _∙_ (ap-∘ − (_H∪G embase) (emloop h₁))
                      (ap-∘ − (_H∪G embase) (emloop h₂)) ∙
            ap2 (ap2 _∙_) (!ap-∘=∘-ap − (_H∪G embase) (emloop h₁))
                          (!ap-∘=∘-ap − (_H∪G embase) (emloop h₂)) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap2 _∙_ (! (ap (ap −) (HG.ap-cp₁₁-embase h₁))) (! (ap (ap −) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ap2 _∙_ (∘-ap − (_H∪G embase) (emloop h₁))
              (∘-ap − (_H∪G embase) (emloop h₂)) ◃∙
      ! (ap-∙ (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ◃∎
        =ₛ₁⟨ 3 & 1 & !ap-∙=∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂) ⟩
      ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
      ap2 _∙_ (! (ap (ap −) (HG.ap-cp₁₁-embase h₁))) (! (ap (ap −) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ap2 _∙_ (∘-ap − (_H∪G embase) (emloop h₁))
              (∘-ap − (_H∪G embase) (emloop h₂)) ◃∙
      ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂) ◃∎
        =ₛ⟨ 0 & 1 &
            ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∎
              =ₛ⟨ 1 & 0 & contract ⟩
            ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
            idp ◃∎
              =ₛ₁⟨ 1 & 1 & ! (ap-cst idp (emloop-comp h₁ h₂)) ⟩
            ap-cst [ north ] (emloop (H.comp h₁ h₂)) ◃∙
            ap (λ _ → idp) (emloop-comp h₁ h₂) ◃∎
              =ₛ⟨ !ₛ $ homotopy-naturality (ap (embase G∪H_))
                                           (λ _ → idp)
                                           (ap-cst [ north ])
                                           (emloop-comp h₁ h₂) ⟩
            ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ◃∙
            ap-cst [ north ] (emloop h₁ ∙ emloop h₂) ◃∎
              =ₛ⟨ 1 & 1 & ap-cst-coh [ north ] (emloop h₁) (emloop h₂) ⟩
            ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ◃∙
            ap-∙ (cst [ north ]) (emloop h₁) (emloop h₂) ◃∙
            ap2 _∙_ (ap-cst [ north ] (emloop h₁)) (ap-cst [ north ] (emloop h₂)) ◃∎ ∎ₛ
          ⟩
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ◃∙
      ap-∙ (cst [ north ]) (emloop h₁) (emloop h₂) ◃∙
      ap2 _∙_ (ap-cst [ north ] (emloop h₁)) (ap-cst [ north ] (emloop h₂)) ◃∙
      ap2 _∙_ (! (ap (ap −) (HG.ap-cp₁₁-embase h₁))) (! (ap (ap −) (HG.ap-cp₁₁-embase h₂))) ◃∙
      ap2 _∙_ (∘-ap − (_H∪G embase) (emloop h₁))
              (∘-ap − (_H∪G embase) (emloop h₂)) ◃∙
      ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂) ◃∎
        =ₛ⟨ 2 & 3 & ∙-ap2-seq _∙_ (comm-embase-emloop-seq h₁) (comm-embase-emloop-seq h₂) ⟩
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ◃∙
      ap-∙ (embase G∪H_) (emloop h₁) (emloop h₂) ◃∙
      ap2 _∙_ (comm-embase-emloop' h₁) (comm-embase-emloop' h₂) ◃∙
      ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂) ◃∎ ∎ₛ

    comm-emloop-comp-embase' : ∀ g₁ g₂ →
      comm-emloop-embase' (G.comp g₁ g₂) ◃∙
      ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂) ◃∎
      =ₛ
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (comm-emloop-embase' g₁) (comm-emloop-embase' g₂) ◃∙
      ∙-ap (λ x → − (embase H∪G x)) (emloop g₁) (emloop g₂) ◃∎
    comm-emloop-comp-embase' g₁ g₂ =
      comm-emloop-embase' (G.comp g₁ g₂) ◃∙
      ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂) ◃∎
        =ₛ⟨ 0 & 1 & expand (comm-emloop-embase-seq (G.comp g₁ g₂)) ⟩
      GH.ap-cp₁₁-embase (G.comp g₁ g₂) ◃∙
      ! (ap-cst [ north ] (emloop (G.comp g₁ g₂))) ◃∙
      ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂) ◃∎
        =ₛ⟨ 1 & 2 & !ₛ $
            homotopy-naturality
              (λ _ → idp)
              (ap (cst [ north ]))
              (λ p → ! (ap-cst [ north ] p))
              (emloop-comp g₁ g₂) ⟩
      GH.ap-cp₁₁-embase (G.comp g₁ g₂) ◃∙
      ap (λ _ → idp) (emloop-comp g₁ g₂) ◃∙
      ! (ap-cst [ north ] (emloop g₁ ∙ emloop g₂)) ◃∎
        =ₛ⟨ 1 & 1 & =ₛ-in {t = []} (ap-cst idp (emloop-comp g₁ g₂)) ⟩
      GH.ap-cp₁₁-embase (G.comp g₁ g₂) ◃∙
      ! (ap-cst [ north ] (emloop g₁ ∙ emloop g₂)) ◃∎
        =ₛ⟨ 0 & 1 & GH.ap-cp₁₁-embase-coh g₁ g₂ ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (GH.ap-cp₁₁-embase g₁) (GH.ap-cp₁₁-embase g₂) ◃∙
      ! (ap-cst [ north ] (emloop g₁ ∙ emloop g₂)) ◃∎
        =ₛ⟨ 3 & 1 & !-=ₛ $ ap-cst-coh [ north ] (emloop g₁) (emloop g₂) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (GH.ap-cp₁₁-embase g₁) (GH.ap-cp₁₁-embase g₂) ◃∙
      ! (ap2 _∙_ (ap-cst [ north ] (emloop g₁)) (ap-cst [ north ] (emloop g₂))) ◃∙
      ! (ap-∙ (cst [ north ]) (emloop g₁) (emloop g₂)) ◃∎
        =ₛ₁⟨ 3 & 1 & ! (ap2-! _∙_ (ap-cst [ north ] (emloop g₁)) (ap-cst [ north ] (emloop g₂))) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (GH.ap-cp₁₁-embase g₁) (GH.ap-cp₁₁-embase g₂) ◃∙
      ap2 _∙_ (! (ap-cst [ north ] (emloop g₁))) (! (ap-cst [ north ] (emloop g₂))) ◃∙
      ! (ap-∙ (cst [ north ]) (emloop g₁) (emloop g₂)) ◃∎
        =ₛ⟨ 2 & 2 & ∙-ap2-seq _∙_ (comm-emloop-embase-seq g₁) (comm-emloop-embase-seq g₂) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (comm-emloop-embase' g₁) (comm-emloop-embase' g₂) ◃∙
      ! (ap-∙ (cst [ north ]) (emloop g₁) (emloop g₂)) ◃∎
        =ₛ₁⟨ 3 & 1 & !ap-∙=∙-ap (cst [ north ]) (emloop g₁) (emloop g₂) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ◃∙
      ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ◃∙
      ap2 _∙_ (comm-emloop-embase' g₁) (comm-emloop-embase' g₂) ◃∙
      ∙-ap (cst [ north ]) (emloop g₁) (emloop g₂) ◃∎ ∎ₛ

    comm-emloop-emloop' : ∀ g h →
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap2 _∙_ (comm-embase-emloop' h) (comm-emloop-embase' g) ◃∎
      =ₛ
      ap2 _∙_ (comm-emloop-embase' g) (comm-embase-emloop' h) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
    comm-emloop-emloop' g h =
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap2 _∙_ (comm-embase-emloop' h) (comm-emloop-embase' g) ◃∎
        =ₛ⟨ 1 & 1 & ap2-out _∙_ (comm-embase-emloop' h) (comm-emloop-embase' g) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (comm-embase-emloop' h) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (comm-emloop-embase' g) ◃∎
        =ₛ⟨ 1 & 1 & ap-seq-=ₛ (_∙ ap (_G∪H embase) (emloop g))
                              (take-drop-split 1 (comm-embase-emloop-seq h)) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (comm-emloop-embase' g) ◃∎
        =ₛ⟨ 3 & 1 & ap-seq-∙ (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (comm-emloop-embase-seq g) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (GH.ap-cp₁₁-embase g) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (ap-cst [ north ] (emloop g))) ◃∎
        =ₛ⟨ 4 & 1 & ap-seq-=ₛ (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) step₄' ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (GH.ap-cp₁₁-embase g) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (↯ h₁'-seq) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
          (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ⟨ 2 & 2 & ap-comm-=ₛ _∙_ (↯ (tail (comm-embase-emloop-seq h))) (GH.ap-cp₁₁-embase g) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∙
      ap (_∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (↯ h₁'-seq) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
          (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ⟨ 3 & 2 & ap-comm-=ₛ _∙_ (↯ (tail (comm-embase-emloop-seq h))) (↯ h₁'-seq) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∙
      ap (idp ∙_) (↯ h₁'-seq) ◃∙
      ap (λ a → a ∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
          (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ₁⟨ 3 & 1 & ap (ap (idp ∙_)) (! (=ₛ-out heart))⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
      ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
      ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∙
      ap (idp ∙_) (↯ h₁-seq) ◃∙
      ap (λ a → a ∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
          (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ⟨ 0 & 3 & top-part ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_)
         (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
      ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∙
      ap (idp ∙_) (↯ h₁-seq) ◃∙
      ap (λ a → a ∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
      ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
         (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ⟨ 4 & 3 & bottom-part ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_)
         (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
      ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∙
      ap (idp ∙_) (↯ h₁-seq) ◃∙
      ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (! (ap-cst [ north ]₂ (emloop g))) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 2 & 2 & ap-comm-=ₛ _∙_ (GH.ap-cp₁₁-embase g) (↯ h₁-seq) ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_)
         (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ h₁-seq) ◃∙
      ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∙
      ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (! (ap-cst [ north ]₂ (emloop g))) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 3 & 2 & ap-comm-=ₛ _∙_ (GH.ap-cp₁₁-embase g) (↯ (tail (comm-embase-emloop-seq h))) ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_)
         (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ h₁-seq) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (GH.ap-cp₁₁-embase g) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (! (ap-cst [ north ]₂ (emloop g))) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 4 & 2 & ∙-ap-seq (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (comm-emloop-embase-seq g) ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_)
         (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ h₁-seq) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (comm-emloop-embase' g) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 0 & 3 & ap-seq-=ₛ (ap (_G∪H embase) (emloop g) ∙_) step₁₃' ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_) (ap-cst [ north ]₂ (emloop h)) ◃∙
      ap (ap (_G∪H embase) (emloop g) ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (comm-emloop-embase' g) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 0 & 2 & !ₛ $ ap-seq-=ₛ (ap (_G∪H embase) (emloop g) ∙_) $
                    take-drop-split 1 (comm-embase-emloop-seq h) ⟩
      ap (ap (_G∪H embase) (emloop g) ∙_) (comm-embase-emloop' h) ◃∙
      ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (comm-emloop-embase' g) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
        =ₛ⟨ 0 & 2 & !ₛ (ap2-out' _∙_ (comm-emloop-embase' g) (comm-embase-emloop' h)) ⟩
      ap2 _∙_ (comm-emloop-embase' g) (comm-embase-emloop' h) ◃∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎ ∎ₛ
      where
      h₀ : ∀ y → embase G∪H y == [ north ]₂
      h₀ y = idp
      h₁ : ∀ y → embase G∪H y == [ north ]₂
      h₁ = transport (λ x → ∀ y → x G∪H y == [ north ]₂) (emloop g) h₀
      h₀' : ∀ x → − (embase H∪G x) == [ north ]₂
      h₀' x = idp
      h₁' : ∀ x → − (embase H∪G x) == [ north ]₂
      h₁' = transport (λ y → ∀ x → − (y H∪G x) == [ north ]₂) (emloop h) h₀'
      h₁-path : ∀ y → h₁ y == ! (ap [_]₂ (GH.η (GH.cp₀₁ g y)))
      h₁-path y =
        transport (λ x → ∀ y → x G∪H y == [ north ]₂) (emloop g) h₀ y
          =⟨ app= (transp-naturality {B = λ x → ∀ y → x G∪H y == [ north ]₂}
                                     {C = λ x → x G∪H y == [ north ]₂}
                                     (λ k → k y)
                                     (emloop g)) h₀ ⟩
        transport (λ x → x G∪H y == [ north ]₂) (emloop g) (h₀ y)
          =⟨ to-transp {B = λ x → x G∪H y == [ north ]₂} {p = emloop g} $
             ↓-app=cst-in {f = _G∪H y}
                          {p = emloop g} {u = idp}
                          {v = ! (ap (_G∪H y) (emloop g))} $
             ! (!-inv-r (ap (_G∪H y) (emloop g))) ⟩
        ! (ap (_G∪H y) (emloop g))
          =⟨ ap ! (GH.ap-cp₁₁ g y) ⟩
        ! (ap [_] (GH.η (GH.cp₀₁ g y))) =∎
      h₁'-path : ∀ x → h₁' x == ! (ap [_]₂ (GH.η (−₁ (HG.cp₀₁ h x))))
      h₁'-path x =
        transport (λ y → ∀ x → − (y H∪G x) == [ north ]₂) (emloop h) h₀' x
          =⟨ app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                     {C = λ y → − (y H∪G x) == [ north ]₂}
                                     (λ k → k x)
                                     (emloop h)) h₀' ⟩
        transport (λ y → − (y H∪G x) == [ north ]₂) (emloop h) (h₀' x)
          =⟨ to-transp {B = λ y → − (y H∪G x) == [ north ]₂} {p = emloop h} $
             ↓-app=cst-in {f = λ y → − (y H∪G x)}
                          {p = emloop h} {u = idp}
                          {v = ! (ap (λ y → − (y H∪G x)) (emloop h))} $
             ! (!-inv-r (ap (λ y → − (y H∪G x)) (emloop h))) ⟩
        ! (ap (λ y → − (y H∪G x)) (emloop h))
          =⟨ ap ! (ap-∘ − (_H∪G x) (emloop h)) ⟩
        ! (ap − (ap (_H∪G x) (emloop h)))
          =⟨ ap (! ∘ ap −) (HG.ap-cp₁₁ h x) ⟩
        ! (ap − (ap [_]₂ (HG.η (HG.cp₀₁ h x))))
          =⟨ ap ! (∘-ap − [_]₂ (HG.η (HG.cp₀₁ h x))) ⟩
        ! (ap (λ p → [ Susp-fmap −₁ p ]₂) (HG.η (HG.cp₀₁ h x)))
          =⟨ ap ! (ap-∘ [_]₂ (Susp-fmap −₁) (HG.η (HG.cp₀₁ h x))) ⟩
        ! (ap [_]₂ (ap (Susp-fmap −₁) (HG.η (HG.cp₀₁ h x))))
          =⟨ ! (ap (! ∘ ap [_]₂) (app= (ap fst (η-natural ⊙−₁)) (HG.cp₀₁ h x))) ⟩
        ! (ap [_]₂ (GH.η (−₁ (HG.cp₀₁ h x)))) =∎
        where open import homotopy.SuspAdjointLoop using (η-natural)
      h₁-seq : idp {a = [ north ]₂} =-= idp
      h₁-seq = ! (!-inv-r (h₁ embase)) ◃∙
                ap (λ v → h₁ v ∙ ! (h₁ embase)) (emloop h) ◃∙
                !-inv-r (h₁ embase) ◃∎
      h₁'-seq : idp {a = [ north ]₂} =-= idp
      h₁'-seq = ! (!-inv-r (h₁' embase)) ◃∙
                ! (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g)) ◃∙
                !-inv-r (h₁' embase) ◃∎
      {- the crucial step in the commutative diagram -}
      heart : h₁-seq =ₛ h₁'-seq
      heart =
        ! (!-inv-r (h₁ embase)) ◃∙
        ap (λ v → h₁ v ∙ ! (h₁ embase)) (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∎
          =ₛ⟨ =ₛ-in {t = ! (!-inv-r (! (ap [_]₂ (GH.η embase)))) ◃∙
                         ap (λ v → ! (ap [_]₂ (GH.η (GH.cp₀₁ g v))) ∙ ! (! (ap [_] (GH.η embase)))) (emloop h) ◃∙
                         !-inv-r (! (ap [_]₂ (GH.η embase))) ◃∎} $
              ap (λ f → ! (!-inv-r (f embase)) ∙
                        ap (λ v → f v ∙ ! (f embase)) (emloop h) ∙
                        !-inv-r (f embase))
                  (λ= h₁-path) ⟩
        ! (!-inv-r (! (ap [_]₂ (GH.η embase)))) ◃∙
        ap (λ v → ! (ap [_]₂ (GH.η (GH.cp₀₁ g v))) ∙ ! (! (ap [_]₂ (GH.η embase)))) (emloop h) ◃∙
        !-inv-r (! (ap [_]₂ (GH.η embase))) ◃∎
          =ₛ₁⟨ 1 & 1 &
                ap (λ v → ! (ap [_]₂ (GH.η (GH.cp₀₁ g v))) ∙ ! (! (ap [_]₂ (GH.η embase)))) (emloop h)
                  =⟨ ap-∘ (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (GH.cp₀₁ g) (emloop h) ⟩
                ap (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (ap (GH.cp₀₁ g) (emloop h))
                  =⟨ ap (ap (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase))))) $
                    ap (GH.cp₀₁ g) (emloop h)
                      =⟨ CP₀₁-comm.cp₀₁-comm G H g h ⟩
                    ap (EM₁-fmap H⊗G.swap ∘ HG.cp₀₁ h) (emloop g)
                      =⟨ ! (!-! _) ⟩
                    ! (! (ap (EM₁-fmap H⊗G.swap ∘ HG.cp₀₁ h) (emloop g)))
                      =⟨ ap ! (! (EM₁-neg-! G⊗H.abgroup _)) ⟩
                    ! (ap (EM₁-neg G⊗H.abgroup) (ap (EM₁-fmap H⊗G.swap ∘ HG.cp₀₁ h) (emloop g)))
                      =⟨ ap ! (∘-ap (EM₁-neg G⊗H.abgroup) (EM₁-fmap H⊗G.swap ∘ HG.cp₀₁ h) (emloop g)) ⟩
                    ! (ap (−₁ ∘ HG.cp₀₁ h) (emloop g)) =∎
                    -- Yo dawg, I herd you like continued equalities,
                    -- so we put continued equalities into your continued equalities,
                    -- so u can reason equationally while u reason equationally.
                  ⟩
                ap (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (! (ap (−₁ ∘ HG.cp₀₁ h) (emloop g)))
                  =⟨ ap-! (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (ap (−₁ ∘ HG.cp₀₁ h) (emloop g)) ⟩
                ! (ap (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (ap (−₁ ∘ HG.cp₀₁ h) (emloop g)))
                  =⟨ ap ! (∘-ap (λ w → ! (ap [_]₂ (GH.η w)) ∙ ! (! (ap [_]₂ (GH.η embase)))) (−₁ ∘ HG.cp₀₁ h) (emloop g)) ⟩
                ! (ap (λ v → ! (ap [_]₂ (GH.η (−₁ (HG.cp₀₁ h v)))) ∙ ! (! (ap [_]₂ (GH.η embase)))) (emloop g)) =∎
              ⟩
        ! (!-inv-r (! (ap [_]₂ (GH.η embase)))) ◃∙
        ! (ap (λ v → ! (ap [_]₂ (GH.η (−₁ (HG.cp₀₁ h v)))) ∙ ! (! (ap [_]₂ (GH.η embase)))) (emloop g)) ◃∙
        !-inv-r (! (ap [_]₂ (GH.η embase))) ◃∎
          =ₛ⟨ =ₛ-in {t = ! (!-inv-r (h₁' embase)) ◃∙
                         ! (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g)) ◃∙
                         !-inv-r (h₁' embase) ◃∎} $
              ap (λ f → ! (!-inv-r (f embase)) ∙
                        ! (ap (λ v → f v ∙ ! (f embase)) (emloop g)) ∙
                        !-inv-r (f embase))
                  (! (λ= h₁'-path)) ⟩
        ! (!-inv-r (h₁' embase)) ◃∙
        ! (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g)) ◃∙
        !-inv-r (h₁' embase) ◃∎ ∎ₛ
      transp-nat-idp : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B → C)
        {a₀ a₁ : A} (p : a₀ == a₁) (b : B)
        (c : C) (h₀ : ∀ b' → f a₀ b' == c)
        → app= (transp-naturality {B = λ a → ∀ b → f a b == c} (λ h → h b ∙ ! (h b)) p) h₀ ◃∎
          =ₛ
          !-inv-r (transport (λ a → ∀ b → f a b == c) p h₀ b) ◃∙
          ! (transp-idp (λ a → f a b) p) ◃∙
          ap (transport (λ a → f a b == f a b) p) (! (!-inv-r (h₀ b))) ◃∎
      transp-nat-idp f p@idp b c h₀ = !ₛ $
        !-inv-r (h₀ b) ◃∙
        idp ◃∙
        ap (λ r → r) (! (!-inv-r (h₀ b))) ◃∎
          =ₛ⟨ 1 & 1 & expand [] ⟩
        !-inv-r (h₀ b) ◃∙
        ap (λ r → r) (! (!-inv-r (h₀ b))) ◃∎
          =ₛ₁⟨ 1 & 1 & ap-idf (! (!-inv-r (h₀ b))) ⟩
        !-inv-r (h₀ b) ◃∙
        ! (!-inv-r (h₀ b)) ◃∎
          =ₛ₁⟨ !-inv-r (!-inv-r (h₀ b)) ⟩
        idp ◃∎ ∎ₛ
      top-part :
        ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
        ap (_∙ ap (_G∪H embase) (emloop g)) (ap-cst [ north ] (emloop h)) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∎
      top-part =
        ap-comm _G∪H_ (emloop g) (emloop h) ◃∙
        ap (_∙ ap (_G∪H embase) (emloop g))
           (ap-null-homotopic (λ y → [ north ]₂) (λ y → idp) (emloop' H.grp h)) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ⟨ 0 & 2 & post-rotate-out {r = _ ◃∙ _ ◃∙ _ ◃∎} $
                      ap-comm-cst-coh _G∪H_ (emloop g) (emloop h) [ north ]₂ (λ y → idp) ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (app= (transp-naturality {B = λ x → ∀ y → x G∪H y == [ north ]₂} {C = λ x → x G∪H embase == x G∪H embase}
                                    (λ h → h embase ∙ ! (h embase)) (emloop g))
                 (λ y → idp)) ◃∙
        ! (ap-transp (_G∪H embase) (_G∪H embase) (emloop g) idp) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ⟨ 1 & 1 & ap-seq-=ₛ (ap (_G∪H embase) (emloop g) ∙_)
                                (transp-nat-idp _G∪H_ (emloop g) embase [ north ]₂ (λ y → idp)) ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_)
            (! (transp-idp (_G∪H embase) (emloop g))) ◃∙
        idp ◃∙
        ! (ap-transp (_G∪H embase) (_G∪H embase) (emloop g) idp) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ⟨ 3 & 1 & expand [] ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (! (transp-idp (_G∪H embase) (emloop g))) ◃∙
        ! (ap-transp (_G∪H embase) (_G∪H embase) (emloop g) idp) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ₁⟨ 2 & 1 & ap-! (ap (_G∪H embase) (emloop g) ∙_) (transp-idp (_G∪H embase) (emloop g)) ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ! (ap (ap (_G∪H embase) (emloop g) ∙_)
              (transp-idp (_G∪H embase) (emloop g))) ◃∙
        ! (ap-transp (_G∪H embase) (_G∪H embase) (emloop g) idp) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ⟨ 2 & 2 & pre-rotate'-seq-in {p = _ ◃∙ _ ◃∎} {r = []} $
                      !ₛ $ ap-transp-idp (_G∪H embase) (emloop g) ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ∙-unit-r (ap (_G∪H embase) (emloop g)) ◃∙
        ap (idp ∙_) (GH.ap-cp₁₁-embase g) ◃∎
          =ₛ⟨ 2 & 2 & !ₛ $ homotopy-naturality (_∙ idp) (idp ∙_) ∙-unit-r (GH.ap-cp₁₁-embase g) ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∙
        idp ◃∎
          =ₛ⟨ 3 & 1 & expand [] ⟩
        ap (ap (_G∪H embase) (emloop g) ∙_)
           (ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h)) ◃∙
        ap (ap (_G∪H embase) (emloop g) ∙_) (!-inv-r (h₁ embase)) ◃∙
        ap (_∙ idp) (GH.ap-cp₁₁-embase g) ◃∎ ∎ₛ
      bottom-part :
        ap (_∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
        =ₛ
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (! (ap-cst [ north ]₂ (emloop g))) ◃∙
        ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
      bottom-part =
        ap (_∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ⟨ 0 & 0 & contract ⟩
        idp ◃∙
        ap (_∙ idp) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ⟨ 0 & 2 & !ₛ (homotopy-naturality (idp ∙_) (_∙ idp) (! ∘ ∙-unit-r) (↯ (tail (comm-embase-emloop-seq h)))) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ! (∙-unit-r (ap (λ y → − (y H∪G embase)) (emloop h))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ⟨ 1 & 1 & !ₛ $ post-rotate-in {p = _ ◃∙ _ ◃∎} $
                      ap-transp-idp (λ y → − (y H∪G embase)) (emloop h) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap-transp (λ y → − (y H∪G embase)) (λ y → − (y H∪G embase)) (emloop h) idp ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (transp-idp (λ y → − (y H∪G embase)) (emloop h)) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) (! (!-inv-r (h₁' embase))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ⟨ 2 & 2 & ap-seq-=ₛ (ap (λ y → − (y H∪G embase)) (emloop h) ∙_) $
              transp-idp (λ y → − (y H∪G embase)) (emloop h) ◃∙
              ! (!-inv-r (h₁' embase)) ◃∎
                =ₛ⟨ pre-rotate-out $ pre-rotate'-in $ post-rotate-in {p = []} $
                    transp-nat-idp (λ y x → − (y H∪G x)) (emloop h) embase [ north ]₂ (λ x → idp) ⟩
              idp ◃∙
              ! (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                          (λ h → h embase ∙ ! (h embase)) (emloop h))
                      (λ x → idp)) ◃∎
                =ₛ⟨ 0 & 1 & expand [] ⟩
              ! (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                          (λ h → h embase ∙ ! (h embase)) (emloop h))
                      (λ x → idp)) ◃∎ ∎ₛ
            ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap-transp (λ y → − (y H∪G embase)) (λ y → − (y H∪G embase)) (emloop h) idp ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                        (λ h → h embase ∙ ! (h embase)) (emloop h))
                    (λ x → idp))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ₁⟨ 2 & 1 & ap-! (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
                            (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                                      (λ h → h embase ∙ ! (h embase)) (emloop h))
                                  (λ x → idp)) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap-transp (λ y → − (y H∪G embase)) (λ y → − (y H∪G embase)) (emloop h) idp ◃∙
        ! (ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
              (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                        (λ h → h embase ∙ ! (h embase)) (emloop h))
                    (λ x → idp))) ◃∙
        ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
           (! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ₁⟨ 3 & 1 & ap-! (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
                            (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g)) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap-transp (λ y → − (y H∪G embase)) (λ y → − (y H∪G embase)) (emloop h) idp ◃∙
        ! (ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
              (app= (transp-naturality {B = λ y → ∀ x → − (y H∪G x) == [ north ]₂}
                                        (λ h → h embase ∙ ! (h embase)) (emloop h))
                    (λ x → idp))) ◃∙
        ! (ap (ap (λ y → − (y H∪G embase)) (emloop h) ∙_)
              (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g))) ◃∎
          =ₛ⟨ 1 & 3 & pre-rotate-out $
                      pre-rotate'-seq-in {p = _ ◃∙ _ ◃∎} $
                      post-rotate-in {p = []} $
                      ap-comm-cst-coh (λ y x → − (y H∪G x))
                                      (emloop h) (emloop g) [ north ]₂ (λ x → idp) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ! (ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h))
              (ap-null-homotopic (λ x → − (embase H∪G x)) (λ x → idp) (emloop g))) ◃∙
        ! (ap-comm (λ y x → − (y H∪G x)) (emloop h) (emloop g)) ◃∎
          =ₛ₁⟨ 2 & 1 & ! (ap-comm-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h)) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ! (ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h))
              (ap-null-homotopic (λ x → − (embase H∪G x)) (λ x → idp) (emloop g))) ◃∙
        ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎
          =ₛ₁⟨ 1 & 1 &
               !-ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h))
                    (ap-null-homotopic (λ x → − (embase H∪G x)) (λ x → idp) (emloop g)) ⟩
        ap (idp ∙_) (↯ (tail (comm-embase-emloop-seq h))) ◃∙
        ap (_∙ ap (λ y → − (y H∪G embase)) (emloop h)) (! (ap-cst [ north ]₂ (emloop g))) ◃∙
        ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) ◃∎ ∎ₛ
      step₄' : ! (ap-cst [ north ] (emloop g)) ◃∎
                =ₛ
                ↯ h₁'-seq ◃∙
                ! (!-inv-r (h₁' embase)) ◃∙
                ! (ap-null-homotopic (λ x → [ north ]₂) h₁' (emloop g)) ◃∎
      step₄' = pre-rotate'-in $ post-rotate-seq-in {p = []} $ !ₛ $
        ap-cst [ north ]₂ (emloop g) ◃∙
        ↯ h₁'-seq ◃∎
          =ₛ⟨ 1 & 1 & expand h₁'-seq ⟩
        ap-cst [ north ] (emloop g) ◃∙
        ! (!-inv-r (h₁' embase)) ◃∙
        ! (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g)) ◃∙
        !-inv-r (h₁' embase) ◃∎
          =ₛ⟨ 0 & 2 & !ₛ $ post-rotate-in {p = _ ◃∙ _ ◃∎} $
                      ap-null-homotopic-cst [ north ]₂ [ north ]₂ h₁' (emloop g) ⟩
        ap-null-homotopic (cst [ north ]₂) h₁' (emloop g) ◃∙
        ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g) ◃∙
        ! (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g)) ◃∙
        !-inv-r (h₁' embase) ◃∎
          =ₛ⟨ 1 & 2 & seq-!-inv-r (ap (λ v → h₁' v ∙ ! (h₁' embase)) (emloop g) ◃∎) ⟩
        ap-null-homotopic (cst [ north ]₂) h₁' (emloop g) ◃∙
        !-inv-r (h₁' embase) ◃∎ ∎ₛ
      step₁₃' :
        ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∙
        ↯ h₁-seq ◃∎
        =ₛ
        ap-cst [ north ]₂ (emloop h) ◃∎
      step₁₃' =
        ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∙
        ↯ h₁-seq ◃∎
          =ₛ⟨ 2 & 1 & expand h₁-seq ⟩
        ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∙
        ! (!-inv-r (h₁ embase)) ◃∙
        ap (λ v → h₁ v ∙ ! (h₁ embase)) (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∎
          =ₛ⟨ 1 & 2 & seq-!-inv-r (!-inv-r (h₁ embase) ◃∎) ⟩
        ap-null-homotopic (λ y → [ north ]₂) h₁ (emloop h) ◃∙
        ap (λ v → h₁ v ∙ ! (h₁ embase)) (emloop h) ◃∙
        !-inv-r (h₁ embase) ◃∎
          =ₛ⟨ ap-null-homotopic-cst [ north ]₂ [ north ]₂ h₁ (emloop h) ⟩
        ap-cst [ north ]₂ (emloop h) ◃∎ ∎ₛ

  comm-embase-emloop : ∀ h →
    Square idp
            (ap (embase G∪H_) (emloop h))
            (ap (λ y → − (y H∪G embase)) (emloop h))
            idp
  comm-embase-emloop h = vert-degen-square (comm-embase-emloop' h)

  comm-emloop-embase : ∀ g →
    Square idp
            (ap (_G∪H embase) (emloop g))
            (ap (λ x → − (embase H∪G x)) (emloop g))
            idp
  comm-emloop-embase g = vert-degen-square (comm-emloop-embase' g)

  abstract

    square-helper : ∀ {i} {A : Type i}
      {a a' a'' : A}
      {p₀ : a == a'} {q₀ : a' == a''} {r₀ : a == a''}
      {p₁ : a == a'} {q₁ : a' == a''} {r₁ : a == a''}
      (s : r₀ == p₀ ∙ q₀)
      (p : p₀ == p₁)
      (q : q₀ == q₁)
      (t : p₁ ∙ q₁ == r₁)
      → s ∙v⊡ (vert-degen-square p ⊡h vert-degen-square q) ⊡v∙ t ==
        vert-degen-square (s ∙ ap2 _∙_ p q ∙ t)
    square-helper s p q t =
      s ∙v⊡ (vert-degen-square p ⊡h vert-degen-square q) ⊡v∙ t
        =⟨ ap (λ u → s ∙v⊡ u ⊡v∙ t) (vert-degen-square-⊡h p q) ⟩
      s ∙v⊡ vert-degen-square (ap2 _∙_ p q) ⊡v∙ t
        =⟨ ap (s ∙v⊡_) (vert-degen-square-⊡v∙ (ap2 _∙_ p q) t) ⟩
      s ∙v⊡ vert-degen-square (ap2 _∙_ p q ∙ t)
        =⟨ vert-degen-square-∙v⊡ s (ap2 _∙_ p q ∙ t) ⟩
      vert-degen-square (s ∙ ap2 _∙_ p q ∙ t) =∎

    comm-embase-emloop-comp : ∀ h₁ h₂ →
      comm-embase-emloop (H.comp h₁ h₂) ⊡v∙
      ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂)
      ==
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡
      ↓-='-square-comp (comm-embase-emloop h₁) (comm-embase-emloop h₂)
    comm-embase-emloop-comp h₁ h₂ =
      comm-embase-emloop (H.comp h₁ h₂) ⊡v∙
      ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂)
        =⟨ vert-degen-square-⊡v∙
              (comm-embase-emloop' (H.comp h₁ h₂))
              (ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂)) ⟩
      vert-degen-square
        (comm-embase-emloop' (H.comp h₁ h₂) ∙
          ap (ap (λ y → − (y H∪G embase))) (emloop-comp h₁ h₂))
        =⟨ ap vert-degen-square (=ₛ-out (comm-embase-emloop-comp' h₁ h₂)) ⟩
      vert-degen-square
        (ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙
          ap-∙ (embase G∪H_) (emloop h₁) (emloop h₂) ∙
          ap2 _∙_ (comm-embase-emloop' h₁) (comm-embase-emloop' h₂) ∙
          ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂))
        =⟨ ! $ vert-degen-square-∙v⊡ (ap (ap (embase G∪H_)) (emloop-comp h₁ h₂)) _ ⟩
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡
      vert-degen-square
        (ap-∙ (embase G∪H_) (emloop h₁) (emloop h₂) ∙
          ap2 _∙_ (comm-embase-emloop' h₁) (comm-embase-emloop' h₂) ∙
          ∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂))
        =⟨ ap (ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡_) $ ! $
           square-helper (ap-∙ (embase G∪H_) (emloop h₁) (emloop h₂))
                         (comm-embase-emloop' h₁) (comm-embase-emloop' h₂)
                         (∙-ap (λ y → − (y H∪G embase)) (emloop h₁) (emloop h₂)) ⟩
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡
      ↓-='-square-comp' (comm-embase-emloop h₁) (comm-embase-emloop h₂)
        =⟨ ap (ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡_) $
           ↓-='-square-comp'=↓-='-square-comp (comm-embase-emloop h₁)
                                              (comm-embase-emloop h₂) ⟩
      ap (ap (embase G∪H_)) (emloop-comp h₁ h₂) ∙v⊡
      ↓-='-square-comp (comm-embase-emloop h₁) (comm-embase-emloop h₂) =∎

    comm-emloop-comp-embase : ∀ g₁ g₂ →
      comm-emloop-embase (G.comp g₁ g₂) ⊡v∙
      ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂)
      ==
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡
      ↓-='-square-comp (comm-emloop-embase g₁) (comm-emloop-embase g₂)
    comm-emloop-comp-embase g₁ g₂ =
      comm-emloop-embase (G.comp g₁ g₂) ⊡v∙
      ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂)
        =⟨ vert-degen-square-⊡v∙
             (comm-emloop-embase' (G.comp g₁ g₂))
             (ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂)) ⟩
      vert-degen-square
        (comm-emloop-embase' (G.comp g₁ g₂) ∙
          ap (ap (λ x → − (embase H∪G x))) (emloop-comp g₁ g₂))
          =⟨ ap vert-degen-square (=ₛ-out (comm-emloop-comp-embase' g₁ g₂)) ⟩
      vert-degen-square
        (ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙
         ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ∙
         ap2 _∙_ (comm-emloop-embase' g₁) (comm-emloop-embase' g₂) ∙
         ∙-ap (λ x → − (embase H∪G x)) (emloop g₁) (emloop g₂))
        =⟨ ! $ vert-degen-square-∙v⊡ (ap (ap (_G∪H embase)) (emloop-comp g₁ g₂)) _ ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡
      vert-degen-square
        (ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂) ∙
         ap2 _∙_ (comm-emloop-embase' g₁) (comm-emloop-embase' g₂) ∙
         ∙-ap (λ x → − (embase H∪G x)) (emloop g₁) (emloop g₂))
        =⟨ ap (ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡_) $ ! $
           square-helper
             (ap-∙ (_G∪H embase) (emloop g₁) (emloop g₂))
             (comm-emloop-embase' g₁) (comm-emloop-embase' g₂)
             (∙-ap (λ x → − (embase H∪G x)) (emloop g₁) (emloop g₂)) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡
      ↓-='-square-comp' (comm-emloop-embase g₁) (comm-emloop-embase g₂)
        =⟨ ap (ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡_) $
           ↓-='-square-comp'=↓-='-square-comp
             (comm-emloop-embase g₁) (comm-emloop-embase g₂) ⟩
      ap (ap (_G∪H embase)) (emloop-comp g₁ g₂) ∙v⊡
      ↓-='-square-comp (comm-emloop-embase g₁) (comm-emloop-embase g₂) =∎

    comm-emloop-emloop : ∀ g h →
      ap-comm _G∪H_ (emloop g) (emloop h) ∙v⊡
      comm-embase-emloop h ⊡h comm-emloop-embase g
      ==
      (comm-emloop-embase g ⊡h comm-embase-emloop h) ⊡v∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h)
    comm-emloop-emloop g h =
      ap-comm _G∪H_ (emloop g) (emloop h) ∙v⊡
      comm-embase-emloop h ⊡h comm-emloop-embase g
        =⟨ ap (ap-comm _G∪H_ (emloop g) (emloop h) ∙v⊡_) $
           vert-degen-square-⊡h (comm-embase-emloop' h) (comm-emloop-embase' g) ⟩
      ap-comm _G∪H_ (emloop g) (emloop h) ∙v⊡
      vert-degen-square (ap2 _∙_ (comm-embase-emloop' h) (comm-emloop-embase' g))
        =⟨ vert-degen-square-∙v⊡ (ap-comm _G∪H_ (emloop g) (emloop h)) _ ⟩
      vert-degen-square
        (ap-comm _G∪H_ (emloop g) (emloop h) ∙
         ap2 _∙_ (comm-embase-emloop' h) (comm-emloop-embase' g))
        =⟨ ap vert-degen-square (=ₛ-out (comm-emloop-emloop' g h)) ⟩
      vert-degen-square
        (ap2 _∙_ (comm-emloop-embase' g) (comm-embase-emloop' h) ∙
         ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h))
        =⟨ ! $ vert-degen-square-⊡v∙ _ (ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h)) ⟩
      vert-degen-square (ap2 _∙_ (comm-emloop-embase' g) (comm-embase-emloop' h)) ⊡v∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h)
        =⟨ ap (_⊡v∙ ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h)) $ ! $
           vert-degen-square-⊡h (comm-emloop-embase' g) (comm-embase-emloop' h) ⟩
      (comm-emloop-embase g ⊡h comm-embase-emloop h) ⊡v∙
      ap-comm (λ x y → − (y H∪G x)) (emloop g) (emloop h) =∎

  module CP₁₁Comm =
    EM₁Level₂DoublePathElim G.grp H.grp {C = EMExplicit.EM G⊗H.abgroup 2} {{Trunc-level}}
      _G∪H_
      (λ x y → − (y H∪G x))
      idp
      comm-embase-emloop
      comm-emloop-embase
      comm-embase-emloop-comp
      comm-emloop-comp-embase
      comm-emloop-emloop

  abstract
    cp₁₁-comm : ∀ x y → x G∪H y == − (y H∪G x)
    cp₁₁-comm = CP₁₁Comm.f

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module EqBase where
import PolyDepPrelude
open PolyDepPrelude using
  ( Bool; true; false; _&&_
  ; Unit; unit
  ; Pair; pair
  ; Either; left; right
  ; Absurd
  ; Datoid; datoid; pElem
  ; True )

-- import And
And = Pair

-- import Sigma
data Sigma (A : Set)(B : A -> Set) : Set where
  si : (a : A) -> (b : B a) -> Sigma A B

Eq : Set -> Set -> Set
Eq a b = a -> b -> Bool

eqEmpty : Eq Absurd Absurd
eqEmpty () -- empty

eqUnit : Eq Unit Unit
eqUnit unit unit = true

eqPair : {A1 A2 B1 B2 : Set} ->
         (Eq     A1          A2) ->
         (Eq        B1          B2) ->
         Eq (And A1 B1) (And A2 B2)
eqPair ea eb (pair a b) (pair a' b') = ea a a' && eb b b'

caseOn : (D : Datoid)
         {B1 B2 : pElem D -> Set}
         (ifTrue : (b : pElem D) -> B1 b -> B2 b -> Bool)
         (a b : pElem D)
         (pa : B1 a)
         (pb : B2 b)
         (e : Bool)
         (cast : True e -> B1 a -> B1 b)
         -> Bool
caseOn D ifTrue a b pa pb (false) cast = false
caseOn D ifTrue a b pa pb (true)  cast = ifTrue b (cast unit pa) pb

eqEither : {A1 A2 B1 B2 : Set}
           (eq1 : A1 -> B1 -> Bool)
           (eq2 : A2 -> B2 -> Bool)
         -> Either A1 A2 -> Either B1 B2 -> Bool
eqEither eq1 eq2 (left  a1) (left  b1) = eq1 a1 b1
eqEither eq1 eq2 (right a2) (right b2) = eq2 a2 b2
eqEither eq1 eq2 _          _          = false

{-
            case x of {
              (inl x') ->
                case y of {
                  (inl x0) -> eq1 x' x0;
                  (inr y') -> false@_;};
              (inr y') ->
                case y of {
                  (inl x') -> false@_;
                  (inr y0) -> eq2 y' y0;};}
-}
{-

eqSigma2 (D : Datoid)
         (|B1 |B2 : pElem D -> Set)
         (ifTrue : (b : pElem D) -> Eq (B1 b) (B2 b))
         (x : Sigma pElem D B1)
         (y : Sigma pElem D B2)
  : Bool
  = case x of {
      (si a pa) ->
        case y of {
          (si b pb) ->
            caseOn D ifTrue a b pa pb (D.eq a b) (D.subst B1);};}

eqSigma (D : Datoid)(|B1 : (a : pElem D) -> Set)(|B2 : (a : pElem D) -> Set)
  : ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
     Eq (Sigma pElem D B1) (Sigma pElem D B2)
  = eqSigma2 D
-- More readable but less useful definition of eqSigma :

eqSigmaLocalLet (D : Datoid)
                (|B1 |B2 : pElem D -> Set)
                (ifTrue : (b : pElem D) -> Eq (B1 b) (B2 b))
                (x : Sigma pElem D B1)
                (y : Sigma pElem D B2)
  : Bool
  = case x of {
      (si a pa) ->
        case y of {
          (si b pb) ->
            let caseOn (e : Bool)(cast : True e -> B1 a -> B1 b) : Bool
                  = case e of {
                      (false) -> false@_;
                      (true) -> ifTrue b (cast tt@_ pa) pb;}
            in  caseOn (D.eq a b) (D.subst B1);};}

eqSum' (D : Datoid)
     (|B1 |B2 : (a : pElem D) -> Set)
  : ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
     Eq (Sum pElem D B1) (Sum pElem D B2)
  = \(e : (a : pElem D) -> Eq (B1 a) (B2 a)) ->
    \(p1 : Sum pElem D B1) ->
    \(p2 : Sum pElem D B2) ->
    caseOn D e p1.fst p2.fst p1.snd p2.snd (D.eq p1.fst p2.fst)
      (D.subst B1)

eqSum : (D : Datoid)
        {B1 B2 : (a : pElem D) -> Set}
  -> ((a : pElem D) -> Eq (B1 a) (B2 a)) ->
     Eq (Sum pElem D B1) (Sum pElem D B2)
eqSum e p1 p2 =
    caseOn D e p1.fst p2.fst p1.snd p2.snd (D.eq p1.fst p2.fst)
      (D.subst B1)
-}

max_stars_repo_name: asr/agda-kanso


text:
open import Data.Nat hiding (_^_)
open import Data.List as List hiding (null)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.List.Prefix
open import Data.Product hiding (map)
open import Data.Unit
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

-- This file contains the definition of monads used for computation in
-- the definitional interpreter for MJ using scopes and frames,
-- described in Section 5 of the paper.

module MJSF.Monad (k : ℕ) where

open import MJSF.Syntax k
open import MJSF.Values k
open import ScopesFrames.ScopesFrames k Ty

module MonadG (g : Graph) where

  open SyntaxG g
  open ValuesG g
  open UsesVal Valᵗ valᵗ-weaken renaming (getFrame to getFrame')
  open import Common.Weakening

  -- Computations may either time out, raise a null-pointer exception,
  -- or successfully terminate to produce a result:

  data Res (a : Set) : Set where
    timeout : Res a
    nullpointer : Res a
    ok : (x : a) → Res a

  -- The monad is similar to the monad used for STLCSF, except it uses
  -- `Res` instead of `Maybe`:

  M : (s : Scope) → (List Scope → Set) → List Scope → Set
  M s p Σ = Frame s Σ → Heap Σ → Res (∃ λ Σ' → (Heap Σ' × p Σ' × Σ ⊑ Σ'))

  -- We define some usual monad operations:

  return     :  ∀ {s Σ}{p : List Scope → Set} → p Σ → M s p Σ
  return v f h = ok (_ , h , v , ⊑-refl)

  fmap : ∀ {A B : List Scope → Set}{Γ Σ} → (∀ {Σ} → A Σ → B Σ) → M Γ A Σ → M Γ B Σ
  fmap g m f h
    with (m f h)
  ...  | timeout = timeout
  ...  | nullpointer = nullpointer
  ...  | ok (Σ' , h' , v' , ext') = ok (Σ' , h' , g v' , ext')

  join : ∀ {A : List Scope → Set}{Γ Σ} → M Γ (M Γ A) Σ → M Γ A Σ
  join m f h
    with (m f h)
  ...  | timeout = timeout
  ...  | nullpointer = nullpointer
  ...  | ok (Σ' , h' , m' , ext')
       with (m' (wk ext' f) h')
  ...     | timeout = timeout
  ...     | nullpointer = nullpointer
  ...     | ok (Σ'' , h'' , v'' , ext'') = ok ((Σ'' , h'' , v'' , ext' ⊚ ext''))

  _>>=_     :  ∀ {s Σ}{p q : List Scope → Set} →
               M s p Σ → (∀ {Σ'} → p Σ' → M s q Σ') → M s q Σ
  (a >>= b) = join (fmap b a)

  -- To program in dependent-passing style, we use the variant of
  -- monadic strength also used for STLCSF.

  _^_  :  ∀ {Σ Γ}{p q : List Scope → Set} ⦃ w : Weakenable q ⦄ →
          M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ
  (a ^ x) f h
    with (a f h)
  ...  | timeout = timeout
  ...  | nullpointer = nullpointer
  ...  | ok (Σ , h' , v , ext) = ok (Σ , h' , (v , wk ext x) , ext)

  -- The remaining definitions in this file are straightforward
  -- monadic liftings of the coercion function from `MJSF.Values` and
  -- of the frame operations.

  getFrame   :  ∀ {s Σ} → M s (Frame s) Σ
  getFrame f = return f f

  usingFrame  :  ∀ {s s' Σ}{p : List Scope → Set} → Frame s Σ → M s p Σ → M s' p Σ
  usingFrame f a _ = a f

  timeoutᴹ    :  ∀ {s Σ}{p : List Scope → Set} → M s p Σ
  timeoutᴹ _ _ = timeout

  raise : ∀ {s Σ}{p : List Scope → Set} → M s p Σ
  raise _ _ = nullpointer

  init : ∀ {Σ s' ds es} → (s : Scope) → ⦃ shape : g s ≡ (ds , es) ⦄ →
               Slots ds Σ → Links es Σ → M s' (Frame s) Σ
  init {Σ} s slots links _ h
    with (initFrame s slots links h)
  ...  | (f' , h') = ok (_ , h' , f' , ∷ʳ-⊒ s Σ)

  initι : ∀ {Σ s' ds es} → (s : Scope) → ⦃ shape : g s ≡ (ds , es) ⦄ →
               (Frame s (Σ ∷ʳ s) → Slots ds (Σ ∷ʳ s)) → Links es Σ → M s' (Frame s) Σ
  initι {Σ} s slots links _ h
    with (initFrameι s slots links h)
  ...  | (f' , h') = ok (_ , h' , f' , ∷ʳ-⊒ s Σ)

  getv : ∀ {s t Σ} → (s ↦ t) → M s (Valᵗ t) Σ
  getv p f h = return (getVal p f h) f h

  getf : ∀ {s s' Σ} → (s ⟶ s')  → M s (Frame s') Σ
  getf p f h = return (getFrame' p f h) f h

  getd : ∀ {s t Σ} → t ∈ declsOf s → M s (Valᵗ t) Σ
  getd d f h = return (getSlot d f h) f h

  getl : ∀ {s s' Σ} → s' ∈ edgesOf s → M s (Frame s') Σ
  getl e f h = return (getLink e f h) f h

  setd  :  ∀ {s t Σ} → t ∈ declsOf s → Valᵗ t Σ → M s (λ _ → ⊤) Σ
  setd d v f h with (setSlot d v f h)
  ...             | h' = return tt f h'

  setv  :  ∀ {s t Σ} → (s ↦ t) → Valᵗ t Σ → M s (λ _ → ⊤) Σ
  setv p v f h with (setVal p v f h)
  ...             | h' = return tt f h'