08/10/12
defined subobject classifier, did examples for the category of Sets, Sets^(1+1),
groups acting on sets, monoids acting on sets
15/10/12
introduced sieves, proved the bijection between sieves on C and subfunctors of yC,
did the subobject classifier in the general case of Sets^(C^op)
introduced sheaves (of sets) for topological spaces, partially discussed
sheafification
22/10/12
discussed the subobject classifier in simplicial sets (as \n."co-scott-topology
on 2^n), discussed a generalization of the subobject classifier for graphs,
tried to find the connection. Tried to get it by collapsing standard simplices,
calculated the number of antichains in 2^n and concluded that the collapsing
will not work for cardinality reasons.
29/10/12
Paolo: reviewed smooth manifolds as a source of examples of bundles
(and sheaves), introduced tensor bundles and general vector bundles,
briefly mentioned complex manifolds, principal bundles and covering
maps.
Paolo: continued with germs and sheafification, stated that the sheaf
of sections of germs of a sheaf F is isomorphic to F, started a proof.
Christian: devised a purely categorical definition of the
sheafification functor for $\mathcal{C}$-valued sheafs, where
$\mathcal{C}$ is any category with colimits and equalizers.
05/11/12
discussed Christian's idea of defining * : Presheaves -> Sheaves (the Sheafification)
as a filtered colimit (works only in some cases)
started with Grothendieck topologies: definition of a topology in a small category,
definition of a base, some simple lemmas
12/11/12
skipped
19/11/12
Venanzio: repeated Grothendieck topology, base (basis), discussed topology generated
from base and vice versa, refinement of bases, bases and topologies for Heyting
algebras.
Observations: If X is a space, O(X) is a complete Heyting algebra. O(X)^op is a complete
lattice, but no Heyting algebra (no exponentials/no infinite distributiv law).
Further, a the notions of "complete lattice" and "complete small category" are the
same.
26/11/12
Venanzio continued with examples of topologies, defined sheaf over a topology,
+-construction with proof
3/12/12
Paolo started discussing elementary topoi
13/12/12 (replacement for 10/12)
Paolo continued with elementary topoi, in particular the construction of exponentials
[Christmas break]
06/02/13 (?)
Venanzio talked about subobjects as a Heyting Algebra
07/02/13 (?)
Nicolai: Categorical Semantics of Type Theory 0
11/02/13
Nicolai: Categorical Semantics of Type Theory I, Contextual Categories from universe
18/02/13
Nicolai: Categorical Semantics of Type Theory II - using a universe to get coherence (repetition), structure for 0, 1, identity types