John Chandler Burnham johnchandlerburnham

💭

Λ∀

johnchandlerburnham / Univalence.fm

Last active October 9, 2019 08:44

Univalence in Formality

	// based on https://arxiv.org/pdf/1803.02294.pdf

	import Relation.Equality

	K : { X : Type} -> Type
	{x : X, y : X, p : Path(X,x,y), q : Path(X,x,y)} -> Path(Path(X,x,y),p,q)

	J :
	{ X : Type
	, x : X

johnchandlerburnham / AnnotationProto.hs

Created February 5, 2019 13:59

Some thoughts on how to do type annotations in Michelson

	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE ExistentialQuantification #-}
	{-# LANGUAGE ExplicitNamespaces #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeApplications #-}

johnchandlerburnham / solarized-dark.css

Created August 20, 2017 01:31 — forked from nicolashery/solarized-dark.css

Solarized theme stylesheets for Jekyll and Pygments

	/* Solarized Dark

	For use with Jekyll and Pygments

	http://ethanschoonover.com/solarized

	SOLARIZED HEX ROLE
	--------- -------- ------------------------------------------
	base03 #002b36 background
	base01 #586e75 comments / secondary content