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

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