From 07c4a784b46f6cfe47d1c37329051b4b5d459755 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 6 Jul 2022 01:11:03 +0100
Subject: Simplify alpha equivalence.

---
 src/Data/Type.agda | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/Data/Type.agda b/src/Data/Type.agda
index e0637ba..9773db0 100644
--- a/src/Data/Type.agda
+++ b/src/Data/Type.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.List using (List; _++_; map; filter; foldl)
-open import Data.Nat using (ℕ; _≟_)
+open import Data.List using (List)
+open import Data.Nat using (ℕ)
 
 module Data.Type
   (mkFresh : List ℕ → ℕ)
@@ -9,10 +9,10 @@ module Data.Type
 
 open import Data.BinOp using (BinOp)
 open import Data.Bool using (if_then_else_)
-open import Data.Nat.Properties using (≤-totalOrder)
+open Data.List using (_++_; map; filter; foldl)
+open import Data.List.Membership.Propositional using (_∉_)
+open Data.Nat using (_≟_; _+_)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality using (_≢_)
-open import Relation.Nullary using (¬_)
 open import Relation.Nullary.Decidable using (isYes)
 open import Relation.Nullary.Negation using (¬?)
 
@@ -30,12 +30,26 @@ data Type : Set where
   bin  : (⊗ : BinOp) → Type → Type → Type
   all  : (α : ℕ) → Type → Type
 
+-- Basic Properties -----------------------------------------------------------
+
 free : Type → List ℕ
 free (var α)     = α ∷ []
 free unit        = []
 free (bin ⊗ A B) = free A ++ free B
 free (all α A)   = filter (¬? ∘ (α ≟_)) (free A)
 
+#∀ : Type → ℕ
+#∀ (var α)     = 0
+#∀ unit        = 0
+#∀ (bin ⊗ A B) = #∀ A + #∀ B
+#∀ (all α A)   = suc (#∀ A)
+
+size : Type → ℕ
+size (var α)     = 1
+size unit        = 1
+size (bin ⊗ A B) = suc (size A + size B)
+size (all α A)   = suc (size A)
+
 -- Variable Renaming ----------------------------------------------------------
 
 record Subst {a} (A : Set a) : Set a where
@@ -76,8 +90,10 @@ data _≈_ : Type → Type → Set where
   var  : ∀ α → var α ≈ var α
   unit : unit ≈ unit
   bin  : A ≈ C → B ≈ D → bin ⊗ A B ≈ bin ⊗ C D
-  all  : let γ = mkFresh (free (all α A) ++ free (all β B)) in
-         rename ((γ , α) ∷ []) A ≈ rename ((γ , β) ∷ []) B → all α A ≈ all β B
+  all  :
+    (∀ γ → γ ∉ free (all α A) → γ ∉ free (all β B) →
+     rename ((γ , α) ∷ []) A ≈ rename ((γ , β) ∷ []) B) →
+    all α A ≈ all β B
 
 -- Basic Manipulations --------------------------------------------------------
 
-- 
cgit v1.2.3