Skip to content

Instantly share code, notes, and snippets.

View atennapel's full-sized avatar

Albert ten Napel atennapel

39 followers · 31 following
  • Netherlands
View GitHub Profile
@atennapel
atennapel / SPropSketch.hs
Last active June 15, 2022 08:10
SProp sketch
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE OverloadedStrings #-}
import Data.String (IsString(..))
type Ix = Int
type Lvl = Int
type ULvl = Int
data Sort = Type ULvl | Prop
@atennapel
atennapel / infinitary-mutual-single-index.agda
Created January 5, 2022 15:36
Infinitary mutual inductive families signatures with a single index
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Data.Product
data IxCtx : Set where
Nil : IxCtx
Cons : Set -> IxCtx -> IxCtx
@atennapel
atennapel / infinitary-indexed-single-index.agda
Last active January 5, 2022 14:34
Infinitary indexed datatype signatures with a single index
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Data.Product
data Ind (I : Set) : Set where
U : I -> Ind I
Pi : (A : Set) -> (A -> Ind I) -> Ind I
@atennapel
atennapel / infinitary-indexed-uncurried.agda
Created January 4, 2022 15:39
Infinitary indexed datatypes signatures with uncurried index
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ix : Set where
U : Ix
Pi : (A : Set) -> (A -> Ix) -> Ix
@atennapel
atennapel / non-inductive.agda
Created January 4, 2022 14:26
Non-inductive datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
@atennapel
atennapel / finite.agda
Created January 4, 2022 14:25
Finite datatypes signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
record Ty : Set where
instance constructor U
data Ctx : Set where
@atennapel
atennapel / infinitary.agda
Created January 4, 2022 14:23
Infinitary non-indexed datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ind : Set where
U : Ind
Pi : (A : Set) -> (A -> Ind) -> Ind
@atennapel
atennapel / finitary.agda
Last active January 4, 2022 17:50
Finitary non-indexed datatype signatures
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Data.Product
data Ty : Set where
U : Ty
Pi : (A : Set) -> (A -> Ty) -> Ty
PiInd : Ty -> Ty
@atennapel
atennapel / UnivPoly.hs
Last active July 7, 2021 04:51
Universe Polymorphism
-- universe polymorphism
module UnivPoly where
-- core language
type Ix = Int
data Term
= Var Ix
| Abs Term
| App Term Term
@atennapel
atennapel / Self.hs
Created May 30, 2021 14:45
Self types
module Self where
-- core language
type Ix = Int
data Core
= Var Ix
| Abs Core
| App Core Core
| Pi Core Core