fact: Record t := mk { eta : FId ~> G \O F ; eps : F \O G ~> FId ; triL : TriangularLaws.left eta eps ; triR : TriangularLaws.right eta eps }.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)