{-# 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

infixr 9 _∘_

∘-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

_◐_ : ∀{A : Set}  {x y z : A}  {f g : Id A x y}  (α : Id (Id A x y) f g) 
          (h : Id A y z)  Id (Id A x z) (h  f) (h  g)
_◐_ {_}{_}{_}{_}{f} α h = J  i _  Id (Id _ _ _) (h  f) (h  i)) α refl

_◑_ : ∀{A : Set}  {x y z : A}  {f g : Id A y z}  (h : Id A x y) 
          (α : Id (Id A y z) f g)  Id (Id A x z) (f  h) (g  h)
_◑_ {_}{_}{_}{_}{f} h α = J  i _  Id (Id _ _ _) (f  h) (i  h)) α 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

_×_ : Set  Set  Set
A × B = Σ _  (x : A)  B)

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₃ : Set
  S₃ = Σ[ x  A ] Σ[ y  A ] Σ[ z  A ] Σ[ w  A ]
       Σ[ f  Id A x y ] Σ[ g  Id A y z ] Σ[ h  Id A z w ]
       Σ[ α  Id A y w ] Σ[ β  Id A x z ] Σ[ Θ  Id A x w ]
       Σ[ H  Id (Id A x z) (g  f) β ]
       Σ[ G  Id (Id A y w) (h  g) α ]
       Σ[ I  Id (Id A x w) (h  g  f) Θ ]
       Σ[ J  Id (Id A x w) (h  β) Θ ]
       Σ[ K  Id (Id A x w) (α  f) Θ ]
         (Id (Id (Id A x w) (h  g  f) Θ) (J  (H  h)) I)
--         × (Id (Id (Id A x w) (h ∘ g ∘ f) Θ) (K ∘ (f ◑ G)) I)

  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)

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

  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₃ :  x y  (f : Id A x y)  Id _ (d₁₂ (s₁₁ (x , y , f))) (x , y , f)
  lemma₃ x y f = refl