=Paper=
{{Paper
|id=Vol-2307/WiP2
|storemode=property
|title=Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper)
|pdfUrl=https://ceur-ws.org/Vol-2307/WiP2.pdf
|volume=Vol-2307
|authors=Alberto Fiori,Claudio Sacerdoti Coen
|dblpUrl=https://dblp.org/rec/conf/mkm/FioriC18
}}
==Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper)==
<pdf width="1500px">https://ceur-ws.org/Vol-2307/WiP2.pdf</pdf>
<pre>
   Towards an Implementation in LambdaProlog of the Two Level
                    Minimalist Foundation

                                     Alberto Fiori                                Claudio Sacerdoti Coen
                              alberto.fiori92@gmail.com                           University of Bologna
                                                                                   sacerdot@cs.unibo.it




                                                                   Abstract
                           In this work we will present an implementation of the Minimalist Foundation
                           [MS05; Mai09] using the 𝜆Prolog [NM88] implementation ELPI [Dun+15].
                           The Minimalist Foundation is a two level constructive type theory with both
                           an extensional level with quotients and sets and an intensional level satisfy-
                           ing the proof-as-programs interpretation. Linking the two level there is an
                           interpretation of the extensional level in a dependent setoid model build upon
                           the intensional level where extensionality is modeled by intensional proposi-
                           tions. In our work we have implemented type checkers for both levels and the
                           translation for a significant subset of well-typed extensional terms and types
                           to well-typed intensional terms and types. Future works include: formal ver-
                           ification in Abella for our implementation, code extraction at the intensional
                           level and finally a proof assistant at the extensional level (using the constraint
                           programming functionality offered by ELPI).




Copyright © by the paper’s authors. Copying permitted for private and academic purposes.
In: O. Hasan, F. Rabe (eds.): Proceedings of the CICM 2018, Hagenberg, Austria, 13-08-2018, published at http://ceur-ws.org
Introduction
In 2005 M. Maietti and G. Sambin [MS05] argued about the necessity of building a foundation for constructive mathematics
to be taken as a common core among relevant existing foundations in axiomatic set theory, such as Aczel-Myhill’s CZF
and Mizar’s Tarski-Grothendieck set theory, or in category theory, such as the internal theory of a topos, or in type theory,
such as Martin-Löf’s type theory and Coquand’s Calculus of Inductive Constructions. Moreover, they asked the foundation
to satisfy the “proofs-as-programs” paradigm, namely the existence of a realizability model where to extract programs
from proofs. Finally, the authors wanted the theory to be appealing to standard mathematicians and therefore they wanted
extensionality in the theory, e.g. to reason with quotient types and to avoid the intricacies of dependent types in intensional
theories.
   In the same paper they noticed that theories satisfying extensional properties, like extensionality of functions, cannot
satisfy the proofs-as-programs requirement. Therefore they concluded that in a proofs-as-programs theory one can only
represent extensional concepts by modelling them via intensional ones in a suitable way, as already partially shown in some
categorical contexts.
   Finally, they ended up proposing a constructive foundation for mathematics equipped with two levels: an intensional
level that acts as a programming language and is the actual proofs-as-programs theory, and an extensional level that acts as
the set theory where to formalize mathematical proofs. Then, the constructivity of the whole foundation relies on the fact
that the extensional level must be implemented over the intensional level, but not only this. Indeed, following Sambin’s
forget-restore principle, they also required that extensional concepts must be abstractions of intensional ones as result of
forgetting irrelevant computational information. Such information is then restored when extensional concepts are translated
back at the intensional level.
   In 2009 M. Maietti [Mai09] presented the syntax and judgements of the two levels, together with a proof that a suit-
able completion of the intentional level provides a model of the extensional one. The proof is constructive and based on
a sequence of categorical constructions, the most important being the construction of a quotient model within the inten-
sional level, where setoids are used to encode extensional equality in an intensional language, and a notion of canonical
isomorphism between intensional dependent setoids.
   In this work we will present an implementation of the following software components:

    1. a type checker for the intensional level

    2. a reformulation of the extensional level that allows to store sintactically proof objects that are later used to provide the
       information to be restored when going from the extensional to the intensional level so to avoid general proof search
       during the interpretation

    3. a type checker for the obtained extensional level

    4. a translator from well-typed extensional terms and types to well-typed intensional terms and types

     As a future extension we hope to implement also other software components:

    1. a formal validation (in Abella) of our reformulation of the extensional level and of the correctness of the implementation

    2. code extraction at the intensional level (in Haskell/Lisp)

    3. a proof assistant at the extensional level (using the constraint programming functionality offered by ELPI)

Combining the translator with a proof extraction component it will be possible to extract programs from proofs written in
the extensional level.
   We have chosen 𝜆Prolog [NM88] (and in particular its recent implementation ELPI [Dun+15]) as the programming
language to write the two type checkers and the interpreter. The benefits are that 𝜆Prolog takes care of the intricacies of
dealing with binders and alpha-conversion and moreover a 𝜆Prolog implementation of a syntax-directed judgement is just
made of simple clauses that are almost literal translations of the judgemental rules. This allows humans (and logicians in
particular) to easily inspect the code to spot possible errors.

1     Higher Order Logic Programming
At the beginning of our work it was decided that the this project should be implemented using 𝜆Prolog and ELPI, one of
its implementations which allows for more flexibility (e.g. optional type declarations) more functionality (e.g. constraint
programming, which will be useful in later phases of the project) and also improved performances compared to other major
implementations of 𝜆Prolog.
   As a programming language 𝜆Prolog is naturally a good fit for a binder-heavy project like ours as it natively offer all
the functionality required to handle 𝛼-equivalence, capture avoiding substitutions and higher-order unification; moreover
the high level abstractions and backtracking allow for almost a 1-1 encoding of inference rules. As an example below we
can see the comparison between a natural deduction inference rule and a 𝜆Prolog clause in the case of Π-Introduction. In
natural deduction style we have the following inference rule
                                                𝐶(𝑥) 𝑠𝑒𝑡 [𝑥 ∈ 𝐵]       𝐵 𝑠𝑒𝑡
                                                                               Π-F
                                                       Π𝑥∈𝐵 𝐶(𝑥) 𝑠𝑒𝑡
while in 𝜆Prolog we would write
ofType (setPi B C) KIND3 IE
    :- ofType B KIND1 IE
    , (pi x\ locDecl x B
        => ofType (C x) KIND2 IE)
    , pts_fun KIND1 KIND2 KIND3
    .
where ofType represent the 𝑠𝑒𝑡 judgement, locDecl is used to locally introduce hypothesis in the context and pts_fun is
used to decide whether the produced type is a set or a collection.
   While the 𝜆Prolog version is more verbose it should be noted that this one rule encode the Π-Formation rule for both the
extensional and the intensional level and also for all combination of arguments kinds between sets, collections, propositions
and small proposition.

1.1     Changes to the calculus
As pointed out in the introduction before we could begin the implementation we had to apply some changes to the calculi
exposed in [Mai09].

1.1.1    Syntax Directed Rules
Between the rules of mTT and emTT there is a rule which states that equal type have the same elements, that is:
                                                     𝑎∈𝐴 𝐴=𝐵
                                                             conv
                                                       𝑎∈𝐵
   This rule is problematic from an implementation point of view since it can be triggered at any moment and (at the
extensional level) would start a proof search trying to prove 𝐴 = 𝐵 for a unknown 𝐴. A simple solution is to preemptively
compose this rule to all other rule that might need it; for example we can see that the elimination rule for dependents
products changes from
                                                𝑓 ∈ Π𝑥∈𝐵 𝐶(𝑥)      𝑡∈𝐵
                                                                         Π-E
                                                   𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝑡) ∈ 𝐶(𝑡)
to
                                         𝑓 ∈ Π𝑥∈𝐵 𝐶(𝑥)        𝑡 ∈ 𝐵′   𝐵 = 𝐵′
                                                                              Π-E
                                                   𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝑡) ∈ 𝐶(𝑡)
the main difference being that in the syntax directed version we check that the domain type of 𝑓 and the inferred type of
𝑡 are convertible instead of requiring syntactic equality like in the original rule. In this way the power of the calculus is
surely not increased as the syntax directed rule is admissible in the calculus with the two previous rules, indeed

                                                             𝑡 ∈ 𝐵′  𝐵 = 𝐵′
                                                                            conv
                                          𝑓 ∈ Π𝑥∈𝐵 𝐶(𝑥)            𝑡∈𝐵
                                                                       Π-E
                                               𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝑡) ∈ 𝐶(𝑡)
is a derivation of the same judgement from the same hypothesis.
    For this change to be effective we also need to reformulate the conversion rules given by the calculi (e.g. 𝖺𝗉𝗉𝗅𝗒(𝜆𝐵 𝑥.𝑓 , 𝑡) =
𝑓 {𝑡∕𝑥}) in directed rules describing a reduction predicate ⊳ (e.g. 𝖺𝗉𝗉𝗅𝗒(𝜆𝐵 𝑥.𝑓 , 𝑡) ⊳ 𝑓 {𝑡∕𝑥}) from which we will define
equality as reducibility to a common term, which is equivalent to the original equality given that both calculi of the Min-
imalist Foundation have both the property of Church-Rosser confluence and strong normalization. This new relation will
be implemented by the predicate conv.
   The full modifications to the calculi in our implementation with respect to making the rule syntax directed are mostly
about checking for convertibility/equality where mTT/emTT require syntactical equality. We plan to provide a full proof of
the validity of this modification, and also of the followings, in Abella in the future.

1.1.2   Informative Proof-terms at the Extensional Level and
        Extensional Equality
                        𝑏∈𝐵        𝗍𝗋𝗎𝖾 ∈ 𝐶(𝑏)     𝐶(𝑥) 𝑝𝑟𝑜𝑝 [𝑥 ∈ 𝐵]          𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐴, 𝑎, 𝑏)
                                                                        ∃-I                        Eq-E
                                       𝗍𝗋𝗎𝖾 ∈ ∃𝑥∈𝐵 𝐶(𝑥)                           𝑎=𝑏∈𝐴
In the calculus emTT a token proof term 𝗍𝗋𝗎𝖾 is used to represent all proofs of propositions and small propositions; this poses
problems during the interpretation when we need to construct intensional proof terms given only the token 𝗍𝗋𝗎𝖾. Moreover
the strong elimination rule for the propositional extensional equality turns every conversion in an undecidable problem of
general proof search for 𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐴, 𝑎, 𝑏). To reasonably implement the extensional calculus and the interpretation we
need a way to construct intensional proofs from extensional proof and a way to contain the undecidability of the strong
elimination rule for the extensional propositional equality.
    A first approach to the problem could have been to have both the extensional type checker and the interpretation work
on full derivations; this is the method chosen by Maietti in [Mai09] and would solve the problems regarding the missing
informations in the extensional calculus and language, but was discarded as a solution because from an implementation
standpoint the code to encode a derivation would be almost a copy of the code needed to encode terms, yet with subtle, but
non trivial, differences.
    The chosen solution was to both add informative proof terms to the extensional level and weaken the elimination rule of
the propositional extensional equality. The first part of the solution makes the extensional rule for proposition more similar
to the intensional ones
                                       𝑏∈𝐵        𝑝 ∈ 𝐶(𝑏) 𝐶(𝑥) 𝑝𝑟𝑜𝑝 [𝑥 ∈ 𝐵]
                                                                                    ∃-I
                                                  < 𝑏,∃ 𝑝 >∈ ∃𝑥∈𝐵 𝐶(𝑥)
so that during the interpretation more informations are available.
   The second part modifies the extensional propositional equality elimination rule to a weaker but equivalent form; the
rule
                                                  𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐴, 𝑎, 𝑏)
                                                                     Eq-E
                                                      𝑎=𝑏∈𝐴
becomes
                                                                         Eq-E
                                             𝑎 = 𝑏 ∈ 𝐴 [𝗁 ∈ 𝖤𝗊(𝐴, 𝑎, 𝑏)]
This weaker form has nicer computational properties, the most important one being that it is always deterministic and
terminating to check if it is possible to apply given a specific context while still allowing to locally definitions in a context
via implication or dependents types.
    This solution can be seen as an extension of simply encoding proofs in 𝜆-terms; we have already noted that at the exten-
sional level there are not satisfying such encoding because of the propositional equality elimination rule, whose appearances
in the 𝜆-terms would be confusing at the extensional level. From this point of view our solution can be thought of as real-
izing that adding the needed equalities to the context is enough, and that the locally scoped nature of the context provide
exactly the functionality we need to use equalities. Compared to using whole derivation trees we now use 𝜆-terms plus
some context.
    A drawback of this solution is that it is complex to use even simple lemmas; to this problem we offer two solutions: to
manually use the cut elimination of the calculus or to introduce a new let in construct

                                                     𝗅𝖾𝗍 𝑥 ∶= 𝑡1 ∈ 𝑇 𝗂𝗇 𝑡2

used to introduce locally typed definitions.
    As of this writing this let in in not yet implemented as there many different ways the needed functionality can be obtained
each with different compromises and it is not entirely clear which implementation method is the most adeguate to our project.
In our simple cases it is acceptable to manually perform the cut elimination to locally include the desired lemma so we plan
to implement a proper let in once there is a strong need for it.
1.1.3 𝜉-Rule
Another difference between the calculus in Maietti’s work and ours is that our model validates the 𝜉-rule at the intensional
level, removing it would require a refactoring of the conversion to include a list of forbidden variables that block conversion.
Until this moment it was not a priority to implement this functionality, but still we have some feasible implementation paths.

2     The Interpretation
One of the main result of [Mai09] is a categorical proof of the validity of an interpretation of an extensional type theory
into an intensional one.
   In particular first a quotient model Q(mTT) is built on the theory mTT, this model is given as a category where objects
are pairs of (𝐴, =𝐴 ) (abbreviated to 𝐴= when =𝐴 it is clear from the context) where A is an intensional type called support
and
                                              𝑥 =𝐴 𝑦 𝑝𝑟𝑜𝑝𝑠 [𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴]
is an equivalence relation on 𝐴; which means that there are terms 𝗋𝖿 𝗅𝐴 , 𝗌𝗒𝗆𝗆𝐴 and 𝗍𝗋𝖺𝐴 such that the following judgements
hold in mTT

                                          𝗋𝖿 𝗅𝐴 (𝑥) ∈ 𝑥 =𝐴 𝑥 [𝑥 ∈ 𝐴]
                                𝗌𝗒𝗆𝐴 (𝑥, 𝑦, 𝑢) ∈ 𝑦 =𝐴 𝑥 [𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴, 𝑢 ∈ 𝑥 =𝐴 𝑦]
                            𝗍𝗋𝖺𝐴 (𝑥, 𝑦, 𝑧, 𝑢, 𝑣) ∈ 𝑥 =𝐴 𝑧 [𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴, 𝑧 ∈ 𝐴, 𝑢 ∈ 𝑥 =𝐴 𝑦, 𝑣 ∈ 𝑦 =𝐴 𝑧]

In the following we will refers to the objects of Q(mTT) as setoids.
   The morphisms of Q(mTT) from (𝐴, =𝐴 ) to (𝐵, =𝐵 ) are all the well-typed terms of mTT

                                                                   𝑓 (𝑥) ∈ 𝐵(𝑥) [𝑥 ∈ 𝐴]

that preserve the setoid equality, that is there exist a proof-term

                                          𝗉𝗋𝟣 (𝑥, 𝑦, 𝑧) ∈ 𝑓 (𝑥) =𝐵 𝑓 (𝑦) [𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴, 𝑧 ∈ 𝑥 =𝐴 𝑦]

Equality between two morphisms f,g : (𝐴, =𝐴 ) → (𝐵, =𝐵 ) holds if they maps equal elements of 𝐴= to equal elements of
𝐵= , that is if there is a proof-term
                                          𝗉𝗋𝟤 (𝑥) ∈ 𝑓 (𝑥) =𝐵 𝑔(𝑥) [𝑥 ∈ 𝐴]
    Starting from the category Q(mTT) we can define also dependent setoids, given a setoid 𝐴= we say that

                                                                       𝐵= (𝑥) [𝑥 ∈ 𝐴= ]

is a dependent setoid if its support is a dependent type 𝐵(𝑥) 𝑡𝑦𝑝𝑒 [𝑥 ∈ 𝐴𝑠], if its relation is a dependent proposition

                                                    𝑦 =𝐵(𝑥) 𝑦′ [𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵(𝑥), 𝑦′ ∈ 𝐵(𝑥)]

and if there is a substitution morphism
                                      𝑥
                                    𝜎𝑥12 (𝑑, 𝑦) ∈ 𝐵(𝑥2 ) [𝑥1 ∈ 𝐴, 𝑥2 ∈ 𝐴, 𝑑 ∈ 𝑥1 =𝐴 𝑥2 , 𝑦 ∈ 𝐵(𝑥1 )]

that satisfies the properties given by definition 4.9 in [Mai09], that is it needs to preserve the equality of 𝐵= , to be proof-
                                                                                                                         𝑥
irrelevant by not depending on the particular choice of the proof-term 𝑑 ∈ 𝑥1 = 𝑥2 (so that we can write 𝜎𝑥12 (𝑦) in place of
  𝑥                                                                      𝑥
𝜎𝑥12 (𝑑, 𝑦)), there need to always exists the identity substitution 1 𝜎𝑥11 (𝗋𝖿 𝗅𝐵(𝑥1 ) (𝑥1 ), –) and lastly substitution morphisms need
to be composable, that is we require
                                                      𝑥     𝑥                 𝑥
                                                     𝜎𝑥23 (𝜎𝑥12 (𝑦)) =𝐵(𝑥3 ) 𝜎𝑥13 (𝑦)
    1 Which in general does not need to be the identity morphism, for example


                                     𝜎𝑥𝑥 (𝗋𝖿 𝗅𝐴 (𝑥), 𝑤) ≡ 𝖾𝗅𝗂𝗆+ (𝑤, (𝑧).𝗂𝗇𝗅(𝜎𝑥𝑥 (𝗋𝖿 𝗅𝐴 (𝑥)(𝑥), 𝑧)), (𝑧).𝗂𝗇𝗋(𝜎𝑥𝑥 (𝗋𝖿 𝗅𝐴 (𝑥)(𝑥), 𝑧)))

if 𝑤 ∈ 𝐵 + 𝐶 [𝑥 ∈ 𝐴].
in the appropriate context2 .
    Over these substitution we can define canonical isomorphism between two type 𝐵1 and 𝐵2 as the only 𝜎 between them.
In our code we have implemented these isomorphisms as with the predicate tau B B’ P.
    The reason these construction are needed is because the strong elimination rule of the extensional propositional equality
can derive a judgemental equality from just an hypothetical assumption. For an example we can see that a judgement like
𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐶, 𝑐, 𝑑) [𝑐 ∈ 𝐶, 𝑑 ∈ 𝐶] is a well formed but not derivable judgement in emTT, but if we add one more assumption
to the context we obtain
                              𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐶 + 𝐶, 𝗂𝗇𝗅(𝑐), 𝗂𝗇𝗅(𝑑)) [𝑐 ∈ 𝐶, 𝑑 ∈ 𝐶, ℎ ∈ 𝖤𝗊(𝐶, 𝑐, 𝑑)]
which is derivable since we can use the rules 𝗉𝗋𝗈𝗉 − 𝗍𝗋𝗎𝖾 and E-Eq to derive the judgement 𝑐 = 𝑑 ∈ 𝐶 from the given
context.
   This can be seen also in the fact that this judgement

    ∀𝑥∈1 ∀𝑓 ∈Π(𝖤𝗊(1,𝑥,⋆),1) 𝖤𝗊(1, ⋆, 𝑥) ⇒
                                                                                     𝖤𝗊(1, 𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝖾𝗊(1, ⋆)), 𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝖾𝗊(1, ⋆))) 𝑝𝑟𝑜𝑝𝑠3
is derivable in the empty context even if there is a mismatch between the types of 𝑓 and 𝖾𝗊(1, ⋆). Here for example we
would want to apply a canonical isomorphism to ⟦𝖾𝗊(1, ⋆)⟧4 so that its type match with the domain of ⟦𝑓 ⟧; after the
                                  ⟦𝖤𝗊(1,𝑥,⋆)⟧
correction we obtain 𝖺𝗉𝗉𝗅𝗒(𝑓 , 𝜏⟦𝖤𝗊(1,⋆,⋆)⟧ (⟦𝖾𝗊(1, ⋆)⟧)) which is well-typed in mTT
   From this introduction to the structure of the interpretation we can see that the method used to force the semantics of
emTT on mTT (via Q(mTT)) is to require the creation of suitable proof terms thus restricting the available language to a
subset that preserve the extensional semantic.
   We can see another more explicit application of this method in the interpretation of dependent products, indeed in this
case a function term of emTT is interpreted as a pair whose first projection is an intensional function and whose second
projection is a proof that the first projection preserves the setoid equalities of Q(mTT).
   From the point of view of the implementation this means that we have to produce various proof for each of the type
constructor we wish to include in our implementation.
   As of now we have implemented all that is needed to fully interpret the subset of emTT comprised of singletons, depen-
dent products, implications, universal quantifications, propositional equality. We believe that this subset exhibits enough
of the complexity of the interpretation and feel confident that the structure of our implementation will be able to cover also
the needs of the remaining constructors.

3     The Code
All the code was written in 𝜆Prolog (in particular it was written for the ELPI implementation [Dun+15] of 𝜆Prolog) and
make extensive use of many high level features that in other languages would not be available. Still our code does not use
many of the more advanced features offered by ELPI like constraint programming which we plan to use in the next phase
of the project when we will start to implement a kernel for the planned proof checker
   In this section we will show some extract of the code and explain how we obtained the desired functionalities.

3.1    Project Structure and Extensibility
We have divided the code 4 categories main, calc, test, debug. The first, main holds type declaration for the other
modules and define the general functionality of the theory shared by all type constructor of both levels. the second is a
folder containing a .elpi file for each type constructor; in each of these files we implement the typing and conversion
rules for that particular type constructor. For example in calc/setPi.elpi we keep all definitions related to dependent
products, like the implementation of Π-I or the interpretation of a function term.
of (lambda B F) (setPi B C) IE
    :- ofType B _ IE
    , (pi x\ locDecl x B => isa (F x) (C x) IE)
    .
   2 It is worth noting that in the Minimalist Foundation the only type that directly takes terms as arguments are the propositional equalities (written 𝖤𝗊

and 𝖨𝖽 in emTT and mTT respectively). For any 𝐵(𝑥) 𝑡𝑦𝑝𝑒 [𝑥 ∈ 𝐴] the only possible occurrences of 𝑥 are as an argument of 𝖤𝗊 (resp. 𝖨𝖽 if in mTT),
together with the absence of strong elimination of terms towards types this means that conversion of types is always only reduced to conversion of terms
and that types containing no propositions cannot be truly dependent. For example the canonical way to construct a type list of type 𝐶 of length 𝑛 is via a
dependent sum Σ(𝖫𝗂𝗌𝗍(𝐶), (𝑙).𝑃 (𝑙, 𝑛)) where 𝑃 (𝑙, 𝑛) is the proposition length of 𝑙 equals 𝑛.
   4 In this work we use the double bracket notation for the interpretation instead of the λI used in [Mai09].
interp (lambda B F) R
    :- spy(of (lambda B F) (setPi B C) ext)
    , spy(interp (setPi B C) (setSigma (setPi Bi Ci) H ))
    , macro_interp B ( x\_\_\xi\_\_\ interp (F x) (Fi xi))
    , setoid_eq B EquB
    , macro_interp B (x1\x2\h\x1i\x2i\hi\tau_proof_eq
        (F x1)
        (F x2)
        (C x2)
        (K_EQU x1i x2i hi))
    , R = pair (setPi Bi Ci) (H) (lambda Bi Fi)
        (forall_lam Bi x1\
         forall_lam Bi x2\
             forall_lam (EquB x1 x2) h\ K_EQU x1 x2 h)
    .

   The last two, test and debug, hold utilities to quickly test the predicates from main and calc in addition to useful
predicates needed to inspect the runtime behaviour of the type checking and of the interpretation.

3.2     Explanation of the Predicates
We can divide the predicate defined in our implementation in three groups: judgement predicates, conversion predicates
and interpretation predicates.

3.2.1 of, isa, ofType, isaType and locDecl
In the first group are the predicate corresponding to the judgements 𝐴 𝑡𝑦𝑝𝑒 [Γ] or 𝑎 ∈ 𝐴 [Γ]. We use the
of Term Type Level predicate to represent the judgement 𝑇 𝑒𝑟𝑚 ∈ 𝑇 𝑦𝑝𝑒 [Γ] at the level indicated by the third argu-
ment, we also define another predicate isa Term Type Level to check if the inferred type of Term is convertible with
Type at level Level; a major difference between these two predicate is that for of the first and last argument are inputs
and the middle is an output, while for isa all three arguments are inputs. Similarly ofType Type Kind Level and
isaType Type Kind Level implement the corresponding functionality at the type level.
   locDecl is used to form the context where of will look up the types of variables via the clause
of X Y _ :- locDecl X Y.. We have no need to have a parameter to indicate the level for locDecl because exten-
sional and intensional variables are disjoint and we can assume that we will never try to compute the extensional type of
an intensional variable. Moreover as of now our implementation validates the 𝜉-rule at the intensional level so that also the
conversion can be level agnostic.

3.2.2    pts_* Predicates
In the Minimalist Foundation in general the kind of a type is not unique but admit a most general unifier, this unifier will
be the intended output of ofType and the logic to find it is implemented in the various PTS predicates. As an example a
dependent product Π(𝐵, 𝐶) is never a proposition and is a set if both 𝐴 𝑠𝑒𝑡 and 𝐵(𝑥) 𝑠𝑒𝑡 [𝑥 ∈ 𝐴] hold.
   This can be expressed with the following code:

pts_leq A A.
pts_leq set col.
pts_leq props set.
pts_leq propc col.
pts_leq props propc.
pts_leq props col.

pts_fun A B set :- pts_leq A set, pts_leq B set, !.
pts_fun _ _ col.

Other variations allow to decide the most general kind of universal/existential quantifiers, connectives or lists.
3.2.3 conv, dconv, hnf and hstep
While conversion at the intensional level is almost straightforward at the extensional level we need to be more careful as a
naive implementation would be extremely inefficient due to the rule Eq-E

                                                𝗍𝗋𝗎𝖾 ∈ 𝖤𝗊(𝐶, 𝑐, 𝑑) [𝑐 ∈ 𝐶, 𝑑 ∈ 𝐶]
                                                             𝑐=𝑑∈𝐶
   The solution we have chose to implement consist of two step, first we weaken the Eq-E rule to perform a context lookup
instead of trying to prove a judgement and then we divide the conversion in three different operations.

conv A A :- !.
conv A B :- locDecl _ (propEq _ A B).
conv A B :- (hnf A A’), (hnf B B’), (dconv A’ B’).

   The predicate that will actually implement the conversion judgement will be conv, for this predicate both arguments will
be inputs. When called between two terms the predicate will first check if the two terms are unifiable at the meta-level, if
this fail then it will search for a context declaration that states the equality it wants; if this also fail then if will reduces both
term to head normal form and apply a dconv step on the head normal forms. dconv role is to propagate the conversion to
subterms; it assumes to receive two terms in head normal form (as it will only ever be called on output of hnf) and and will
check for conversion on the corresponding subterms of its arguments.

dconv (setSigma B C) (setSigma B’ C’)
    :- (conv B B’)
    , (pi x\ locDecl x B => conv (C x) (C’ x))
    .
dconv (pair B C BB CC) (pair B’ C’ BB’ CC’)
    :- (conv B B’)
    , (pi x\ locDecl x B => conv (C x) (C’ x))
    , (conv BB BB)
    , (conv CC CC’)
    .
dconv (elim_setSigma Pair M MM) (elim_setSigma Pair’ M’ MM’)
    :- (conv Pair Pair’)
    , (of Pair (setSigma B C))
    , (pi z\ locDecl z (setSigma B C) => conv (M z) (M’ z))
    , (pi x\ pi y\ locDecl x B
        => locDecl y (C x)
        => conv (MM x y) (MM’ x y))
    .

In general it will be needed to declare a dconv clause for each new non-constant constructor (constant constructors are
all handled by a dconv A A :- !. clause) the main reason to use dconv is that is does not trigger the context lookup
associated with the Eq-E rule.

3.2.4 tau, setoid_*, proof_eq and interp
The main entry point of the interpretation is the predicate interpr, for example the typical structure of our test is

  1. Construct a suitable extensional type

  2. Typecheck the type at the extensional level

  3. Interpret the type to the instensional level

  4. Typecheck this last result.

During the interpretation many other auxiliary predicates are needed. Here we will give a description of the most important
ones.
   As explained above during the interpretation we need to correct the types of interpreted terms to compensate for the
different rules at the two levels; in our code we have chosen to implement this functionality with the predicate tau T1 T2 P.
tau takes in input 2 mutually convertible extensional types and return a 𝜆Prolog function which convert elements of type
T1 to elements of type T2. It is important to note that P is a pure 𝜆-function at the meta-level and thus in the conversion
between the two types T1 and T2 we can not use backtracking or patter matching; thankfully a pure function is all we need
because canonical isomorphism only apply 𝜂-expansions and do not actually inspect the term they are applied to, only its
type and that is completely know to tau. As an example we show how this type correction would look like for a disjoint
sum for a variable 𝑤 ∈ ⟦𝐵(𝑥) + 𝐶(𝑥)⟧ [⟦𝑥 ∈ 𝐴⟧] when transitioning to a type ⟦𝐵(𝑥′ ) + 𝐶(𝑥′ )⟧
                                          ′                            ′              ′
                                        𝜎𝑥𝑥 (𝑤) ≡ 𝖤𝗅𝗂𝗆+ (𝑤, (𝑦1 ).𝜎𝑥𝑥 (𝑦1 ), (𝑦2 ).𝜎𝑥𝑥 (𝑦2 ))

    We can see that we have applied structural recursion over the types even when computing a function over terms, this is
helpful when treating types with more than one canonical constructor and when dealing with variables, but in general it is
necessary since we cannot assume that all terms will have a canonical head normal form.
    It is important to note that all predicates working at the interpretation level will always assume to handle well formed
and well typed terms and types so that we do not need to fill our code with an enormous amount of runtime checks.
    A related predicate is tau_eq, which at the moment is conceptually the most complex predicate in the code and its aim
is to implement the second and third property of required of substitution morphisms: preserving equalities of Q(mTT). In
formulae this means that the following hypothetical judgment should be derivable for some choice of 𝑑2
          𝑥             𝑥
  𝑑2 ∈ 𝜎𝑥12 (𝑦) =𝐵(𝑥2 ) 𝜎𝑥12 (𝑦′ ) [𝑥1 ∈ 𝐴, 𝑥2 ∈ 𝐴, 𝑑1 ∈ 𝑥1 = 𝑥2 ,
                                                                                    𝑦 ∈ 𝐵(𝑥1 ), 𝑦 ∈ 𝐵(𝑥2 ), 𝑤 ∈ 𝑦 =𝐵(𝑥1 ) 𝑦′ ] (1)

tau_eq role is exactly to find a constructive and functional (after taking as inputs 𝐵(𝑥1 ) and 𝐵(𝑥2 )) transformation that
produces such 𝑑2 from 𝑦, 𝑦′ and 𝑑1 .
   This predicate becomes most useful during the interpretation of dependent products, since in Q(mTT) a dependent
function is represented as a pair containing a mTT function 𝑓 and a proof that 𝑓 preserve the extensionality of Q(mTT),
similarly to how it is done in [Nec97].
   Another problem is that in dealing with dependent products is that we need to automatically generate a proof that the
interpretations of emTT function will preserve the equalities of Q(mTT). The generation of these proofs is handled by the
predicate proof_eq.
   A family of related predicates is built around the setoids of Q(mTT), the principal one setoid_eq takes an exten-
sional type in input and return an mTT proposition representing the setoid equality of the interpretation of the given type,
three related predicates setoid_refl, setoid_symm and setoid_trans produce proofs that the proposition returned by
setoid_eq is indeed an equivalence relation.

References
[Dun+15]      Cvetan Dunchev et al. “ELPI: Fast, Embeddable,∖lambda Prolog Interpreter”. In: Logic for Programming,
              Artificial Intelligence, and Reasoning. Springer. 2015, pp. 460–468.
[Mai09]       Maria Emilia Maietti. “A minimalist two-level foundation for constructive mathematics”. In: Annals of Pure
              and Applied Logic 160.3 (2009), pp. 319–354.
[MS05]        Maria Emilia Maietti and Giovanni Sambin. “Toward a minimalist foundation for constructive mathematics”.
              In: From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics 48
              (2005), pp. 91–114.
[Nec97]       George C Necula. “Proof-carrying code”. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on
              Principles of programming languages. ACM. 1997, pp. 106–119.
[NM88]        Gopalan Nadathur and Dale Miller. “An overview of Lambda-PROLOG”. In: (1988).

</pre>