Homotopy Type Theory
Latest Revisions

• 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 ( limited principle of omniscience(rev # 1) | history )
  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
• inductive-recursive type ( inductive-recursive 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
• inductive-inductive type ( inductive-inductive type(rev # 3) | history )
  by Bas Spitters at June 3, 2014 at 04:20:43
• inductive-inductive type ( inductive-inductive type(rev # 2) | history )
  by Alexis Hazell? at June 3, 2014 at 02:41:28
• inductive-inductive type ( inductive-inductive 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? 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
• Martin-Löf Type Theory ( Martin-Lö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 Martin-Löf ( Per Martin-Lö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
• loop space of a wedge of circles ( loop space of a wedge of circles(rev # 2) | history )
  by Alexis Hazell? at May 10, 2014 at 20:33:27
• model invariance problem ( model invariance problem(rev # 2) | history )
  by Alexis Hazell? at May 10, 2014 at 20:27:44
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 5) | history )
  by Alexis Hazell? at May 10, 2014 at 20:24:49
• Martin-Löf Type Theory ( Martin-Löf Type Theory(rev # 2) | history )
  by Alexis Hazell? at May 10, 2014 at 20:22:18
• universe ( universe(rev # 6) | history )
  by Alexis Hazell? at May 10, 2014 at 20:17:30
• type theories ( type theories(rev # 6) | history )
  by Alexis Hazell? at May 10, 2014 at 20:15:33
• type theory ( type theory(rev # 1) | history )
  by Alexis Hazell? at May 9, 2014 at 22:04:43
• type theories ( type theories(rev # 5) | history )
  by Alexis Hazell? at May 9, 2014 at 22:03:17
• dependent type ( dependent type(rev # 1) | history )
  by Alexis Hazell? at May 9, 2014 at 21:56:20
• universe ( universe(rev # 5) | history )
  by Alexis Hazell? at May 9, 2014 at 21:55:37
• Agda ( Agda(rev # 3) | history )
  by Alexis Hazell? at May 9, 2014 at 21:50:00
• open problems ( open problems(rev # 24) | history )
  by Alexis Hazell? at May 9, 2014 at 21:49:03
• inductive-recursive type ( inductive-recursive type(rev # 1) | history )
  by Alexis Hazell? at May 9, 2014 at 21:47:47
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 4) | history )
  by Alexis Hazell? at May 9, 2014 at 21:32:43
• Homotopy Type System ( Homotopy Type System(rev # 6) | history )
  by Alexis Hazell? at May 9, 2014 at 02:40:26
• Categorical Homotopy Type Theory ( Categorical Homotopy Type Theory(rev # 2) | history )
  by Alexis Hazell? at May 9, 2014 at 02:33:26
• Agda ( Agda(rev # 2) | history )
  by Alexis Hazell? at May 9, 2014 at 02:20:53
• type theories ( type theories(rev # 4) | history )
  by Alexis Hazell? at May 9, 2014 at 02:20:14
• Martin-Löf Type Theory ( Martin-Löf Type Theory(rev # 1) | history )
  by Alexis Hazell? at May 9, 2014 at 02:19:32
• open problems ( open problems(rev # 23) | history )
  by Alexis Hazell? at May 9, 2014 at 02:18:10
• definitional equality ( definitional equality(rev # 7) | history )
  by Alexis Hazell? at May 9, 2014 at 02:07:40
• universe ( universe(rev # 4) | history )
  by Alexis Hazell? at May 9, 2014 at 02:04:39
• loop space ( loop space(rev # 2) | history )
  by Alexis Hazell? at May 9, 2014 at 02:02:50
• type theories ( type theories(rev # 3) | history )
  by Steve Awodey at May 9, 2014 at 00:41:23
• HomePage ( HomePage(rev # 6) | history )
  by Steve Awodey at May 9, 2014 at 00:37:51
• HoTT book ( HoTT book(rev # 1) | history )
  by Steve Awodey at May 9, 2014 at 00:36:58
• Homotopy Type System ( Homotopy Type System(rev # 5) | history )
  by Alexis Hazell? at May 4, 2014 at 23:19:11
• Homotopy Type System ( Homotopy Type System(rev # 4) | history )
  by Mike Shulman at May 4, 2014 at 06:35:08
• Homotopy Type System ( Homotopy Type System(rev # 3) | history )
  by Mike Shulman at May 3, 2014 at 21:00:01
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 3) | history )
  by Mike Shulman at May 3, 2014 at 12:29:23
• univalence axiom ( univalence axiom(rev # 7) | history )
  by Mike Shulman at May 3, 2014 at 12:28:55
• universe ( universe(rev # 3) | history )
  by Mike Shulman at May 3, 2014 at 12:28:32
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 2) | history )
  by Mike Shulman at May 2, 2014 at 13:54:28
• universe ( universe(rev # 2) | history )
  by Mike Shulman at May 2, 2014 at 12:18:36
• elementary (infinity,1)-topos
  by Bas Spitters at April 25, 2014 at 02:59:11
• HomePage ( HomePage(rev # 5) | history )
  by Martin Escardo? at April 18, 2014 at 12:22:25
• open problems ( open problems(rev # 22) | history )
  by Bas Spitters at April 16, 2014 at 23:23:37
• open problems ( open problems(rev # 21) | history )
  by Bas Spitters at April 6, 2014 at 23:10:28
• David Roberts ( David Roberts(rev # 1) | history )
  by David Roberts at March 31, 2014 at 18:07:58
• Formalized Homotopy Theory ( Formalized Homotopy Theory(rev # 3) | history )
  by David Roberts at March 31, 2014 at 18:06:55
• universe ( universe(rev # 1) | history )
  by Mike Shulman at March 31, 2014 at 11:54:13
• semantics ( semantics(rev # 8) | history )
  by Anonymous? at March 24, 2014 at 12:53:56
• semantics ( semantics(rev # 7) | history )
  by Steve Awodey at March 24, 2014 at 08:59:24
• Categorical Homotopy Type Theory ( Categorical Homotopy Type Theory(rev # 1) | history )
  by Steve Awodey at March 24, 2014 at 08:54:17
• higher inductive type ( higher inductive type(rev # 3) | history )
  by Mike Shulman at March 17, 2014 at 09:57:25
• Agda ( Agda(rev # 1) | history )
  by Mike Shulman at March 17, 2014 at 08:45:43
• Homotopy Type System ( Homotopy Type System(rev # 2) | history )
  by Mike Shulman at March 11, 2014 at 06:46:49
• open problems ( open problems(rev # 20) | history )
  by Mike Shulman at March 11, 2014 at 06:33:57
• model invariance problem ( model invariance problem(rev # 1) | history )
  by Mike Shulman at March 11, 2014 at 06:33:43