module Type.Function where
import Type.Logic
import Type.Set
import Data.Type.Equality
import Control.Arrow
import Helper
import Type.Dummies
#include "../Defs.hs"
data ExSnd (f :: SET) (a :: *) :: * where
ExSnd :: (a, ex) :∈: f -> ExSnd f a
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)
data ((dom :: SET) :~>: (cod :: SET)) :: SET1 where
IsFun ::
(f :⊆: (dom :×: cod))
-> Total dom f
-> Sval f
-> (dom :~>: cod) f
infixr 6 :~>:, :~~>:
relation :: (dom :~>: cod) f -> f :⊆: (dom :×: cod)
relation (IsFun p _ _) = p
total :: (dom :~>: cod) f -> a :∈: dom -> ExSnd f a
total (IsFun _ p _) = p
totalCPS :: (dom :~>: cod) f -> a :∈: dom ->
(forall totalCPS_y. (a,totalCPS_y) :∈: f -> totalCPS_return) ->
totalCPS_return
totalCPS f a k = case total f a of
ExSnd fab -> k fab
sval :: forall dom cod a b1 b2 f.
(dom :~>: cod) f ->
(a, b1) :∈: f ->
(a, b2) :∈: f ->
b1 :=: b2
sval f fab1 fab2 = svalCPS f fab1 fab2 (Refl :: b1 ~ b2 => b1 :=: b2)
svalCoerce :: forall dom cod a b1 b2 f.
(dom :~>: cod) f ->
(a, b1) :∈: f ->
(a, b2) :∈: f ->
b1 -> b2
svalCoerce f p1 p2 x = svalCPS f p1 p2 (x :: b1 ~ b2 => b2)
svalCPS :: (dom :~>: cod) f ->
(a, b1) :∈: f ->
(a, b2) :∈: f ->
((b1 ~ b2) => r) ->
r
svalCPS (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 k
svalCPS' :: (dom :~>: cod) f ->
(a, b1) :∈: f ->
(a, b2) :∈: f ->
(b1 :=: b2 -> r) ->
r
svalCPS' (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 (k Refl)
rel :: (dom :~>: cod) f -> pair :∈: f -> pair :∈: (dom :×: cod)
rel f fp = relation f `scoerce` fp
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
relCPS f fxy k = case rel f fxy of
x :×: y -> k x y
inDom :: (dom :~>: cod) f -> (a, b) :∈: f -> a :∈: dom
inDom f p = fstPrf (relation f `scoerce` p)
inCod :: (dom :~>: cod) f -> (a, b) :∈: f -> b :∈: cod
inCod f p = sndPrf (relation f `scoerce` p)
domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2
domUniq f f' = SetEq (domUniq0 f f') (domUniq0 f' f)
where
domUniq0 f f' = Subset (\a -> case total f a of
ExSnd fa -> inDom f' fa)
type (dom :~~>: cod) = Lower1 (dom :~>: cod)
instance (Fact ((dom :~>: cod) f), Lower f ~ lf) => (Fact ((dom :~~>: cod) lf))
where
auto = LowerElement auto
lowerFun :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f)
lowerFun = LowerElement
raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f
raiseFun (LowerElement x) = x
raiseFunCPS :: (dom :~~>: cod) lf ->
(forall f. (lf ~ Lower f) => (dom :~>: cod) f -> r) -> r
raiseFunCPS (LowerElement x) k = k x
data Image (f :: SET) (s :: SET) :: SET where
Image :: a :∈: s ->
(a, b) :∈: f ->
Image f s b
imageCod :: (dom :~>: cod) f -> Image f s :⊆: cod
imageCod f = Subset (\(Image _ p) -> inCod f p)
setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) f
setCodToImage f = adjustCod f subsetRefl
adjustCod :: (dom :~>: cod) f ->
(Image f dom :⊆: cod')
-> (dom :~>: cod') f
adjustCod f p =
IsFun (Subset (\fab -> case relation f `scoerce` fab of
p1 :×: _ -> p1 :×: p `scoerce`
(Image p1 fab )))
(total f) (\p1 p2 k -> svalCPS f p1 p2 k)
extendCod :: (dom :~>: cod) f ->
(cod :⊆: cod')
-> (dom :~>: cod') f
extendCod f q = adjustCod f (Subset (\(Image _ fab) -> q `scoerce` inCod f fab))
imageMonotonic :: (s1 :⊆: s2) -> Image f s1 :⊆: Image f s2
imageMonotonic p = Subset( \(Image x fxy) -> Image (p `scoerce` x) fxy)
imageEmpty :: Image f Empty :==: Empty
imageEmpty = SetEq (Subset (\(Image (Empty e) _) -> Empty e)) emptySubset
imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom)
imageOfInclusion = SetEq (Subset (\(Image s (Incl dom)) -> Inter s dom))
(Subset (\(Inter s dom) -> Image s (Incl dom)))
fullImageOfInclusion :: dom :⊆: cod -> Image (Incl dom cod) dom :==: dom
fullImageOfInclusion s = imageOfInclusion `setEqTrans` interIdempotent
imageUnion :: forall dom cod s1 s2 f.
(dom :~>: cod) f ->
(Image f (s1 :∪: s2) )
:==:
(Image f s1 :∪: Image f s2)
imageUnion f = SetEq
(Subset
(\(Image x fxy) -> case elimUnion x of
Left x1 -> (Union . Left) (Image x1 fxy)
Right x1 -> (Union . Right) (Image x1 fxy)))
(unionMinimal
(imageMonotonic auto)
(imageMonotonic auto)
)
instance (cod' ~ cod'_copy, Fact ((dom :~>: cod) f)) =>
Fact (
(cod :⊆: cod'_copy)
-> (dom :~>: cod') f
)
where
auto x = extendCod auto x
funEq :: forall dom cod cod' f f'.
(dom :~>: cod) f
-> (dom :~>: cod') f'
-> f :⊆: f'
-> f :==: f'
funEq f f' pSub =
SetEq pSub
(Subset (\(f'ab :: ab :∈: f') ->
relCPS f' f'ab
(\(a :: dom a) _ ->
totalCPS f a (\ (fab' :: (a,b') :∈: f) ->
case pSub `scoerce` fab' of
(f'ab' :: (a,b') :∈: f') ->
svalCPS f' f'ab' f'ab
(fab' :: ab :∈: f))
)))
funEq' ::
(dom :~>: cod) f
-> (dom :~>: cod') f'
-> f' :⊆: f
-> f :==: f'
funEq' f f' pSub = setEqSym (funEq f' f pSub)
equal_f :: (d :~>: c) f' ->
f :==: f' ->
(x,y) :∈: f ->
(x,y') :∈: f' ->
y :=: y'
equal_f f' eq fxy fxy' = sval f' (eq `ecoerce` fxy) fxy'
equal_f_coerce :: (d :~>: c) f' ->
f :==: f' ->
(x,y) :∈: f ->
(x,y') :∈: f' ->
y -> y'
equal_f_coerce f' eq fxy fxy' = coerce (equal_f f' eq fxy fxy')
isFun_congruence :: (d :~>: c) f ->
f :==: f' ->
(d :~>: c) f'
isFun_congruence f eq = IsFun
(Subset (\p -> rel f (eq `ecoerceFlip` p)))
(\p -> totalCPS f p (\fxy -> ExSnd (eq `ecoerce` fxy)))
(\p1 p2 k -> svalCPS f
(eq `ecoerceFlip` p1)
(eq `ecoerceFlip` p2)
k)
data Incl (dom :: SET) (cod :: SET) :: SET where
Incl :: dom a -> Incl dom cod (a,a)
type Id dom = Incl dom dom
inclusionIsFun :: dom :⊆: cod -> (dom :~>: cod) (Incl dom cod)
inclusionIsFun q = IsFun
(Subset (\(Incl p1) -> p1 :×: (q `scoerce` p1)))
(\p -> ExSnd (Incl p))
(\(Incl _) (Incl _) k -> k)
instance (Fact (dom :⊆: cod))
=> Fact ((dom :~>: cod) (Incl dom cod))
where
auto = inclusionIsFun auto
idIsFun :: (dom :~>: dom) (Id dom)
idIsFun = inclusionIsFun subsetRefl
data ((g :: SET) :○: (f :: SET)) :: SET where
Compo ::
(b, c) :∈: g ->
(a, b) :∈: f ->
(g :○: f) (a, c)
infixr 5 :○:
compoIsFun :: (s2 :~>: s3) g ->
(s1 :~>: s2) f ->
(s1 :~>: s3) (g :○: f)
compoIsFun g f =
IsFun
(Subset (\(Compo gbc fab) -> case (rel g gbc, rel f fab) of
( _ :×: pc
, pa :×: _ ) ->
pa :×: pc))
(\p -> case total f p of
ExSnd fab ->
case total g (inCod f fab) of
ExSnd gbc ->
ExSnd (Compo gbc fab))
(\(Compo gbc fab) (Compo gbc' fab') k -> svalCPS f fab fab'
(svalCPS g gbc gbc' k))
instance
( Fact ( (s2 :~>: s3) g )
, Fact ( (s1 :~>: s2) f )
)
=>
Fact ((s1 :~>: s3) (g :○: f))
where
auto = compoIsFun (auto :: (s2 :~>: s3) g) auto
compo_idl :: (d :~>: c) f -> (Id c :○: f) :==: f
compo_idl f = funEq (compoIsFun idIsFun f) f
(Subset (\(Compo (Incl y) fxy) -> fxy))
compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: f
compo_idr f = funEq (compoIsFun f idIsFun) f
(Subset (\(Compo fxy (Incl x)) -> fxy))
compo_assoc
::
(:~>:) s2 cod g
-> (:~>:) s21 s2 f
-> (:~>:) dom s21 f1
-> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1))
compo_assoc h g f = funEq ((compoIsFun h g) `compoIsFun` f)
(h `compoIsFun` (g `compoIsFun` f))
(Subset (\(Compo (Compo vh vg) vf) ->
Compo vh (Compo vg vf)))
data Equaliser (f1 :: SET) (f2 :: SET) :: SET where
Equaliser :: (a, b) :∈: f1 -> (a, b) :∈: f2 -> Equaliser f1 f2 a
type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) s
equaliserSubset :: (s :~>: t) f1
-> (Equaliser f1 f2) :⊆: s
equaliserSubset f = Subset (\(Equaliser p _) -> inDom f p)
equaliserIsFun :: (s :~>: t) f1
-> ((Equaliser f1 f2) :~>: s)
(EqualiserIncl s f1 f2)
equaliserIsFun f = inclusionIsFun (equaliserSubset f)
equaliserUni :: (s0 :~>: s) g
-> (s :~>: t) f1
-> (f1 :○: g) :==: (f2 :○: g)
-> (s0 :~>: (Equaliser f1 f2)) g
equaliserUni g f1 pEq =
adjustCod g
(Subset (\(Image _ gab) ->
case total f1 (inCod g gab) of
ExSnd f1bc ->
case pEq `ecoerce` (Compo f1bc gab) of
Compo f2b'c gab' ->
case sval g gab gab' of
Refl -> Equaliser f1bc f2b'c))
data Injective (f :: SET) :: * where
Injective :: (forall a1 a2 b r.
( a1, b) :∈: f ->
( a2, b) :∈: f ->
(a1 ~ a2 => r) ->
r)
-> Injective f
injective :: forall f a1 a2 b .
Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) ->
a1 :=: a2
injective (Injective p) p1 p2 = p p1 p2 (Refl :: (a1 ~ a2) => a1 :=: a2)
inclusion_Injective :: Injective (Incl dom cod)
inclusion_Injective = Injective (\(Incl _) (Incl _) k -> k)
data Preimage (f :: SET) (s :: SET) :: SET where
Preimage :: (a, b) :∈: f -> b :∈: s -> Preimage f s a
preimage_Image ::
(dom :~>: cod) f ->
set :⊆: dom ->
set :⊆: Preimage f (Image f set)
preimage_Image f s = Subset
(\x ->
let
dom_x = s `scoerce` x
in
totalCPS f dom_x
(\fxy -> Preimage fxy (Image x fxy)))
image_Preimage ::
(dom :~>: cod) f ->
Image f (Preimage f set) :⊆: set
image_Preimage f = Subset
(\(Image (Preimage fxy y) fxy') -> case sval f fxy fxy' of
Refl -> y)
data Fst (s1 :: SET) (s2 :: SET) :: SET where
Fst :: a :∈: s1 -> b :∈: s2 -> Fst s1 s2 ((,) ((,) a b) a)
data Snd (s1 :: SET) (s2 :: SET) :: SET where
Snd :: a :∈: s1 -> b :∈: s2 -> Snd s1 s2 ((,) ((,) a b) b)
data ((f1 :: SET) :***: (f2 :: SET)) :: SET where
(:***:) :: ((,) a b1) :∈: f1 ->
((,) a b2) :∈: f2 ->
(f1 :***: f2) (a,((,) b1 b2))
infixr 3 :***:
fstIsFun :: ((s1 :×: s2) :~>: s1) (Fst s1 s2)
fstIsFun = IsFun
(Subset (\(Fst p q) -> (p :×: q) :×: p))
(\(p :×: q) -> ExSnd (Fst p q))
(\(Fst _ _) (Fst _ _) k -> k)
sndIsFun :: ( (s1 :×: s2) :~>: s2) (Snd s1 s2)
sndIsFun = IsFun
(Subset (\(Snd p q) -> (p :×: q) :×: q))
(\(p :×: q) -> ExSnd (Snd p q))
(\(Snd _ _) (Snd _ _) k -> k)
targetTuplingIsFun :: (dom :~>: cod1) f1
-> (dom :~>: cod2) f2
-> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2)
targetTuplingIsFun f1 f2 = IsFun
(Subset (\(p1 :***: p2) -> inDom f1 p1
:×:
(inCod f1 p1 :×: inCod f2 p2)))
(\p -> case (total f1 p , total f2 p) of
(ExSnd p1, ExSnd p2) -> ExSnd (p1 :***: p2))
(\(p1 :***: p2)
(q1 :***: q2) k
-> svalCPS f1 p1 q1
(svalCPS f2 p2 q2 k))
instance (
Fact ((dom :~>: cod1) f1)
, Fact ((dom :~>: cod2) f2)
)
=> Fact (
(dom :~>: (cod1 :×: cod2))
(f1 :***: f2)
)
where
auto = targetTuplingIsFun auto auto
fst_tupling ::
(dom :~>: cod1) f1 ->
(dom :~>: cod2) f2 ->
Fst cod1 cod2 :○: (f1 :***: f2) :==: f1
fst_tupling f1 f2 = funEq (compoIsFun fstIsFun (targetTuplingIsFun f1 f2)) f1
(Subset (\(Compo (Fst _ _) (vf1 :***: _)) -> vf1))
snd_tupling ::
(dom :~>: cod1) f1 ->
(dom :~>: cod2) f2 ->
Snd cod1 cod2 :○: (f1 :***: f2) :==: f2
snd_tupling f1 f2 = funEq (compoIsFun sndIsFun (targetTuplingIsFun f1 f2)) f2
(Subset (\(Compo (Snd _ _) (_ :***: vf2)) -> vf2))
tupling_eta ::
(dom :~>: (cod1 :×: cod2)) f ->
((Fst cod1 cod2 :○: f)
:***:
(Snd cod1 cod2 :○: f))
:==: f
tupling_eta f = funEq (targetTuplingIsFun (fstIsFun `compoIsFun` f)
(sndIsFun `compoIsFun` f)) f
(Subset (\((Compo (Fst _ _) vf) :***: (Compo (Snd _ _) vf')) ->
case sval f vf vf' of
Refl -> vf))
data HaskFun :: SET where
HaskFun :: HaskFun ((,) ((,) a b) (a -> b))
instance (a_copy~a, b_copy~b) => Fact (((a_copy, b_copy), a -> b) :∈: HaskFun) where
auto = HaskFun
haskFunIsFun :: ((Univ :×: Univ) :~>: FunctionType) HaskFun
haskFunIsFun = IsFun
(Subset (\HaskFun -> ((Univ :×: Univ) :×: FunctionType)))
(\(_ :×: _) -> ExSnd HaskFun)
(\HaskFun HaskFun k -> k)
haskFunInjective :: Injective HaskFun
haskFunInjective = Injective (\HaskFun HaskFun k -> k)
data KleisliHom (m :: * -> *) :: SET where
KleisliHom :: KleisliHom m ((,) ((,) a b) (a -> m b))
kleisliHomIsFun :: ((Univ :×: Univ) :~>: (KleisliType m)) (KleisliHom m)
kleisliHomIsFun = IsFun
(Subset (\KleisliHom -> ((Univ :×: Univ) :×: KleisliType)))
(\(_ :×: _) -> ExSnd KleisliHom)
(\KleisliHom KleisliHom k -> k)
kleisliHomInjective :: Injective (KleisliHom m)
kleisliHomInjective = Injective (\KleisliHom KleisliHom k -> k)
instance (a1~a, b1~b, m1~m) => Fact (((a1, b1), a -> m1 b) :∈: KleisliHom m) where
auto = KleisliHom
data Graph f :: SET where
Graph :: Graph f (a, (f a))
graphIsFun :: (Univ :~>: Univ) (Graph f)
graphIsFun = IsFun
(Subset (\Graph -> Univ :×: Univ))
(\_ -> ExSnd Graph)
(\Graph Graph k -> k)
graphCPS :: pair :∈: Graph f ->
(forall a. (pair ~ (a,f a)) => r) ->
r
graphCPS Graph k = k
graphInjective :: Injective (Graph f)
graphInjective = Injective (\Graph Graph k -> k)
imageGraphList ::
[a] :∈: Image (Graph []) Univ
imageGraphList = Image Univ Graph
instance (a~a_copy) => Fact ((a_copy, f a) :∈: Graph f) where
auto = Graph
data ToTyCon (f::SET) x = forall y. ToTyCon ((x,y) :∈: f) y
introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f x
introToTyCon = ToTyCon
elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x,z) :∈: f) -> z
elimToTyCon f (ToTyCon fxy y) fxz = svalCoerce f fxy fxz y
toTCG :: f x -> ToTyCon (Graph f) x
toTCG fx = ToTyCon Graph fx
fromTCG :: ToTyCon (Graph f) x -> f x
fromTCG (ToTyCon Graph fx) = fx
data BiGraph f :: SET where
BiGraph :: BiGraph f ((a,b) , (f a b))
biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f)
biGraphIsFun = IsFun
(Subset (\BiGraph -> (Univ :×: Univ) :×: Univ))
(\(_ :×: _) -> ExSnd BiGraph)
(\BiGraph BiGraph k -> k)
biGraphInjective :: Injective (BiGraph f)
biGraphInjective = Injective (\BiGraph BiGraph k -> k)
instance (a~a_copy, b~b_copy) => Fact (((a_copy,b_copy), f a b) :∈: BiGraph f) where
auto = BiGraph
biGraph_eq_HaskFun :: BiGraph (->) :==: HaskFun
biGraph_eq_HaskFun = funEq biGraphIsFun haskFunIsFun
(Subset (\BiGraph -> HaskFun))
data Const dom x :: SET where
Const :: a :∈: dom -> Const dom x (a,x)
constIsFun :: x :∈: cod -> (dom :~>: cod) (Const dom x)
constIsFun x = IsFun
(Subset (\(Const a) -> a :×: x))
(\a -> ExSnd (Const a))
(\(Const a) (Const a') k -> k)
constEq :: Ex dom -> Const dom x :==: Const dom' x' -> x :=: x'
constEq (Ex a) eq = case eq `ecoerce` (Const a) of
Const _ -> Refl
data (Π (fam :: SET)) (f :: SET) where
Π ::
(base :~>: Unions fam) f
->
(forall x y s. (x,y) :∈: f ->
(x,Lower s) :∈: fam ->
x :∈: s)
->
Π fam f
data (Section (bundleMap :: SET)) (f::SET) where
Section ::
(forall x y. (x,y) :∈: f -> (y,x) :∈: bundleMap)
->
Section bundleMap f
idLemma :: ((dom :~>: dom) f) ->
(forall x y. (x,y) :∈: f -> x :=: y) ->
(Id dom :==: f)
idLemma f p = funEq idIsFun f
(Subset (\(Incl x) -> case total f x of
ExSnd fxy -> case p fxy of
Refl -> fxy))
section_CompoId ::
(total :~>: base) bun ->
(base :~>: total) f ->
( Section bun f ) ->
(bun :○: f :==: Id base)
section_CompoId bun f (Section s) =
setEqSym (idLemma (compoIsFun bun f)
(\(Compo bun_yx f_xy) -> case sval bun bun_yx (s f_xy) of
Refl -> Refl)
)
compoId_Section ::
( (total :~>: base) bun ) ->
( (base :~>: total) f ) ->
(bun :○: f :==: Id base)
-> ( Section bun f )
compoId_Section bun f eq =
Section (\f_xy -> case rel f f_xy of
(x :×: y) ->
case total bun y of
ExSnd bun_yx' ->
case equal_f
idIsFun
eq
(Compo bun_yx' f_xy)
(Incl x) of
Refl -> bun_yx')
data Inv (f :: SET) :: SET where
Inv :: (a,b) :∈: f -> Inv f (b,a)
invInv0 :: Inv (Inv f) :⊆: f
invInv0 = Subset (\(Inv (Inv p)) -> p)
invInv :: (dom :~>: cod) f -> (Inv (Inv f)) :==: f
invInv f = SetEq invInv0
(Subset (\fxy -> case rel f fxy of
_ :×: _ -> Inv (Inv fxy)))
injective_Inv :: (dom :~>: cod) f -> Injective f ->
(Image f dom :~>: dom) (Inv f)
injective_Inv f (Injective inj) =
IsFun
(Subset (\(Inv fxy) -> case rel f fxy of
x :×: _ -> Image x fxy :×: x))
(\(Image _ fxy) -> ExSnd (Inv fxy))
(\(Inv fxy) (Inv fx'y) k -> inj fxy fx'y k)
invId :: Inv (Id dom) :==: Id dom
invId = SetEq (Subset (\(Inv (Incl xx)) -> Incl xx))
(Subset (\(Incl xx) -> (Inv (Incl xx))))
$(lemmata ''Fact ['targetTuplingIsFun,'fstIsFun,'sndIsFun
,'haskFunIsFun, 'haskFunInjective
,'kleisliHomIsFun, 'kleisliHomInjective
,'compoIsFun, 'idIsFun, 'inclusionIsFun
,'sval,'relation,'rel,'total
, 'graphInjective, 'graphIsFun
, 'biGraphInjective, 'biGraphIsFun
, 'funEq
, 'extendCod
, 'equaliserSubset, 'equaliserUni, 'equaliserIsFun
, 'equal_f
,'inDom,'inCod,'domUniq
,'imageUnion
,'compo_idl,'compo_idr
,'lowerFun, 'raiseFun
,'constIsFun, 'constEq
,'section_CompoId,'compoId_Section
,'injective_Inv, 'inclusion_Injective, 'invId
,'preimage_Image, 'image_Preimage
,'compo_assoc
,'fst_tupling, 'snd_tupling, 'tupling_eta
])