latte-prelude.fun
A function with domain T and codomain U has type (==> T U).
This namespace provides some important properties about such functions.
The main source of properties is the consideration of types as objects and functions as arrows in the so-called LaTTe category.
<<
A notation for iterated compositions of functions.
Example :
(<< f g h i) == (compose f (compose g h i))
== (compose f (compose g (compose h i)))
>>
A notation for sequential composition of functions.
Example :
(>> f g h i) == (<< i h g f)
bijective
(bijective [f (==> T U)])(and (injective f) (surjective f))
Definition: A bijective function.
bijective-is-injective
(bijective-is-injective [f (==> T U)])(==> (bijective f) (injective f))
Theorem: A bijection is an injection.
bijective-is-surjective
(bijective-is-surjective [f (==> T U)])(==> (bijective f) (surjective f))
Theorem: A bijection is a surjection.
bijective-unique
(bijective-unique [f (==> T U)])(==>
(bijective f)
(forall [y U] (q/unique (lambda [x T] (equal (f x) y)))))
Theorem: A bijective function has exactly one antecedent for each image.
codomain
(codomain [f (==> T U)])U
Definition: The codomain of function f
compose
(compose [f (==> U V)] [g (==> T U)])(lambda [x T] (f (g x)))
Definition: The composition of two functions f and g, or f “after” g.
compose-injective
(compose-injective [f (==> U V)] [g (==> T U)])(==> (injective f) (injective g) (injective (compose f g)))
Theorem: The composition of two injective functions is injective.
domain
(domain [f (==> T U)])T
Definition: The domain of function f
fun-equal-ext
(fun-equal-ext [f (==> T U)] [g (==> T U)])(==> (equal f g) (forall [x T] (equal (f x) (g x))))
Theorem: Functional equality is extensional.
functional-extensionality
(functional-extensionality [f (==> T U)] [g (==> T U)])(==> (forall [x T] (equal (f x) (g x))) (equal f g))
Axiom:
identity
(identity [T :type])(lambda [x T] x)
Definition: The identity function.
injective
(injective [f (==> T U)])(forall [x y T] (==> (equal (f x) (f y)) (equal x y)))
Definition: An injective function.
injective-single
(injective-single [f (==> T U)])(==>
(injective f)
(forall [y U] (q/single (lambda [x T] (equal (f x) y)))))
Theorem: An injective function has at most one antecedent for each image.
inverse
(inverse [f (==> T U)] [b (bijective f)])(lambda [y U] (q/the ((bijective-unique f) b y)))
Definition: The inverse of bijective function f.
inverse-bijective
(inverse-bijective [f (==> T U)] [b (bijective f)])(bijective (inverse f b))
Theorem: The inverse of a bijection is a bijection.
inverse-injective
(inverse-injective [f (==> T U)] [b (bijective f)])(injective (inverse f b))
Theorem: The inverse function of a bijection, is injective.
inverse-prop
(inverse-prop [f (==> T U)] [b (bijective f)])(forall [y U] (equal (f ((inverse f b) y)) y))
Theorem: The basic property of the inverse of a bijective function f.
inverse-prop-conv
(inverse-prop-conv [f (==> T U)] [b (bijective f)])(forall [x T] (equal ((inverse f b) (f x)) x))
Theorem: The basic property of the inverse function, the converse of inverse-prop.
inverse-surjective
(inverse-surjective [f (==> T U)] [b (bijective f)])(surjective (inverse f b))
Theorem: The inverse function of a bijection, is surjective.
law-associativity
(law-associativity [T :type] [U :type] [V :type] [W :type])(forall
[f (==> T U)]
(forall
[g (==> U V)]
(forall
[h (==> V W)]
(equal (compose h (compose g f)) (compose (compose h g) f)))))
Theorem: The categorical associativity law for functions.
law-identity-left
(law-identity-left [T :type] [U :type])(forall [g (==> T U)] (equal (<< g (identity T)) g))
Theorem: The categorical left identity law for functions.
law-identity-right
(law-identity-right [T :type] [U :type])(forall [f (==> T U)] (equal (<< (identity U) f) f))
Theorem: The categorical right identity law for functions.
point
(point [T :type])(==> Unit T)
Definition: The notion of a point in the LaTTe category.
retraction
(retraction [f (==> T U)] [r (==> U T)])(equal (<< r f) (identity T))
Definition: The function r is a retraction of f.
section
(section [f (==> T U)] [s (==> U T)])(equal (<< f s) (identity U))
Definition: The function s is a section of f.
solve-section
(solve-section [f (==> T U)] [s (==> U T)])(==>
(section f s)
(forall
[V :type]
(forall [y (==> V U)] (exists [x (==> V T)] (equal (<< f x) y)))))
Theorem:
surjective
(surjective [f (==> T U)])(forall [y U] (exists [x T] (equal (f x) y)))
Definition: A surjective function.
Unit
(Unit):type
Axiom: The singleton type.
unit
(unit)Unit
Axiom: The unique habitant of Unit.