{-# OPTIONS --type-in-type --without-K --rewriting #-}

open import Data.Nat
open import Data.Unit
open import Data.Product
open import Data.Fin
open import Relation.Binary.PropositionalEquality
{-# BUILTIN REWRITE _≡_ #-}

record _⇒+_ (m n : ℕ) : Set where
--m ⇒+ n = Σ (Fin (S m) → Fin (S n)) is-increasing

-- composition:

_∘+_ : {l m n : ℕ} → (m ⇒+ n) → (l ⇒+ m) → (l ⇒+ n)
f ∘+ g = {!!}
--(g , p₂) ∘+ (f , p₁) = (λ i → g(f(i))) , (λ p → p₂ (p₁ p))

SST : ℕ → Set

-- skeleton of a k-simplex: cells lower (!) than level j
Sk : {j : ℕ} → (SST j) → (k : ℕ) → Set

Skm : {j : ℕ}(X : SST j)
  → {k₁ k₂ : ℕ} → (k₁ ⇒+ k₂) → Sk X k₂ → Sk X k₁


Skm-∘ : {j : ℕ}(X : SST j)
        → {k₁ k₂ k₃ : ℕ}(f : k₁ ⇒+ k₂)(g : k₂ ⇒+ k₃)
        → (x : Sk X k₃) → Skm X f (Skm X g x)≡ Skm X (g ∘+ f) x
--        → (x : Sk X k₃) → Skm X (g ∘+ f) x ≡ Skm X f (Skm X g x)
-- doesn't work
{-# REWRITE Skm-∘ #-}   

SST 0 = ⊤
SST (suc j) = Σ (SST j) λ X → Sk X j → Set

Sk {0} ⋆ k = ⊤
Sk {suc j} (X , Fibʲ) k =
  Σ (Sk X k) λ sk → (f : j ⇒+ k) → Fibʲ (Skm X f sk)

Skm {0} ⋆ f sk = ⋆
Skm {suc j} (X , Fibʲ) f (x , fibs) =
  Skm {j} X f x , λ g → fibs (f ∘+ g) 

Skm-∘ = ?