Term injective, Univ constant

encodings/cf.lp

 // PVS cert with functional PTS
-symbol Sort : TYPE
-symbol Univ : Sort ⇒ TYPE
+constant symbol Sort : TYPE
+constant symbol Univ : Sort ⇒ TYPE
 
 constant symbol Kind : Sort
 constant symbol Type : Sort
@@ -8,9 +8,9 @@ constant symbol Prop : Sort
 
 // Axioms: (Prop, Type), (Type, Kind)
 // Prop: Type
-symbol uProp : Univ Type
+constant symbol uProp : Univ Type
 // Type: Kind
-symbol uType : Univ Kind
+constant symbol uType : Univ Kind
 
 // Encoding of rules
 // (Prop, Prop, Prop), (Type, Type, Type), (Type, Prop, Prop)
@@ -22,34 +22,33 @@ rule Rule Prop Prop → Prop
  and Rule Type Prop → Prop
 
 // [Term s t] decodes term [t] of encoded sort [s]
-symbol Term {s : Sort} : Univ s ⇒ TYPE
+injective symbol Term {s : Sort} : Univ s ⇒ TYPE
 
 rule Term uProp → Univ Prop
  and Term uType → Univ Type
 
 // [prod s1 s2 A B] encodes [Π x : (A: s1). (B x: s2)]
 symbol prod {s1 s2 : Sort} (A : Univ s1) :
-  (@Term s1 A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
+  (Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
 
-rule Term _ (prod &s1 &s2 &A &B) → ∀ x : Term &A, Term (&B x)
+rule Term (prod &s1 &s2 &A &B) → ∀ x : Term &A, Term (&B x)
 
 // Predicate subtyping
 // can be seen as a dependant pair type with
 // - first element is a term of some type [A] and
 // - second is a predicate on [A] verified by the first element.
-symbol psub (A : Univ Type) : (@Term Type A ⇒ Univ Prop) ⇒ Univ Type
+symbol psub (A : Univ Type) : (Term A ⇒ Univ Prop) ⇒ Univ Type
 
 // Γ ⊢ M : { v : T | U }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-symbol fst {T : Univ Type} {U : @Term Type T ⇒ Univ Prop}:
-  @Term Type (psub T U) ⇒ @Term Type T
+symbol fst {T : Univ Type} {U : Term T ⇒ Univ Prop}: Term (psub T U) ⇒ Term T
 
 //  Γ ⊢ M : { v : T | U }
 // ——————————————————————————PROJr
 // Γ ⊢ snd(M) : U[v ≔ fst(M)]
-symbol snd (T: Univ Type) (U: @Term Type T ⇒ Univ Prop)
-  (M: @Term Type (psub T U)): @Term Prop (U (@fst T U M))
+symbol snd (T: Univ Type) (U: Term T ⇒ Univ Prop) (M: Term (psub T U)):
+  Term (U (@fst T U M))
 
 // An inhabitant of a predicate subtype, that is, a pair of
 // an element and the proof that it satisfies the predicate
@@ -57,7 +56,7 @@ symbol snd (T: Univ Type) (U: @Term Type T ⇒ Univ Prop)
 // ——————————————————————————————————————————————————PAIR
 //           Γ ⊢ ⟨M, N⟩ : {v : T | U}
 symbol pair {T: Univ Type} (U: @Term Type T ⇒ Univ Prop) (M: @Term Type T):
-  @Term Prop (U M) ⇒ @Term Type (psub T U)
+  Term (U M) ⇒ Term (psub T U)
 
 rule @fst &T &U (@pair &T &U &M _) → &M
 rule @snd &T &U (@pair &T &U _ &P) → &P

prelude/cf/booleans.lp

@@ -2,6 +2,6 @@ require open encodings.cf
 
 definition bool ≔ Prop
 definition false ≔ @prod Type Prop uProp (λ x : @Term Type uProp, x)
-definition true ≔ @Term Prop false ⇒ @Term Prop false
+definition true ≔ Term false ⇒ Term false
 
-definition bnot (P: @Term Type uProp) ≔ @prod Prop Prop P (λ x, false)
+definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ x, false)

prelude/cf/equalities.lp

 require open encodings.cf prelude.cf.booleans
 
-symbol eq {T: @Term Kind uType}: @Term Type T ⇒ @Term Type T ⇒ @Term Type uProp
+symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp

prelude/cf/naturalnumbers.lp

 require open encodings.cf prelude.cf.booleans
 
-constant symbol nat : @Term Kind uType
-constant symbol zero : @Term Type nat
-symbol succ : @Term Type nat ⇒ @Term Type nat
+constant symbol nat : Term uType
+constant symbol zero : Term nat
+injective symbol succ : Term nat ⇒ Term nat
 
 set builtin "0" ≔ zero
 set builtin "+1" ≔ succ

prelude/cf/notequal.lp

 require open encodings.cf prelude.cf.booleans prelude.cf.equalities
 
-definition neq {T: @Term Kind uType} (x y: @Term Type T) ≔ bnot (@eq T x y)
+definition neq {T: Term uType} (x y: Term T) ≔ bnot (eq x y)