cubical Basic results about comonadic modalities

Basic results about comonadic modalities

Open felixwellen opened this issue 3 years ago • 1 comments

A couple of basic proofs for the 'flat modality' supported by Agda.

Oct 25 '21 08:10 felixwellen

Put on hold, since it uses flat in a way that is not supported by the latest master of agda.

Jul 10 '22 07:07 felixwellen

This will be incompatible with the --safe mode of agda 2.6.3 -> I will move this stuff to https://github.com/felixwellen/synthetic-geometry

Oct 30 '22 09:10 felixwellen

Done: https://github.com/felixwellen/synthetic-geometry/pull/23 -> Closing

Oct 30 '22 10:10 felixwellen