Department of Mathematics
Indian Institute of Science
Bangalore
Words and Rules
Sets and Predicate Calculus
Why we need new foundations
“ Since the first half of the 20th century mathematics has been presented as a science based on ZFC and ZFC was introduced as a particular theory in Predicate Logic.
“ Therefore someone who wanted to get to the bottom of things in mathematics had a simple road to follow - learn what Predicate Logic is, then learn a particular theory called ZFC, then learn how to translate propositions about a few basic mathematical concepts into formulas of ZFC, and then learn to believe, through examples, that the rest of mathematics can be reduced to these few basic concepts.”
“ The roadblock that prevented generations of interested mathematicians and computer scientists
from solving the problem of computer verification of mathematical reasoning was the
unpreparedness of foundations of mathematics for the requirements of this task.”
“ Formulating mathematical reasoning in a language precise enough for a computer to follow
meant using a foundational system of mathematics not as a standard of consistency applied only
to establish a few fundamental theorems, but as a tool that can be employed in everyday
mathematical work. ”
Syntax with types
Types for sets
Propositions as Types
Fix a type family $B : A \to \mathfrak{U}$.
Let $A$ and $B$ be types, regarded as representing propositions.
Terms, Types, Rules
Inductive types
Propositions as types
Proofs by inductions
In programming language design, a first-class citizen (also type, object, entity, or value) in a given programming language is an entity which supports all the operations generally available to other entities. These operations typically include being passed as an argument, returned from a function, and assigned to a variable.
data Bool : Type where
true : Bool
false : Bool
idBool : Bool → Bool -- lambda
idBool x = x
alwaysTrue : Bool → Bool
alwaysTrue x = true
not : Bool → Bool -- case defn
not true = false
not false = true
notnot : Bool → Bool -- lambda
notnot x = not(not(x))
_&_ : Bool → Bool → Bool --curried function
true & x = x
false & _ = false
data ℕ : Type where -- infinite type
zero : ℕ
succ : ℕ → ℕ
even : ℕ → Bool -- recursive definition
even zero = true
even (succ x) = not (even x)
_+_ : ℕ → ℕ → ℕ
zero + y = y
(succ x) + y = succ (x + y)
data ℕList : Type where --list type
[] : ℕList -- empty list
_::_ : ℕ → ℕList → ℕList -- add number to head of list
mylist : ℕList
mylist = 3 :: (4 :: (2 :: [])) -- the list [3, 4, 2]
data Vector : ℕ → Type where -- inductive type family
[] : Vector 0
_::_ : {n : ℕ} → ℕ → Vector n → Vector (succ n)
countdown : (n : ℕ) → Vector n -- dependent function
countdown 0 = []
countdown (succ n) = (succ n) :: (countdown n)
sum : {n : ℕ} → Vector n → ℕ
sum [] = 0
sum (x :: l) = x + sum l
sumToN : ℕ → ℕ -- calculation
sumToN n = sum(countdown n)
data isEven : ℕ → Type where
0even : isEven 0
+2even : (n : ℕ) → isEven n → isEven (succ(succ(n)))
4even : isEven 4
4even = +2even _ (+2even _ 0even)
data False : Type where
1odd : isEven 1 → False
1odd ()
3odd : isEven 3 → False
3odd (+2even .1 ())
half : (n : ℕ) → isEven n → ℕ
half .0 0even = 0
half .(succ (succ n)) (+2even n pf) = succ(half n pf)
double : ℕ → ℕ
double 0 = 0
double (succ n) = succ(succ(double(n)))
thm : (n : ℕ) → isEven (double n)
thm zero = 0even
thm (succ n) = +2even _ (thm n)
halfOfDouble : ℕ → ℕ
halfOfDouble n = half (double n) (thm n)
data True : Type where
qed : True
data False : Type where
data _×_ (A B : Type) : Type where
_,_ : A → B → A × B
data _⊕_ (A B : Type) : Type where
ι₁ : A → A ⊕ B
ι₂ : B → A ⊕ B
data Σ (A : Type) (B : A → Type) : Type where
_,_ : (a : A) → (B a) → Σ A B
data _==_ {A : Type} : A → A → Type where
refl : (a : A) → a == a
sym : {A : Type} → {x y : A} → (x == y) → (y == x)
sym (refl a) = refl a
_&&_ : {A : Type} → {x y z : A} → (x == y) → (y == z) → (x == z)
(refl a) && (refl .a) = refl a
Equality and Paths
$\infty$-groupoids from induction for equality
Type families as fibrations
Homotopy $n$-types (dimension)
Classifying spaces and Univalence
Synthetic homotopy theory
In analogy with attaching cells of dimension $2$ and above, we can introduce (consistent) rules for introducing higher inductive types.
In the other direction, by axiomatizing type theoretic principles, we can develop synthetic homotopy theory, where the primitive concepts are spaces, points, maps, paths etc. but without requiring sets or topologies on them.