From 1366e1f741462517ef517f2628508476484c4dc4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 16 Jul 2026 18:12:57 +0200
Subject: [PATCH 1/5] add Univ.v

---
 Tactic.lp | 48 ++++++++++++++++++++++++++++++++----------------
 Univ.lp   | 23 +++++++++++++++++++++++
 2 files changed, 55 insertions(+), 16 deletions(-)
 create mode 100644 Univ.lp

diff --git a/Tactic.lp b/Tactic.lp
index 6d4597e..fefd76e 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -1,28 +1,44 @@
 // define a type representing Lambdapi tactics
 
-require open Stdlib.String Stdlib.Option Stdlib.List;
-
-constant symbol Tactic : TYPE;
+require open Stdlib.String Stdlib.Univ;
 
 // mandatory builtins
 
+constant symbol Tactic : TYPE;
+builtin "Tactic" ≔ Tactic;
+
 constant symbol #admit : Tactic;
 builtin "admit" ≔ #admit;
 
-symbol & : Tactic → Tactic → Tactic;
-builtin "and" ≔ &;
-notation & infix right 10;
+constant symbol #all_hyps: (Π [l] [a:U l], ε a → Tactic) → Tactic;
+builtin "all_hyps" ≔ #all_hyps;
 
-constant symbol #apply [p] : π p → Tactic;
+constant symbol #apply: Π [l] [a:U l], ε a → Tactic;
 builtin "apply" ≔ #apply;
 
-constant symbol #assume : String → Tactic;
+constant symbol #assume : String → Π [l], Π [a:U l], (ε a → Tactic) → Tactic;
 builtin "assume" ≔ #assume;
 
+constant symbol #assumption : Tactic;
+builtin "assumption" ≔ #assumption;
+
+constant symbol #change: Π [l] [a:U l], ε a → Tactic;
+builtin "change" ≔ #change;
+
+constant symbol & : Tactic → Tactic → Tactic;
+builtin "compose" ≔ &;
+notation & infix right 10;
+
 constant symbol #fail : Tactic;
 builtin "fail" ≔ #fail;
 
-constant symbol #generalize : Π [a], τ a → Tactic;
+constant symbol #first_hyp: (Π [l] [a:U l], ε a → Tactic) → Tactic;
+builtin "first_hyp" ≔ #first_hyp;
+
+constant symbol #focus : String → Tactic;
+builtin "focus" ≔ #focus;
+
+constant symbol #generalize : Π [l] [a:U l], ε a → Tactic;
 builtin "generalize" ≔ #generalize;
 
 constant symbol #have : String → Prop → Tactic;
@@ -34,22 +50,25 @@ builtin "induction" ≔ #induction;
 constant symbol #orelse : Tactic → Tactic → Tactic;
 builtin "orelse" ≔ #orelse;
 
-constant symbol #refine [p] : π p → Tactic;
+constant symbol #print : String → Tactic;
+builtin "print" ≔ #print;
+
+constant symbol #refine: String → Tactic;
 builtin "refine" ≔ #refine;
 
 constant symbol #reflexivity : Tactic;
 builtin "reflexivity" ≔ #reflexivity;
 
-constant symbol #remove : Π [a], π a → Tactic;
+constant symbol #remove : Π [l] [a:U l], ε a → Tactic;
 builtin "remove" ≔ #remove;
 
 constant symbol #repeat : Tactic → Tactic;
 builtin "repeat" ≔ #repeat;
 
- symbol #rewrite : String → String → Π [a], π a → Tactic;
+ symbol #rewrite : String → String → Π [l] [a:U l], ε a → Tactic;
 builtin "rewrite" ≔ #rewrite;
 
-constant symbol #set : String → Π [a], τ a → Tactic;
+constant symbol #set : String → Π [l] [a:U l], ε a → Tactic;
 builtin "set" ≔ #set;
 
 constant symbol #simplify : Tactic;
@@ -70,9 +89,6 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
-constant symbol #change : Tactic;
-builtin "change" ≔ #change;
-
 // defined tactics
 
 symbol nothing ≔ #try #fail;
diff --git a/Univ.lp b/Univ.lp
new file mode 100644
index 0000000..331f167
--- /dev/null
+++ b/Univ.lp
@@ -0,0 +1,23 @@
+require open Stdlib.Set Stdlib.Prop;
+
+constant symbol L:TYPE;
+
+builtin "Level" ≔ L;
+
+constant symbol prop:L;
+constant symbol set_:L;
+
+injective symbol U:L → TYPE;
+
+builtin "Univ" ≔ U;
+
+rule U prop ↪ Prop
+with U set_ ↪ Set;
+
+symbol ε:Π [l:L], U l → TYPE;
+
+rule ε [prop] $a ↪ π $a
+with ε [set_] $a ↪ τ $a;
+
+unif_rule ε $a ≡ π $b ↪ [$a ≡ $b];
+unif_rule ε $a ≡ τ $b ↪ [$a ≡ $b];

From 37474370976401b148172540cd2ec691ea604f7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 16 Jul 2026 18:34:20 +0200
Subject: [PATCH 2/5] wip

---
 Tactic.lp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Tactic.lp b/Tactic.lp
index fefd76e..4fa591e 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -13,6 +13,10 @@ builtin "admit" ≔ #admit;
 constant symbol #all_hyps: (Π [l] [a:U l], ε a → Tactic) → Tactic;
 builtin "all_hyps" ≔ #all_hyps;
 
+constant symbol & : Tactic → Tactic → Tactic;
+builtin "and" ≔ &;
+notation & infix right 10;
+
 constant symbol #apply: Π [l] [a:U l], ε a → Tactic;
 builtin "apply" ≔ #apply;
 
@@ -25,10 +29,6 @@ builtin "assumption" ≔ #assumption;
 constant symbol #change: Π [l] [a:U l], ε a → Tactic;
 builtin "change" ≔ #change;
 
-constant symbol & : Tactic → Tactic → Tactic;
-builtin "compose" ≔ &;
-notation & infix right 10;
-
 constant symbol #fail : Tactic;
 builtin "fail" ≔ #fail;
 

From c0058a207ba3e4a39e63af28e244244ec4c31faf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 16 Jul 2026 18:53:46 +0200
Subject: [PATCH 3/5] wip

---
 Univ.lp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Univ.lp b/Univ.lp
index 331f167..5511729 100644
--- a/Univ.lp
+++ b/Univ.lp
@@ -16,6 +16,8 @@ with U set_ ↪ Set;
 
 symbol ε:Π [l:L], U l → TYPE;
 
+builtin "Type" ≔ ε;
+
 rule ε [prop] $a ↪ π $a
 with ε [set_] $a ↪ τ $a;
 

From 08864e1e6253acd2feeae350822997b9a8faaa67 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Mon, 20 Jul 2026 14:55:14 +0200
Subject: [PATCH 4/5] wip

---
 HOL.lp    | 12 ++++++++++--
 Tactic.lp | 28 ++++++++++++++--------------
 Univ.lp   | 21 +++++++++++++++------
 3 files changed, 39 insertions(+), 22 deletions(-)

diff --git a/HOL.lp b/HOL.lp
index 8bb76f7..f5e4ac6 100644
--- a/HOL.lp
+++ b/HOL.lp
@@ -1,7 +1,15 @@
 require open Stdlib.Set;
 
-symbol ⤳ : Set → Set → Set; // \leadsto
+constant symbol ⤳ : Set → Set → Set; // \leadsto
 
 notation ⤳ infix right 20;
 
-rule τ ($x ⤳ $y) ↪ τ $x → τ $y;
+rule τ ($a ⤳ $b) ↪ τ $a → τ $b;
+
+injective symbol ⤳d : Π a:Set, (τ a → Set) → Set;
+
+notation ⤳d infix right 20;
+
+rule $a ⤳d λ _,$b.[] ↪ $a ⤳ $b;
+
+rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x];
diff --git a/Tactic.lp b/Tactic.lp
index 4fa591e..2b37519 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -10,38 +10,38 @@ builtin "Tactic" ≔ Tactic;
 constant symbol #admit : Tactic;
 builtin "admit" ≔ #admit;
 
-constant symbol #all_hyps: (Π [l] [a:U l], ε a → Tactic) → Tactic;
+constant symbol #all_hyps: (Π [l] [a:U l], η a → Tactic) → Tactic;
 builtin "all_hyps" ≔ #all_hyps;
 
-constant symbol & : Tactic → Tactic → Tactic;
-builtin "and" ≔ &;
-notation & infix right 10;
-
-constant symbol #apply: Π [l] [a:U l], ε a → Tactic;
+constant symbol #apply: Π [l] [a:U l], η a → Tactic;
 builtin "apply" ≔ #apply;
 
-constant symbol #assume : String → Π [l], Π [a:U l], (ε a → Tactic) → Tactic;
+constant symbol #assume : String → Π [l], Π [a:U l], (η a → Tactic) → Tactic;
 builtin "assume" ≔ #assume;
 
 constant symbol #assumption : Tactic;
 builtin "assumption" ≔ #assumption;
 
-constant symbol #change: Π [l] [a:U l], ε a → Tactic;
+constant symbol #change: Π [l] [a:U l], η a → Tactic;
 builtin "change" ≔ #change;
 
+constant symbol & : Tactic → Tactic → Tactic;
+builtin "compose" ≔ &;
+notation & infix right 10;
+
 constant symbol #fail : Tactic;
 builtin "fail" ≔ #fail;
 
-constant symbol #first_hyp: (Π [l] [a:U l], ε a → Tactic) → Tactic;
+constant symbol #first_hyp: (Π [l] [a:U l], η a → Tactic) → Tactic;
 builtin "first_hyp" ≔ #first_hyp;
 
 constant symbol #focus : String → Tactic;
 builtin "focus" ≔ #focus;
 
-constant symbol #generalize : Π [l] [a:U l], ε a → Tactic;
+constant symbol #generalize : Π [l] [a:U l], η a → Tactic;
 builtin "generalize" ≔ #generalize;
 
-constant symbol #have : String → Prop → Tactic;
+constant symbol #have : String → Π [l] [a:U l], η a → Tactic;
 builtin "have" ≔ #have;
 
 constant symbol #induction : Tactic;
@@ -59,16 +59,16 @@ builtin "refine" ≔ #refine;
 constant symbol #reflexivity : Tactic;
 builtin "reflexivity" ≔ #reflexivity;
 
-constant symbol #remove : Π [l] [a:U l], ε a → Tactic;
+constant symbol #remove : Π [l] [a:U l], η a → Tactic;
 builtin "remove" ≔ #remove;
 
 constant symbol #repeat : Tactic → Tactic;
 builtin "repeat" ≔ #repeat;
 
- symbol #rewrite : String → String → Π [l] [a:U l], ε a → Tactic;
+ symbol #rewrite : String → String → Π [l] [a:U l], η a → Tactic;
 builtin "rewrite" ≔ #rewrite;
 
-constant symbol #set : String → Π [l] [a:U l], ε a → Tactic;
+constant symbol #set : String → Π [l] [a:U l], η a → Tactic;
 builtin "set" ≔ #set;
 
 constant symbol #simplify : Tactic;
diff --git a/Univ.lp b/Univ.lp
index 5511729..1b76885 100644
--- a/Univ.lp
+++ b/Univ.lp
@@ -14,12 +14,21 @@ builtin "Univ" ≔ U;
 rule U prop ↪ Prop
 with U set_ ↪ Set;
 
-symbol ε:Π [l:L], U l → TYPE;
+injective symbol η:Π [l:L], U l → TYPE; // \eta
 
-builtin "Type" ≔ ε;
+builtin "Type" ≔ η;
 
-rule ε [prop] $a ↪ π $a
-with ε [set_] $a ↪ τ $a;
+rule @η prop ↪ π
+with @η set_ ↪ τ;
 
-unif_rule ε $a ≡ π $b ↪ [$a ≡ $b];
-unif_rule ε $a ≡ τ $b ↪ [$a ≡ $b];
+unif_rule @η $l $a ≡ π $b ↪ [$l ≡ prop; $a ≡ $b];
+unif_rule @η $l $a ≡ τ $b ↪ [$l ≡ set_; $a ≡ $b];
+
+require open Stdlib.FOL;
+
+unif_rule @η $l $a ≡ Π x:τ $b, π $c.[x] ↪ [$l ≡ prop; $a ≡ @∀ $b (λ x:τ $b, $c.[x])];
+
+require open Stdlib.HOL;
+
+unif_rule @η $l $a ≡ Π _:τ $b, τ $c.[] ↪ [$l ≡ set_; $a ≡ $b ⤳ $c.[]];
+unif_rule @η $l $a ≡ Π x:τ $b, τ $c.[x] ↪ [$l ≡ set_; $a ≡ $b ⤳d λ x:τ $b, $c.[x]];

From 7e8e6be12faa06c7f6d8c687606b33c87d456124 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 21 Jul 2026 11:01:12 +0200
Subject: [PATCH 5/5] wip

---
 Prop.lp | 2 +-
 Set.lp  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Prop.lp b/Prop.lp
index 2bfa70c..32f0f22 100644
--- a/Prop.lp
+++ b/Prop.lp
@@ -8,7 +8,7 @@ builtin "Prop" ≔ Prop;
 
 injective symbol π : Prop → TYPE; // `p
 
-builtin "P" ≔ π;
+builtin "Prf" ≔ π;
 
 // true
 
diff --git a/Set.lp b/Set.lp
index fea919a..81d1758 100644
--- a/Set.lp
+++ b/Set.lp
@@ -10,7 +10,7 @@ constant symbol ι : Set;
 
 injective symbol τ : Set → TYPE; // `t or \tau
 
-builtin "T" ≔ τ;
+builtin "El" ≔ τ;
 
 // We assume that sets are non-empty