Issues

• Generalising DComma to sections of categories

  mikeshulman/Coq-HoTT#45 · Filter by author Alizter opened on Mar 4, 2020
  3

• Make pi_functor definitionally equal to the expected pointed map

  mikeshulman/Coq-HoTT#43 · Filter by author fpvandoorn opened on Feb 20, 2020
  1

• Opposite wild (oo,oo)-cats

  mikeshulman/Coq-HoTT#39 · Filter by author Alizter opened on Jan 26, 2020
  6

• Speed up proofs in loops

  mikeshulman/Coq-HoTT#37 · Filter by author mikeshulman opened on Jan 23, 2020

• The category of Prespectra as an inserter

  mikeshulman/Coq-HoTT#36 · Filter by author Alizter opened on Jan 16, 2020
  6

• Comma categories

  mikeshulman/Coq-HoTT#35 · Filter by author Alizter opened on Jan 10, 2020
  2

  

• Reflective subcategories

  mikeshulman/Coq-HoTT#34 · Filter by author mikeshulman opened on Jan 9, 2020

• Use wildcat functors in Types?

  mikeshulman/Coq-HoTT#33 · Filter by author mikeshulman opened on Jan 9, 2020
  1

  

• 2-coherent 2-categories

  mikeshulman/Coq-HoTT#32 · Filter by author mikeshulman opened on Jan 9, 2020
  1

  

• Category of categories

  mikeshulman/Coq-HoTT#30 · Filter by author mikeshulman opened on Jan 9, 2020
  

• Limits and colimits

  mikeshulman/Coq-HoTT#27 · Filter by author mikeshulman opened on Jan 9, 2020
  3

  

• hfiber categories

  mikeshulman/Coq-HoTT#26 · Filter by author Alizter opened on Jan 8, 2020
  3

  

• Closed wild categories

  mikeshulman/Coq-HoTT#25 · Filter by author mikeshulman opened on Jan 7, 2020
  

• Integrate with the Pointed directory

  mikeshulman/Coq-HoTT#24 · Filter by author mikeshulman opened on Jan 7, 2020
  1

  

• Grothendieck constructions

  mikeshulman/Coq-HoTT#22 · Filter by author mikeshulman opened on Jan 7, 2020
  1

• Integrate with the 1-categories library

  mikeshulman/Coq-HoTT#21 · Filter by author mikeshulman opened on Jan 7, 2020

• Define adjunctions

  mikeshulman/Coq-HoTT#18 · Filter by author mikeshulman opened on Jan 7, 2020
  3