From 7c729cb30aaf56b8f13c3e3f74c4762467914a71 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Fri, 26 Nov 2021 14:08:10 +0100
Subject: [PATCH] some notes, pair' constant

---
 encoding/lhol.lp     |  3 +++
 encoding/pvs_cert.lp | 12 ++++++------
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/encoding/lhol.lp b/encoding/lhol.lp
index d834dce..0b9353d 100644
--- a/encoding/lhol.lp
+++ b/encoding/lhol.lp
@@ -2,6 +2,7 @@
 constant symbol Set: TYPE;
 constant symbol Prop: TYPE;
 
+// WARNING: El and Prf are not injective.
 injective symbol El: Set → TYPE;
 injective symbol Prf: Prop → TYPE;
 
@@ -16,6 +17,8 @@ rule Prf ($P ⇒ $Q) ↪ Π h: Prf $P, Prf ($Q h);
 
 constant symbol arrd (x: Set): (El x → Set) → Set;
 rule El (arrd $X $T) ↪ Π x: El $X, El ($T x);
+// To have injectivity wrt. El, the above rule may be replaced by
+// rule El (arrd $X (\x, $T[x])) ↪ Π y: El $X, El ($T[y]);
 
 constant symbol arr: Set → Set → Set;
 rule El (arr $X $Y) ↪ (El $X) → (El $Y);
diff --git a/encoding/pvs_cert.lp b/encoding/pvs_cert.lp
index 601d23a..d6fef9e 100644
--- a/encoding/pvs_cert.lp
+++ b/encoding/pvs_cert.lp
@@ -2,13 +2,13 @@
 require open personoj.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
-protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
-symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t;
+protected constant symbol pair': Π(a: Set) (p: El a → Prop), El a → El (@psub a p);
+symbol fst: Π{a: Set} {p: El a → Prop}, El (@psub a p) → El a;
 
-symbol snd {t: Set} {p: El t → Prop} (m: El (psub p)): Prf (p (fst m));
+symbol snd {a: Set} {p: El a → Prop} (m: El (@psub a p)): Prf (p (@fst a p m));
 
 // Proof irrelevance
-symbol pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
-     ≔ pair' t p m;
+symbol pair {a: Set} {p: El a → Prop} (m: El a) (_: Prf (p m))
+     ≔ pair' a p m;
 
-rule fst (pair' _ _ $M) ↪ $M;
+rule @fst _ _ (pair' _ _ $M) ↪ $M;
-- 
GitLab