louisswarren

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x

louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

louisswarren

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.String

_>>_ = primStringAppend
infixl 1 _>>_

postulate ω : ℕ

data Singular : ℕ → Set where
  singular : (n : ℕ) → Singular n

louisswarren

module Decidable where

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

⊥-elim : {A : Set} → ⊥ → A

louisswarren

module Weich where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

open import Decidable
open import List
  renaming (
    _∈_        to _[∈]_        ;
    _∉_        to _[∉]_        ;

louisswarren

open import Decidable
open import List

data Arrow (A : Set) : Set where
  Atom : A → Arrow A
  _⇒_  : A → Arrow A → Arrow A

data _⊢_ {A : Set} (αs : List (Arrow A)) : Arrow A → Set where
  triv : ∀{α}   → α ∈ αs → αs ⊢ α
  elim : ∀{α β} → αs ⊢ (α ⇒ β) → αs ⊢ (Atom α) → αs ⊢ β

louisswarren

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Equality

-- See http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

open import Search

module Declist (A : Set)(_=dec=_ : BiDecidable _≡_) where

louisswarren

The (θ\η)

Pronounced like theta, without the eta bit.

louisswarren

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.String

data Inspect {A : Set}(x : A) : Set where
  _with≡_ : (y : A) → x ≡ y → Inspect x

inspect : {A : Set} → (x : A) → Inspect x
inspect x = x with≡ refl

louisswarren

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)


_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
infixr 4 _++_