switched to nondep function in IF sort signatures

javra · Oct 21, 2020 · 4cf0326 · 4cf0326
1 parent 54697a3
commit 4cf0326
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 20 deletions.
diff --git a/IF.agda b/IF.agda
@@ -11,8 +11,8 @@ infixl 8 _[_]tP
 infixl 8 _[_]t
 
 data TyS : Set₁ where
-  U  : TyS
-  Π̂S : (T : Set) → (T → TyS) → TyS
+  U    : TyS
+  _⇒̂S_ : (T : Set) → TyS → TyS
 
 data SCon : Set₁ where
   ∙c   : SCon
@@ -24,7 +24,7 @@ data Var : SCon → TyS → Set₁ where
 
 data Tm (Γc : SCon) : TyS → Set₁ where
   var  : ∀{A} → Var Γc A → Tm Γc A
-  _$S_ : ∀{T B} → Tm Γc (Π̂S T B) → (τ : T) → Tm Γc (B τ)
+  _$S_ : ∀{T B} → Tm Γc (T ⇒̂S B) → T → Tm Γc B
 
 data TyP (Γc : SCon) : Set₁ where
   El   : Tm Γc U → TyP Γc
@@ -41,9 +41,6 @@ Tm∙c (var ())
 Tm∙c (t $S α) = Tm∙c t
 
 -- Non dependent, recursive functions
-_⇒̂S_ : Set → TyS → TyS
-T ⇒̂S A = Π̂S T (λ _ → A)
-
 _⇒̂P_ : ∀{Γc} → Set → TyP Γc → TyP Γc
 T ⇒̂P A = Π̂P T (λ _ → A)
 
@@ -177,7 +174,7 @@ El[] = refl
 Π̂P[] : ∀{Γ Δ}{δ : Sub Γ Δ}{T}{A : T → TyP Δ} → (Π̂P T A) [ δ ]T ≡ Π̂P T λ α → A α [ δ ]T
 Π̂P[] = refl
 
-$S[] : ∀{Γ Δ}{δ : Sub Γ Δ}{T}{B}{t : Tm Δ (Π̂S T B)}{α} → (t $S α) [ δ ]t ≡ (t [ δ ]t) $S α
+$S[] : ∀{Γ Δ}{δ : Sub Γ Δ}{T}{B}{t : Tm Δ (T ⇒̂S B)}{α} → (t $S α) [ δ ]t ≡ (t [ δ ]t) $S α
 $S[] = refl
 
 ⇒P[] : ∀{Γ Δ}{δ : Sub Γ Δ}{a : Tm Δ U}{A : TyP Δ} → (a ⇒P A) [ δ ]T ≡ (a [ δ ]t) ⇒P (A [ δ ]T)

diff --git a/IFA.agda b/IFA.agda
@@ -6,7 +6,7 @@ open import IF
 
 _ᵃS : ∀{ℓ} → TyS → Set (suc ℓ)
 _ᵃS {ℓ} U        = Set ℓ
-_ᵃS {ℓ} (Π̂S T B) = (τ : T) → _ᵃS {ℓ} (B τ)
+_ᵃS {ℓ} (T ⇒̂S B) = T → _ᵃS {ℓ} B
 
 _ᵃc : ∀{ℓ} → SCon → Set (suc ℓ)
 ∙c ᵃc             = Lift _ ⊤

diff --git a/IFD.agda b/IFD.agda
@@ -7,7 +7,7 @@ open import IFA
 
 ᵈS : ∀{ℓ' ℓ}(B : TyS)(α : _ᵃS {ℓ} B) → Set (suc ℓ' ⊔ suc ℓ)
 ᵈS {ℓ'}{ℓ} U       α = α → Set (ℓ' ⊔ ℓ)
-ᵈS {ℓ'}   (Π̂S T B) π = (τ : T) → ᵈS {ℓ'} (B τ) (π τ)
+ᵈS {ℓ'}   (T ⇒̂S B) π = (τ : T) → ᵈS {ℓ'} B (π τ)
 
 ᵈc : ∀{ℓ' ℓ}(Γc : SCon)(γc : _ᵃc {ℓ} Γc) → Set (suc ℓ' ⊔ suc ℓ)
 ᵈc      ∙c        γc       = Lift _ ⊤

diff --git a/IFEx.agda b/IFEx.agda
@@ -11,7 +11,7 @@ module Constructor {Ωc}(Ω : Con Ωc) where
 
   conSᵃ' : ∀{B}(t : Tm Ωc B) → _ᵃS {suc zero} B
   conSᵃ' {U}      t     = TmP Ω (El t)
-  conSᵃ' {Π̂S T B} t     = λ τ → conSᵃ' (t $S τ)
+  conSᵃ' {T ⇒̂S B} t     = λ τ → conSᵃ' (t $S τ)
 
   concᵃ' : ∀{Γc}(σ : Sub Ωc Γc) → _ᵃc {suc zero} Γc
   concᵃ' ε       = lift tt
@@ -54,7 +54,7 @@ module Eliminator {Ωc}(Ω : Con Ωc){ωcᵈ}(ωᵈ : ᵈC {suc zero} Ω ωcᵈ
   elimSᵃ' {U}      a = λ α → coe (ᵈt a _ & (contPᵃ' idP (coe (contᵃ' id a) α)
                                  ◾ coecoe⁻¹' (contᵃ' id a) α))
                                    (ᵈtP {suc zero} {suc zero} (coe (contᵃ' id a) α) ωᵈ)
-  elimSᵃ' {Π̂S T B} t = λ τ → elimSᵃ' {B τ} (t $S τ)
+  elimSᵃ' {T ⇒̂S B} t = λ τ → elimSᵃ' {B} (t $S τ)
 
   elimcᵃ' : ∀{Γc}(σ : Sub Ωc Γc) → ˢc Γc (ᵈs σ ωcᵈ)
   elimcᵃ' ε       = lift tt

diff --git a/IFEx_REW.agda b/IFEx_REW.agda
@@ -9,7 +9,7 @@ open import IFS
 
 conSᵃ' : ∀{Ωc}(Ω : Con Ωc){B}(t : Tm Ωc B) → _ᵃS {suc zero} B
 conSᵃ' Ω {U}      t     = TmP Ω (El t)
-conSᵃ' Ω {Π̂S T B} t     = λ τ → conSᵃ' Ω (t $S τ)
+conSᵃ' Ω {T ⇒̂S B} t     = λ τ → conSᵃ' Ω (t $S τ)
 
 concᵃ' : ∀{Ωc}(Ω : Con Ωc)(Γc : SCon)(σ : Sub Ωc Γc) → _ᵃc {suc zero} Γc
 concᵃ' Ω ∙c        ε       = lift tt
@@ -20,7 +20,7 @@ contᵃ' : ∀{Ωc}(Ω : Con Ωc){Γc}(σ : Sub Ωc Γc){B}(t : Tm Γc B)
 contᵃ' Ω ε           t                   = ⊥-elim (Tm∙c t)
 contᵃ' Ω (σ , s)     (var vvz)           = refl
 contᵃ' Ω (σ , s) {B} (var (vvs x))       = contᵃ' Ω σ (var x)
-contᵃ' Ω (σ , s) {B} (_$S_ {T}{B''} t α) = happly (contᵃ' Ω (σ , s) {Π̂S T B''} t) α
+contᵃ' Ω (σ , s) {B} (_$S_ {T}{B''} t α) = happly (contᵃ' Ω (σ , s) {T ⇒̂S B''} t) α
 {-# REWRITE contᵃ' #-}
 
 contᵃ'' : ∀{Ωc}(Ω : Con Ωc){Γc}(σ : Sub Ωc Γc){B}(t : Tm Γc B)
@@ -54,8 +54,8 @@ conᵃ : ∀{Γc}(Γ : Con Γc) → (Γ ᵃC) (concᵃ Γ)
 conᵃ Γ = conᵃ' Γ Γ idP
 
 elimSᵃ' : ∀{Ωc}(Ω : Con Ωc){ωcᵈ}(ωᵈ : ᵈC {suc zero} Ω ωcᵈ (conᵃ Ω)){B}(t : Tm Ωc B) → ˢS B (ᵈt t ωcᵈ)
-elimSᵃ' Ω ωᵈ {U}      t = λ α → lower (ᵈtP α ωᵈ)
-elimSᵃ' Ω ωᵈ {Π̂S T B} t = λ τ → elimSᵃ' Ω ωᵈ {B τ} (t $S τ)
+elimSᵃ' Ω ωᵈ {U}      t = λ α → ᵈtP α ωᵈ
+elimSᵃ' Ω ωᵈ {T ⇒̂S B} t = λ τ → elimSᵃ' Ω ωᵈ {B} (t $S τ)
 
 elimcᵃ' : ∀{Ωc}(Ω : Con Ωc){ωcᵈ}(ωᵈ : ᵈC Ω ωcᵈ (conᵃ Ω)){Γc}(σ : Sub Ωc Γc) → ˢc Γc (ᵈs σ ωcᵈ)
 elimcᵃ' Ω ωᵈ ε       = lift tt
@@ -101,7 +101,7 @@ nsucc : nat → nat
 nsucc = ₂ (₁ (conᵃ Γnat))
 
 nrec : ∀(P : nat → Set₁)(ps : ∀ n → P n → P (nsucc n))(pz : P nzero) → ∀ n → P n
-nrec P ps pz = elimSᵃ' Γnat (_ , (λ m p → lift (ps m p)) , lift pz) vz
+nrec P ps pz = elimSᵃ' Γnat (_ , (λ m p → ps m p) , pz) vz
 
 Γuu : Con (∙c ▶c U ▶c U)
 Γuu = ∙ ▶P El (vs vz) ▶P El vz
@@ -120,13 +120,13 @@ st2 = ₂ (conᵃ Γuu)
 
 uurec : ∀(P : uu1 → Set₁)(Q : uu2 → Set₁)(p : P st1)(q : Q st2) →
          ˢc (∙c ▶c U ▶c U) (_ , P , Q)
-uurec P Q p q = elimcᵃ Γuu (_ , lift p , lift q)
+uurec P Q p q = elimcᵃ Γuu (_ , p , q)
 
 postulate N : Set
 postulate Nz  : N
 postulate Ns  : N → N
 
-Γvec : Set → Con (∙c ▶c Π̂S N (λ _ → U))
+Γvec : Set → Con (∙c ▶c N ⇒̂S U)
 Γvec A = ∙ ▶P El (vz $S Nz) ▶P (Π̂P A (λ a → Π̂P N λ m → (vz $S m) ⇒P El (vz $S Ns m)))
 
 vec : Set → N → Set₁

diff --git a/IFM.agda b/IFM.agda
@@ -7,7 +7,7 @@ open import IFA
 
 ᵐS : ∀{ℓ' ℓ} B (αc : _ᵃS {ℓ} B)(βc : _ᵃS {ℓ'} B) → Set (ℓ' ⊔ ℓ)
 ᵐS U        αc βc = αc → βc
-ᵐS (Π̂S T B) αc βc = (τ : T) → ᵐS (B τ) (αc τ) (βc τ)
+ᵐS (T ⇒̂S B) αc βc = (τ : T) → ᵐS B (αc τ) (βc τ)
 
 ᵐc : ∀{ℓ' ℓ} Γc (γc : _ᵃc {ℓ} Γc)(δc : _ᵃc {ℓ'} Γc) → Set (ℓ' ⊔ ℓ)
 ᵐc ∙c        γc        δc        = Lift _ ⊤

diff --git a/IFS.agda b/IFS.agda
@@ -8,7 +8,7 @@ open import IFD
 
 ˢS : ∀{ℓ' ℓ} B {α} → ᵈS {ℓ'}{ℓ} B α → Set (ℓ' ⊔ ℓ)
 ˢS U        αᵈ = ∀ x → αᵈ x
-ˢS (Π̂S T B) πᵈ = (τ : T) → ˢS (B τ) (πᵈ τ)
+ˢS (T ⇒̂S B) πᵈ = (τ : T) → ˢS B (πᵈ τ)
 
 ˢc : ∀{ℓ' ℓ} Γc {γc} → ᵈc {ℓ'}{ℓ} Γc γc → Set (ℓ' ⊔ ℓ)
 ˢc ∙c        γcᵈ         = Lift _ ⊤