brendanzab

fn main() {
    swizzle_gen();
}

fn swizzle_gen() {
    swizzle_gen0("x");
    swizzle_gen0("y");
    swizzle_gen0("z");
    swizzle_gen0("w");
}

brendanzab

I think I’ve figured out most parts of the cubical type theory paper(s); I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory? A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then? A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

Q: So what are HIT and UA? A: A HIT is a type equipped with custom equality, as an example, you can write a type similar to the natural numbers but with an equality between all even numbers. Well, it cannot be called natural numbers then.

brendanzab

data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Uni
  deriving (Show, Eq)
data Clos = Clos Tm Env
  deriving (Show, Eq)
data Dm = DVar Int | DAbs Clos | DApp Dm Dm | DPi Dm Clos | DUni
  deriving (Show, Eq)
type Env = [Dm]

appd :: Clos -> Dm -> Dm
appd (Clos b e) t = eval (t : e) b