Theorem CategoryTheory.NatTrans.hcomp_id_app

Modification history