Initial commit with readme and basic definitions

README.md

@@ -0,0 +1,5 @@
+# Thinnings
+
+Inspired by Conor McBride's paper Everybody's Got To Be Somewhere.
+
+This is exploration and not currently intended to be used as a library.

src/Thinning.agda

@@ -0,0 +1,47 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Thinning where
+
+open import Data.List.Base using (List; []; _∷_)
+open import Level using (Level)
+open import Relation.Binary.Core using (Rel)
+
+private
+  variable
+    a : Level
+    A : Set a
+    xs ys zs : List A
+
+-- The type of a Thinning
+------------------------------------------------------------------------
+
+-- A thinning is a way of saying how we can find every element of a list in
+-- another list, in the right order.
+data Thinning (A : Set a) : Rel (List A) a where
+  -- We can certainly find every element of the empty list in the empty list.
+  -- This is generally the base case for recursion on thinnings.
+  end : Thinning A [] []
+  -- It's possible we'll find the first element of the smaller list at the head
+  -- of the larger list.
+  include : {x : A} → Thinning A xs ys → Thinning A (x ∷ xs) (x ∷ ys)
+  -- It's also possible that we won't, and have to look deeper in the larger
+  -- list.
+  exclude : {x : A} → Thinning A xs ys → Thinning A xs (x ∷ ys)
+
+-- Operations on Thinnings
+------------------------------------------------------------------------
+
+-- I'm choosing the names here to emphasize that there is a category of
+-- Thinnings.
+
+-- There is always a Thinning from the list to itself. We include at every step.
+id : Thinning A xs xs
+id {xs = []} = end
+id {xs = x ∷ xs} = include id
+
+-- We can compose two Thinnings!
+_∘_ : Thinning A ys zs → Thinning A xs ys → Thinning A xs zs
+end ∘ end = end
+include α ∘ include β = include (α ∘ β)
+include α ∘ exclude β = exclude (α ∘ β)
+exclude α ∘ β = exclude (α ∘ β)

thinnings.agda-lib

@@ -0,0 +1,3 @@
+name: thinnings
+include: src
+depend: standard-library-2.0 agda-categories