issues
search
jwiegley
/
category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
757
stars
70
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Make universe polymorphism on functors explicit
#102
jwiegley
closed
2 years ago
0
Fix categories at 3 universes
#101
jwiegley
closed
2 years ago
0
Remove a slow hint
#100
jwiegley
closed
2 years ago
0
Prove Monad composition for the simple compose monad
#99
jwiegley
closed
2 years ago
0
Complete basic Functor proofs and Applicative proofs
#98
jwiegley
closed
2 years ago
0
Move some files around, and other reorganization
#97
jwiegley
closed
2 years ago
0
Work on proving that Coq's applicatives map to the general one
#96
jwiegley
closed
2 years ago
0
General Applicative functors only require closed monoidal
#95
jwiegley
closed
2 years ago
0
Transfer several definitions into Theory/Coq/Category.v
#94
jwiegley
closed
2 years ago
0
Set Default Goal Selector "!" project-wide
#93
jwiegley
closed
2 years ago
0
Apply Unset Intuition Negation Unfolding project-wide
#92
jwiegley
closed
2 years ago
0
Port parts of coq-haskell to a new Category.Theory.Coq sub-library
#91
jwiegley
closed
2 years ago
0
Move library-wide settings into Lib.v
#90
jwiegley
closed
2 years ago
0
Use #[export] rather than #[global] in almost all modules
#89
jwiegley
closed
2 years ago
0
Use Require Import, not Require Export, wherever possible
#88
jwiegley
closed
2 years ago
0
Cleanup of requires in Lib and Algebra
#87
jwiegley
closed
2 years ago
0
Remove unnecessary require statements
#86
jwiegley
closed
2 years ago
0
Make the Cartesian_Limit proof closed under the global context
#85
jwiegley
closed
2 years ago
0
Consistency in how multiple requires are declared
#84
jwiegley
closed
2 years ago
0
Prove that products are a limit from the discrete category 2
#83
jwiegley
closed
2 years ago
0
Restore two uses of universe polymorphism
#82
jwiegley
closed
2 years ago
0
Prove that any terminal object is the limit for diagrams from 0
#81
jwiegley
closed
2 years ago
0
Rename revelant monoidal to relevance monoidal, to match nLab
#80
jwiegley
closed
2 years ago
0
Fix remaining warnings in the 8.16 build
#79
jwiegley
closed
2 years ago
0
Add FunctorParts for fixing the object mapping of a functor
#78
jwiegley
closed
2 years ago
0
Add some clarifying tacticals to Construction/Comma/Adjunction.v
#77
jwiegley
closed
2 years ago
0
Bump the nixpkgs pin
#76
jwiegley
closed
2 years ago
0
Add more definitions to Structure/Monoidal/Closed.v
#75
jwiegley
closed
2 years ago
0
Binoidal, premonoidal categories and other structures
#74
jwiegley
closed
2 years ago
0
The funny tensor product and discrete categories
#73
jwiegley
closed
2 years ago
0
Some harmless simplifications
#72
jwiegley
closed
2 years ago
0
Define unnatural transformations
#71
jwiegley
closed
2 years ago
0
Sort _CoqProject
#70
jwiegley
closed
2 years ago
0
Move some code around under Structure/Monoidal
#69
jwiegley
closed
2 years ago
0
Use utf-8 in more places, lots of monoidal refactoring, work in Par.v
#68
jwiegley
closed
2 years ago
0
Begin implementation of Structure/Monoidal/Closed.v
#67
jwiegley
closed
2 years ago
0
Some minor simplification in Structure/Cartesian/Closed.v
#66
jwiegley
closed
2 years ago
0
Many simplifications, remove several unneeded files
#65
jwiegley
closed
2 years ago
0
Many simplifications in the solver's normalization code
#64
jwiegley
closed
2 years ago
0
Add comments on bicategories and other clarifications
#63
jwiegley
closed
2 years ago
0
Some general cleanup in the solver
#62
jwiegley
closed
2 years ago
0
Remove Solver.Categories, add some helper lemmas
#61
jwiegley
closed
2 years ago
0
Simplify the solver code by removing richly-typed terms
#60
jwiegley
closed
2 years ago
0
Introduce the TermRel constructive relation
#59
jwiegley
closed
2 years ago
0
Remove Lib/Equality.v and simplify the solver a bit
#58
jwiegley
closed
2 years ago
0
Some general simplifications
#57
jwiegley
closed
2 years ago
0
Speed up Structure/Monoidal/Internal/Product.v, thanks to Columbus240
#56
jwiegley
closed
2 years ago
1
Restore the categorical solver using Equations
#55
jwiegley
closed
2 years ago
0
Add ParE.v, the category of partial functions that yield errors
#54
jwiegley
closed
2 years ago
0
Significant speedups in Construction/Comma.v, thanks to Columbus240
#53
jwiegley
closed
2 years ago
0
Previous
Next