Naive question about inductives

Stream: general

[Ioannis Konstantoulas]

I have been playing around with constructors and recursors to get a feel for types in Lean, and I have a question: when we have a type like the following:

inductive I where
  | mk : I -> I

from which we cannot get any terms (I assume?), what can we say about the type? For example, if we define the iterated composition of I.mk, can we say that these compositions are extensionally equal, or that they are not equal? Similarly, if we build another type J on top of I as follows:

inductive J where
  | mk : J -> (I -> I) -> J

can we something similar about self-compositions of J.mk? Can Lean prove I = J or Not (I = J)?

Also, surely it is not the case that definitionally I = Empty(?), but is there a notion of "type extensionality" that would make such an equality true?

This is all for educational purposes, as I do not know any type theory, but I would love to get some basic info at least in how Lean views types like the above.

[Mario Carneiro]

I is empty

[Mario Carneiro]

It is not (provably) true that I = Empty, but I is empty in the sense that I -> False, I -> Empty or various other expressions

[Mario Carneiro]

mathlib has IsEmpty I to express this condition

[Mario Carneiro]

import Mathlib.Logic.IsEmpty

inductive I where
  | mk : I -> I

example : IsEmpty I :=
  let rec go : I → False
    | .mk i => go i
  ⟨go⟩

inductive J where
  | mk : J -> (I -> I) -> J

example : IsEmpty J :=
  let rec go : J → False
    | .mk j _ => go j
  ⟨go⟩

[Ioannis Konstantoulas]

Thank you! This is exactly what I was suspecting, that you could get I -> False, but I didn't know how to do it.

[Ioannis Konstantoulas]

This leads me to another question, now: what is the difference between the following two? Lean accepts the first, but rejects the second complaining about non-termination:

def con₀ : I → False :=
  let rec go : I → False
    | .mk i => go i
  go

unsafe def con : I → False :=
  fun i => con i

I would assume the first would also have termination problems.

[Mario Carneiro]

the first one is recursive on I

[Mario Carneiro]

it terminates because there can only be finitely many applications of mk

[Mario Carneiro]

and the reason I is empty is because once you get to the bottom there is nothing else to apply

[Mario Carneiro]

To give an analogy, compare to Nat: there are no "infinitely large Nats", every Nat has a Nat.zero subterm in it. So if we take Nat and delete the Nat.zero constructor there are no elements left

[Ioannis Konstantoulas]

Fantastic; equivalently, Lean accepts this:

def con : I → False
  | .mk i => con i

[Mario Carneiro]

yes, the extra step was just to wrap it in the IsEmpty structure

[Trebor Huang]

"Type extensionality" is another name in some places for univalence, are you sure you mean that?

[Ioannis Konstantoulas]

Trebor Huang said:

"Type extensionality" is another name in some places for univalence, are you sure you mean that?

No, not really; I am not educated enough on these things to formulate clear questions.