Initial.

Fun/Predicates.lidr

+> module Fun.Predicates
+
+
+> %default total
+> %access public export
+> %auto_implicits off
+
+Domain and codomain:
+
+> ||| Domain
+> Domain : {A, B : Type} -> (f : A -> B) -> Type
+> Domain {A} f = A
+
+> ||| Codomain
+> Codomain : {A, B : Type} -> (f : A -> B) -> Type
+> Codomain {B} f = B
+
+
+Extensional equality:
+
+> ||| Extensional equality
+> ExtEq : {A, B : Type} -> (f, g : A -> B) -> Type
+> -- ExtEq f g = (a : Domain f) -> f a = g a
+> ExtEq {A} f g = (a : A) -> f a = g a