misc

encodings/subtype.lp

 require open personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
 
 set declared "↑"
 set declared "↓"
@@ -26,6 +26,8 @@ rule μ (psub {&T} _) → μ &T
 symbol μ₀: Set ⇒ Set
 rule μ₀ (psub {&T} _) → μ₀ &T
 
+compute λT: Set, μ (μ T)
+
 // Constraints
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B
 definition ↑ {A} {B} ≔ upcast {A} {B}
@@ -37,11 +39,12 @@ admit
 
 symbol π {T: Set}: η (μ T) ⇒ Bool
 symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
-                (a: η A) (p: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
+                (a: η A) (_: ε (π {A} (↑ {A} {μ A} (sub_of_sup A) a))): η B
 definition ↓ {A} {B} ≔ downcast {A} {B}
 
 set flag "print_implicits" on
 rule π {&T ~> &U} → λx: η &T ⇒ η (μ &U), forall (λy, π {&U} (x y))
+// rule π {psub {&T} &a} → λx: η (μ &T), π {&T} x
 rule π {psub {&T} &a}
-   → λx: η (μ &T), impd {π {&T} x} (λy, &a (↓ {μ &T} {&T} _ x y))
+   → λx: η (μ &T), (π {&T} x) ∧ (λy: ε (π {&T} x), &a (↓ {μ &T} {&T} _ x y))
 // FIXME: does not type check because μ (μ &T) is not reduced to μ &T