-- This file can be used to generate the Agda definitions of (truncated) semi-simplicial types. For explanations, see the accompanying Agda file.
-- For general explanations of the problem, see
-- http://uf-ias-2012.wikispaces.com/Semi-simplicial+types
-- Caveat: This is a rather ugly ad-hoc implementation. A better way to do this would be to use Haskell's packages for Agda's Syntax and generate the abstract syntax tree before printing it nicely.
-- The main function is the following.
-- generateAll n will, for some number n, generate the types of semi-simplicial "standard" simplices Xi (together with their boundaries, here called 'Pi').
-- Putting the output into the Agda file Semisimplicial.agda allows to check whether everything type checks (it works with Agda 2.3.3 and probably most other versions, as I do not use any special features at all and not even any kind of library)
generateAll n = generateAllAux n 0
-- The actual construction (for explanations, see the Agda file).
-- First: generate the list [ λ (gj : (S j) ⇒+ (S k)) . x_j(fk ∘+ gj)]_{j : Fin k} with a "*" (unique element of the unit type) in the end.
genArgsAux k j =
if k == j
then "*"
else "(λ (g" ++ (show j) ++ " : (S " ++ (show j) ++ ") ⇒+ (S " ++ (show k) ++ ")) " ++
"→ x" ++ (show j) ++ "(f" ++ (show k) ++ " ∘+ g" ++ (show j) ++ ")) , " ++ (genArgsAux k (j + 1))
genArgs k = genArgsAux k 0
genSkelAux n k =
if k == n
then "⊤"
else "Σ ((f" ++ (show k) ++ " : (S " ++ (show k) ++ ") ⇒+ (S " ++ (show n) ++ ")) " ++
"→ X" ++ (show k) ++ " (" ++ genArgs k ++ "))" ++
" λ x" ++ (show k) ++ " → " ++ (genSkelAux n (k+1)) ++ " "
genSkel n = genSkelAux n 0
genP n = ("P" ++ (show n) ++ " = " ++ genSkel n)
genXty n = "X" ++ (show n) ++ " : P" ++ (show n) ++ " → Type"
genXtm n = "X" ++ (show n) ++ " = ?"
generateAllAux n k =
if k > n
then putStrLn ""
else
do
putStrLn (genP k ++ "\n\n" ++ genXty k ++ "\n" ++ genXtm k ++ "\n\n")
generateAllAux n (k+1)