Tuesday (and general) meeting log

organizer: Christian, more or less


21/02/12

- general discussion about the topic
- interests:
- higher dimensional type theory, model in simplicial sets, Voevodsky's completeness conjecture (Christian)
- topos theory, modern homotopy theory (in model categories), (abstract) homology (Nicolai)
- topos theory, completeness conjecture, category theory in (traditional?) homotopy theory (Venanzio)
- suggestions for books: "Sketches of an Elephant: A Topos Theory
   Compendium", "Sheaves in Geometry and Logic: A First Introduction to
   Topos Theory" (Venanzio)

today's topic: Homotopy Type Theory, motivation and inutition (speaker: Nicolai)

- repeated J and K
- J is true in the interpretation of identity proofs as paths in a space, but K is not
- can we, assuming K for identity proofs, get K for all other
- inductive types? [update: yes, K is enough to implement Pattern
   Matching, proved by Conor McBride - Nicolai]
- we can! (Venanzio) this justifies the treatment of identity types axiomatically (Christian)
- discussed Seely's interpretation in locally cartesian closed categories
- contexts: objects, types: morphisms, terms: sections
- "weird thing": morphisms can be both a type and a term
- this makes A isomorphic to Id_A
- discussed the notion of a "fibration", Serre fibration in homotopy theory

open questions:
- how to express the different notions of "fibrations" uniformely, can
they all be described by a lifting property in a specific diagram
(Christian)? - [updated] usually, fibrations carry this name because they are
fibrations in some model category, i.e. they can indeed be
characterized by a lifting propery (Nicolai)


06/03/12

topic: singular and simplicial homology (speaker: Christian)

- defined both notions of homology
- simplicial homology depends on choice of "simplicial cover"
- [I still think that it should be possible to prove the independence
 by simple induction] update: no, the so-called Hauptvermutung is wrong! 
- proof of the snake lemma (diagram chasing with "elements")
- proof that singular homology = simplicial homology


08/03/12

- first topic: my "proof" that (postulation any equations) uncanonical
numbers are equal to canonical ones [problem: type dependency]
(Nicolai)
- second topic: proof of the 5-lemma (Christian)
- general stuff in abelian categories (McLane)


20/03/12

topic: weak factorization systems and Awodey's model construction
(speaker: Nicolai)
- defined weak factorization system with examples
- repeated interpretation of contexts as objects, types as fibrations,
terms as sections, substitution as pullbacks and so on

comments/results of discussion:
- weakening rule needed
- rule "Gamma |- A type => Gamma.A |- a : A" needed
- proof of awodey's theorem - is it really complete?
- coherence conditions for j? E.g. if we construct j for Gamma and
Gamma.B, where B is not important?
- eta-rules for j? (Christian: eta is dual to beta)
- inductive types in general in this setting? (there is at least one
paper about inductive types in hott, see hott-blog)


19/04/12

planned