# Library UniMath.Foundations.Preamble

# Introduction. Vladimir Voevodsky . Feb. 2010 - Sep. 2011

Universe structure

The empty type

The one-element type

The two-element type

Inductive bool : UU :=

| true : bool

| false : bool.

Definition negb (b:bool) := if b then false else true.

The coproduct of two types

Inductive coprod (A B:UU) : UU :=

| ii1 : A -> coprod A B

| ii2 : B -> coprod A B.

Arguments coprod_rect {_ _} _ _ _ _.

Arguments ii1 {_ _} _.

Arguments ii2 {_ _} _.

Notation inl := ii1. Notation inr := ii2.

Notation "X ⨿ Y" := (coprod X Y).

The natural numbers

Inductive nat : UU :=

| O : nat

| S : nat -> nat.

Definition succ := S.

Declare Scope nat_scope.

Delimit Scope nat_scope with nat.

Bind Scope nat_scope with nat.

Arguments S _%nat.

Open Scope nat_scope.

Fixpoint add n m :=

match n with

| O => m

| S p => S (p + m)

end

where "n + m" := (add n m) : nat_scope.

Fixpoint sub n m :=

match n, m with

| S k, S l => k - l

| _, _ => n

end

where "n - m" := (sub n m) : nat_scope.

Definition mul : nat -> nat -> nat.

Show proof.

Notation "n * m" := (mul n m) : nat_scope.

Fixpoint max n m :=

match n, m with

| O, _ => m

| S n', O => n

| S n', S m' => S (max n' m')

end.

Fixpoint min n m :=

match n, m with

| O, _ => O

| S n', O => O

| S n', S m' => S (min n' m')

end.

Notation "0" := (O) : nat_scope.

Notation "1" := (S 0) : nat_scope.

Notation "2" := (S 1) : nat_scope.

Notation "3" := (S 2) : nat_scope.

Notation "4" := (S 3) : nat_scope.

Notation "5" := (S 4) : nat_scope.

Notation "6" := (S 5) : nat_scope.

Notation "7" := (S 6) : nat_scope.

Notation "8" := (S 7) : nat_scope.

Notation "9" := (S 8) : nat_scope.

Notation "10" := (S 9) : nat_scope.

Notation "11" := (S 10) : nat_scope.

Notation "12" := (S 11) : nat_scope.

Notation "13" := (S 12) : nat_scope.

Notation "14" := (S 13) : nat_scope.

Notation "15" := (S 14) : nat_scope.

Notation "16" := (S 15) : nat_scope.

Notation "17" := (S 16) : nat_scope.

Notation "18" := (S 17) : nat_scope.

Notation "19" := (S 18) : nat_scope.

Notation "20" := (S 19) : nat_scope.

Notation "21" := (S 20) : nat_scope.

Notation "22" := (S 21) : nat_scope.

Notation "23" := (S 22) : nat_scope.

Notation "24" := (S 23) : nat_scope.

Notation "100" := (10 * 10) : nat_scope.

Notation "1000" := (10 * 100) : nat_scope.

Identity Types

Inductive paths {A:UU} (a:A) : A -> UU := paths_refl : paths a a.

#[global]

Hint Resolve paths_refl : core .

Notation "a = b" := (paths a b) : type_scope.

Notation idpath := paths_refl .

Dependent sums.
One can not use a new record each time one needs it because the general theorems about this
construction would not apply to new instances of "Record" due to the "generativity" of inductive
definitions in Coq.
We use "Record", which is equivalent to "Structure", instead of "Inductive" here, so we can take
advantage of the "primitive projections" feature of Coq, which introduces η-reduction for pairs, by
adding the option "Set Primitive Projections". It also speeds up compilation by 56 percent.
The terms produced by the "induction" tactic, when we define "total2" as a record, contain the
"match" construction instead appealing to the eliminator. However, assuming the eliminator will be
justified mathematically, the way to justify the the "match" construction is to point out that it
can be regarded as an abbreviation for the eliminator that omits explicit mention of the first two
parameters (X:Type) and (Y:X->Type).
I.e., whenever you see
match w as t0 return TYPE with | tpair _ _ x y => BODY end
in a proof term, just mentally replace it by
@total2_rect _ _ (λ t0, TYPE) (λ x y, BODY) w

Set Primitive Projections.

Set Nonrecursive Elimination Schemes.

Record total2 { T: UU } ( P: T -> UU ) := tpair { pr1 : T; pr2 : P pr1 }.

Arguments tpair {_} _ _ _.

Arguments pr1 {_ _} _.

Arguments pr2 {_ _} _.

Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))

(at level 200, x binder, y binder, right associativity) : type_scope.

Notation "x ,, y" := (tpair _ x y).