Type.Function
 Contents Preliminary Functions Set of functions Images Equality Inclusion functions, identity, composition Equalisers Injectivity Preimages Binary product projections, target tupling Particular functions Conversions type constructors <-> type-level functions Constant functions Dependent product Sections Inverses
Description

Notes

• Functions are coded as functional relations (in particular, functions are sets)
• Extensional equality of functions coincedes with extensional equality of sets.
Synopsis
data ExSnd f 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 :~>: cod where
 IsFun :: (f :⊆: (dom :×: cod)) -> Total dom f -> Sval f -> (dom :~>: cod) f
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
data Image f s where
 Image :: (a :∈: s) -> ((a, b) :∈: f) -> Image f s b
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'
data Incl dom cod where
 Incl :: dom a -> Incl dom cod (a, a)
type Id dom = Incl dom dom
inclusionIsFun :: (dom :⊆: cod) -> (dom :~>: cod) (Incl dom cod)
idIsFun :: (dom :~>: dom) (Id dom)
data g :○: f where
 Compo :: ((b, c) :∈: g) -> ((a, b) :∈: f) -> (g :○: f) (a, c)
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))
data Equaliser f1 f2 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
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
data Injective f 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
inclusion_Injective :: Injective (Incl dom cod)
data Preimage f s where
 Preimage :: ((a, b) :∈: f) -> (b :∈: s) -> Preimage f s a
preimage_Image :: (dom :~>: cod) f -> (set :⊆: dom) -> set :⊆: Preimage f (Image f set)
image_Preimage :: (dom :~>: cod) f -> Image f (Preimage f set) :⊆: set
data Fst s1 s2 where
 Fst :: (a :∈: s1) -> (b :∈: s2) -> Fst s1 s2 ((,) ((,) a b) a)
data Snd s1 s2 where
 Snd :: (a :∈: s1) -> (b :∈: s2) -> Snd s1 s2 ((,) ((,) a b) b)
data f1 :***: f2 where
 :***: :: ((,) a b1 :∈: f1) -> ((,) a b2 :∈: f2) -> (f1 :***: f2) (a, (,) b1 b2)
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
data KleisliHom m where
 KleisliHom :: KleisliHom m ((,) ((,) a b) (a -> m b))
kleisliHomIsFun :: ((Univ :×: Univ) :~>: KleisliType m) (KleisliHom m)
kleisliHomInjective :: Injective (KleisliHom m)
data Graph f where
 Graph :: Graph f (a, f a)
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
data BiGraph f where
 BiGraph :: BiGraph f ((a, b), f a b)
biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f)
biGraphInjective :: Injective (BiGraph f)
data Const dom x where
 Const :: (a :∈: dom) -> Const dom x (a, x)
constIsFun :: (x :∈: cod) -> (dom :~>: cod) (Const dom x)
constEq :: Ex dom -> (Const dom x :==: Const dom' x') -> x :=: x'
data Π fam f where
 Π :: (base :~>: Unions fam) f -> (forall x y s. ((x, y) :∈: f) -> ((x, Lower s) :∈: fam) -> x :∈: s) -> Π fam f
data Section bundleMap f 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
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
data Inv f where
 Inv :: ((a, b) :∈: f) -> Inv f (b, a)
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
 data ExSnd f a where Source
Existential quantification over the first component of a pair
Constructors
 ExSnd :: ((a, ex) :∈: f) -> ExSnd f a
 type Total dom f = forall a. (a :∈: dom) -> ExSnd f a Source
Totality
 type Sval f = forall a b1 b2 r. ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> r Source
Single-valuedness (CPS)
Functions
 data dom :~>: cod where Source

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
 IsFun :: (f :⊆: (dom :×: cod)) -> Total dom f -> Sval f -> (dom :~>: cod) f
Instances
 (Fact ((dom :~>: cod1) f1), Fact ((dom :~>: cod2) f2)) => Fact ((dom :~>: (cod1 :×: cod2)) (f1 :***: f2)) (Fact ((s2 :~>: s3) g), Fact ((s1 :~>: s2) f)) => Fact ((s1 :~>: s3) (g :○: f)) Fact (dom :⊆: cod) => Fact ((dom :~>: cod) (Incl dom cod)) Fact ((dom :~>: dom) (Id dom)) Fact ((Univ :~>: Univ) (Graph f)) Fact (((s1 :×: s2) :~>: s2) (Snd s1 s2)) Fact (((s1 :×: s2) :~>: s1) (Fst s1 s2)) Fact (((Univ :×: Univ) :~>: KleisliType m) (KleisliHom m)) Fact (((Univ :×: Univ) :~>: FunctionType) HaskFun) Fact (((Univ :×: Univ) :~>: Univ) (BiGraph f))
 relation :: (dom :~>: cod) f -> f :⊆: (dom :×: cod) Source
Functions are relations
 total :: (dom :~>: cod) f -> (a :∈: dom) -> ExSnd f a Source
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
 rel :: (dom :~>: cod) f -> (pair :∈: f) -> pair :∈: (dom :×: cod) 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
 inDom :: (dom :~>: cod) f -> ((a, b) :∈: f) -> a :∈: dom Source
If f a = b, then a is in the domain of f
 inCod :: (dom :~>: cod) f -> ((a, b) :∈: f) -> b :∈: cod Source
If f a = b, then b is in the codomain of f
 domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2 Source
The domain of a function is uniquely determined
Set of functions
 type :~~>: dom cod = Lower1 (dom :~>: cod) Source

Kind-casted variant (function space as a set)

Convention: Instances of Fact should always prove ':~>:' rather than this type.

 lowerFun :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f) Source
 raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f Source
 raiseFunCPS :: (dom :~~>: cod) lf -> (forall f. lf ~ Lower f => (dom :~>: cod) f -> r) -> r Source
This is stronger than raiseFun since it introduces the knowledge that lf is of the form Lower f, rather than assuming it.
Images
 data Image f s where Source
Image of a set under the function
Constructors
 Image :: (a :∈: s) -> ((a, b) :∈: f) -> Image f s b
 imageCod :: (dom :~>: cod) f -> Image f s :⊆: cod Source
Every image is a subset of every possible codomain
 setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) f Source
The full image is a codomain
 adjustCod :: (dom :~>: cod) f -> (Image f dom :⊆: cod') -> (dom :~>: cod') f Source
Change the codomain by proving that the full image is included in the new codomain
 extendCod :: (dom :~>: cod) f -> (cod :⊆: cod') -> (dom :~>: cod') f Source
Enlargen the codomain
 imageMonotonic :: (s1 :⊆: s2) -> Image f s1 :⊆: Image f s2 Source
 imageEmpty :: Image f Empty :==: Empty Source
 imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom) Source
 fullImageOfInclusion :: (dom :⊆: cod) -> Image (Incl dom cod) dom :==: dom Source
 imageUnion :: forall dom cod s1 s2 f. (dom :~>: cod) f -> Image f (s1 :∪: s2) :==: (Image f s1 :∪: Image f s2) Source
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' :: (dom :~>: cod) f -> (dom :~>: cod') f' -> (f' :⊆: f) -> f :==: f' Source
funEq with the inclusion argument flipped
 equal_f :: (d :~>: c) f' -> (f :==: f') -> ((x, y) :∈: f) -> ((x, y') :∈: f') -> y :=: y' Source
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
 isFun_congruence :: (d :~>: c) f -> (f :==: f') -> (d :~>: c) f' Source
Inclusion functions, identity, composition
 data Incl dom cod where Source

Inclusion function of a subset

Inclusions do know their codomain (somewhat arbitrary design decision)

Constructors
 Incl :: dom a -> Incl dom cod (a, a)
 type Id dom = Incl dom dom Source
Identity function on dom
 inclusionIsFun :: (dom :⊆: cod) -> (dom :~>: cod) (Incl dom cod) Source
Inclusion is a function
 idIsFun :: (dom :~>: dom) (Id dom) Source
Id is a function
 data g :○: f where Source
Composition
Constructors
 Compo :: ((b, c) :∈: g) -> ((a, b) :∈: f) -> (g :○: f) (a, c)
 compoIsFun :: (s2 :~>: s3) g -> (s1 :~>: s2) f -> (s1 :~>: s3) (g :○: f) Source
The composition is a function
 compo_idl :: (d :~>: c) f -> (Id c :○: f) :==: f Source
Id is a left identity for composition
 compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: f Source
Id is a right identity for composition
 compo_assoc :: :~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1)) Source
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
 Equaliser :: ((a, b) :∈: f1) -> ((a, b) :∈: f2) -> Equaliser f1 f2 a
 type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) s Source
Inclusion of the equaliser into the domain of the parallel functions
 equaliserSubset :: (s :~>: t) f1 -> Equaliser f1 f2 :⊆: s Source
The equaliser is a subset of the domain of the parallel functions
 equaliserIsFun :: (s :~>: t) f1 -> (Equaliser f1 f2 :~>: s) (EqualiserIncl s f1 f2) Source
The equaliser inclusion is a function
 equaliserUni :: (s0 :~>: s) g -> (s :~>: t) f1 -> ((f1 :○: g) :==: (f2 :○: g)) -> (s0 :~>: Equaliser f1 f2) g Source

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
 data Injective f where Source

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
 Fact (Injective (BiGraph f)) Fact (Injective (Graph f)) Fact (Injective (KleisliHom m)) Fact (Injective HaskFun) Fact (Injective (Incl dom cod))
 injective :: forall f a1 a2 b. Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> a1 :=: a2 Source
 inclusion_Injective :: Injective (Incl dom cod) Source
Preimages
 data Preimage f s where Source
Constructors
 Preimage :: ((a, b) :∈: f) -> (b :∈: s) -> Preimage f s a
 preimage_Image :: (dom :~>: cod) f -> (set :⊆: dom) -> set :⊆: Preimage f (Image f set) Source
 image_Preimage :: (dom :~>: cod) f -> Image f (Preimage f set) :⊆: set Source
Binary product projections, target tupling
 data Fst s1 s2 where Source
Constructors
 Fst :: (a :∈: s1) -> (b :∈: s2) -> Fst s1 s2 ((,) ((,) a b) a)
 data Snd s1 s2 where Source
Constructors
 Snd :: (a :∈: s1) -> (b :∈: s2) -> Snd s1 s2 ((,) ((,) a b) b)
 data f1 :***: f2 where Source
Analogous to ***
Constructors
 :***: :: ((,) a b1 :∈: f1) -> ((,) a b2 :∈: f2) -> (f1 :***: f2) (a, (,) b1 b2)
 fstIsFun :: ((s1 :×: s2) :~>: s1) (Fst s1 s2) Source
 sndIsFun :: ((s1 :×: s2) :~>: s2) (Snd s1 s2) Source
 targetTuplingIsFun :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2) Source
 fst_tupling :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (Fst cod1 cod2 :○: (f1 :***: f2)) :==: f1 Source
 snd_tupling :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (Snd cod1 cod2 :○: (f1 :***: f2)) :==: f2 Source
 tupling_eta :: (dom :~>: (cod1 :×: cod2)) f -> ((Fst cod1 cod2 :○: f) :***: (Snd cod1 cod2 :○: f)) :==: f Source
Particular functions

The type-level function:

Constructors
Instances
 (a_copy ~ a, b_copy ~ b) => Fact ((,) ((,) a_copy b_copy) (a -> b) :∈: HaskFun)
 data KleisliHom m where Source

The type-level function:

KleisliHom(a,b) = (a -> m b)

Constructors
 KleisliHom :: KleisliHom m ((,) ((,) a b) (a -> m b))
Instances
 (a1 ~ a, b1 ~ b, m1 ~ m) => Fact ((,) ((,) a1 b1) (a -> m1 b) :∈: KleisliHom m)
 kleisliHomIsFun :: ((Univ :×: Univ) :~>: KleisliType m) (KleisliHom m) Source
 kleisliHomInjective :: Injective (KleisliHom m) Source
Conversions type constructors <-> type-level functions
 data Graph f where Source
Graph of a (* -> *) type constructor
Constructors
 Graph :: Graph f (a, f a)
Instances
 a ~ a_copy => Fact ((,) a_copy (f a) :∈: Graph f)
 graphIsFun :: (Univ :~>: Univ) (Graph f) Source
 graphCPS :: (pair :∈: Graph f) -> (forall a. pair ~ (a, f a) => r) -> r Source
 graphInjective :: Injective (Graph f) Source
Type constructors are injective
 imageGraphList :: [a] :∈: Image (Graph []) Univ Source
 data ToTyCon f x Source
Constructors
 forall y . ToTyCon ((x, y) :∈: f) y
 introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f x Source
 elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x, z) :∈: f) -> z Source
NB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness
 toTCG :: f x -> ToTyCon (Graph f) x Source
 fromTCG :: ToTyCon (Graph f) x -> f x Source
 data BiGraph f where Source
Graph of a (* -> * -> *) type constructor
Constructors
 BiGraph :: BiGraph f ((a, b), f a b)
Instances
 (a ~ a_copy, b ~ b_copy) => Fact ((,) ((,) a_copy b_copy) (f a b) :∈: BiGraph f)
 biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f) Source
 biGraphInjective :: Injective (BiGraph f) Source
Type constructors are injective
Example of an extensional equation between functions
Constant functions
 data Const dom x where Source
Constructors
 Const :: (a :∈: dom) -> Const dom x (a, x)
 constIsFun :: (x :∈: cod) -> (dom :~>: cod) (Const dom x) Source
 constEq :: Ex dom -> (Const dom x :==: Const dom' x') -> x :=: x' Source
Dependent product
 data Π fam f where Source
NB: fam must be a function mapping some set to a set of sets, or the second condition in the constructor is vacuous
Constructors
 Π :: (base :~>: Unions fam) f -> (forall x y s. ((x, y) :∈: f) -> ((x, Lower s) :∈: fam) -> x :∈: s) -> Π fam f
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
 idLemma :: (dom :~>: dom) f -> (forall x y. ((x, y) :∈: f) -> x :=: y) -> Id dom :==: f Source
Lemma for proving a function equal to the identity
 section_CompoId :: (total :~>: base) bun -> (base :~>: total) f -> Section bun f -> (bun :○: f) :==: Id base Source
Is section ==> composition is id
 compoId_Section :: (total :~>: base) bun -> (base :~>: total) f -> ((bun :○: f) :==: Id base) -> Section bun f Source
Composition is id ==> is section
Inverses
 data Inv f where Source
Constructors
 Inv :: ((a, b) :∈: f) -> Inv f (b, a)
 invInv0 :: Inv (Inv f) :⊆: f Source
 invInv :: (dom :~>: cod) f -> Inv (Inv f) :==: f Source
 injective_Inv :: (dom :~>: cod) f -> Injective f -> (Image f dom :~>: dom) (Inv f) Source
An injective function has an inverse, with domain the image
 invId :: Inv (Id dom) :==: Id dom Source