search

AndrasKovacs / elaboration-zoo

Minimal implementations for dependent type checking and elaboration
BSD 3-Clause "New" or "Revised" License
600 stars 34 forks source link

This example has wrong universe level, maybe remove? #29

Closed molikto closed 3 years ago

AndrasKovacs commented 3 years ago

What do you mean? The package does not have universe levels at all, it has type-in-type.

molikto commented 3 years ago

I am porting the examples to my implementation which has universe levels, and it seems to me there is not a consistent assigment of universe levels to this example

AndrasKovacs commented 3 years ago

If you have universe levels, it's a bit weird that you only get an error at this point in the file. With predicative levels, Bool and Nat should already fail to check.

molikto commented 3 years ago

I have added proper universe levels to all of the definitions, but this one doesn't seems to have a proper assignment of universe levels? The proof for sym in this paper https://jesper.sikanda.be/files/leibniz-equality.pdf is different

AndrasKovacs commented 3 years ago

If we wanted to assign levels to the example file, it would be possible using impredicative U0. This would fail though if there were large elimination in the example file.

The paper with Leibniz equality can only show the construction of Martin-Löf identity from Leibniz identity if we also assume

  1. Parametric quantifiers
  2. Parametricity
  3. Resizing axioms
  4. Funext

See section 6 of the paper. In a plain predicative type theory Martin-Löf identity is not derivable.

If the goal is to justify a type-in-type construction by a translation to a consistent TT, then the right way to do it is to translate Church-encodings to inductive definitions, not to keep Church-encodings and attempt to assign levels for that. Assigning levels to Church-encodings is impossible in plain predicative TT. To make that work, we'd have to move to a significantly different theory; perhaps 1)-4) from the Leibniz paper is enough in general, perhaps it isn't, as the paper only shows the construction for the identity type and not other inductive types.

molikto commented 3 years ago

Thanks! I am just mindlessly porting the examples to a predicative system, without thinking too much. My point is that it seems this term cannot type in a predictive system. So I thought it cannot be typed in a consistent system. But it seems it can be typed with a impredicative universe of prop?

Sorry for that. This PR is not a good way to raise a question. I had too much unsaid assumptions both I am and not aware of.

AndrasKovacs commented 3 years ago

But it seems it can be typed with a impredicative universe of prop?

Sure, or with impredicative Set0. The restriction is that we can only eliminate into Prop or Set0 respectively. Then sym works as in the file. In Coq:

Require Import Coq.Unicode.Utf8.
Set Maximal Implicit Insertion.

Definition Id {A : Set}(x y : A) : Prop := ∀ (P : A → Prop), P x → P y.
Definition Refl {A : Set}(x : A) : Id x x := λ P px, px.
Definition Sym {A : Set}{x y : A} (p : Id x y) : Id y x := p (λ y, Id y x) (Refl x).