# Zulip Chat Archive

## Stream: new members

### Topic: Inductive Types vs. Axioms

#### Marcus Rossel (Mar 16 2021 at 07:41):

IIRC, using the `constant`

keyword in Lean is the same as declaring an axiom. So e.g:

```
constant fruit : Type*
constant apple : fruit
```

would axiomatically define a `fruit`

type with a member `apple`

.

What I don't understand is how inductive type declarations are different from this. E.g. if I write ...

```
inductive fruit : Type*
| apple : fruit
```

... then where are this new type and value coming from, if not by axioms?

#### Ruben Van de Velde (Mar 16 2021 at 07:44):

My understanding is that you're right that they're essentially similar, but `inductive`

is more limited in what axioms it creates, so it can't make your logic inconsistent

#### Kevin Buzzard (Mar 16 2021 at 07:45):

Right -- you have the guarantee that you didn't just enable a proof of false with the inductive definition. You can just make a constant term of type `false`

#### Kevin Buzzard (Mar 16 2021 at 07:46):

The inductive definition also makes a recursor, which is also defined as a constant

#### Kevin Buzzard (Mar 16 2021 at 07:46):

Check out `#print fruit.rec`

#### Kevin Buzzard (Mar 16 2021 at 07:47):

And then an internal system makes a bunch more stuff -- check out `#print prefix fruit`

#### Kevin Buzzard (Mar 16 2021 at 07:48):

The recursor says "apples are the only fruit" -- you don't get this with the constant definition

#### Marcus Rossel (Mar 16 2021 at 07:48):

Wow ok, so we *are* in fact adding axioms with every inductive type definition.

Would there be other ways of creating new types, or is there a particular reason we need to do it by adding axioms?

#### Kevin Buzzard (Mar 16 2021 at 07:52):

I'm not a type theorist. My basic understanding is that this is just how the calculus of inductive constructions works

#### Kevin Buzzard (Mar 16 2021 at 07:52):

There are three ways of making types in lean, inductive types, function types and quotient types, and as far as I am concerned each thing just happens by magic

#### Marcus Rossel (Mar 16 2021 at 07:53):

That's why we need @Mario Carneiros in this world :D

#### Kevin Buzzard (Mar 16 2021 at 07:54):

You make terms of inductive types using the constructors (which were magically added as constants when the inductive type was made), you make terms of function types with lambdas, and you make terms of quotient types with `quot.mk`

#### Marcus Rossel (Mar 16 2021 at 07:57):

I never knew that quotient types were so foundational. Do they basically behave as "take a type and make a new one by collapsing members according to a given equivalence relation"?

#### Mario Carneiro (Mar 16 2021 at 08:02):

That's what it means to be a quotient type, but if it were just that you could build them with set-quotients

#### Mario Carneiro (Mar 16 2021 at 08:03):

The reason they are axiomatic is so that they get the computational rule `lift f h (quot.mk a) = f a`

#### Mario Carneiro (Mar 16 2021 at 08:04):

you can't add custom definitional equalities in lean's type theory, so any new defeqs have to be axiomatized as part of the theory

#### Mario Carneiro (Mar 16 2021 at 08:04):

Same thing with inductive types - you can kind of build them using church encodings if you don't care about the computational rules

#### Mario Carneiro (Mar 16 2021 at 08:05):

that doesn't completely work though because inductive types are magical in that the recursor for a (large-eliminating) inductive type mentions a free universe variable

#### Mario Carneiro (Mar 16 2021 at 08:06):

```
inductive nat' : Type
| zero : nat'
| succ : nat' → nat'
#print nat'.rec
-- protected eliminator nat'.rec : Π {C : nat' → Sort l}, C nat'.zero → (Π (ᾰ : nat'), C ᾰ → C ᾰ.succ) → Π (n : nat'), C n
```

where did that universe `l`

come from? :thinking:

#### Mario Carneiro (Mar 16 2021 at 08:13):

Here's a definition of `nat`

using church encodings:

```
def nat' : Type 1 :=
{ f : Π {C : Type}, C → (C → C) → C //
∀ A B (e : A → B) (a0 : A) (b0 : B) (h0 : e a0 = b0)
(as : A → A) (bs : B → B) (h1 : ∀ a, e (as a) = bs (e a)),
e (f a0 as) = f b0 bs }
```

You can kind of tell this definition has a universe issue though, because it's in the wrong universe - it lives in `Type 1`

but the recursor for this type only works in `Type`

instead of `Type u`

like the axiomatic inductive type `nat`

Last updated: May 12 2021 at 23:13 UTC