What is the name of fundamental notion of Type Theory?

*Type*- Usual objects —
*i.e.*structures, functions, propositions — are reframed as*Types*.

What is a *proposition*?

A proposition is:

- a statement susceptible to proof.

What is a *theorem*?

A theorem is:

- a statement that has been proven.

In the context of Type Theory, what does *proving a theorem* means?

It means:

*constructing*a type that represents a proposition.*constructing*a term of that type that represents a proof.

Provide an informal description of a deductive system.

A deductive system is:

- A collections of
*rules* - that are used to derive
`judgements`

How to represent a judgement?

The judgement the term a has type A

is written:

- a : A

What does it mean: a and b are propositionally equal

?

It means that there is a term

What does it mean: a and b are judgmentally equal

?

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

Why these two equalities are useful?

These equalities are useful because:

- Given:
x ~:~ ℕ f(x) \equiv{} x^2 p ~:~ 3^2 = 9

- We want to be able to derive:
p ~:~ f(3) = 9

In other words:

- Given:
p ~:~ A A \equiv{} B

- We may conclude:
p ~:~ B

How to introduce a definitional equality?

With

What is a *context*?

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

What is a *type former*?

A type former is:

- a way to construct a type
- rules for the construction and behavior of elements of that type

Are there any *axioms*?

No, only rules.

- 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.
- 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.
- 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”.

Define the function type.

- Given: A,B:U, then: A → B
- Given: a formula F, then: f :≡ λa:F
- Given: f : A → B, then: f(a) :≡ (λx:F)(a) : B

What are *universes*?

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

How to model a collection of types varying over a given type A?

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

What is the dependent function types?

- Given: A, B : A → U, then: ΠA→B
- Given: a formula F, then: f :≡ λa:F
- Given: f : ΠA→B, then: f(a) :≡ (λx:F)(a) : B(a)

What is the product type?

- Given: A,B:U, then: A × B
- Given: a:A, b:B, then: (a,b) : A × B
- Given: (a,b) : A × B, g : A → B → C, then: f((a,b)) :≡ g(a,b) : C

What is the recursor on A × B?

It specifies how to build functions on A × B.

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

What is the induction on A × B?

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

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

What is the dependent pair Σ-types?

- Given: A:U, B:A→U, then: ΣA,B
- Given: a:A, b:B(a), then: (a,b) : ΣA,B
- rec : Π(C:U),(ΠA,B → C) → (ΣA,B → C)
- rec C g (a,b) :≡ g(a,b)
- ind : Π(C:Π(ΣA,B),U) → (ΠA,(ΠB,C)) → (Π(ΣA,B),C)
- ind C g (a,b) :≡ g(a,b)

Define a Magma.

- Magam :≡ ΣA:U,A → A → A

Define a pointed magma.

- Magam :≡ ΣA:U,(A → A → A) × A

Define the coproduct type.

- Given: A,B:U , then: A+B
- Given: a:A, b:B, then: inl(a), inr(b) : A+B
- rec : Π(C:U),(A→C) → (B→C) → (A+B → C)
- rec C (f,g) inl(a) :≡ f(a)
- rec C (f,g) inr(b) :≡ g(b)
- ind : Π(C:A+B → U), (ΠA,C) → (ΠB,C)→ (ΠA+B,C)
- ind C (f,g) inl(a) :≡ f(a)
- ind C (f,g) inr(b) :≡ g(b)

Define the natural numbers.

- ℕ is the type of natural numbers.
- 0 : ℕ
- Given: n:ℕ, then: succ(n):ℕ
- rec : ΠC:U, C → (ℕ→C→C) → (ℕ→C)
- rec C c0 cs 0 :≡ c0
- rec C c0 cs succ(n) :≡ cs n rec(C c0 cs n)
- ind :
- ind
:≡

Correspondance between logical operations on propositions and type-theoretic operations.

- True ↔ 1
- False ↔ 0
- A and B ↔ A × B
- A or B ↔ A + B
- If A, then: B ↔ A → B
- A iff B ↔ (A → B) × (B → A)
- Not A ↔ A → 0
- ∀x:A,P(x) ↔ Π(x:A),P(x)
- ∃x:A,P(x) ↔ Σ(x:A),P(x)

- These chapters of the book Homotopy Type Theory are considered:
Chapter 1: Type Theory

Chapter 5: Induction

Appendix A