[TYPES] reference request: MLTT with Russell's non-cumulative universes

Wed Aug 17 11:58:16 EDT 2022

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:sandro.stucki at gmail.com>
> Sent: Monday, August 15, 2022 5:28 PM
> To: Jason Hu<mailto:fdhzs2010 at hotmail.com>
> Cc:types-list at LISTS.SEAS.UPENN.EDU<mailto:types-list at lists.seas.upenn.edu>
> 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<fdhzs2010 at hotmail.com>  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
>>