Skip to main content
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
Higher Inductive Types
Edit
0
6
…
0
Tags
No tags
Notify
RSS
Backlinks
Source
Print
Export (PDF)
Notes and code from Mike Shulman's Nov. 14 talk on a proposed general formulation of higher inductive types that could be implemented.
Lecture notes
(significantly expanded from the talk itself)
Coq code axiomatising “1dimensional Wtypes”
along the lines of this proposal (due to Peter L.)
Notes from Mike Shulman's Feb. 27 talk on semantics of higher inductive types in model categories (such as simplicial sets).
A rather dense note
describing in some more detail the construction of semantics sketched in the talk, including indices, parameters, and coherence.
Some blog posts about:
truncations
,
1HITs
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...
Notes from Mike Shulman's Feb. 27 talk on semantics of higher inductive types in model categories (such as simplicial sets).
 A rather dense note describing in some more detail the construction of semantics sketched in the talk, including indices, parameters, and coherence.
Some blog posts about: truncations, 1HITs