Make β-λ more generic (Argument can now be any type T instead of `Setn L)

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≈∀')
 ... | ⟨ ≈₁ , ≈₂ ⟩ 

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
-