1. Type
2. Usual objects — i.e. structures, functions, propositions — are reframed as Types.

A proposition is:

1. a statement susceptible to proof.

A theorem is:

1. a statement that has been proven.

It means:

1. constructing a type that represents a proposition.
2. constructing a term of that type that represents a proof.

A deductive system is:

1. A collections of rules
2. that are used to derive judgements

The judgement the term a has type A is written:

1. a : A

It means that there is a term p ~:~ a =_A b

It means that a and b are equal by definition.

The expression used to refer to the term may be different, but it is same term.

For instance, if we define f(x) = x^2, then we write:

f(3) \equiv{} 3^2 ~:~ ℕ

These equalities are useful because:

1. Given:
   1. x ~:~ ℕ
   2. f(x) \equiv{} x^2
   3. p ~:~ 3^2 = 9
2. We want to be able to derive:
   1. p ~:~ f(3) = 9

In other words:

1. Given:
   1. p ~:~ A
   2. A \equiv{} B
2. We may conclude: p ~:~ B

With :\equiv{}. For instance: f(x) ~:\equiv{}~ x^2

1. A context is the ordered list of assumptions that may lead to a judgement.
2. For instance: given a,b~:~N and p~:~a = b, we may construct p^{-1}~:~b=a
3. The context is: a,b~:~N, p~:~a = b

A type former is:

1. a way to construct a type
2. rules for the construction and behavior of elements of that type

No, only rules.

1. In the description of deductive systems in terms of judgments, the rules are what allow us to conclude one judgment from a collection of others, while the axioms are the judgments we are given at the outset.
2. If we think of a deductive system as a formal game, then the rules are the rules of the game, while the axioms are the starting position.
3. The advantage of formulating type theory using only rules is that rules are “procedural”. In particular, this property is what makes possible (though it does not automatically ensure) the good computational properties of type theory, such as “canonicity”.

1. Given: A,B:U, then: A → B
2. Given: a formula F, then: f :≡ λa:F
3. Given: f : A → B, then: f(a) :≡ (λx:F)(a) : B

1. A uniserve is a type whose elements are types.
2. U_0 ~:~ U_1 ~ …
3. Universes are cumulative.
4. A small type is a type of some universe U.

1. B ~:~ A \rightarrow{} U
2. It is called a family of types or dependent types.

1. Given: A, B : A → U, then: ΠA→B
2. Given: a formula F, then: f :≡ λa:F
3. Given: f : ΠA→B, then: f(a) :≡ (λx:F)(a) : B(a)

1. Given: A,B:U, then: A × B
2. Given: a:A, b:B, then: (a,b) : A × B
3. Given: (a,b) : A × B, g : A → B → C, then: f((a,b)) :≡ g(a,b) : C

It specifies how to build functions on A × B.

1. rec : Π(C:U)→(A→B→C)→(A×B→C)
2. rec C g (a,b) :≡ g(a,b)

It specifies how to build dependent functions on A × B.

1. ind : Π(C:A×B→U)→(ΠA→ΠB→C)→(ΠA×B→C)
2. ind C g (a,b) :≡ g(a,b)

1. Given: A:U, B:A→U, then: ΣA,B
2. Given: a:A, b:B(a), then: (a,b) : ΣA,B
3. rec : Π(C:U),(ΠA,B → C) → (ΣA,B → C)
4. rec C g (a,b) :≡ g(a,b)
5. ind : Π(C:Π(ΣA,B),U) → (ΠA,(ΠB,C)) → (Π(ΣA,B),C)
6. ind C g (a,b) :≡ g(a,b)

1. Magam :≡ ΣA:U,A → A → A

1. Magam :≡ ΣA:U,(A → A → A) × A

1. Given: A,B:U , then: A+B
2. Given: a:A, b:B, then: inl(a), inr(b) : A+B
3. rec : Π(C:U),(A→C) → (B→C) → (A+B → C)
4. rec C (f,g) inl(a) :≡ f(a)
5. rec C (f,g) inr(b) :≡ g(b)
6. ind : Π(C:A+B → U), (ΠA,C) → (ΠB,C)→ (ΠA+B,C)
7. ind C (f,g) inl(a) :≡ f(a)
8. ind C (f,g) inr(b) :≡ g(b)

1. ℕ is the type of natural numbers.
2. 0 : ℕ
3. Given: n:ℕ, then: succ(n):ℕ
4. rec : ΠC:U, C → (ℕ→C→C) → (ℕ→C)
5. rec C c0 cs 0 :≡ c0
6. rec C c0 cs succ(n) :≡ cs n rec(C c0 cs n)
7. ind :
8. ind :≡

1. True ↔ 1
2. False ↔ 0
3. A and B ↔ A × B
4. A or B ↔ A + B
5. If A, then: B ↔ A → B
6. A iff B ↔ (A → B) × (B → A)
7. Not A ↔ A → 0
8. ∀x:A,P(x) ↔ Π(x:A),P(x)
9. ∃x:A,P(x) ↔ Σ(x:A),P(x)