refactor(builtin/heq): remove axiom hpiext since we don't use it anymore

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/heq.lean

@@ -40,8 +40,15 @@ theorem hsfunext {A : TypeM} {B B' : A → TypeU} {f : ∀ x, B x} {f' : ∀ x,
                        s2 : f' x  == f' x' := hcongr (hrefl f') Hx
                    in htrans s1 s2)
 
-axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
-      A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
-
 axiom hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} :
       A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
+
+-- The following axiom is not very useful, since the resultant
+-- equality is actually (@eq TypeM (∀ x, B x) (∀ x, B' x)).
+-- This is the case even if A, A', B and B' live in smaller universes (e.g., Type)
+-- To support this kind of axiom, it seems we have two options:
+--    1) Universe level parameters like Agda
+--    2) Axiom schema/template, where we create instances of hpiext for different universes.
+--       BTW, this is essentially what Coq does since the levels are implicit in Coq.
+-- axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
+--      A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)

src/library/heq_decls.cpp

@@ -17,6 +17,5 @@ MK_CONSTANT(hcongr_fn, name("hcongr"));
 MK_CONSTANT(TypeM, name("TypeM"));
 MK_CONSTANT(hfunext_fn, name("hfunext"));
 MK_CONSTANT(hsfunext_fn, name("hsfunext"));
-MK_CONSTANT(hpiext_fn, name("hpiext"));
 MK_CONSTANT(hallext_fn, name("hallext"));
 }

src/library/heq_decls.h

@@ -38,9 +38,6 @@ inline expr mk_hfunext_th(expr const & e1, expr const & e2, expr const & e3, exp
 expr mk_hsfunext_fn();
 bool is_hsfunext_fn(expr const & e);
 inline expr mk_hsfunext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hsfunext_fn(), e1, e2, e3, e4, e5, e6}); }
-expr mk_hpiext_fn();
-bool is_hpiext_fn(expr const & e);
-inline expr mk_hpiext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hpiext_fn(), e1, e2, e3, e4, e5, e6}); }
 expr mk_hallext_fn();
 bool is_hallext_fn(expr const & e);
 inline expr mk_hallext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_hallext_fn(), e1, e2, e3, e4, e5, e6}); }