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

module Simplex where

data Id (A : Set) (x : A) : A → Set where
  refl : Id A x x

J : ∀{A : Set} {x : A} (P : ∀ y → Id A x y → Set)
  → ∀{y} → (id : Id A x y) → P x refl → P y id
J P refl Pxr = Pxr

_∘_ : ∀{A : Set} → {x y z : A} → (g : Id A y z) → (f : Id A x y) → Id A x z
g ∘ f = J (λ v _ → Id _ _ v) g f

∘-idʳ : ∀{A : Set} → {x y : A} → (g : Id A x y) → Id _ (g ∘ refl) g
∘-idʳ g = J (λ z h → Id _ (h ∘ refl) h) g refl

record Σ (A : Set) (T : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : T proj₁

infixr  _,_
open Σ

syntax Σ A (\x → P) = Σ[ x ∈ A ] P

module Plex (A : Set) where
  S₀ : Set
  S₀ = A

  S₁ : Set
  S₁ = Σ[ x ∈ A ] Σ[ y ∈ A ] (Id A x y)

  S₂ : Set
  S₂ = Σ[ x ∈ A ] Σ[ y ∈ A ] Σ[ z ∈ A ]
       Σ[ f ∈ Id A x y ] Σ[ g ∈ Id A y z ] Σ[ h ∈ Id A x z ]
         (Id (Id A x z) (g ∘ f) h)

  s₀₀ : S₀ → S₁
  s₀₀ x = (x , x , refl)

  s₁₀ : S₁ → S₂
  s₁₀ (x , y , f) = (x , x , y , refl , f , f , ∘-idʳ f)

  s₁₁ : S₁ → S₂
  s₁₁ (x , y , f) = (x , y , y , f , refl , f , refl)

  lemma₀ : ∀ x → Id _ (s₁₁ (s₀₀ x)) (s₁₀ (s₀₀ x))
  lemma₀ x = refl

  d₁₀ : S₂ → S₁
  d₁₀ (x , y , z , xy , yz , xz , coh) = (y , z , yz)

  d₁₁ : S₂ → S₁
  d₁₁ (x , y , z , xy , yz , xz , coh) = (x , z , xz)

  lemma₁ : ∀ x y → (f : Id A x y) → Id _ (d₁₀ (s₁₀ (x , y , f))) (x , y , f)
  lemma₁ x y f = refl

  lemma₂ : ∀ x y → (f : Id A x y) → Id _ (d₁₁ (s₁₀ (x , y , f))) (x , y , f)
  lemma₂ x y f = refl

  lemma₃ : Id (S₁ → S₁) (λ s → d₁₀ (s₁₀ s)) (λ s → s)
  lemma₃ = refl

  lemma₄ : Id (S₁ → S₁) (λ s → d₁₁ (s₁₀ s)) (λ s → s)
  lemma₄ = refl