display of inhabited

Stream: general

[ZHAO Jinxiang]

#eval inhabited ℕ
#eval inhabited ℕ × ℕ
#eval nat.add (1 : ℕ) (inhabited ℕ)
#eval inhabited (Type*)

I found all of these are

result type does not have an instance of type class 'has_repr', dumping internal representation
#0

Is there any way to display it?

[Eric Wieser]

What do you want it to display?

[Eric Wieser]

What should #eval inhabited empty display?

[ZHAO Jinxiang]

I want to know what will happen if I calculate it.

[Eric Wieser]

What do you mean by "calculate"? What does #eval ℕ mean to you, and what does it calculate?

[Eric Wieser]

(I think the real answer here is that you meant to write #eval (default : ℕ))

[ZHAO Jinxiang]

Yes, default is what I need.

[ZHAO Jinxiang]

What's the meaning of #eval (default : Type*).
I think this is the terminal object of category_theory.types

So I think this is unit

---

Oh, the display of #eval ℕ is also #0

[ZHAO Jinxiang]

Oh, I find it works.

#eval (unit.star : (default : Type*))

[ZHAO Jinxiang]

Is there other way to check default : Type* is unit?

[Kyle Miller]

You'll have better luck with #reduce

#reduce (default : Type*)
-- punit

[Kyle Miller]

#eval uses the VM compiler and evaluation, but #reduce uses term reduction

[ZHAO Jinxiang]

Thanks!

[ZHAO Jinxiang]

Another question:

#reduce (category_theory.with_terminal.inhabited Type*).default
#reduce (category_theory.with_initial.inhabited Type*).default
#reduce (category_theory.with_terminal.inhabited Group).default
#reduce (category_theory.with_initial.inhabited Group).default

Why both initial object and terminal object of category_theory.types is punit?

[ZHAO Jinxiang]

In the category of sets, the initial object is the empty set.
Why in category of type, the initial object is not pempty?

[Adam Topaz]

pempty is an initial object. There is no "the" initial object.

[Adam Topaz]

punit is not an initial object in Type*

[Adam Topaz]

with_initial formally adds an initial object. I think that's the source of your confusion.

[ZHAO Jinxiang]

#reduce (category_theory.with_initial.inhabited Type*).default
-- with_initial.of punit

[Adam Topaz]

And?

[ZHAO Jinxiang]

I don't understand the result of it.

[Adam Topaz]

docs#category_theory.with_initial

[Adam Topaz]

As I said, that construction formally adds an initial object. It has an inhabited instance, and the default elemt happens to be punit.star

[ZHAO Jinxiang]

Oh, I see. Thank you.

[ZHAO Jinxiang]

Is there any lemma told me that pempty is an initial object for type category.

[Adam Topaz]

Existence of initial and terminal objects is handled by the typeclass system. See docs#category_theory.limits.initial

[Adam Topaz]

docs#category_theory.type.is_initial_pempty perhaps?

[Adam Topaz]

Hmmm... sorry I'm on mobile right now so I can't help much.

[ZHAO Jinxiang]

category_theory.limits.types.initial_iso

category_theory.limits.types.terminal_iso