Skip to content

Instantly share code, notes, and snippets.

AndyShiue

Block or report user

Report or block AndyShiue

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@AndyShiue
AndyShiue / CuTT.md
Last active Jun 17, 2019
Cubical type theory for dummies
View CuTT.md

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.

@AndyShiue
AndyShiue / openpgp.txt
Created Dec 1, 2017
OpenKeychain Linked Identity
View openpgp.txt
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
AndyShiue / openpgp.txt
Created Dec 1, 2017
OpenKeychain Linked Identity
View openpgp.txt
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]
View lambda.agda
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
AndyShiue / lib.rs
Created Jan 7, 2016
implementation of the untyped lambda calculus in Rust and simple tests for it.
View lib.rs
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>),
You can’t perform that action at this time.