3a95734fae
in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5 in sigma.lean, finish proving equality of triples in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator |
||
---|---|---|
.. | ||
algebra.md | ||
binary.lean | ||
category.lean | ||
function.lean | ||
relation.lean | ||
wf.lean |