fruitUniverse

Stream: general

[Phiroc]

Hello,
in the below code, why is Π of type fruitUniverse, not, say, fruitType,
because it is a Proposition? What does the universe have to do
with the proposition?

Many thanks.

Phiroc

universe fruitUniverse
constant fruitType : Type
constants ft1 ft2 : fruitType

-- Prop = Statement
-- apple and apple are equal atoms
#check ft1 = ft2

namespace hidden
constant list : Type fruitUniverse → Type fruitUniverse
-- variables l : list fruitType
namespace list
    constant cons' : Π fruitType : Type fruitUniverse, fruitType → list fruitType → list fruitType
    constant nil' : Π fruitType  : Type fruitUniverse, list fruitType
    constant append' : Π fruitType : Type fruitUniverse, list fruitType → list fruitType → list fruitType
end list
end hidden

lean

[Yury G. Kudryashov]

Please add "lean" after opening "```", then syntax highlighting will work.

[Kenny Lau]

also I didn't understand the question

[Yury G. Kudryashov]

Note that fruitType in Π fruitType ... has nothing to do with constant fruitType : Type

[Phiroc]

I'm trying to create a cons' function which I can later use to create a list of Fruits. The only way to make Lean validate the above code is to make Π fruitType of type fruitUniverse.

[Phiroc]

What is Π? A Prop?

[Phiroc]

If I understand Lean, to create a cons function, you need to create a Proposal, Π.

[Yury G. Kudryashov]

1. universe is a way to deal with "type of all types"; most probably you don't need it.
2. Π is a pi type, not a proposition. E.g., Π n : nat, {m : nat // n < m} means "a function that takes a natural number n and returns another natural number m together with a proof of the fact n < m.
3. constant is like an axiom, not a variable. When you declare constant list, it declares a type named hidden.list with no extra information about this type.

[Kenny Lau]

this isn’t C; there is no preamble

[Kenny Lau]

y'all like tomatos very much even though it isn't a fruit fruit

[Marc Huisinga]

i did my best to counteract the bias for tomatoes

[Sebastian Ullrich]

Does the fruit universe also contain fruit Pies, or is it predicative?