3
$\begingroup$

I'm writing a library in the Lean computer proof assistant.

Evidently,

X : Type
x : X
y : X
#check x = y

Produces "Prop" and not "Type"; propositions are handled within the prop type. Unfortunately, I wanted to actually obtain the pullback of sets like so:

X : Type
Y : Type
Z : Type
f : X \rightarrow Z
g : Y \rightarrow Z
\Sigma (x : X), \Sigma (y : Y) , f(x) = g(y)

Since f(x) = g(y) produces a proposition instead of the singleton I'm at a loss to construct the pullback the way I'd like. Is there an alternative to the equality type in Lean which produces instead the singleton? It'd be nice to have a way of constructing maps Prop -> Type, particularly the one sending 1 to * and 0 to empty type.

$\endgroup$
5
  • 2
    $\begingroup$ Is def fiber_product {X Y Z} (f : X → Z) (g : Y → Z) : set (X × Y) := { x | f x.1 = g x.2 } what you had in mind? $\endgroup$
    – damiano
    Sep 7, 2022 at 21:19
  • 1
    $\begingroup$ Just a comment: before you go too far in Lean, note that Lean isn’t very good for doing purely constructive mathematics. I don’t know your goals, but you be in for a lot of pain if you need to say redefine equality. $\endgroup$
    – Jason Rute
    Sep 7, 2022 at 22:26
  • $\begingroup$ Section 7.7 of TPIL has the definition of equality in Lean. You should be able to make a Type valued version which would have the right eliminators. $\endgroup$
    – Jason Rute
    Sep 7, 2022 at 22:32
  • $\begingroup$ Also if you are looking to redefine equality, check out github.com/gebner/hott3 which does this. $\endgroup$
    – Jason Rute
    Sep 7, 2022 at 22:38
  • 1
    $\begingroup$ Do you mean sub-singleton instead of “singleton”? Also, what is the problem with Prop? Propositons are subsingletons. $\endgroup$ Sep 8, 2022 at 20:25

1 Answer 1

2
$\begingroup$

Here are a few ways I believe you can define the pullback:

def pullback1 {X Y Z : Type*} (f : X → Z) (g : Y → Z) : Type* :=
  Σ' (x : X) (y : Y), f x = g y
def pullback2 {X Y Z : Type*} (f : X → Z) (g : Y → Z) : Type* := 
  { x : (X × Y) // f x.1 = g x.2 }
def pullback3 {X Y Z : Type*} (f : X → Z) (g : Y → Z) : Type* := 
  Σ (x : X) (y : Y), { u : unit // f x = g y }
def pullback4 {X Y Z : Type*} (f : X → Z) (g : Y → Z) : Type* := 
  Σ (x : X) (y : Y), plift (f x = g y)

I believe they are all isomorphic types (but likely not provably equal, since few types in Lean are provably equal unless they are definitionally so).

The first is using psigma (Σ') instead of sigma (Σ) or Exists (). psigma works with Prop unlike sigma and returns a Type unlike Exists.

The second uses subtypes. In particular, the difference between damiano's suggestion of a fiber product using { x | f x.1 = g x.2 } and this suggestion of a pullback using { x : (X × Y) // f x.1 = g x.2 } is that the former is a subset and the later is a subtype. A subset of X is an element of set X which is the same as X -> Prop. But if you want to turn your set into a type, you use a subtype instead. See Section 7.3 of Theorem Proving in Lean.

The third is a bit of a hack to get you what you asked for, namely a way to turn a Prop into a Type. The subtype {u : unit // p} is a Type which behaves like the prop p. Of course, this is a hack that we likely never need, but if it was actually useful, one could define this directly, by modifying the definition of subtype removing the val field.

Edit: The fourth way (just added) uses plift which is the proper way to lift a Prop to a Type.


You asked for a way to turn a Prop into a Type such that true maps to unit and false maps to empty. That is certainly possibly using classical.dec. This uses the axiom of choice to show that every element of Prop is decidable and is therefore either true or false, and you can do a case split mapping one to unit and the other to empty.

But I doubt there is a nicer way to do that, mostly again since one can't prove isomorphic types are equal. For example, I don't think the subtypes {u : unit // true} and {u : unit // false} are provably equal to unit and empty respectively.


In the comments above, I likely overreacted to the idea of you wanting to "redefine equality" in Lean. In some other set theories equality is a type, but it is build deeply into Lean that equality is a Prop and the equality proofs are unique. This limits the ability to do homotopy type theory in Lean, or very pure constructive mathematics. I see now you were just trying to get sigma to work with a Prop.


If you are interested, here is the definition of a pullback in Lean. You could use this to find the pullback that mathlib uses for the category of Types and how they define it.

$\endgroup$
2
  • $\begingroup$ Thanks Jason this is very helpful. $\endgroup$ Sep 8, 2022 at 21:44
  • $\begingroup$ @Topologic I just added another version using plift which is the proper way to lift a Prop to a Type. $\endgroup$
    – Jason Rute
    Sep 9, 2022 at 22:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.