From a0a743ac717008c242221746418b39b6dc9f0997 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 20 Jun 2024 09:31:14 +0200 Subject: [PATCH] Show that it's unique --- src/Thinning/Properties.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Thinning/Properties.agda b/src/Thinning/Properties.agda index a77a20a..6559fc8 100644 --- a/src/Thinning/Properties.agda +++ b/src/Thinning/Properties.agda @@ -2,7 +2,7 @@ module Thinning.Properties where -open import Data.List.Base using (List) +open import Data.List.Base using (List; []) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) @@ -48,3 +48,8 @@ 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 φ) ψ) + +-- ¡ is the only Thinning from [] +¡-unique : (θ : Thinning A [] xs) → ¡ ≡ θ +¡-unique end = refl +¡-unique (exclude θ) = cong exclude (¡-unique θ)