[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Jason,
Have you looked into the work of Abel and others (starting
with/Decidability of Conversion for Type Theory in Type Theory/ at POPL
2018, with various extensions since, all available on Github
<https://urldefense.com/v3/__https://github.com/mr-ohman/logrel-mltt__;!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACWct_mHU$ >)? They only have one universe
instead of a full hierarchy, and as far as I can tell only uniqueness of
types for neutral terms is proven (here
<https://urldefense.com/v3/__https://github.com/mr-ohman/logrel-mltt/blob/2f1bae017f74c2d8486ae980994a96191ea4b821/Definition/Typed/Consequences/NeTypeEq.agda*L30__;Iw!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACU8Rwb7M$ >),
but this might still be of interest to you. From what I understand, the
key idea to go around your issue with substitution is to define
reducibility judgments universally with respect to all substitutions, so
as to get a strong enough induction principle.
You might also be interested in the strategy taken in the MetaCoq
<https://urldefense.com/v3/__https://github.com/MetaCoq/metacoq__;!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACeivomQQ$ > project. The whole development is
done in the cumulative setting, but I do not think that any idea in the
proof would not carry over if we chose to degenerate cumulativity and
take it to be equal to conversion: the key technical property is
confluence of reduction, from which many things follow, including
injectivity of type constructors. The idea is to make a detour through
bidirectional typing. The main three steps are the following: 1) show
that if |- t : T then also t infers some T' such that T' <= T (with <=
being cumulativity) 2) show that if t infers T', then also |- t : T' 3)
show that inferred types are unique (up to conversion, or even a
stronger relation: in MetaCoq, we show that they have a common reduct).
From this, you get type principality (the equivalent of type uniqueness
in the cumulative setting, saying that any typable term has a minimal
type). If you want to read more about this, the best source is probably
my PhD thesis <https://urldefense.com/v3/__https://www.meven.ac/category/phd-thesis.html__;!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACqhbyBoA$ >.
Best,
Meven LENNON-BERTRAND
Doctorant, Équipe Gallinette – LS2N – Université de Nantes
https://urldefense.com/v3/__http://www.meven.ac__;!!IBzWLUs!Vb4IFWcpXSjUT-97xXI-eN3VNzUlkEDre6l38Mv26CpuKQZmjJORIllYIVB6Xl3Jeix7mFvsQ9rAGo0wvo_B8INVsUyZb6bKcFACUrmXZmo$
Le 16/08/2022 à 03:12, Jason Hu a écrit :
[ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Sandro,
Thanks for your reference. I don’t actually necessarily mean a syntactic proof
but is more generally wondering whether these properties have been looked into
in details and if so, what is the earliest work. I will definitely look into
your PTS mechanization.
Thanks,
Jason
From: Sandro Stucki<mailto:[email protected]>
Sent: Monday, August 15, 2022 5:28 PM
To: Jason Hu<mailto:[email protected]>
Cc:[email protected]<mailto:[email protected]>
Subject: Re: [TYPES] reference request: MLTT with Russell's non-cumulative
universes
Hi Jason!
If I understand correctly, you're looking for a syntactic proof of
uniqueness of types, and the crucial property you need to make
progress here is injectivity of the Pi type constructor
(Pi-injectivity). As usual, the devil is in the details, but if you're
happy with a formulation of type theory that 1) only has Pi types and
universes, but no Sigma types (aka a pure type system) and 2) treats
types and terms up to (untyped) beta-equivalence (no eta-conversions)
then Pi-injectivity is relatively easy to prove syntactically (via
Church-Rosser). I believe that pure type systems (PTS) are sufficient
for expressing the sort of non-cumulative universes you want, and that
uniqueness of types holds for the relevant class of PTSs.
A nice reference for PTSs is Barendregt's "Lambda calculi with types"
(1993) -- the chapter, not the book. See Lemma 5.2.21 (p. 109) for a
proof of uniqueness of types (I believe the system you have in mind
should indeed be singly-sorted).
Since you mentioned Agda: I mechanized the basic meta-theory of PTSs
(including Pi-injectivity, but not uniqueness of types) a while ago in
Agda. It probably won't type-check using an up-to-date version of
Agda, but it might still be useful to get the basic ideas:
https://urldefense.com/v3/__https://github.com/sstucki/pts-agda__;!!IBzWLUs!XpsRNnHe2MectpW2xSjPR6jeL3VYpZNpP3Pp67bKzE3fTEp5g-n2GsuiGcG65q7JgV2C3p_8JyaJUSV0MK8WafnTf4iFiJM$
Cheers
/Sandro
On Mon, Aug 15, 2022 at 10:14 PM Jason Hu<[email protected]> wrote:
[ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi all,
I am writing to see if anyone has formalized a formulation MLTT with
non-cumulative universes. This type theory is useful and interesting and is a
foundation for, e.g. Agda. In particular, I would like to see some proofs of
some properties like type uniqueness. I saw in many places that people say with
non-cumulative universes, every term has a unique type (up to equivalence).
However, it does not seem very obvious how to prove it easily by syntactic
method. For example, consider function application
t s : T1 [ s ] and t s : T2 [ s ]
where [ s ] denotes substitution of the topmost variable only. Now we want to
prove T1 [ s ] and T2 [ s ] are equivalent. However, induction on t only shows
that for some S1 and S2, such that
t : (x : S1). T1 and t : (x : S2). T2 ==> : (x : S1). T1 ~ (x : S2). T2
where ~ is the definitional equivalence relation, but then we are stuck,
because we are not able to show T1 ~ T2 without doing a logical relation
argument.
The type uniqueness property is important to prove the property that every type
lives in precisely one universe, where we need another property that also needs
logical relations to establish:
Set i ~ Set j ==> i = j
Is there any document that systematically looks into non-cumulativity? Many I
read only talk about cumulative universes and non-cumulativity seems often
elided.
Thanks,
Jason
