Homotopy Type Theory
Latest Revisions

• CMU local activities ( CMU local activities(rev # 4) | history )
  by Anonymous? at September 18, 2020 at 16:25:40
• Martin-Löf Type Theory ( Martin-Löf Type Theory(rev # 4) | history )
  by Ali Caglayan at May 27, 2020 at 15:20:22
• Book HoTT
  by Ali Caglayan at May 27, 2020 at 14:54:36
• type theory ( type theory(rev # 10) | history )
  by Ali Caglayan at May 27, 2020 at 14:39:54
• Events ( Events(rev # 21) | history )
  by Robin Adams? at May 22, 2020 at 11:23:41
• Events ( Events(rev # 20) | history )
  by Bas Spitters at May 13, 2020 at 10:37:00
• Events ( Events(rev # 19) | history )
  by Anonymous? at April 6, 2020 at 22:53:13
• Events ( Events(rev # 18) | history )
  by Anonymous? at March 23, 2020 at 11:30:41
• Events ( Events(rev # 17) | history )
  by nicolas tabareau? at March 21, 2020 at 10:11:39
• Events ( Events(rev # 16) | history )
  by Bas Spitters at March 7, 2020 at 11:17:18
• Events ( Events(rev # 15) | history )
  by Guillaume Brunerie at February 12, 2020 at 06:22:45
• Events ( Events(rev # 14) | history )
  by Bas Spitters at February 12, 2020 at 03:12:39
• Events ( Events(rev # 13) | history )
  by Bas Spitters at February 10, 2020 at 10:10:57
• Events ( Events(rev # 12) | history )
  by Bas Spitters at February 10, 2020 at 07:30:39
• Events ( Events(rev # 11) | history )
  by Bas Spitters at January 24, 2020 at 17:12:30
• Events ( Events(rev # 10) | history )
  by Bas Spitters at January 22, 2020 at 17:45:42
• Proof Assistants ( Proof Assistants(rev # 5) | history )
  by Anonymous? at November 18, 2019 at 09:40:21
• open problems ( open problems(rev # 47) | history )
  by Bas Spitters at November 18, 2019 at 07:58:40
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 17) | history )
  by Ramkumar Ramachandra? at November 12, 2019 at 05:47:00
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 16) | history )
  by Ramkumar Ramachandra? at November 12, 2019 at 05:46:59
• Agda ( Agda(rev # 10) | history )
  by Anonymous? at September 30, 2019 at 11:05:19
• Agda ( Agda(rev # 9) | history )
  by Anonymous? at September 30, 2019 at 11:05:12
• Higher Groups in Homotopy Type Theory ( Higher Groups in Homotopy Type Theory(rev # 2) | history )
  by Mike Shulman at September 6, 2019 at 04:58:01
• Events ( Events(rev # 9) | history )
  by steveawodey? at August 18, 2019 at 17:16:12
• Bonn2018 ( Bonn2018(rev # 11) | history )
  by steveawodey? at August 18, 2019 at 17:15:18
• open problems ( open problems(rev # 46) | history )
  by Bas Spitters at August 15, 2019 at 14:15:54
• HoTT2019 Summer School open problems list ( HoTT2019 Summer School open problems list(rev # 4) | history )
  by Anonymous? at August 11, 2019 at 21:21:44
• HoTT2019 Summer School open problems list ( HoTT2019 Summer School open problems list(rev # 3) | history )
  by Mathieu? at August 11, 2019 at 11:26:09
• HoTT2019 Summer School open problems list ( HoTT2019 Summer School open problems list(rev # 2) | history )
  by steveawodey? at August 10, 2019 at 23:08:36
• HoTT2019 Summer School open problems list ( HoTT2019 Summer School open problems list(rev # 1) | history )
  by steveawodey? at August 10, 2019 at 16:54:44
• open problems ( open problems(rev # 45) | history )
  by steveawodey? at August 10, 2019 at 16:49:29
• universe ( universe(rev # 23) | history )
  by Anonymous? at August 10, 2019 at 00:54:06
• Resources ( Resources(rev # 10) | history )
  by Bas Spitters at July 31, 2019 at 04:14:45
• Resources ( Resources(rev # 9) | history )
  by Anonymous? at July 31, 2019 at 03:55:22
• Andrea Vezzosi ( Andrea Vezzosi(rev # 3) | history )
  by Urs Schreiber at July 16, 2019 at 18:37:40
• limited principle of omniscience ( limited principle of omniscience(rev # 2) | history )
  by Urs Schreiber at June 20, 2019 at 12:11:42
• References ( References(rev # 71) | history )
  by Ali Caglayan at April 15, 2019 at 22:10:53
• References ( References(rev # 70) | history )
  by Ali Caglayan at April 1, 2019 at 03:39:56
• Eric Finster, Towards Higher Universal Algebra in Type Theory ( Eric Finster, Towards Higher Universal Algebra in Type Theory(rev # 14) | history )
  by Ali Caglayan at March 16, 2019 at 19:46:08
• model of type theory in an (infinity,1)-topos ( model of type theory in an (infinity,1)-topos(rev # 15) | history )
  by Urs Schreiber at March 13, 2019 at 07:16:31
• References ( References(rev # 69) | history )
  by steveawodey? at March 12, 2019 at 16:31:54
• References ( References(rev # 68) | history )
  by Ali Caglayan at March 10, 2019 at 23:38:49
• References ( References(rev # 67) | history )
  by Ali Caglayan at February 19, 2019 at 16:41:08
• loop space of a wedge of circles ( loop space of a wedge of circles(rev # 5) | history )
  by Ali Caglayan at February 19, 2019 at 16:37:55
• The join construction ( The join construction(rev # 2) | history )
  by Ali Caglayan at February 19, 2019 at 16:34:07
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory ( A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory(rev # 2) | history )
  by Ali Caglayan at February 19, 2019 at 16:32:56
• References ( References(rev # 66) | history )
  by Ali Caglayan at February 19, 2019 at 09:47:18
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory ( A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory(rev # 1) | history )
  by Ali Caglayan at February 19, 2019 at 09:44:36
• Eric Finster, Towards Higher Universal Algebra in Type Theory ( Eric Finster, Towards Higher Universal Algebra in Type Theory(rev # 13) | history )
  by Leo? at February 16, 2019 at 08:39:32
• spheres ( spheres(rev # 2) | history )
  by Mike Shulman at February 14, 2019 at 15:19:40
• join
  by Ali Caglayan at February 14, 2019 at 12:00:15
• empty type
  by Ali Caglayan at February 14, 2019 at 11:56:34
• The join construction ( The join construction(rev # 1) | history )
  by Ali Caglayan at February 14, 2019 at 11:39:20
• References ( References(rev # 65) | history )
  by Ali Caglayan at February 14, 2019 at 10:24:12
• A Cubical Approach to Synthetic Homotopy Theory
  by Ali Caglayan at February 14, 2019 at 10:15:35
• homotopy groups of spheres ( homotopy groups of spheres(rev # 18) | history )
  by Ali Caglayan at February 14, 2019 at 06:14:33
• spheres ( spheres(rev # 1) | history )
  by Ali Caglayan at February 14, 2019 at 03:46:26
• Higher-Dimensional Types in the Mechanization of Homotopy Theory
  by Ali Caglayan at February 14, 2019 at 03:39:12
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory ( On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory(rev # 2) | history )
  by Ali Caglayan at February 14, 2019 at 03:31:10
• smash product ( smash product(rev # 7) | history )
  by Ali Caglayan at February 14, 2019 at 03:28:55
• smash product ( smash product(rev # 6) | history )
  by Anonymous? at February 14, 2019 at 03:04:50
• wild category ( wild category(rev # 2) | history )
  by Mike Shulman at February 10, 2019 at 18:18:04
• set
  by Ali Caglayan at January 28, 2019 at 16:34:46
• wild category ( wild category(rev # 1) | history )
  by Mike Shulman at January 28, 2019 at 16:11:23
• References ( References(rev # 64) | history )
  by Mike Shulman at January 25, 2019 at 19:50:39
• circle ( circle(rev # 7) | history )
  by Ali Caglayan at January 19, 2019 at 15:35:09
• circle ( circle(rev # 6) | history )
  by Todd Trimble? at January 19, 2019 at 15:20:20
• Formalized Homotopy Theory ( Formalized Homotopy Theory(rev # 12) | history )
  by Ali Caglayan at January 19, 2019 at 14:06:38
• Seifert-van Kampen theorem
  by Ali Caglayan at January 19, 2019 at 14:05:25
• Synthetic homotopy theory ( Synthetic homotopy theory(rev # 20) | history )
  by Ali Caglayan at January 19, 2019 at 13:41:06
• Eilenberg-MacLane space ( Eilenberg-MacLane space(rev # 2) | history )
  by Ali Caglayan at January 19, 2019 at 13:39:40
• localization ( localization(rev # 7) | history )
  by Ali Caglayan at January 19, 2019 at 13:30:40
• circle ( circle(rev # 5) | history )
  by Ali Caglayan at January 19, 2019 at 13:20:08
• Univalent categories and the Rezk completion ( Univalent categories and the Rezk completion(rev # 2) | history )
  by Ali Caglayan at January 19, 2019 at 13:11:40
• Localization in Homotopy Type Theory ( Localization in Homotopy Type Theory(rev # 3) | history )
  by Ali Caglayan at January 19, 2019 at 13:11:09
• Higher Groups in Homotopy Type Theory ( Higher Groups in Homotopy Type Theory(rev # 1) | history )
  by Ali Caglayan at January 19, 2019 at 13:10:56
• HoTT book ( HoTT book(rev # 5) | history )
  by Ali Caglayan at January 19, 2019 at 13:10:08
• Cellular Cohomology in Homotopy Type Theory
  by Ali Caglayan at January 19, 2019 at 13:08:58
• Modalities in homotopy type theory ( Modalities in homotopy type theory(rev # 3) | history )
  by Ali Caglayan at January 19, 2019 at 13:06:09
• desired articles ( desired articles(rev # 3) | history )
  by Ali Caglayan at January 19, 2019 at 13:03:56
• homotopy groups of spheres ( homotopy groups of spheres(rev # 17) | history )
  by Ali Caglayan at January 19, 2019 at 12:54:53
• Formalized Homotopy Theory ( Formalized Homotopy Theory(rev # 11) | history )
  by Ali Caglayan at January 19, 2019 at 12:54:05
• empty
  by Ali Caglayan at January 19, 2019 at 12:45:28
• type ( type(rev # 4) | history )
  by Ali Caglayan at January 19, 2019 at 12:44:23
• type theory ( type theory(rev # 9) | history )
  by Ali Caglayan at January 19, 2019 at 12:43:59
• type theory ( type theory(rev # 8) | history )
  by Ali Caglayan at January 19, 2019 at 12:42:49
• HomePage ( HomePage(rev # 32) | history )
  by Ali Caglayan at January 19, 2019 at 12:40:25
• wedge sum ( wedge sum(rev # 5) | history )
  by Ali Caglayan at January 19, 2019 at 10:54:32
• wedge sum ( wedge sum(rev # 4) | history )
  by Ali Caglayan at January 19, 2019 at 10:54:06
• type family ( type family(rev # 9) | history )
  by Ali Caglayan at January 19, 2019 at 10:49:03
• H-space ( H-space(rev # 8) | history )
  by Ali Caglayan at January 19, 2019 at 10:46:09
• type ( type(rev # 3) | history )
  by Ali Caglayan at January 19, 2019 at 10:26:52
• type theory ( type theory(rev # 7) | history )
  by Ali Caglayan at January 19, 2019 at 10:26:12
• function type ( function type(rev # 2) | history )
  by Ali Caglayan at January 19, 2019 at 10:22:54
• Eric Finster, Towards Higher Universal Algebra in Type Theory ( Eric Finster, Towards Higher Universal Algebra in Type Theory(rev # 12) | history )
  by Ali Caglayan at January 10, 2019 at 07:17:58
• Peter LeFanu Lumsdaine ( Peter LeFanu Lumsdaine(rev # 3) | history )
  by Ali Caglayan at January 1, 2019 at 21:09:51
• hopf fibration ( hopf fibration(rev # 7) | history )
  by Ali Caglayan at January 1, 2019 at 21:08:54
• H-space ( H-space(rev # 7) | history )
  by Ali Caglayan at January 1, 2019 at 20:51:23
• Eric Finster, Towards Higher Universal Algebra in Type Theory ( Eric Finster, Towards Higher Universal Algebra in Type Theory(rev # 11) | history )
  by Ali Caglayan at December 25, 2018 at 07:15:42
• Eric Finster, Towards Higher Universal Algebra in Type Theory ( Eric Finster, Towards Higher Universal Algebra in Type Theory(rev # 10) | history )
  by Ali Caglayan at December 24, 2018 at 18:44:09