affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

rebase infotheo over (concrete) categories #94

Open t6s opened 1 year ago

t6s commented 1 year ago

This draft PR moves category theory from monae to infotheo, rebasing all algebraic structures (eg convex spaces) in infotheo over it.

Suggestion by @CohenCyril