effective epimorphisms

Stream: Type theory

[Andrew Pitts]

I trying to find out what Lean has to offer me. Part of that process involves understanding Lean's underlying type theory.

Here's a test case: prove that every surjective function (f : A -> B such that for all b : B there exits a : A with f a = b) is an effective epimorphism (for all types C and functions g : A -> C satisfying for all a,a':A , f a = f a' -> g a = g a', there exists a unique function h : B -> C whose composition with f equals g)

In my go-to prover, Agda, that is not a theorem, but it becomes one if one postulates an axiom of unique choice (a very uncontentious axiom!).

Question: how do people prove that surjections are effective epimorphisms in Lean? Is it by an appeal to AC (Hilbert choice operator), or by more subtle means? What is the status of unique choice in Lean?

[Eric Wieser]

docs#classical.some is non-unique choice if that helps

[Kevin Buzzard]

I'm not sure what the question is. In Lean's maths library there are no extra axioms assumed beyond those in core lean and I would just prove the contentious part of this by proving every surjective function has a one-sided inverse using AC and then it's easy. AC is an axiom in Lean and I use it 6 times before breakfast. But I suspect you're asking something else.

[Kevin Buzzard]

There is not really a community of people here working on any kind of mathematics other than classical mathematics

[Mac]

It is probably worth noting that AC is an axiom in Lean and not thus not part of its foundational logic. That is, you can still do logic in Lean without assuming choice should you so desire. In fact, that is the default. You only get AC rolled into the environment if you open the classical (Lean 3) or Classical (Lean 4) namespace.

[Andrew Pitts]

Kevin Buzzard said:

I'm not sure what the question is. In Lean's maths library there are no extra axioms assumed beyond those in core lean and I would just prove the contentious part of this by proving every surjective function has a one-sided inverse using AC and then it's easy. AC is an axiom in Lean and I use it 6 times before breakfast. But I suspect you're asking something else.

OK so the answer is: just use AC (as I suspected).
(I was asking because I was interested to know whether Lean's core logic (before assuming any axioms) entailed unique choice. For example in set theory, where a function is the same thing as single-valued total binary relation, it's provable that surjections are effective epis without any appeal to AC. )

[Kevin Buzzard]

I have heard it said that unique choice cannot be proved in lean without invoking some of the axioms in lean. By the way you don't have to open classical to use classical axioms, you can use classical.some whether or not it's open.

To be quite frank, the fact that the axiom of choice is baked into core lean was one of the things which attracted me to it over the other theorem provers. It made me feel like lean was taking classical mathematics (the kind of mathematics which wins Fields Medals) more seriously than the other provers.

[Kevin Buzzard]

By the way I have also heard it said that you can tell which of the axioms a theorem uses with the #print axioms command

[François G. Dorais]

@Andrew Pitts Lean has built-in quotient types. In particular, there is a nice epi/mono image factorization. However, since Lean's Prop is impredicative, it takes axioms to let it bleed into the Type hierarchy. In particular, unique choice makes everything impredicative (which is not that big a deal by my taste, but some palates are more sensitive than mine). To keep a predicative hierarchy, you can ignore Lean's Prop and think of propositions as subsingletons in the Type hierarchy. Interpreted this way, all surjections are effective since "surjection" then basically means that there is an induced bijection between the codomain and the image.

Keep in mind that Lean's universe hierarchy is _not_ cumulative!

[François G. Dorais]

Something I did a long while ago is relevant: https://github.com/fgdorais/uniq

[Andrew Pitts]

François G. Dorais said:

Andrew Pitts Lean has built-in quotient types.

Built-in? Wouldn't "built-on" be better? -- I though quotients are axiomatized and given tactic support, but are not part of the core type theory.

In particular, there is a nice epi/mono image factorization. However, since Lean's Prop is impredicative, it takes axioms to let it bleed into the Type hierarchy. In particular, unique choice makes everything impredicative

I don't see that postulating unique choice implies impredicativity. For example in Agda I use a postulate

A!C : {l : Level}{A : Set l} → (∃ x ∶ A , ∀(x' : A) → x =x') → A

where the equality x = x' is (implicitly) in the predicative universe of propositions Prop l when the type A of x and x' are in universe Set l.

I understand that Lean's Prop is impredicative and hence one has to be careful how many inductively defined propositions can be eliminated in types, but I don't see that unique choice is affected by that.

Thanks for sharing your Lean snippet axiomatizing unique choice.

[David Wärn]

I think you're right that this issue with unique choice is unrelated to predicativity (you can have either one without the other)

[David Wärn]

As I understand, the only non-built-on aspect of quotients in Lean is that the computation rule holds definitionally, as in:

example (α β : Type) (r : α → α → Prop) (f : α → β) (h : ∀ a a', r a a' → f a = f a') (a : α) :
  quot.lift f h (quot.mk r a) = f a := rfl

[Anne Baanen]

In case you haven't found it already, Mario's thesis is the best source on Lean's type theory, such as the quotient types.

[François G. Dorais]

I never said unique choice was impredicative. Lean has quotients, an impredicative Prop, and a non-cumulative hierarchy. Combined with unique choice, the impredicativity of Prop leaks into the Type hierarchy.

As I hinted, there is a way to have predicativity and unique choice, which is to ignore Lean's impredicative Prop and work with "constructive propositions", i.e. subsingletons in the type hierarchy. So, for example, the existential quantifier would be interpreted as squashing a Sigma type to a subsingleton by quotienting with the always true equivalence relation. (Like hProp in HoTT.) This way, we still have predicative Type universes and unique choice is actually provable! Of course, none of the Lean tools are meant to work with constructive propositions, so you would need to fork Lean or use something else to make this practical.

[David Wärn]

This seems like an odd way of thinking about the issue. Is there any sense in which Lean-without-choice is predicative at the level of types? If we put on our predicative hat and imagine that Lean is inconsistent as a result of impredicativity, then not only are all Props inhabited, all Typess are also inhabited by exfalso, so we haven't salvaged anything by avoiding unique choice.

[David Wärn]

A more pedestrian way of understanding why Lean-without-choice doesn't prove unique choice is that when you define a term of a type, Lean remembers how to construct that thing, whereas when you prove a proposition, Lean just remembers that it's true. It's a separation between "constructions" and "properties of constructions", and you can't use a property of a construction to carry out some other construction.

[David Wärn]

Also, while it's true that impredicativity is a major selling point of Prop over subsingleton types for the classical mathematician, it's not the only one. Lean also uses definitional proof irrelevance a lot.

[François G. Dorais]

That's right. Lean's Prop is very isolated from higher Types by design. That is actually really nice since it allows Lean's Prop to behave much more like the meta-theory of Lean. For example, adding LEM for Prop only has very little impact in Lean. After all, it doesn't matter whether a programmer thinks classically, intuitionistically, or whatever, the written program runs exactly the same.

[Eric Wieser]

Note we already have some tools for quotients by the always-true relation as docs#trunc