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.

tioover

{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# LANGUAGE TypeOperators, DeriveFunctor, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, OverlappingInstances #-}
module ALaCarte where
-- Definitions
newtype Expr f = In (f (Expr f))

-- We define a separate data type for each constructor we want to use
-- then we can combine them together using the (:+:) operator to make
-- our data types à la carte.

androidfred

Haskell, Stack and Intellij IDEA IDE setup tutorial how to get started

Upon completion you will have a sane, productive Haskell environment adhering to best practices.

Basics

• Haskell is a programming language.
• Stack is tool for Haskell projects. (similar tools for other languages include Maven, Gradle, npm, RubyGems etc)
• Intellij IDEA IDE is a popular IDE.

Install required libraries

sudo apt-get install libtinfo-dev libghc-zlib-dev libghc-zlib-bindings-dev

pchiusano

-- A port of: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html

{-# LANGUAGE DeriveFunctor #-}

module ABT where

import qualified Data.Foldable as Foldable
import Data.Foldable (Foldable)
import Data.Set (Set)
import qualified Data.Set as Set

neel-krishnaswami

(* -*- mode: ocaml; -*- *)

module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

type var = string

aztek

open import Level
open import Data.List
open import Data.Sum
open import Relation.Binary

module InsertionSort {ℓ ℓ₁ ℓ₂} (totalOrder : TotalOrder ℓ ℓ₁ ℓ₂) where

open TotalOrder totalOrder renaming (Carrier to A)
open IsTotalOrder isTotalOrder renaming (trans to ≤-trans; total to _≤?_)

hanbzu

val a = Stream(1)
//a: scala.collection.immutable.Stream[Int] = Stream(1, ?)

def b: Stream[Int] = Stream(b.head)
//b: Stream[Int]

a #::: b
//res0: scala.collection.immutable.Stream[Int] = Stream(1, ?)

a append b

favonia

{-# OPTIONS --type-in-type #-}

-- Burali-Forti's paradox in MLTT-ish without W-types

-- I was following Coquand's paper "An Analysis of Girard's Paradox"
-- and Hurkens's paper "A Simplification of Girard's Paradox".
-- Code is released under CC0.

-- Σ-types
record Σ (A : Set) (B : A → Set) : Set where