projects / coq-hetmet.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7300187) | patch
use WeakFunctorCategory to prove GArrow/Reification isomorphism
authorAdam Megacz <megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 02:12:36 +0000 (19:12 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Sun, 27 Mar 2011 02:12:36 +0000 (19:12 -0700)
commitf9297f3fba59884fe98eb4f9257a1fb7552bfd0a
tree22ad7970693bc4c2dcb8d696f63e9e1ba1d6da08tree | snapshot
parent7300187652058f4c24fd4527d9a5833583959fb4commit | diff
use WeakFunctorCategory to prove GArrow/Reification isomorphism
src/All.v diff | blob | history
src/GeneralizedArrowCategory.v diff | blob | history
src/ReificationCategory.v diff | blob | history
src/ReificationFromGeneralizedArrow.v diff | blob | history
src/ReificationsEquivalentToGeneralizedArrows.v diff | blob | history
src/ReificationsIsomorphicToGeneralizedArrows.v [new file with mode: 0644] blob
src/SmallSMMEs.v [new file with mode: 0644] blob
src/WeakFunctorCategory.v [new file with mode: 0644] blob
Coq proofs and code accompanying the HetMet extensions for GHC