Homotopy Type Theory
Latest Revisions
Skip the Navigation Links

Home Page

All Pages

Latest Revisions

Authors

open problems
(
open problems(rev # 35)

history
)
by
Bas Spitters
at July 13, 2015 at 07:53:07
open problems
(
open problems(rev # 34)

history
)
by
Bas Spitters
at July 13, 2015 at 07:01:10
References
(
References(rev # 4)

history
)
by
Mike Shulman
at June 29, 2015 at 14:52:11
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 14)

history
)
by
Bas Spitters
at June 24, 2015 at 05:40:27
universe
(
universe(rev # 18)

history
)
by
Bas Spitters
at June 24, 2015 at 05:38:35
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 13)

history
)
by
Mike Shulman
at June 24, 2015 at 00:34:25
universe
(
universe(rev # 17)

history
)
by
Mike Shulman
at June 24, 2015 at 00:34:23
semisimplicial types
(
semisimplicial types(rev # 3)

history
)
by
Anonymous Coward
?
at June 17, 2015 at 18:36:03
universe
(
universe(rev # 16)

history
)
by
Bas Spitters
at June 4, 2015 at 04:28:30
References
(
References(rev # 3)

history
)
by
David Roberts
at April 23, 2015 at 03:10:18
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 12)

history
)
by
Urs Schreiber
at April 13, 2015 at 11:13:02
References
(
References(rev # 2)

history
)
by
Mike Shulman
at March 28, 2015 at 13:01:53
algebraic formulation of dependent type theory
(
algebraic formulation of dependent type theory(rev # 2)

history
)
by
Bas Spitters
at March 15, 2015 at 00:37:33
realizability
(
realizability(rev # 2)

history
)
by
Bas Spitters
at March 15, 2015 at 00:01:43
algebraic formulation of dependent type theory
(
algebraic formulation of dependent type theory(rev # 1)

history
)
by
Bas Spitters
at March 14, 2015 at 17:26:33
realizability
(
realizability(rev # 1)

history
)
by
Bas Spitters
at March 14, 2015 at 16:59:43
Formalized Homotopy Theory
(
Formalized Homotopy Theory(rev # 6)

history
)
by
ecavallo
?
at March 1, 2015 at 01:13:41
HomePage
(
HomePage(rev # 14)

history
)
by
Floris van Doorn
at February 28, 2015 at 16:23:16
HomePage
(
HomePage(rev # 13)

history
)
by
Mike Shulman
at February 11, 2015 at 05:35:03
open problems
(
open problems(rev # 33)

history
)
by
Mike Shulman
at February 10, 2015 at 04:20:14
open problems
(
open problems(rev # 32)

history
)
by
Bas Spitters
at January 20, 2015 at 16:33:22
equivalence of precategories
(
equivalence of precategories(rev # 1)

history
)
by
Bas Spitters
at January 18, 2015 at 03:34:02
Formalized Homotopy Theory
(
Formalized Homotopy Theory(rev # 5)

history
)
by
Bas Spitters
at January 18, 2015 at 03:32:27
Carlo Angiuli
(
Carlo Angiuli(rev # 1)

history
)
by
Carlo Angiuli
at January 17, 2015 at 20:44:07
Formalized Homotopy Theory
(
Formalized Homotopy Theory(rev # 4)

history
)
by
Carlo Angiuli
at January 17, 2015 at 20:34:08
open problems
(
open problems(rev # 31)

history
)
by
Bas Spitters
at January 16, 2015 at 21:44:53
HomePage
(
HomePage(rev # 12)

history
)
by
Bas Spitters
at January 16, 2015 at 20:58:52
proof theoretic strength of univalent type theory plus HITs
(
proof theoretic strength of univalent type theory plus HITs(rev # 2)

history
)
by
Ulrik Buchholtz
at January 15, 2015 at 20:44:12
proof theoretic strength of univalent type theory plus HITs
(
proof theoretic strength of univalent type theory plus HITs(rev # 1)

history
)
by
Bas Spitters
at January 12, 2015 at 19:27:53
open problems
(
open problems(rev # 30)

history
)
by
Bas Spitters
at January 12, 2015 at 18:48:11
HomePage
(
HomePage(rev # 11)

history
)
by
Anonymous Coward
?
at December 15, 2014 at 02:57:22
References
(
References(rev # 1)

history
)
by
Anonymous Coward
?
at December 4, 2014 at 20:23:48
HomePage
(
HomePage(rev # 10)

history
)
by
Anonymous Coward
?
at December 4, 2014 at 20:01:26
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 11)

history
)
by
Urs Schreiber
at November 21, 2014 at 15:50:03
universe
(
universe(rev # 15)

history
)
by
Urs Schreiber
at November 21, 2014 at 15:49:40
Agda
(
Agda(rev # 6)

history
)
by
Piyush P Kurur
?
at November 16, 2014 at 16:29:38
Agda
(
Agda(rev # 5)

history
)
by
Piyush P Kurur
?
at November 13, 2014 at 10:31:03
Agda
(
Agda(rev # 4)

history
)
by
Piyush P Kurur
?
at November 13, 2014 at 07:41:28
open problems
(
open problems(rev # 29)

history
)
by
Jason Gross
at November 10, 2014 at 06:39:35
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 10)

history
)
by
Urs Schreiber
at October 24, 2014 at 08:16:09
universe
(
universe(rev # 14)

history
)
by
Urs Schreiber
at October 23, 2014 at 14:03:47
Grothendieck (infinity,1)topos
by
Urs Schreiber
at October 22, 2014 at 03:09:48
universe
(
universe(rev # 13)

history
)
by
Urs Schreiber
at October 17, 2014 at 15:45:18
DenisCharles Cisinski
by
Urs Schreiber
at October 17, 2014 at 15:44:25
Cesare Gallozzi
by
Urs Schreiber
at October 17, 2014 at 15:43:02
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 9)

history
)
by
Urs Schreiber
at October 17, 2014 at 15:42:04
Homotopy Type System
(
Homotopy Type System(rev # 10)

history
)
by
Bas Spitters
at October 13, 2014 at 16:05:15
Homotopy Type System
(
Homotopy Type System(rev # 9)

history
)
by
Bas Spitters
at October 8, 2014 at 14:51:38
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 8)

history
)
by
Bas Spitters
at October 1, 2014 at 14:38:50
de Morgan's law
by
Mike Shulman
at September 2, 2014 at 12:44:56
axioms
(
axioms(rev # 2)

history
)
by
Mike Shulman
at September 2, 2014 at 12:37:16
limited principle of omniscience
by
Mike Shulman
at August 30, 2014 at 10:53:44
axioms
(
axioms(rev # 1)

history
)
by
Mike Shulman
at August 30, 2014 at 10:47:29
Uniqueness of Identity Proofs
(
Uniqueness of Identity Proofs(rev # 2)

history
)
by
Mike Shulman
at August 30, 2014 at 10:44:30
Homotopy Type System
(
Homotopy Type System(rev # 8)

history
)
by
Andrej Bauer
?
at August 29, 2014 at 09:37:07
open problems
(
open problems(rev # 28)

history
)
by
Bas Spitters
at July 1, 2014 at 23:20:12
universe
(
universe(rev # 12)

history
)
by
Cesare Gallozzi
at June 25, 2014 at 05:15:53
inductiverecursive type
(
inductiverecursive type(rev # 2)

history
)
by
Alexis Hazell
?
at June 8, 2014 at 18:46:28
open problems
(
open problems(rev # 27)

history
)
by
Alexis Hazell
?
at June 8, 2014 at 18:13:55
universe
(
universe(rev # 11)

history
)
by
Mike Shulman
at June 6, 2014 at 19:13:55
universe
(
universe(rev # 10)

history
)
by
Mike Shulman
at June 4, 2014 at 05:43:45
about
(
about(rev # 4)

history
)
by
Alexis Hazell
?
at June 3, 2014 at 19:35:20
Resources
(
Resources(rev # 6)

history
)
by
Alexis Hazell
?
at June 3, 2014 at 19:34:43
open problems
(
open problems(rev # 26)

history
)
by
Alexis Hazell
?
at June 3, 2014 at 19:33:46
universe
(
universe(rev # 9)

history
)
by
Mike Shulman
at June 3, 2014 at 08:31:59
inductiveinductive type
(
inductiveinductive type(rev # 3)

history
)
by
Bas Spitters
at June 3, 2014 at 04:20:43
inductiveinductive type
(
inductiveinductive type(rev # 2)

history
)
by
Alexis Hazell
?
at June 3, 2014 at 02:41:28
inductiveinductive type
(
inductiveinductive type(rev # 1)

history
)
by
Bas Spitters
at June 3, 2014 at 01:29:51
Resources
(
Resources(rev # 5)

history
)
by
steve awodey
?
at May 31, 2014 at 06:52:25
semantics
(
semantics(rev # 11)

history
)
by
Mike Shulman
at May 30, 2014 at 05:08:56
natural model
by
Mike Shulman
at May 30, 2014 at 05:08:10
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 7)

history
)
by
Mike Shulman
at May 30, 2014 at 05:07:37
semantics
(
semantics(rev # 10)

history
)
by
Anonymous Coward
?
at May 29, 2014 at 09:16:10
universe
(
universe(rev # 8)

history
)
by
Mike Shulman
at May 29, 2014 at 05:17:57
HoTT book
(
HoTT book(rev # 3)

history
)
by
Mike Shulman
at May 29, 2014 at 05:13:53
topos
by
Bas Spitters
at May 29, 2014 at 04:20:09
semantics
(
semantics(rev # 9)

history
)
by
steve awodey
?
at May 28, 2014 at 05:16:20
definitional equality
(
definitional equality(rev # 8)

history
)
by
Mike Shulman
at May 21, 2014 at 07:37:06
open problems
(
open problems(rev # 25)

history
)
by
Steve Awodey
at May 18, 2014 at 02:30:49
HomePage
(
HomePage(rev # 9)

history
)
by
Steve Awodey
at May 18, 2014 at 02:30:15
Resources
(
Resources(rev # 4)

history
)
by
Steve Awodey
at May 16, 2014 at 05:51:32
Uniqueness of Identity Proofs
(
Uniqueness of Identity Proofs(rev # 1)

history
)
by
Alexis Hazell
?
at May 15, 2014 at 16:52:05
Dan Grayson
(
Dan Grayson(rev # 1)

history
)
by
Daniel R. Grayson
at May 15, 2014 at 15:52:32
HoTT book
(
HoTT book(rev # 2)

history
)
by
Mike Shulman
at May 15, 2014 at 08:45:43
circle
(
circle(rev # 1)

history
)
by
Mike Shulman
at May 15, 2014 at 08:38:29
higher inductive type
(
higher inductive type(rev # 4)

history
)
by
Mike Shulman
at May 15, 2014 at 08:32:07
Resources
(
Resources(rev # 3)

history
)
by
Alexis Hazell
?
at May 15, 2014 at 01:02:51
Resources
(
Resources(rev # 2)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 22:42:32
HomePage
(
HomePage(rev # 8)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 20:23:30
Homotopy Type System
(
Homotopy Type System(rev # 7)

history
)
by
Mike Shulman
at May 14, 2014 at 11:49:12
model of type theory in an (infinity,1)topos
(
model of type theory in an (infinity,1)topos(rev # 6)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 01:56:10
dependent type
(
dependent type(rev # 3)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 01:55:04
Resources
(
Resources(rev # 1)

history
)
by
Steve Awodey
at May 14, 2014 at 01:39:15
MartinLöf Type Theory
(
MartinLöf Type Theory(rev # 3)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 00:39:46
type theory
(
type theory(rev # 2)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 00:37:50
dependent type
(
dependent type(rev # 2)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 00:35:56
universe
(
universe(rev # 7)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 00:27:52
type
(
type(rev # 1)

history
)
by
Alexis Hazell
?
at May 14, 2014 at 00:26:55
Per MartinLöf
(
Per MartinLöf(rev # 1)

history
)
by
Alexis Hazell
?
at May 13, 2014 at 01:00:36
HomePage
(
HomePage(rev # 7)

history
)
by
Alexis Hazell
?
at May 13, 2014 at 00:41:40
« Previous
1
2
3
4
5
6
7
8
9
Next »