copumpkin

module Routing where

open import Function hiding (type-signature)

open import Data.Bool hiding (_≟_)
open import Data.Maybe
open import Data.Char hiding (_≟_)
open import Data.String as String
open import Data.List as List hiding ([_])
open import Data.Product hiding (curry; uncurry)

copumpkin

module Nicomachus where

open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

open import Data.Nat
open import Data.Nat.Properties

-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem

copumpkin

module STLC where

-- Simple substitution à la Conor, as described in http://strictlypositive.org/ren-sub.pdf

id : {A : Set} → A → A
id x = x

data Type : Set where
  *   : Type
  _⇒_ : (S T : Type) → Type

copumpkin

{-# OPTIONS --type-in-type --without-K #-}
module Russell where

open import Data.Empty
open import Data.Product
open import Relation.Nullary hiding (yes; no)
open import Relation.Binary.PropositionalEquality

-- Based on Robert Dockins's Coq reorganization of Chad E Brown's proof of Russell's paradox

copumpkin

module Types where

open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Unit
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary

copumpkin

module Categories.Agda.State where

open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction

copumpkin

module Categories.Agda.List where

open import Level
open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)
open import Categories.Adjunction
open import Categories.Monad
open import Categories.Agda
open import Categories.Support.PropositionalEquality

copumpkin

{-# OPTIONS --without-K #-}
module Unique where

open import Level
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module Unique {a} {A : Set a} (_≟_ : (x y : A) → Dec (x ≡ y)) where
  squish : {x y : A} → x ≡ y → x ≡ y

copumpkin

module Scratch where

open import Level
open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

-- Legend has it that parametricity is just dinaturality
module Parametricity {a} {F G : Set a → Set a → Set a}
                         (mapF : ∀ {A B C D} → (A → B) → (C → D) → F B C → F A D)

copumpkin

{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}

data Empty

data Unit = Unit

data Equal a b where
  Refl :: Equal a a

type family F a :: *