HoTT
UNDER CONSTRUCTION
- just reading chapter 6
- if you have been motivated to read together, feel free to contact me on twitter or gmail.
- Why not share infomation, interpretation of various topics?
# induction on equivalences are interesting
I think, when type theorist says equivalence it means the morphisms in ∞-groupoid i.e. Map(X,Y) for some X and Y which are the objects in a ∞-category.
So,
let me organize in ∞-category.
Datatypes : 0-morphism
Function : 1-morphism
Computation : 2-morphim
when we define an inductive data type, say A,
then PA also defines, A_ind which is function.
A is constructed over 1,Y
inductive A := a : A | y : Y -> A .
A_ind : forall P :A->Type, P(a)->(P(n)->(P(y(n)))->P(A)
# Quillen 's Model Categorical View
Let's abstract the HoTT World with Quillen's Model Categorical View.
These examples handle the same morphisms in proper categorical settings.
Homotopy Theory
- left : suspension $\Sigma := (S^n \mapsto S^{n+1})$
- right : looping space $\Omega := [S^1 ,-]$
Quillen's Classical Model
- left : cofibration (homotopy extension property)
- right : fibration
Segel's Simplicial Model
- left : cofibration
- right : fibration
Presheaf Topos (Externally)
- left : $\exists$
- right : $\forall$
Presheaf Topos (Internally)
- left : Σ
- right : Π
HoTT
- $\frac{a:A\vdash B(a):Type}{\vdash\Pi_{a:A} B(a):Type}$ ( `fibration` )
- $\frac{a:A\vdash B(a):Type}{\vdash\Sigma_{a:A} B(a):Type}$ ( `cofibration` )
and the $\Pi$ types and $\Sigma$ types in HoTT is the generalization of what is described in as follows;
Simple Type Theory
- left : product type $\times$
- right : abstraction type $\to$
# Adjunctions
- $p:Hom_\mathscr{E}(A,B)$
- (External Adjunction) $\exists_p \dashv p^{-1} \dashv \forall_p :Sub(A)\to Sub(B)$
- (Internal Adjunction) $\Sigma_p \dashv p^* \dashv \Pi_p : \mathscr{E}/A \to \mathscr{E}/B$
where $p^*$ is the pullback (inverse composition) of $p$
# Type Theory
# Homotopy Type Theory
## Eckmann-Hilton
## Univalence Axiom
# Set and Logics
# Martin Löf W-Types
## W-Types
## $Rec_W$ recursor
# Higher Induction Type
# Homotopy Theory
# Notes
my thoughts on SNS.
~~~
For me, the answer seems to be relevant with the grothendieck construction.
when we make a slice category C/X, we have an identity element in C/X.
and the element has stems (paths) reaching out the other elements.
( For the interpretation of ind_{=X} (D,d), the whole tree C/X seems to be D ( and its root seems to be d ? ) , if we apply this skelton tree of equivalences to some point a, we will get the whole space which is connected by path since it is groupoid i.e. morphisms in C/X are invertible.
An object of slice categories are a pair (c,f) where c is an object of C and f represents a particular instance of c.
so this is written as Σ-types ( dependent sum ) . c is e.g. the point , the edge, the triagle, ... and thus Σ-types represents exactly C/X . D has the type Π(x,y:X) Π(p: x=y) Univ , i.e. for any points in X and path p, there is some type.
We can interpret this " if we have path p:x=y then true " as the generators of C/X. Since this is category, its generators are morphism and in the case of groupoid they are paths. This is why I feel path induction seems to be relevant to grothendieck construction.
(edited) )
~~~
# HOL / Automation HOL
## History
Reference
- https://plato.stanford.edu/entries/type-theory-church/#AxioRuleInfe
## Type Theories
- RTT (Ramified Theory of Types)
- ETT (Elementary Theory of Types)
- STT (Simple Theory of Types)
- MTT (Martin-Löf Theory of Types)
# Coq / CIC
Formal CIC specification : https://coq.inria.fr/refman/language/cic.html#calculusofinductiveconstructions
- Sorts := {SProp, Prop, Type(i)}
- SProp : Strict Proposition which has a unique proof since all proofs are equivalent in it.
- Types are terms.
## Application
### CompCert
http://compcert.inria.fr
# The Difference between Isabelle/HOL & Coq
- https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t
Style of interaction
Both Coq and Isabelle/HOL are interactive theorem provers. They are languages for writing definitions and proofs about them; these proofs are checked by a computer to ensure that they have no mistakes. In both systems, one writes down a proof by giving commands that explain how to prove something. The way this happens on each system, however, varies.
Isabelle/HOL generally speaking has more mature support for "push-button" proof automation. For instance, it comes with the famous sledgehammer tactic, which invokes several external automatic theorem provers and solvers to try to prove a theorem. Coq also comes with many powerful proof automation procedures, such as omega or congruence, but they are not as generally applicable, and many theorems that can be solved with a single command in Isabelle/HOL require more explicit proofs in Coq.
Of course, this convenience comes with a price. I've been told that it is harder to have control over one's proof in Isabelle/HOL because the system tries to do a lot by itself. This is not a problem when proving simple theorems, but it becomes an issue when proof automation is not powerful enough and you need to tell the theorem prover how to proceed in greater detail.
The situation is a bit different when supporting user-defined, proof-automation procedures. Coq comes with a tactic language for writing proofs, known as Ltac, that is a programming language of its own right. Even though Ltac has some design problems, it does allow users to encode fairly complicated proof automation procedures in a lightweight manner. For heavier tasks, Coq also allows users to write plugins in Coq's implementation language, OCaml. In Isabelle/HOL, in contrast, there is no higher-level automation language like Ltac, and the only way the user can program custom proof automation procedures is with plugins.
# Homotopy Type Theory
deduction
- P → Q (conditional statement)
- P (hypothesis stated)
- Q (conclusion deduced)
- a inhabitant of a type : a proposition
- set theory : first order logic & an axiom on it
- type theory : non
- set theory : set & proposition
- type theory : type
_ | set theory | type theory
-----------|--------------------------------------|-------------
foundation | first order logic
an axiom on it | non
_ | set & proposition | type
_ | "a $ \in $ A" (proposition) | "a:A" judgment
equality | a proposition | a type
### deductive type system
- a deductive system : **rules** for deriving things **judgment**
- a judgment "proposition A has a proof"
- a rule "from A and B infer A $ \land $ B"
### type theory
- a judgment "a:A" ("a" in proposition A is "a witness to the provability of A" or "an evidence that A is true")
"let a:A" is a atomic statement in type theory
- equality in set theory : a proposition
- equality in type theory : a type
"a,b : A" means we have a type "a =A b" called "a and b is propositionally equal"
an equality judgment
- "judgment equality" "a $ \equiv $ b : A"
- "equality" is "a conclusion of the deductive system of a type theory "
Group
- judgements : elements of a Group
- rules : operation
- judgements equality : equality of elements of a Group
context : generator
### some note references
- contextual categories
- categories with families
- comprehension categories [Lurie]
- type-theoritic fibration categories [Shulman 2015]
- categorical description of "logical relations" [Hermida, 1933]
- free theorems [Wadler ,1989]