copumpkin

module Collatz where

open import Coinduction
open import Data.Nat hiding (_+_; _*_)
open import Data.Fin hiding (_+_; fromℕ; toℕ)
open import Data.Bin hiding (suc)
open import Data.Maybe
open import Data.Product
open import Data.List as List
open import Data.Colist

copumpkin

{-# LANGUAGE RankNTypes, BangPatterns #-}
module Mutable where

import Control.Monad
import Control.Monad.ST
import Data.STRef
import Data.Vector.Mutable (MVector)
import qualified Data.Vector.Mutable as MV

-- A read-only view into an MVector or similar

copumpkin

module Lawvere where

open import Function.Equality hiding (cong)
open import Function.Surjection
open import Data.Product
open import Relation.Binary.PropositionalEquality

lawvere : {A B : Set} (f : A ↠ (A → B)) (g : B → B) → ∃ λ x → x ≡ g x
lawvere {A} {B} f g = h a , subst (λ r → h a ≡ g r) (cong (λ f → f a) (from-to refl)) refl
  where

copumpkin

module Polymorphic where

import Level
open Level using (Level; _⊔_)
open import Function
open import Data.Product hiding (map)
open import Data.List hiding (all)

data Index {A : Set} : List A → A → Set where
  zero : ∀ {τ Γ} → Index (τ ∷ Γ) τ

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

-- This is the type we're working with.
data List a = List (forall r. (a -> r -> r) -> r -> r)

-- Implement this signature. It should not be inefficient, so if you're planning
-- on writing something like tail (notoriously inefficient using foldr) on our
-- List type, think again! It should be possible to write with the same time
-- complexity as the original. And of course, converting to/from a conventional
-- list is cheating :)

zipWith :: (a -> b -> c) -> List a -> List b -> List c

copumpkin

module Weird where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Product
open import Data.Conat
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Unary as U

copumpkin

module Telescope where

open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec

infixr 6 _∷_

copumpkin

module Grothendieck where

open import Level using (_⊔_)
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Product
import Relation.Binary.EqReasoning as EqReasoning