monae icon indicating copy to clipboard operation
monae copied to clipboard

Published 20 hours ago • verified publisher icon affeldt-aist

define abstract category, impredicatively

Open t6s opened this issue 1 year ago • 0 comments

This PR adds a definition of abstract categories extending category.v. Due to shortcomings in the constraint solver for universes in Coq, this could only be done only for the impredicative version of monae.

Some compatibility changes are needed and made in imonae_lib to make it resemble more to analysis.boolp.

t6s avatar Mar 20 '23 11:03 t6s