-- An approach to defining semi-simplicial types.
-- This files comes together with a Haskell file (generateSemiSimp.hs) which can be used to generate the definitions of semi-simplicial types.
-- However, there are at least 2 caveats:

-- 1. The Agda definitions that are generated are not literally the "intuitive" ones, but they are equivalent to those that one would probably expect.
-- 2. My approach of generating these definitions is very ad-hoc and ugly (there would be much better ways to do it, see generateSemiSimp.hs). This also results in unreadability of the generated Agda code. This is therefore mainly a "proof of concept" (I wanted to convince myself that the definition I had in mind really type checks for all cases with "fixed n", even though it does not type check for general n).

module Semisimplicial where

Type = Set 

data Empty : Type where

data ⊤ : Type where
  * : ⊤

data ℕ : Type where
  O : ℕ
  S : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO O #-}
{-# BUILTIN SUC S #-}


data Fin : ℕ → Type where
  fz : {n : ℕ} → Fin (S n)
  fs : {n : ℕ} → Fin n → Fin (S n)

_>fin_ : {n : ℕ} → (i j : Fin n) → Set
fz >fin i = Empty
fs j >fin fz = ⊤
fs j >fin fs i = j >fin i

is-increasing : {m n : ℕ} → (Fin m → Fin n) → Type
is-increasing {m} {n} f = {j i : Fin m} → (j >fin i) → ((f j) >fin (f i))


infixr 1 _,_

record Σ (A : Type) (B : A → Type) : Type where
  constructor _,_
  field
    fst : A
    snd : B fst


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

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


{- 
Assume we have already defined the types X₀ , X₁ , ... , Xₙ₋₁. 
These are the types of "standard" semi-simplicial complexes for the first n levels.
It will follow from the inductive definition what their types are; intuitively, they should be like this:

X₀ : Type
X₁ : X₀ → X₀ → Type
X₂ : (a b c : X₀) → (X₁ a b) → (X₁ b c) → (X₁ a c) → Type
...
Xₙ₋₁ : ...

but in fact, the types will only be equivalent (but not strictly equal) to those expressions.

What we would like to say is this:

Let P_n (the n-boundary) be the type of tuples

 (x₁ , x₂ , ... , xₙ₋₁),

 where x_k is of type

    (fk : (S k) ⇒+ (S n)) 
  → X_k ( [ λ (gj : (S j) ⇒+ (S k)) . x_j(fk ∘+ gj)]_{j : Fin k} )

(we write [a_j]_{j : Fin k} for the tupel (a_1 , a_2 , ... , a_{k-1})).

We define Xₙ to be

Xₙ : P_n → Type.

Unfortunately, Agda can not see that this type-checks.

The Haskell file generateSemiSimpl.hs generates the definitions of X₀ , X₁ , ... , Xₙ. They may be copied below to type check them. Here is the output for n ≡ 7:
[note that we want to give the type of "standard" semi-simplicial types, not an actual semi-simplicial type; that is why the definitions of X₀ , X₁ , ... are missing.]
-}


P0 = ⊤

X0 : P0 → Type
X0 = {!!}


P1 = Σ ((f0 : (S 0) ⇒+ (S 1)) → X0 (*))  λ x0 → ⊤ 

X1 : P1 → Type
X1 = {!!}


P2 = Σ ((f0 : (S 0) ⇒+ (S 2)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 2)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → ⊤  

X2 : P2 → Type
X2 = {!!}


P3 = Σ ((f0 : (S 0) ⇒+ (S 3)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 3)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → Σ ((f2 : (S 2) ⇒+ (S 3)) → X2 ((λ (g0 : (S 0) ⇒+ (S 2)) → x0(f2 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 2)) → x1(f2 ∘+ g1)) , *))  λ x2 → ⊤   

X3 : P3 → Type
X3 = {!!}


P4 = Σ ((f0 : (S 0) ⇒+ (S 4)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 4)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → Σ ((f2 : (S 2) ⇒+ (S 4)) → X2 ((λ (g0 : (S 0) ⇒+ (S 2)) → x0(f2 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 2)) → x1(f2 ∘+ g1)) , *))  λ x2 → Σ ((f3 : (S 3) ⇒+ (S 4)) → X3 ((λ (g0 : (S 0) ⇒+ (S 3)) → x0(f3 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 3)) → x1(f3 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 3)) → x2(f3 ∘+ g2)) , *))  λ x3 → ⊤    

X4 : P4 → Type
X4 = {!!}


P5 = Σ ((f0 : (S 0) ⇒+ (S 5)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 5)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → Σ ((f2 : (S 2) ⇒+ (S 5)) → X2 ((λ (g0 : (S 0) ⇒+ (S 2)) → x0(f2 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 2)) → x1(f2 ∘+ g1)) , *))  λ x2 → Σ ((f3 : (S 3) ⇒+ (S 5)) → X3 ((λ (g0 : (S 0) ⇒+ (S 3)) → x0(f3 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 3)) → x1(f3 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 3)) → x2(f3 ∘+ g2)) , *))  λ x3 → Σ ((f4 : (S 4) ⇒+ (S 5)) → X4 ((λ (g0 : (S 0) ⇒+ (S 4)) → x0(f4 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 4)) → x1(f4 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 4)) → x2(f4 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 4)) → x3(f4 ∘+ g3)) , *))  λ x4 → ⊤     

X5 : P5 → Type
X5 = {!!}


P6 = Σ ((f0 : (S 0) ⇒+ (S 6)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 6)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → Σ ((f2 : (S 2) ⇒+ (S 6)) → X2 ((λ (g0 : (S 0) ⇒+ (S 2)) → x0(f2 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 2)) → x1(f2 ∘+ g1)) , *))  λ x2 → Σ ((f3 : (S 3) ⇒+ (S 6)) → X3 ((λ (g0 : (S 0) ⇒+ (S 3)) → x0(f3 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 3)) → x1(f3 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 3)) → x2(f3 ∘+ g2)) , *))  λ x3 → Σ ((f4 : (S 4) ⇒+ (S 6)) → X4 ((λ (g0 : (S 0) ⇒+ (S 4)) → x0(f4 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 4)) → x1(f4 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 4)) → x2(f4 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 4)) → x3(f4 ∘+ g3)) , *))  λ x4 → Σ ((f5 : (S 5) ⇒+ (S 6)) → X5 ((λ (g0 : (S 0) ⇒+ (S 5)) → x0(f5 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 5)) → x1(f5 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 5)) → x2(f5 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 5)) → x3(f5 ∘+ g3)) , (λ (g4 : (S 4) ⇒+ (S 5)) → x4(f5 ∘+ g4)) , *))  λ x5 → ⊤      

X6 : P6 → Type
X6 = {!!}


P7 = Σ ((f0 : (S 0) ⇒+ (S 7)) → X0 (*))  λ x0 → Σ ((f1 : (S 1) ⇒+ (S 7)) → X1 ((λ (g0 : (S 0) ⇒+ (S 1)) → x0(f1 ∘+ g0)) , *))  λ x1 → Σ ((f2 : (S 2) ⇒+ (S 7)) → X2 ((λ (g0 : (S 0) ⇒+ (S 2)) → x0(f2 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 2)) → x1(f2 ∘+ g1)) , *))  λ x2 → Σ ((f3 : (S 3) ⇒+ (S 7)) → X3 ((λ (g0 : (S 0) ⇒+ (S 3)) → x0(f3 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 3)) → x1(f3 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 3)) → x2(f3 ∘+ g2)) , *))  λ x3 → Σ ((f4 : (S 4) ⇒+ (S 7)) → X4 ((λ (g0 : (S 0) ⇒+ (S 4)) → x0(f4 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 4)) → x1(f4 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 4)) → x2(f4 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 4)) → x3(f4 ∘+ g3)) , *))  λ x4 → Σ ((f5 : (S 5) ⇒+ (S 7)) → X5 ((λ (g0 : (S 0) ⇒+ (S 5)) → x0(f5 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 5)) → x1(f5 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 5)) → x2(f5 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 5)) → x3(f5 ∘+ g3)) , (λ (g4 : (S 4) ⇒+ (S 5)) → x4(f5 ∘+ g4)) , *))  λ x5 → Σ ((f6 : (S 6) ⇒+ (S 7)) → X6 ((λ (g0 : (S 0) ⇒+ (S 6)) → x0(f6 ∘+ g0)) , (λ (g1 : (S 1) ⇒+ (S 6)) → x1(f6 ∘+ g1)) , (λ (g2 : (S 2) ⇒+ (S 6)) → x2(f6 ∘+ g2)) , (λ (g3 : (S 3) ⇒+ (S 6)) → x3(f6 ∘+ g3)) , (λ (g4 : (S 4) ⇒+ (S 6)) → x4(f6 ∘+ g4)) , (λ (g5 : (S 5) ⇒+ (S 6)) → x5(f6 ∘+ g5)) , *))  λ x6 → ⊤       

X7 : P7 → Type
X7 = {!!}