Skip to main content
Try Wikispaces Classroom now.
Brand new from Wikispaces.
guest
Join

Help

Sign In
UFIAS2012
Home
guest

Join

Help

Sign In
UFIAS2012
Wiki Home
Projects
Recent Changes
Pages and Files
Members
Favorites
20
All Pages
20
Home
Calendar
Categorical Semantics WG
Coq for UF
Coq Working Group
Definitional Equality
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
HomotopyGroupsOfSpheres
how to add a plugin
IAS program participants
Informal Type Theory
Logical Frameworks
Math in HoTT
Meaning Explanations
Modal type theory
Notation and terminology
Notes
Open Problems
see more
Add
Add "All Pages"
Done
Math in HoTT
Edit
0
15
…
0
Tags
No tags
Notify
RSS
Backlinks
Source
Print
Export (PDF)
Page for the working group on math in HoTT. Please add what you're working on, or ideas, or descriptions of the ideas below.
Done
See
Formalized Homotopy Theory
What people are working on
See
Formalized Homotopy Theory
Descent theorem and toposes: Egbert
Sets and truncation: Bas and Egbert
Thorsten and students are working on 1truncations and the connection to Hedberg's theorem
Univalent categories (doing category theory nicely in HoTT): Mike, Benedikt, and Chris
Higher groupoids and quotient types: Steve/Guillaume/Thorsten at least
Idea for things to work on
homology: see the answer to the following question
http://mathoverflow.net/questions/78450/homologytheoryconstructedinahomotopyinvariantway
)
stable homotopy theory
Postnikov towers
Covering spaces and actions of fundamental groups on covering spaces
simple results in cohesive HoTT
limit sketches
start going through Lurie's book and formalizing things
formalizing higher category theory
See also the page on
Open Problems
and
Formalized Homotopy Theory
Javascript Required
You need to enable Javascript in your browser to edit pages.
help on how to format text
Turn off "Getting Started"
Home
...
Loading...
Done
What people are working on
Thorsten and students are working on 1truncations and the connection to Hedberg's theorem
Idea for things to work on
See also the page on Open Problems and Formalized Homotopy Theory