copumpkin

module Primes where

open import Level using (_⊔_)
open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility

copumpkin

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

data Empty

data Unit = Unit

data Equal a b where
  Refl :: Equal a a

type family F a :: *

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

{-# 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 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

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 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

{-# 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 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

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