AndyShiue

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>),

AndyShiue

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

AndyShiue

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]

AndyShiue

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]

AndyShiue

open import Agda.Primitive using (Setω)

test : Setω₂
test = Setω₁

AndyShiue

use std::fmt::Display;

trait A<T> where T : Display {}

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

AndyShiue

trait Foo {}

trait Bar {}

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

struct Test;

AndyShiue

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)

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.