diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 7898a04f80..cc5123ecef 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/options.h"
 #include "util/sexpr/format.h"
 #include "kernel/environment.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 #include "frontends/lean/token_table.h"
 
 namespace lean {
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 2d9362b72c..e611840a97 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
-for_each_fn.cpp replace_fn.cpp abstract.cpp
-instantiate.cpp local_ctx.cpp declaration.cpp environment.cpp
-type_checker.cpp init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-abstract_type_context.cpp inductive.cpp)
+for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
+local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
+init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
+inductive.cpp)
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 26de303b35..99512915ac 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -16,12 +16,11 @@ Author: Leonardo de Moura
 #include "kernel/local_ctx.h"
 #include "kernel/expr_maps.h"
 #include "kernel/equiv_manager.h"
-#include "kernel/abstract_type_context.h"
 
 namespace lean {
 /** \brief Lean Type Checker. It can also be used to infer types, check whether a
     type \c A is convertible to a type \c B, etc. */
-class type_checker : public abstract_type_context {
+class type_checker {
     /* In the type checker cache, we must take into account binder information.
        Examples:
        The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 25f6a4659d..fe781e8f23 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -16,4 +16,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   check.cpp parray.cpp process.cpp
   pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp
   context_cache.cpp scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp
-  derive_attribute.cpp)
+  derive_attribute.cpp abstract_type_context.cpp)
diff --git a/src/kernel/abstract_type_context.cpp b/src/library/abstract_type_context.cpp
similarity index 92%
rename from src/kernel/abstract_type_context.cpp
rename to src/library/abstract_type_context.cpp
index 59522a7bf1..de4b7d4367 100644
--- a/src/kernel/abstract_type_context.cpp
+++ b/src/library/abstract_type_context.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/fresh_name.h"
-#include "kernel/abstract_type_context.h"
 #include "kernel/abstract.h"
+#include "library/abstract_type_context.h"
 
 namespace lean {
 expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info bi) {
diff --git a/src/kernel/abstract_type_context.h b/src/library/abstract_type_context.h
similarity index 88%
rename from src/kernel/abstract_type_context.h
rename to src/library/abstract_type_context.h
index 3402de0a8b..42bbf288df 100644
--- a/src/kernel/abstract_type_context.h
+++ b/src/library/abstract_type_context.h
@@ -8,12 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-/** \brief This is a basic API for implementing macro definitions,
-    kernel extensions, formatters, etc.
-
-    \remark This class will eventually replace the class extension_context.
-
-    TODO(Leo): try to remove this class from Lean4. */
 class abstract_type_context {
 public:
     virtual ~abstract_type_context() {}
diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp
index 5aa4f08520..ea2b7efdc8 100644
--- a/src/library/annotation.cpp
+++ b/src/library/annotation.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <string>
 #include "runtime/sstream.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 #include "library/annotation.h"
 #include "library/pos_info_provider.h"
 
diff --git a/src/library/constructions/util.cpp b/src/library/constructions/util.cpp
index 44c3af7d6c..705958c0d6 100644
--- a/src/library/constructions/util.cpp
+++ b/src/library/constructions/util.cpp
@@ -5,10 +5,78 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/name_generator.h"
+#include "kernel/type_checker.h"
+#include "library/util.h"
+#include "library/constants.h"
 
 namespace lean {
 static name * g_constructions_fresh = nullptr;
 
+static level get_level(type_checker & ctx, expr const & A) {
+    expr S = ctx.whnf(ctx.infer(A));
+    if (!is_sort(S))
+        throw exception("invalid expression, sort expected");
+    return sort_level(S);
+}
+
+expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) {
+    return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
+}
+
+expr mk_and_elim_left(type_checker & ctx, expr const & H) {
+    expr a_and_b = ctx.whnf(ctx.infer(H));
+    return mk_app(mk_constant(get_and_elim_left_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
+}
+
+expr mk_and_elim_right(type_checker & ctx, expr const & H) {
+    expr a_and_b = ctx.whnf(ctx.infer(H));
+    return mk_app(mk_constant(get_and_elim_right_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
+}
+
+expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) {
+    level l1 = get_level(ctx, A);
+    level l2 = get_level(ctx, B);
+    return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
+}
+
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) {
+    expr A = ctx.infer(a);
+    expr B = ctx.infer(b);
+    level l1 = get_level(ctx, A);
+    level l2 = get_level(ctx, B);
+    return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
+}
+
+expr mk_pprod_fst(type_checker & ctx, expr const & p) {
+    expr AxB = ctx.whnf(ctx.infer(p));
+    expr const & A = app_arg(app_fn(AxB));
+    expr const & B = app_arg(AxB);
+    return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
+}
+
+expr mk_pprod_snd(type_checker & ctx, expr const & p) {
+    expr AxB = ctx.whnf(ctx.infer(p));
+    expr const & A = app_arg(app_fn(AxB));
+    expr const & B = app_arg(AxB);
+    return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
+}
+
+expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) {
+    return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
+}
+
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop) {
+    return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
+}
+
+expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop) {
+    return prop ? mk_and_elim_left(ctx, p) : mk_pprod_fst(ctx, p);
+}
+
+expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop) {
+    return prop ? mk_and_elim_right(ctx, p) : mk_pprod_snd(ctx, p);
+}
+
 name_generator mk_constructions_name_generator() {
     return name_generator(*g_constructions_fresh);
 }
diff --git a/src/library/constructions/util.h b/src/library/constructions/util.h
index 6391378439..fc57f56c9c 100644
--- a/src/library/constructions/util.h
+++ b/src/library/constructions/util.h
@@ -6,8 +6,14 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/name_generator.h"
+#include "kernel/type_checker.h"
 
 namespace lean {
+expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop);
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop);
+expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop);
+expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop);
+
 name_generator mk_constructions_name_generator();
 void initialize_constructions_util();
 void finalize_constructions_util();
diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h
index fa3355fb4e..6278c2ca64 100644
--- a/src/library/io_state_stream.h
+++ b/src/library/io_state_stream.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "kernel/environment.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 #include "library/exception.h"
 #include "library/io_state.h"
 #include "library/ext_exception.h"
diff --git a/src/library/sorry.h b/src/library/sorry.h
index 8919e84671..b39f71a26a 100644
--- a/src/library/sorry.h
+++ b/src/library/sorry.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 
 namespace lean {
 /** \brief Return true iff the given environment contains a sorry macro. */
diff --git a/src/library/string.h b/src/library/string.h
index 3fd94153b3..659f6ac156 100644
--- a/src/library/string.h
+++ b/src/library/string.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include "kernel/environment.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 
 namespace lean {
 /**
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index 44418b3975..2050f78e72 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sexpr/option_declarations.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "library/type_context.h"
 #include "library/io_state.h"
 #include "library/trace.h"
 #include "library/messages.h"
@@ -175,7 +175,7 @@ struct silent_ios_helper {
 };
 
 MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper);
-MK_THREAD_LOCAL_GET(type_checker, get_dummy_tc, get_dummy_env());
+MK_THREAD_LOCAL_GET(type_context_old, get_dummy_tc, get_dummy_env());
 
 scope_trace_silent::scope_trace_silent(bool flag) {
     m_old_value = g_silent;
diff --git a/src/library/type_context.h b/src/library/type_context.h
index a06416cf79..03d1942713 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "util/lbool.h"
 #include "util/fresh_name.h"
 #include "kernel/environment.h"
-#include "kernel/abstract_type_context.h"
+#include "library/abstract_type_context.h"
 #include "library/idx_metavar.h"
 #include "library/projection.h"
 #include "library/metavar_context.h"
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 65dc55dd90..baee222ae1 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -11,8 +11,8 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
-#include "kernel/abstract_type_context.h"
 #include "kernel/inductive.h"
+#include "library/abstract_type_context.h"
 #include "library/error_msgs.h"
 #include "library/locals.h"
 #include "library/util.h"