A unit type equality

Stream: general

[Kind Bubble]

When I tried to create a type like this:

variable {X : Type}
def george (x : X) (y : X) := if x = y then Unit else Empty

I get

Main.lean:13:30: error: failed to synthesize instance
  Decidable (x = y)

[Bolton Bailey]

Do you just want to fix the error? You can put [DecidableEq X] after {X : Type}

[Patrick Stevens]

(This is because Lean doesn't how to determine whether x = y, because the type X is completely arbitrary. The DecidableEq fix says "I will only call george in places where the context contains a way to determine equality in the X I use". If you add DecidableEq, it will be an error at the point where you try and use george if Lean can't work it out.)

[Reid Barton]

Probably docs4#PLift is a better way to achieve the same thing as your george.

[Kind Bubble]

I wanted something which was a constituent of Type but acted like a proposition (so it should be Unit or Empty type but we might not know which). And the simpler the better. Here's what I really wanted:

def type_of (p : Prop) := Σ(_ : p),Unit

but I get

Main.lean:12:23: error: application type mismatch
  (_ : p) × Unit
argument
  fun x => Unit
has type
  p → Type : Type 1
but is expected to have type
  ?m.16705 p → Type : Type (max 1 ?u.16675)

[Kind Bubble]

Patrick Stevens said:

(This is because Lean doesn't how to determine whether x = y, because the type X is completely arbitrary. The DecidableEq fix says "I will only call george in places where the context contains a way to determine equality in the X I use". If you add DecidableEq, it will be an error at the point where you try and use george if Lean can't work it out.)

I guess what I don't understand here is how to make a type which is Unit when x = y, Empty otherwise, but which doesn't require this be settled when defining the type. And I want it to work for any proposition not just x = y. But unfortunately I get the above error when I try the way that occurred to me.

[Reid Barton]

You can use docs4#PSigma for this (notation Σ'). The only difference is that the fields are also allowed to be propositions.
Or just use PLift like I suggested above, which is doing the same thing but simpler (without an extra Unit field).

[Horațiu Cheval]

I wanted something which was a constituent of Type but acted like a proposition (so it should be Unit or Empty type but we might not know which).

If this doesn't mean to act like a specific proposition, but you just one to say that a type behaves like propositions do, in that it is either empty or has one term, you can also use docs4#Subsingleton

[Yaël Dillies]

Spelling out what Reid means, you probably want PLift (x = y).

[Kind Bubble]

Yaël Dillies said:

Spelling out what Reid means, you probably want PLift (x = y).

Ok I think I get it now.

And I can do this too:

notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "*" => Unit.unit
notation "⊛" => Unit
def refl {X : Type} (x : X) : Σ(_:x=x):⊛ := PSigma.mk (Eq.refl x) *