AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; 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.

	data Nat : Set where
	zero : Nat
	succ : Nat -> Nat

	{-# BUILTIN NATURAL Nat #-}

	infix 30 _+_
	_+_ : Nat -> Nat -> Nat
	0 + n = n
	succ m + n = succ (m + n)

	trait Foo {}

	trait Bar {}

	trait Demo<T> {
	fn t(_: T) -> T;
	}

	struct Test;

	use std::fmt::Display;

	trait A<T> where T : Display {}

	fn main() {
	println!("Hello, world!");
	}

	open import Data.String
	open import Data.List
	open import Data.List.Any

	data Term : Set where
	var : String ->　Term
	lam : String -> Term -> Term
	app : Term -> Term -> Term

	sub : Term -> List Term

	use std::collections::HashSet;

	#[derive(Clone, Debug, PartialEq, Eq, Hash)]
	pub struct Var(String);

	#[derive(Clone, Debug, PartialEq, Eq)]
	pub enum Term {
	Var(Var),
	Lam(Var, Box<Term>),
	App(Box<Term>, Box<Term>),

	open import Agda.Primitive using (Setω)

	test : Setω₂
	test = Setω₁

	This Gist confirms the Linked Identity in my OpenPGP key, and links it to this GitHub account.

	Token for proof:
	[Verifying my OpenPGP key: openpgp4fpr:dfac72e8959f47925e93abd8655fbccf6553cbff]