proto

Proto package contains very basic definitions.

idfun (A : U) (a : A) : A constfun (A B: U) (a: A) (b: B): A o (A B C: U) (f: B -> C) (g: A -> B): A -> C and (A B: U): U