From 201fe7942b558661ed149e8a85cdefdc1037c3e9 Mon Sep 17 00:00:00 2001
From: JKF <unijkf@gmail.com>
Date: Sat, 25 Apr 2026 22:24:28 +0200
Subject: [PATCH] =?UTF-8?q?Make=20=CE=B2-=CE=BB=20more=20generic=20(Argume?=
 =?UTF-8?q?nt=20can=20now=20be=20any=20type=20T=20instead=20of=20`Setn=20L?=
 =?UTF-8?q?)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 SubjectReduction/Inversion.agda     | 10 +++++-----
 SubjectReduction/Specification.agda |  6 +++---
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/SubjectReduction/Inversion.agda b/SubjectReduction/Inversion.agda
index 2ae9d87..df24d20 100644
--- a/SubjectReduction/Inversion.agda
+++ b/SubjectReduction/Inversion.agda
@@ -41,9 +41,9 @@ invert-≈-∀ (mk-≈ x ∀₁↪*x ∀₂↪*x) with ↪*-∀-shape ∀₁↪*
 
 invert-⊢λ' : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t : Term n} →
   Γ ⊢ `λ e ⦂ t →
-  ∃[ t₁ ] ∃[ t₂ ] ∃[ l ]
+  ∃[ t₁ ] ∃[ t₂ ] ∃[ T₂ ]
     t ≈ (∀[x⦂ t₁ ] t₂) ×
-    Γ ⊢ t₁ ⦂ (`Setn l) ×
+    Γ ⊢ t₁ ⦂ T₂ ×
     Γ , t₁ ⊢ e ⦂ t₂
 invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩ ⟩
 invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁
@@ -52,12 +52,12 @@ invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁
 
 invert-⊢λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ : Term n} {t₂ : Term (suc n)}
   → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂
-  → ∃[ t₁' ] ∃[ t₂' ] ∃[ l ]
+  → ∃[ t₁' ] ∃[ t₂' ] ∃[ T₁ ]
       t₁ ≈ t₁' ×
       t₂ ≈ t₂' ×
-      Γ ⊢ t₁' ⦂ (`Setn l) ×
+      Γ ⊢ t₁' ⦂ T₁ ×
       Γ , t₁' ⊢ e ⦂ t₂'
-invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ _  , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
+invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ _  , ⟨ ≈-refl , ⟨ ≈-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
 invert-⊢λ (⊢-≈ t≈∀ ⊢λ) with invert-⊢λ' ⊢λ 
 ... | ⟨ X , ⟨ E , ⟨ L , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀')
 ... | ⟨ ≈₁ , ≈₂ ⟩ 
diff --git a/SubjectReduction/Specification.agda b/SubjectReduction/Specification.agda
index e4dc349..1397123 100644
--- a/SubjectReduction/Specification.agda
+++ b/SubjectReduction/Specification.agda
@@ -383,8 +383,8 @@ data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where
       --------------
     → Γ ⊢ ` x ⦂ t
 
-  ⊢-λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ l : Term n} {t₂ : Term (suc n)}
-    → Γ ⊢ t₁ ⦂ `Setn l
+  ⊢-λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ T₁ : Term n} {t₂ : Term (suc n)}
+    → Γ ⊢ t₁ ⦂ T₁
     → Γ , t₁ ⊢ e ⦂ t₂
       -----------------------
     → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂
@@ -447,6 +447,7 @@ data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where
       ------------------------------
     → Γ ⊢ `subst t e₁ e₂ ⦂ t [ u₂ ]
 
+
 -- Extension
   ⊢-Setn : ∀ {n} {Γ : Context n} {l}
     → Γ ⊢ `Setn l ⦂ (`Setn (`lsuc l))
@@ -471,4 +472,3 @@ data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where
 
 cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v a b} → x ≡ y → u ≡ v → a ≡ b → f x u a ≡ f y v b
 cong₃ f refl refl refl = refl
-