diff --git a/tests/lua/hott1.lua b/tests/lua/hott1.lua
new file mode 100644
index 000000000..c024e1e35
--- /dev/null
+++ b/tests/lua/hott1.lua
@@ -0,0 +1,44 @@
+-- Create a HoTT compatible environment.
+-- That is,
+--    Type.{0} is predicative
+--    No proof irrelevance for Type.{0}
+--    Proof irrelevance for Id types
+local env = empty_environment({prop_proof_irrel=false, impredicative=false, cls_proof_irrel={"Id"}})
+assert(not env:prop_proof_irrel())
+assert(not env:impredicative())
+assert(env:cls_proof_irrel():head() == name("Id"))
+assert(env:cls_proof_irrel():tail():is_nil())
+local l   = mk_param_univ("l")
+local U_l = mk_sort(l)
+local A   = Const("A")
+env = add_decl(env, mk_var_decl("Id", {l}, Pi(A, U_l, mk_arrow(A, A, U_l))))
+local Set = mk_sort(mk_level_zero())
+env = add_decl(env, mk_var_decl("N", Set))
+local N   = Const("N")
+env = add_decl(env, mk_var_decl("a", N))
+env = add_decl(env, mk_var_decl("b", N))
+local a   = Const("a")
+local b   = Const("b")
+local Id_z = Const("Id", {mk_level_zero()})
+env = add_decl(env, mk_axiom("H1", Id_z(N, a, b)))
+env = add_decl(env, mk_axiom("H2", Id_z(N, a, b)))
+local tc   = type_checker(env)
+-- H1 and H2 are definitionally equal since both have type Id.{0} N a b
+-- and Id is in env:cls_proof_irrel()
+assert(tc:is_def_eq(Const("H1"), Const("H2")))
+env = add_decl(env, mk_var_decl("Path", {l}, Pi(A, U_l, mk_arrow(A, A, U_l))))
+local Path_z = Const("Path", {mk_level_zero()})
+env = add_decl(env, mk_axiom("H3", Path_z(N, a, b)))
+env = add_decl(env, mk_axiom("H4", Path_z(N, a, b)))
+local tc   = type_checker(env)
+assert(tc:is_def_eq(Const("H1"), Const("H2")))
+assert(not tc:is_def_eq(Const("H3"), Const("H4")))
+assert(tc:is_def_eq(tc:check(Const("H3")), tc:check(Const("H4"))))
+print("H1 : " .. tostring(tc:check(Const("H1"))))
+print("H2 : " .. tostring(tc:check(Const("H2"))))
+print("H3 : " .. tostring(tc:check(Const("H3"))))
+print("H4 : " .. tostring(tc:check(Const("H4"))))
+print("N  : " .. tostring(get_formatter()(env, tc:check(Const("N")))))
+-- N : Type.{0}
+assert(not tc:is_def_eq(Const("a"), Const("b")))
+