(* Author: Alexander Katovsky *) section "Category" theory Category imports "HOL-Library.FuncSet" begin