- Talk 1: Computer Science and Homotopy Theory
- Think of ZFC sets as rooted trees. Have two axioms:
- (1) all branches of all vertices are non-isomorphic (otherwise a set would have two copies of the same element)
- (2) Each leaf must be at finite depth from the root.
- This is horrible to work with, so type theory!
- Talk 2: What if foundations of math is inconsistent?
- We "know" that first order math is consistent. We can prove that it is impossibleto prove that first order math is consistent!
- Choice 1: If we "know" FOL is consistent, then we should be able to transformthis knowledge into a proof, then 2nd incompleteness is false.
- Choice 2: Admit "transcendental" part of math, write dubious philosophy.
- Choice 3: Admit that our sensation that FOL +arithmetic is consistent is an illusionand admit that FOL arithmetic is inconsistent.
- Time to consider Choice 3 seriously?

- Special symbols, names of variables.
- Syntactic rules.
- Deduction rules: Construct new closed formulas from old closed formula.
- Axioms: collection of closed formulas.

`∀, ∃, ⇒, !(not)`

and so on. First order theory is
inconsistent if there a closed formula $A$ such that both $A$ and $!A$ is a
theorem.
- Free variables describe subsets. Eg:
`∃ n: n^2 = m`

describes the set`{ m : ∃ n: n^2 = m }`

. - It's possible to construct subsets (formulae with one free variable) whosemembership is undedicable. So you can prove that it is impossible to sayanything whatsoever about these subsets.

- Inconsistency of FOL implies inconsistency of many other systems(eg. set theory).
- Inconsistency of FOL implies inconsistency of
*constructive*(intuitionistic)mathematics! (WTF?) shown by Godel in 1933. Takes a proof of contradictionin classical and strips off LEM. - We need foundations that can create
*reliable proofs*beinginconsistent!*despite* - Have systems that react to inconsistency in less drastic ways.One possible candidate is constructive type theories.A proof of a formula in such a system is itself a formula in the system.There are no deduction rules, only syntactic rules. So a proof is an objectthat can be studied in the system. If one has a proof of contradiction,then such a proof can be detected --- they have certain properties that canbe detected by an algorithm (what properties?)

- Formalize a problem.
- Construct creative solution.
- Submit proof to a "reliable" verifier. If the verifier terminates, we are done. If the verifier does not terminate, we need to look for other proofs thatcan terminate.
- our abstract thinking cancels out by normalisation :P

- Correct interpretation of 2nd incompleteness is a step of proof of inconsistencyof FOL (Conjecture).
- In math, we need to learn how to use inconsistent theories to obtain reliableproofs. Can lead to more freedom in mathematical workflow.

- Was uncertain about future when working on 2-categories and higher math. No way to ground oneself by doing "computations" (numerical experiments).To make it worse, the existing foundations of set theory is bad for thesetypes of objects.
- Selected papers on Automath.
- Overcoming category theory as new foundations was very difficult for vovodesky.
- Categories are "higher dimensional sets"? NO! Categories are "posets in the next dimension".Correct version of "sets in the next dimension" are groupoids (WHY?)MathOverflow question
- Grothendeick went from isomorphisms to all morphisms, this prevented him fromgravitating towards groupoids.
- Univalent foundations is a complete foundational system.
- Sets are groupoids on the next dimension

- Univanent type theory is arrived at by adding univalence to MLTT.
- Goal of univalent foundations is to apply UTT to foundations.
- Univalence is to type theory what induction principle is to peano arithmetic
- Univalence implies descent. Descent implies Blakers Massey-theorem, whichimplies Goodwille calculus.

- The syntactic system of type theory is a
.*tribe* - A clan is a category equipped with a class of
*carrable maps*called fibrations.A map is carrable if we can pull it back along any other map. - A clan is a category along with maps called "fibrations", such that (1) everyisomorphism is a fibration, (1) closed under composition, (3) fibrations arecarrable, (4) base change of fibration is a fibration, (4) Category has a terminalobject, and map into the terminal object is a fibration.
- A map $u: A \rightarrow B$ is
if it does something good with respectto fibrations.*anodyne* - A
is a clan such that (1) base chnge of anodyne along fibration is anodyne,(2) every map factorizes as anodyne followed by fibration.*tribe* - Kan complexes form a tribe. A fibration is a Kan fibration. A map is anodynehere if it is a monomorphism and a homotopy equivalence.
- Given a tribe $E$, can build a new tribe by slicing $E/A$ (this is apparentlyvery similar to things people do in Quillen Model categories).
- A tribe is like a commutative ring. We can extend by adding new variables to getpolynomial rings. An elementary extension is extending the tribe by adding a newelement.
- If $E$ is a tribe, an object of $E$ is a type. We write
`E |- A : Type`

. - If we have a map $a: 1 -> A$, we regard this as an element of A:
`E |- a : A`

. - A fibration is a family of objects. This is a dependent type
`x : A |- E(x): Type`

.`E(x)`

is the fiber of`p: E -> A`

at a variable element`x : A`

. - A section of a fibration gives an element of the fibration. We write this as
`x : A |- s(x) : E(x)`

.`s(x)`

denotes the value of`s: A -> E`

of a variableelement`x : A`

. (Inhabitance is being able to take the section of a fiber bundle?!) - change of parameters / homomorphism is substitution.

```
y : B |- E(y) : Type
--------------------
x : A |- E(f(x)) : Type
```

This is pulling back along fibrations.
- Elementary extension
`E -> E(A)`

are called as context extensions.

```
|- B : Type
-----------
x : A |- B : Type
```

- A map between types is a variable element
`f(x) : B`

indexed by`x : A`

```
x : A |- f(x) : B
```

- Sigma formation rule: The total space of the union is the sum of all fibers(?)

```
x: A |- E(x): Type
------------------
|- \sum{x : A}E(x): Type
```

```
x: A |- E(x): Type
------------------
y : B |- \sum{x : f^{-1}(y)}E(x): Type
```

- Path object for $A$ is obtained by factorial diagonal map
`diag: a -> (a, a)`

as an anodynemap`r: A -> PA`

followed by a fibration`(s, t) : PA -> A x A`

.

- A homotopy
`h: f ~ g`

between two maps`f, g : A -> B`

is a map`h: A -> PB`

such that`sh = f`

and`th = g`

. homotopy is a congruence. -
`x: A, y : A |- Id_A(x, y) : Type`

called the identity type of A. - An element
`p: Id_A(x, y)`

is a proof that`x =A y`

. - Reflexivity term
`x : A |- r(x) : Id_A(x, x)`

which proves`x =A x`

. - The identity type is a path object
- $\gamma(x, y): Id_A(x, y) -> Eq(E(x), E(y))$. $\gamma$ is some kind ofconnection: given a path from $x$ to $y$, it lets us transport $E(x)$ to $E(y)$,where the $Eq$ is the distortion from the curvature?