/- 
There are several fundamental ways to build types

We have countable cumulative hierarchy of universes Sort 0 ( = Prop) ⊆ Sort 1 ( = Type 0) ⊆ Sort 2 (Type 1) ⊆ ...

We can build Pi types Π x : α, β where β may contain x
A particular instance of the above is function type α → β 

We can build other types, like α × β, α + β, Σ x : α, β and so on
These types are not instances of the above general principles

Turns out such types are instances of the other fundamental principle of building types in Calculus of Constructions

We will now introduce (actually continue) inductive types
-/

/-
 General idea is that an inductive type comes with several constructors which provide means to build object of the  given type

 Along with contructors comes recursor, which, roughly speaking, ensures that the only way to build objects of an inductive type is by subseqeunt application of the constructors  
-/

/-
inductive foo : Sort u
| constructor1 foo
| constructor2  foo
...
| constructorn  foo
-/

/-
We have already seen some inductive types
Enumerated types
Such types have constructors of the form foo
-/

inductive weekday' : Type 0
| sunday : weekday'
| monday : weekday'
| tuesday : weekday'

/-
To build functions on the type weekday we use recursor
-/

#check @weekday'.rec

inductive natural : Type
| zero : natural
| S : natural → natural

#check @natural.rec

namespace hidden

universes u v

inductive prod (α : Type u) (β : Type v)
| mk : α → β → prod

inductive sum (α : Type u) (β : Type v)
| inl : α → sum
| inr : β → sum

def fst {α : Type u} {β : Type v} (p : prod α β) : α :=
prod.rec_on p (λ a b, a)

#reduce λ (α : Type u)(β : Type v) @prod.rec_on α β (λ_, α)

def prod_example (p : prod bool ℕ) : ℕ  :=
prod.rec_on p (λ b n, cond b (2 * n) (2 * n + 1))

#reduce prod_example  (prod.mk tt 3)
#reduce prod_example (prod.mk ff 3)

def sum_example (s : sum ℕ ℕ) : ℕ :=
sum.rec_on s (λ n, 2 * n) (λ n, 2 * n + 1) 

#reduce sum_example (sum.inr 4)
#reduce sum_example (sum.inl 4)

structure prod' (α β : Type*) :=
mk ::

structure triples (α β γ : Type*) :=
random ::

universe d

structure semigroup :=
(carrier : Type u)
(multiplication : carrier → carrier → carrier)
(associativityLaw : ∀ a b c, multiplication (multiplication a b) c = multiplication a (multiplication b c))

end hidden