{-# 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 30 _,_
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