Pinned

1. Type-Theory

   Lecture note on Lambda Calculus and Types for FLOLAC

   TeX 24 3

2. An implementation of McBride's struc...

   1

   {-# LANGUAGE FlexibleContexts, FlexibleInstances #-}

   2

   {-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 

   3

   {-# LANGUAGE GADTs, StandaloneDeriving #-}

   4

   {-# LANGUAGE Safe #-}

   5

3. FiniteSets

   Fintie Sets in Cubical Agda

   Agda 11

4. MtacAR

   Mtac in Agda

   Agda 27