From 4f392d19b730e07251eed7e1e67bf5a051bc2ed0 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 20 Jun 2024 09:06:44 +0200
Subject: [PATCH] Add properties of basic definitions

---
 src/Thinning/Properties.agda | 50 ++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 src/Thinning/Properties.agda

diff --git a/src/Thinning/Properties.agda b/src/Thinning/Properties.agda
new file mode 100644
index 0000000..a77a20a
--- /dev/null
+++ b/src/Thinning/Properties.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Thinning.Properties where
+
+open import Data.List.Base using (List)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+
+open import Thinning
+
+private
+  variable
+    a : Level
+    A : Set a
+    ws xs ys zs : List A
+
+-- In agda-categories, the convention is to have the arguments to many of these
+-- properties implicit. In the standard library, however, the convention is to
+-- make the arguments explicit. I think implicit is better when working with an
+-- abstract instance of the structure, but here we're pretty much always going
+-- to be working with Thinnings concretely, so I'm going to make the arguments
+-- explicit.
+
+-- Composition has a left identity
+identityˡ : ∀ (θ : Thinning A xs ys) → id ∘ θ ≡ θ
+identityˡ end = refl
+identityˡ (include θ) = cong include (identityˡ θ)
+identityˡ (exclude θ) = cong exclude (identityˡ θ)
+
+-- Composition has a right identity
+identityʳ : ∀ (θ : Thinning A xs ys) → θ ∘ id ≡ θ
+identityʳ end = refl
+identityʳ (include θ) = cong include (identityʳ θ)
+identityʳ (exclude θ) = cong exclude (identityʳ θ)
+
+-- Composition is associative
+assoc : (θ : Thinning A ws xs) (φ : Thinning A xs ys) (ψ : Thinning A ys zs)
+      → (ψ ∘ φ) ∘ θ ≡ ψ ∘ (φ ∘ θ)
+assoc end         end         end         = refl
+assoc end         end         (exclude ψ) = cong exclude (assoc end end ψ)
+assoc end         (exclude φ) (include ψ) = cong exclude (assoc end φ ψ)
+assoc end         (exclude φ) (exclude ψ) = cong exclude (assoc end (exclude φ) ψ)
+assoc (include θ) (include φ) (include ψ) = cong include (assoc θ φ ψ)
+assoc (include θ) (include φ) (exclude ψ) = cong exclude (assoc (include θ) (include φ) ψ)
+assoc (include θ) (exclude φ) (include ψ) = cong exclude (assoc (include θ) φ ψ)
+assoc (include θ) (exclude φ) (exclude ψ) = cong exclude (assoc (include θ) (exclude φ) ψ)
+assoc (exclude θ) (include φ) (include ψ) = cong exclude (assoc θ φ ψ)
+assoc (exclude θ) (include φ) (exclude ψ) = cong exclude (assoc (exclude θ) (include φ) ψ)
+assoc (exclude θ) (exclude φ) (include ψ) = cong exclude (assoc (exclude θ) φ ψ)
+assoc (exclude θ) (exclude φ) (exclude ψ) = cong exclude (assoc (exclude θ) (exclude φ) ψ)