diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 2ee3a2a0d9..c0d3ead5f3 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -371,6 +371,13 @@ struct app_builder::imp {
         return ::lean::mk_app(mk_constant(get_iff_name()), a, b);
     }
 
+    expr mk_heq(expr const & a, expr const & b) {
+        expr A    = m_ctx->infer(a);
+        expr B    = m_ctx->infer(b);
+        level lvl = get_level(A);
+        return ::lean::mk_app(mk_constant(get_heq_name(), {lvl}), A, a, B, b);
+    }
+
     expr mk_eq_refl(expr const & a) {
         expr A     = m_ctx->infer(a);
         level lvl  = get_level(A);
@@ -381,14 +388,19 @@ struct app_builder::imp {
         return ::lean::mk_app(mk_constant(get_iff_refl_name()), a);
     }
 
+    expr mk_heq_refl(expr const & a) {
+        expr A     = m_ctx->infer(a);
+        level lvl  = get_level(A);
+        return ::lean::mk_app(mk_constant(get_heq_refl_name(), {lvl}), A, a);
+    }
+
     expr mk_eq_symm(expr const & H) {
         expr p    = m_ctx->relaxed_whnf(m_ctx->infer(H));
-        expr lhs, rhs;
-        if (!is_eq(p, lhs, rhs)) {
+        expr A, lhs, rhs;
+        if (!is_eq(p, A, lhs, rhs)) {
             lean_trace("app_builder", tout() << "failed to build eq.symm, equality expected:\n" << H << "\n";);
             throw app_builder_exception();
         }
-        expr A    = m_ctx->infer(lhs);
         level lvl = get_level(A);
         return ::lean::mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
     }
@@ -403,16 +415,26 @@ struct app_builder::imp {
         }
     }
 
+    expr mk_heq_symm(expr const & H) {
+        expr p     = m_ctx->relaxed_whnf(m_ctx->infer(H));
+        expr A, a, B, b;
+        if (!is_heq(p, A, a, B, b)) {
+            lean_trace("app_builder", tout() << "failed to build heq.symm, heterogeneous equality expected:\n" << H << "\n";);
+            throw app_builder_exception();
+        }
+        level lvl = get_level(A);
+        return ::lean::mk_app({mk_constant(get_heq_symm_name(), {lvl}), A, B, a, b, H});
+    }
+
     expr mk_eq_trans(expr const & H1, expr const & H2) {
         expr p1    = m_ctx->relaxed_whnf(m_ctx->infer(H1));
         expr p2    = m_ctx->relaxed_whnf(m_ctx->infer(H2));
-        expr lhs1, rhs1, lhs2, rhs2;
-        if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) {
+        expr A, lhs1, rhs1, lhs2, rhs2;
+        if (!is_eq(p1, A, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) {
             lean_trace("app_builder", tout() << "failed to build eq.trans, equality expected:\n"
                        << H1 << "\n" << H2 << "\n";);
             throw app_builder_exception();
         }
-        expr A     = m_ctx->infer(lhs1);
         level lvl  = get_level(A);
         return ::lean::mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
     }
@@ -428,6 +450,19 @@ struct app_builder::imp {
         }
     }
 
+    expr mk_heq_trans(expr const & H1, expr const & H2) {
+        expr p1    = m_ctx->relaxed_whnf(m_ctx->infer(H1));
+        expr p2    = m_ctx->relaxed_whnf(m_ctx->infer(H2));
+        expr A1, a1, B1, b1, A2, a2, B2, b2;
+        if (!is_heq(p1, A1, a1, B1, b1) || !is_heq(p2, A2, a2, B2, b2)) {
+            lean_trace("app_builder", tout() << "failed to build heq.trans, heterogeneous equality expected:\n"
+                       << H1 << "\n" << H2 << "\n";);
+            throw app_builder_exception();
+        }
+        level lvl  = get_level(A1);
+        return ::lean::mk_app({mk_constant(get_heq_trans_name(), {lvl}), A1, B1, B2, a1, b1, b2, H1, H2});
+    }
+
     expr mk_rel(name const & n, expr const & lhs, expr const & rhs) {
         if (n == get_eq_name()) {
             return mk_eq(lhs, rhs);
@@ -452,6 +487,8 @@ struct app_builder::imp {
             return mk_eq_refl(a);
         } else if (relname == get_iff_name()) {
             return mk_iff_refl(a);
+        } else if (relname == get_heq_name()) {
+            return mk_heq_refl(a);
         } else if (auto info = m_refl_getter(relname)) {
             return mk_app(info->m_name, 1, &a);
         } else {
@@ -466,6 +503,8 @@ struct app_builder::imp {
             return mk_eq_symm(H);
         } else if (relname == get_iff_name()) {
             return mk_iff_symm(H);
+        } else if (relname == get_heq_name()) {
+            return mk_heq_symm(H);
         } else if (auto info = m_symm_getter(relname)) {
             return mk_app(info->m_name, 1, &H);
         } else {
@@ -480,6 +519,8 @@ struct app_builder::imp {
             return mk_eq_trans(H1, H2);
         } else if (relname == get_iff_name()) {
             return mk_iff_trans(H1, H2);
+        } else if (relname == get_heq_name()) {
+            return mk_heq_trans(H1, H2);
         } else if (auto info = m_trans_getter(relname, relname)) {
             expr args[2] = {H1, H2};
             return mk_app(info->m_name, 2, args);
@@ -509,12 +550,11 @@ struct app_builder::imp {
         if (is_constant(get_app_fn(H2), get_eq_refl_name()))
             return H1;
         expr p       = m_ctx->relaxed_whnf(m_ctx->infer(H2));
-        expr lhs, rhs;
-        if (!is_eq(p, lhs, rhs)) {
+        expr A, lhs, rhs;
+        if (!is_eq(p, A, lhs, rhs)) {
             lean_trace("app_builder", tout() << "failed to build eq.rec, equality proof expected:\n" << H2 << "\n";);
             throw app_builder_exception();
         }
-        expr A      = m_ctx->infer(lhs);
         level A_lvl = get_level(A);
         expr mtype  = m_ctx->relaxed_whnf(m_ctx->infer(motive));
         if (!is_pi(mtype) || !is_sort(binding_body(mtype))) {
@@ -530,12 +570,11 @@ struct app_builder::imp {
         if (is_constant(get_app_fn(H2), get_eq_refl_name()))
             return H1;
         expr p       = m_ctx->relaxed_whnf(m_ctx->infer(H2));
-        expr lhs, rhs;
-        if (!is_eq(p, lhs, rhs)) {
+        expr A, lhs, rhs;
+        if (!is_eq(p, A, lhs, rhs)) {
             lean_trace("app_builder", tout() << "failed to build eq.drec, equality proof expected:\n" << H2 << "\n";);
             throw app_builder_exception();
         }
-        expr A      = m_ctx->infer(lhs);
         level A_lvl = get_level(A);
         expr mtype  = m_ctx->relaxed_whnf(m_ctx->infer(motive));
         if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype)))) {
@@ -547,6 +586,28 @@ struct app_builder::imp {
         return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2});
     }
 
+    expr mk_eq_of_heq(expr const & H) {
+        expr p    = m_ctx->relaxed_whnf(m_ctx->infer(H));
+        expr A, a, B, b;
+        if (!is_heq(p, A, a, B, b)) {
+            lean_trace("app_builder", tout() << "failed to build eq_of_heq, heterogeneous equality expected:\n" << H << "\n";);
+            throw app_builder_exception();
+        }
+        level lvl  = get_level(A);
+        return ::lean::mk_app({mk_constant(get_eq_of_heq_name(), {lvl}), A, a, b, H});
+    }
+
+    expr mk_heq_of_eq(expr const & H) {
+        expr p    = m_ctx->relaxed_whnf(m_ctx->infer(H));
+        expr A, a, b;
+        if (!is_eq(p, A, a, b)) {
+            lean_trace("app_builder", tout() << "failed to build heq_of_eq equality expected:\n" << H << "\n";);
+            throw app_builder_exception();
+        }
+        level lvl  = get_level(A);
+        return ::lean::mk_app({mk_constant(get_heq_of_eq_name(), {lvl}), A, a, b, H});
+    }
+
     expr mk_congr_arg(expr const & f, expr const & H) {
         // TODO(Leo): efficient version
         return mk_app(get_congr_arg_name(), {f, H});
@@ -714,6 +775,10 @@ expr app_builder::mk_iff(expr const & lhs, expr const & rhs) {
     return m_ptr->mk_iff(lhs, rhs);
 }
 
+expr app_builder::mk_heq(expr const & lhs, expr const & rhs) {
+    return m_ptr->mk_heq(lhs, rhs);
+}
+
 expr app_builder::mk_refl(name const & relname, expr const & a) {
     return m_ptr->mk_refl(relname, a);
 }
@@ -738,6 +803,10 @@ expr app_builder::mk_iff_symm(expr const & H) {
     return m_ptr->mk_iff_symm(H);
 }
 
+expr app_builder::mk_heq_symm(expr const & H) {
+    return m_ptr->mk_heq_symm(H);
+}
+
 expr app_builder::mk_trans(name const & relname, expr const & H1, expr const & H2) {
     return m_ptr->mk_trans(relname, H1, H2);
 }
@@ -750,6 +819,10 @@ expr app_builder::mk_iff_trans(expr const & H1, expr const & H2) {
     return m_ptr->mk_iff_trans(H1, H2);
 }
 
+expr app_builder::mk_heq_trans(expr const & H1, expr const & H2) {
+    return m_ptr->mk_heq_trans(H1, H2);
+}
+
 expr app_builder::mk_eq_rec(expr const & C, expr const & H1, expr const & H2) {
     return m_ptr->mk_eq_rec(C, H1, H2);
 }
@@ -774,6 +847,14 @@ expr app_builder::lift_from_eq(name const & R, expr const & H) {
     return m_ptr->lift_from_eq(R, H);
 }
 
+expr app_builder::mk_eq_of_heq(expr const & H) {
+    return m_ptr->mk_eq_of_heq(H);
+}
+
+expr app_builder::mk_heq_of_eq(expr const & H) {
+    return m_ptr->mk_heq_of_eq(H);
+}
+
 expr app_builder::mk_iff_false_intro(expr const & H) {
     return m_ptr->mk_iff_false_intro(H);
 }
diff --git a/src/library/app_builder.h b/src/library/app_builder.h
index 95d1909c1e..16aeab2486 100644
--- a/src/library/app_builder.h
+++ b/src/library/app_builder.h
@@ -94,6 +94,7 @@ public:
     expr mk_rel(name const & n, expr const & lhs, expr const & rhs);
     expr mk_eq(expr const & lhs, expr const & rhs);
     expr mk_iff(expr const & lhs, expr const & rhs);
+    expr mk_heq(expr const & lhs, expr const & rhs);
 
     /** \brief Similar a reflexivity proof for the given relation */
     expr mk_refl(name const & relname, expr const & a);
@@ -104,11 +105,13 @@ public:
     expr mk_symm(name const & relname, expr const & H);
     expr mk_eq_symm(expr const & H);
     expr mk_iff_symm(expr const & H);
+    expr mk_heq_symm(expr const & H);
 
     /** \brief Similar a transitivity proof for the given relation */
     expr mk_trans(name const & relname, expr const & H1, expr const & H2);
     expr mk_eq_trans(expr const & H1, expr const & H2);
     expr mk_iff_trans(expr const & H1, expr const & H2);
+    expr mk_heq_trans(expr const & H1, expr const & H2);
 
     /** \brief Create a (non-dependent) eq.rec application.
         C is the motive. The expected types for C, H1 and H2 are
@@ -132,6 +135,9 @@ public:
         because eq.rec is a dependent eliminator in HoTT. */
     expr mk_eq_drec(expr const & C, expr const & H1, expr const & H2);
 
+    expr mk_eq_of_heq(expr const & H);
+    expr mk_heq_of_eq(expr const & H);
+
     expr mk_congr_arg(expr const & f, expr const & H);
     expr mk_congr_fun(expr const & H, expr const & a);
     expr mk_congr(expr const & H1, expr const & H2);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 82eecda785..4424e76077 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -660,13 +660,22 @@ bool is_eq(expr const & e) {
 }
 
 bool is_eq(expr const & e, expr & lhs, expr & rhs) {
-    if (!is_eq(e) || !is_app(app_fn(e)))
+    if (!is_eq(e) || get_app_num_args(e) != 3)
         return false;
     lhs = app_arg(app_fn(e));
     rhs = app_arg(e);
     return true;
 }
 
+bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs) {
+    if (!is_eq(e) || get_app_num_args(e) != 3)
+        return false;
+    A   = app_arg(app_fn(app_fn(e)));
+    lhs = app_arg(app_fn(e));
+    rhs = app_arg(e);
+    return true;
+}
+
 bool is_eq_a_a(expr const & e) {
     if (!is_eq(e))
         return false;
diff --git a/src/library/util.h b/src/library/util.h
index 2b6a1467ee..8bd0944766 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -179,6 +179,7 @@ bool is_eq_drec(environment const & env, expr const & e);
 
 bool is_eq(expr const & e);
 bool is_eq(expr const & e, expr & lhs, expr & rhs);
+bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
 /** \brief Return true iff \c e is of the form (eq A a a) */
 bool is_eq_a_a(expr const & e);
 /** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */