Les Lightning Talk on HoTT - HoTT for Bluffers

* Les: Getting more comfortable with HoTT - Talk: "Bluffers Guide to HoTT"
	History - Barber's Paradoxes, etc.
	Russell stratifying set theory
	Martin Löf in the 1970s
	In TT - Say term x is of type t -> `x : t`
	This is a judgement
	Curry howard - Types and terms = Conjecture/proposition and Proof
	Things become interesting in the presence of equality
	equality is always with respect to some type
	exists t -> x:t = y:t
	can also think of this as a type: The type of all proofs that x=y
	e.g. 2+3 = 3+2
		Proof by reduciton
		Proof by commutivity of addition
		In TT you can have different proofs of things being equal,
		or think of things being equal in two different ways
	Proofs are also terms, so you can discuss equality of proofs
	There is a structure where you can have different proofs of a proposition,
		but those proofs may or may not be "equal"
		topology or homotopy analogies come into play here
	Equality proofs are paths in the space of objects
		There can also be paths between paths equating proofs
	There is an infinite hierarchy of these correspondence proofs
	Ties into Vladimir Vodovosky's work - Univalence Axiom
	Isomorphism and equality aren't always the same thing
	Mathematicians sometimes will after proof of isomorphism treat objects as equal,
		and lose the provenance
	"Equivalence is equivalent to equality" - Formalised in TT
	This is useful because it provides a fomal basis for common idioms in mathematics
	HoTT people are promoting HoTT as a new foundation of Math
	Vod: Provides a better foundation for mathematics and points out that it matches
		the practice of mathematicians better
	No types in ST
	Bob-Harper:
		"Doing math in ST is like programming
		 in machine code and doing it in TT is like using a HL language"
	UniMath - Coq library that formalises a lot of math as code
	HoTT people did the development of the book as a colab through git!
		100s of mathematicians contributed
	Two formulations of the reals
		- Cauchy sequences
		- Dedekind cuts
	In traditional math these are two approaches to the same thing
	Some work in HoTT was to define both of these in terms of TT and
		shown to be inequivalent without LEM
	i.e. decidable, vs. undecidable
	Proof by contradiction
	One of the problems with HOTT - when invoking univalent axiom you lose computability of proofs
	Bob Harper developed similar approach - CCTT "Cartesian Cubical Type Theory"
		A slightly different approach that preserves computation.
	Back to LEM - In TT - Based on intuitionistic logic - Two things can happen
		- LEM not baked in but can assume if convenient
		- In many situations you can prove LEM in certain circumstances WO axiom
			E.g. Nats
		In FO Predicate calculus LEM baked in
	Often told "in constructive logic you can't use proof by contradiction"
		That's a characature of the actual situation - of course you can use it in TT - it's definitional
		In constructive logic - while you can't prove p by assuming not p and arriving at contradition,
		But you can prove not p by equivalent procedure