|
|
|
|
|
| Description |
Notes
- Functions are coded as functional relations (in particular, functions are sets)
- Extensional equality of functions coincedes with extensional equality of sets.
|
|
| Synopsis |
|
| | | type Total dom f = forall a. (a :∈: dom) -> ExSnd f a | | | type Sval f = forall a b1 b2 r. ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> r | | | | | relation :: (dom :~>: cod) f -> f :⊆: (dom :×: cod) | | | total :: (dom :~>: cod) f -> (a :∈: dom) -> ExSnd f a | | | totalCPS :: (dom :~>: cod) f -> (a :∈: dom) -> (forall totalCPS_y. ((a, totalCPS_y) :∈: f) -> totalCPS_return) -> totalCPS_return | | | sval :: forall dom cod a b1 b2 f. (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> b1 :=: b2 | | | svalCoerce :: forall dom cod a b1 b2 f. (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> b1 -> b2 | | | svalCPS :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> r | | | svalCPS' :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> ((b1 :=: b2) -> r) -> r | | | rel :: (dom :~>: cod) f -> (pair :∈: f) -> pair :∈: (dom :×: cod) | | | relCPS :: (dom :~>: cod) f -> (pair :∈: f) -> (forall relCPS_x relCPS_y. pair ~ (relCPS_x, relCPS_y) => dom relCPS_x -> cod relCPS_y -> relCPS_return) -> relCPS_return | | | inDom :: (dom :~>: cod) f -> ((a, b) :∈: f) -> a :∈: dom | | | inCod :: (dom :~>: cod) f -> ((a, b) :∈: f) -> b :∈: cod | | | domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2 | | | type :~~>: dom cod = Lower1 (dom :~>: cod) | | | lowerFun :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f) | | | raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f | | | raiseFunCPS :: (dom :~~>: cod) lf -> (forall f. lf ~ Lower f => (dom :~>: cod) f -> r) -> r | | | | | imageCod :: (dom :~>: cod) f -> Image f s :⊆: cod | | | setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) f | | | adjustCod :: (dom :~>: cod) f -> (Image f dom :⊆: cod') -> (dom :~>: cod') f | | | extendCod :: (dom :~>: cod) f -> (cod :⊆: cod') -> (dom :~>: cod') f | | | imageMonotonic :: (s1 :⊆: s2) -> Image f s1 :⊆: Image f s2 | | | imageEmpty :: Image f Empty :==: Empty | | | imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom) | | | fullImageOfInclusion :: (dom :⊆: cod) -> Image (Incl dom cod) dom :==: dom | | | imageUnion :: forall dom cod s1 s2 f. (dom :~>: cod) f -> Image f (s1 :∪: s2) :==: (Image f s1 :∪: Image f s2) | | | funEq :: forall dom cod cod' f f'. (dom :~>: cod) f -> (dom :~>: cod') f' -> (f :⊆: f') -> f :==: f' | | | funEq' :: (dom :~>: cod) f -> (dom :~>: cod') f' -> (f' :⊆: f) -> f :==: f' | | | equal_f :: (d :~>: c) f' -> (f :==: f') -> ((x, y) :∈: f) -> ((x, y') :∈: f') -> y :=: y' | | | equal_f_coerce :: (d :~>: c) f' -> (f :==: f') -> ((x, y) :∈: f) -> ((x, y') :∈: f') -> y -> y' | | | isFun_congruence :: (d :~>: c) f -> (f :==: f') -> (d :~>: c) f' | | | | | type Id dom = Incl dom dom | | | inclusionIsFun :: (dom :⊆: cod) -> (dom :~>: cod) (Incl dom cod) | | | idIsFun :: (dom :~>: dom) (Id dom) | | | | | compoIsFun :: (s2 :~>: s3) g -> (s1 :~>: s2) f -> (s1 :~>: s3) (g :○: f) | | | compo_idl :: (d :~>: c) f -> (Id c :○: f) :==: f | | | compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: f | | | compo_assoc :: :~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1)) | | | | | type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) s | | | equaliserSubset :: (s :~>: t) f1 -> Equaliser f1 f2 :⊆: s | | | equaliserIsFun :: (s :~>: t) f1 -> (Equaliser f1 f2 :~>: s) (EqualiserIncl s f1 f2) | | | equaliserUni :: (s0 :~>: s) g -> (s :~>: t) f1 -> ((f1 :○: g) :==: (f2 :○: g)) -> (s0 :~>: Equaliser f1 f2) g | | | | | injective :: forall f a1 a2 b. Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> a1 :=: a2 | | | inclusion_Injective :: Injective (Incl dom cod) | | | | | preimage_Image :: (dom :~>: cod) f -> (set :⊆: dom) -> set :⊆: Preimage f (Image f set) | | | image_Preimage :: (dom :~>: cod) f -> Image f (Preimage f set) :⊆: set | | | | | | | | | fstIsFun :: ((s1 :×: s2) :~>: s1) (Fst s1 s2) | | | sndIsFun :: ((s1 :×: s2) :~>: s2) (Snd s1 s2) | | | targetTuplingIsFun :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2) | | | fst_tupling :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (Fst cod1 cod2 :○: (f1 :***: f2)) :==: f1 | | | snd_tupling :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (Snd cod1 cod2 :○: (f1 :***: f2)) :==: f2 | | | tupling_eta :: (dom :~>: (cod1 :×: cod2)) f -> ((Fst cod1 cod2 :○: f) :***: (Snd cod1 cod2 :○: f)) :==: f | | | | | haskFunIsFun :: ((Univ :×: Univ) :~>: FunctionType) HaskFun | | | haskFunInjective :: Injective HaskFun | | | | | kleisliHomIsFun :: ((Univ :×: Univ) :~>: KleisliType m) (KleisliHom m) | | | kleisliHomInjective :: Injective (KleisliHom m) | | | | | graphIsFun :: (Univ :~>: Univ) (Graph f) | | | graphCPS :: (pair :∈: Graph f) -> (forall a. pair ~ (a, f a) => r) -> r | | | graphInjective :: Injective (Graph f) | | | imageGraphList :: [a] :∈: Image (Graph []) Univ | | | data ToTyCon f x = forall y . ToTyCon ((x, y) :∈: f) y | | | introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f x | | | elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x, z) :∈: f) -> z | | | toTCG :: f x -> ToTyCon (Graph f) x | | | fromTCG :: ToTyCon (Graph f) x -> f x | | | | | biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f) | | | biGraphInjective :: Injective (BiGraph f) | | | biGraph_eq_HaskFun :: BiGraph (->) :==: HaskFun | | | | | constIsFun :: (x :∈: cod) -> (dom :~>: cod) (Const dom x) | | | constEq :: Ex dom -> (Const dom x :==: Const dom' x') -> x :=: x' | | | | | | | idLemma :: (dom :~>: dom) f -> (forall x y. ((x, y) :∈: f) -> x :=: y) -> Id dom :==: f | | | section_CompoId :: (total :~>: base) bun -> (base :~>: total) f -> Section bun f -> (bun :○: f) :==: Id base | | | compoId_Section :: (total :~>: base) bun -> (base :~>: total) f -> ((bun :○: f) :==: Id base) -> Section bun f | | | | | invInv0 :: Inv (Inv f) :⊆: f | | | invInv :: (dom :~>: cod) f -> Inv (Inv f) :==: f | | | injective_Inv :: (dom :~>: cod) f -> Injective f -> (Image f dom :~>: dom) (Inv f) | | | invId :: Inv (Id dom) :==: Id dom |
|
|
|
| Preliminary
|
|
|
| Existential quantification over the first component of a pair
| | Constructors | |
|
|
|
| Totality
|
|
| type Sval f = forall a b1 b2 r. ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> r | Source |
|
| Single-valuedness (CPS)
|
|
| Functions
|
|
|
Functions are encoded as functional relations; the three arguments to the construcor are:
- Is a relation
- Totality
- Single-valuedness (CPS-encoded; using ':=:' would work just as well. I hope that the CPS variant makes the optimizer more happy, but this is pure speculation)
| | Constructors | |  Instances | |
|
|
|
| Functions are relations
|
|
|
| Functions are total
|
|
| totalCPS :: (dom :~>: cod) f -> (a :∈: dom) -> (forall totalCPS_y. ((a, totalCPS_y) :∈: f) -> totalCPS_return) -> totalCPS_return | Source |
|
| The detailed type variable names help debugging proofs
|
|
| sval :: forall dom cod a b1 b2 f. (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> b1 :=: b2 | Source |
|
| Functions are single-valued (reified equality version)
|
|
| svalCoerce :: forall dom cod a b1 b2 f. (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> b1 -> b2 | Source |
|
| Perform coercion using the single-valuedness
|
|
| svalCPS :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> r | Source |
|
| Functions are single-valued (CPS version)
|
|
| svalCPS' :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> ((b1 :=: b2) -> r) -> r | Source |
|
|
|
| Shortcut for unpacking relation
|
|
| relCPS :: (dom :~>: cod) f -> (pair :∈: f) -> (forall relCPS_x relCPS_y. pair ~ (relCPS_x, relCPS_y) => dom relCPS_x -> cod relCPS_y -> relCPS_return) -> relCPS_return | Source |
|
|
|
| If f a = b, then a is in the domain of f
|
|
|
| If f a = b, then b is in the codomain of f
|
|
|
| The domain of a function is uniquely determined
|
|
| Set of functions
|
|
|
Kind-casted variant (function space as a set)
Convention: Instances of Fact should always prove ':~>:' rather than this type.
|
|
|
|
|
|
|
| This is stronger than raiseFun since it introduces the knowledge that lf is of the form Lower f, rather than assuming it.
|
|
| Images
|
|
|
| Image of a set under the function
| | Constructors | |
|
|
|
| Every image is a subset of every possible codomain
|
|
|
| The full image is a codomain
|
|
|
| Change the codomain by proving that the full image is included in the new codomain
|
|
|
| Enlargen the codomain
|
|
|
|
|
|
|
|
|
|
|
| Image distributes over union (in general not over intersection)
|
|
| Equality
|
|
| funEq :: forall dom cod cod' f f'. (dom :~>: cod) f -> (dom :~>: cod') f' -> (f :⊆: f') -> f :==: f' | Source |
|
Very useful lemma for proving equality of functions.
Given the properties of functions, it is enough to show that f is a subset of f' to prove f = f'.
|
|
|
| funEq with the inclusion argument flipped
|
|
|
| Expresses the fact that f = f' ==> f x = f' x
|
|
| equal_f_coerce :: (d :~>: c) f' -> (f :==: f') -> ((x, y) :∈: f) -> ((x, y') :∈: f') -> y -> y' | Source |
|
| Perform coercion using a function equality
|
|
|
|
| Inclusion functions, identity, composition
|
|
|
Inclusion function of a subset
Inclusions do know their codomain (somewhat arbitrary design decision)
| | Constructors | | Incl :: dom a -> Incl dom cod (a, a) | |
|
|
|
|
| Identity function on dom
|
|
|
| Inclusion is a function
|
|
|
| Id is a function
|
|
|
| Composition
| | Constructors | | Compo :: ((b, c) :∈: g) -> ((a, b) :∈: f) -> (g :○: f) (a, c) | |
|
|
|
|
| The composition is a function
|
|
|
| Id is a left identity for composition
|
|
|
| Id is a right identity for composition
|
|
|
|
| Equalisers
|
|
| data Equaliser f1 f2 where | Source |
|
Equalisers :D
In our category, the equaliser of two parallel functions f1 and f2 is the set of types on which f1 and f2 agree; that is:
Equaliser f1 f2 = { x | f1 x = f2 x }
| | Constructors | |
|
|
|
| Inclusion of the equaliser into the domain of the parallel functions
|
|
|
| The equaliser is a subset of the domain of the parallel functions
|
|
|
| The equaliser inclusion is a function
|
|
|
Universal property of equalisers:
f1 . g = f2 . g ==> g factors uniquely through Equaliser f1 f2
Uniqueness is trivial in our case because the function into the equaliser is
identical to g (our functions don't know their codomain)
|
|
| Injectivity
|
|
|
Injective functions
(NB: Surjectivity is meaningless here because our functions don't know their codomain, but we have Image)
| | Constructors | | Injective :: (forall a1 a2 b r. ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> (a1 ~ a2 => r) -> r) -> Injective f | |
| | Instances | |
|
|
|
|
|
|
| Preimages
|
|
|
|
|
|
|
|
|
| Binary product projections, target tupling
|
|
|
|
|
|
|
|
|
| Analogous to ***
| | Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Particular functions
|
|
|
The type-level function:
HaskFun(a,b) = (a -> b)
| | Constructors | | | Instances | |
|
|
|
|
|
|
|
The type-level function:
KleisliHom(a,b) = (a -> m b)
| | Constructors | | | Instances | |
|
|
|
|
|
|
| Conversions type constructors <-> type-level functions
|
|
|
| Graph of a (* -> *) type constructor
| | Constructors | | Graph :: Graph f (a, f a) | |
| | Instances | |
|
|
|
|
| graphCPS :: (pair :∈: Graph f) -> (forall a. pair ~ (a, f a) => r) -> r | Source |
|
|
|
| Type constructors are injective
|
|
|
|
|
| Constructors | | forall y . ToTyCon ((x, y) :∈: f) y | |
|
|
|
|
|
|
| NB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness
|
|
|
|
|
|
|
| Graph of a (* -> * -> *) type constructor
| | Constructors | | BiGraph :: BiGraph f ((a, b), f a b) | |
| | Instances | |
|
|
|
|
|
| Type constructors are injective
|
|
|
| Example of an extensional equation between functions
|
|
| Constant functions
|
|
|
| Constructors | | Const :: (a :∈: dom) -> Const dom x (a, x) | |
|
|
|
|
|
|
|
| Dependent product
|
|
|
| NB: fam must be a function mapping some set to a set of sets, or the second condition in the constructor is vacuous
| | Constructors | |
|
|
| Sections
|
|
| data Section bundleMap f where | Source |
|
| Expresses that f is a section of bundleMap
| | Constructors | | Section :: (forall x y. ((x, y) :∈: f) -> (y, x) :∈: bundleMap) -> Section bundleMap f | |
|
|
|
|
| Lemma for proving a function equal to the identity
|
|
|
| Is section ==> composition is id
|
|
|
| Composition is id ==> is section
|
|
| Inverses
|
|
|
| Constructors | | Inv :: ((a, b) :∈: f) -> Inv f (b, a) | |
|
|
|
|
|
|
|
|
| An injective function has an inverse, with domain the image
|
|
|
|
| Produced by Haddock version 2.4.2 |
