mikeshulman Coq-HoTT issues

mikeshulman / Coq-HoTT

Homotopy type theory

http://homotopytypetheory.org/

Other

12 stars 4 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Generalising DComma to sections of categories

#45 Alizter opened 4 years ago
3
Equivalences in ooCat.v

#44 Alizter closed 4 years ago
2
Make `pi_functor` definitionally equal to the expected pointed map

#43 fpvandoorn opened 4 years ago
1
Fixed Jason's ExponentialLaws tactic and added change to HoTTBook.v due to IsTrunc being unfolded

#42 Alizter closed 4 years ago
0
Universe bug when making IsGraph a parameter

#41 Alizter closed 4 years ago
3
Separated modalities

#40 mikeshulman closed 4 years ago
3
Opposite wild (oo,oo)-cats

#39 Alizter opened 4 years ago
6
Make a PR to the main library including WildCat/Square

#38 mikeshulman closed 4 years ago
1
Speed up proofs in loops

#37 mikeshulman opened 4 years ago
0
The category of Prespectra as an inserter

#36 Alizter opened 4 years ago
6
Comma categories

#35 Alizter opened 4 years ago
2
Reflective subcategories

#34 mikeshulman opened 4 years ago
0
Use wildcat functors in Types?

#33 mikeshulman opened 4 years ago
1
2-coherent 2-categories

#32 mikeshulman opened 4 years ago
1
Displayed categories

#31 mikeshulman closed 4 years ago
4
Category of categories

#30 mikeshulman opened 4 years ago
0
IsGraph?

#29 mikeshulman closed 4 years ago
0
idmap is a functor between Type and Type

#28 Alizter closed 4 years ago
1
Limits and colimits

#27 mikeshulman opened 4 years ago
3
hfiber categories

#26 Alizter opened 4 years ago
3
Closed wild categories

#25 mikeshulman opened 4 years ago
0
Integrate with the Pointed directory

#24 mikeshulman opened 4 years ago
1
Pointed categories

#23 mikeshulman closed 4 years ago
2
Grothendieck constructions

#22 mikeshulman opened 4 years ago
1
Integrate with the 1-categories library

#21 mikeshulman opened 4 years ago
0
Sum of categories is a category

#20 mikeshulman closed 4 years ago
1
Pi type categories

#19 Alizter closed 4 years ago
1
Define adjunctions

#18 mikeshulman opened 4 years ago
3
Arrow is a functor

#17 mikeshulman closed 4 years ago
1
Prod is a functor

#16 mikeshulman closed 4 years ago
0
Sum is a functor

#15 mikeshulman closed 4 years ago
1
some style changes

#14 Alizter closed 4 years ago
1
1-coherent symmetric monoidal wild category

#13 Alizter closed 4 years ago
2
updated HoTT.v

#12 Alizter closed 5 years ago
0
Added Andreas' suggestions

#11 Alizter closed 5 years ago
0
Split up BlakersMassey into GBM, BlakersMassey and Freudenthal

#10 Alizter closed 5 years ago
6
Split up BlakersMassey into GBM, BlakersMassey and Freudenthal

#9 Alizter closed 5 years ago
0
Renamed sh to sh_

#8 Alizter closed 5 years ago
0
Added a pairing and ap for square

#7 Alizter closed 5 years ago
4
fixed order to be more consistent. left right up down

#6 Alizter closed 5 years ago
3
Attempted square over

#5 Alizter closed 5 years ago
2
Squareovers

#4 Alizter closed 5 years ago
3
Add some Ltac magic to one_line_proof

#3 JasonGross closed 6 years ago
1
PropResizing speedup

#2 SkySkimmer closed 7 years ago
0
Speed up propresizing by about 50%

#1 JasonGross closed 7 years ago
0