copumpkin

module Topology where

import Level
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary

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 ExistentialQuantification, TypeOperators #-}
module Fold where
 
import Control.Applicative
import Control.Functor.Contra
 
import Data.Array.Vector
import qualified Data.Foldable as Foldable
 
data Fold b c = forall a. Fold (a -> b -> a) a (a -> c)

copumpkin

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}

-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.

copumpkin

module Unify where

-- Translated from http://strictlypositive.org/unify.ps.gz

open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)

copumpkin

-- See also https://gist.github.com/copumpkin/2636229
module Relations where

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

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

open import Coinduction
open import Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary hiding (Rel)
import Relation.Binary.PropositionalEquality as PropEq
open import Category.Monad

copumpkin

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All

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