You need UIP for lambda calculus

Stream: Type theory

[Chris Hughes]

I'm doing something close to simply typed lambda calculus in Lean right now, and some of my code looks something like this.

def Context (types : Type) := List types

inductive Var {types : Type} : Context types → types → Type
| head {Γ T} : Var (T::Γ) T
| tail {Γ T T'} : Var Γ T → Var (T'::Γ) T

theorem singleton_of_singleton {types : Type} (T : types) :
  ∀ v₁ v₂ : Var [T] T, v₁ = v₂
| Var.head, Var.head => rfl

Am I correct in saying that singleton_of_singleton is not provable without UIP?

[Andrea Vezzosi]

You need UIP for the types parameter at least.