no axioms

Stream: general

[Kenny Lau]

inductive tower : set (set (set α))
| empty : tower ∅
| succ  : ∀ {t}, tower t → tower (succ S t)
| chain : ∀ {C}, C ⊆ chains S → is_chain C → (∀ A ∈ C, tower A) → tower { A | ∃ t ∈ C, A ∈ t }
#print axioms succ -- classical.choice quot.sound propext
#print axioms tower -- no axioms

Why does tower use no axioms even though I clearly see succ?

[Kevin Buzzard]

Kenny you are posting code which doesn't run

[Kenny Lau]

oops

[Kevin Buzzard]

so I can only conjecture

[Kevin Buzzard]

but not verify

[Kevin Buzzard]

that if you instead try #print axioms tower.mk

[Kevin Buzzard]

you will see the axioms you used

[Kevin Buzzard]

let me know if I answered your question

[Kenny Lau]

it's a prop so it has no k

[Kenny Lau]

mk

[Kevin Buzzard]

If it's a prop then maybe it really does use no axioms

[Kevin Buzzard]

because all those cases H which you had to change to classical.some H when you were working with data

[Simon Hudon]

An inductive type definition is not a definition in the kernel. It's built by postulating that tower is a type of the proper universe, that empty, succ and chain are functions that return a tower and that a recursor exists

[Kevin Buzzard]

sorry, someone came round

[Kevin Buzzard]

was going to finish "...can be changed back somehow"

[Kevin Buzzard]

Actually I really do not understand what is going on here.

[Kevin Buzzard]

Am I right in thinking that in general it is possible to construct Props which don't use axioms but whose construction essentially uses types which are not props and whose construction involves axioms?

[Kevin Buzzard]

How much will Prop let us forget?

[Kevin Buzzard]

I do not know if I can make my question rigorous

[Simon Hudon]

I don't get your question. Do you mean constructing pops that only uses inductive definitions?

[Gabriel Ebner]

The technical answer is that the code for #print axioms does not traverse inductive declarations. It only looks at the contents and types of definitions, and types of axioms. This is probably not a problem since you presumably don't require choice if you never use tower.succ.