arend-lib

arend-lib copied to clipboard

As title.

ice1000

So we no longer need relative paths :)

ice1000

We should have it

ice1000

As title

ice1000

added representation category, schur's lemma

s3midetnov

This contains a proof that the category of presheaves is complete together with the yoneda lemma and the universal property of the presheves category.

FeorgeGeorge

Closes #44

bakinovsky-m

If the user forgets to surround mcases tactic with parentheses he won't get an error message. Instead he will get "missing clauses" message (despite the fact that clauses are present...

sxhya