type-settheory-0.1.3: Sets and functions-as-relations in the type system

Type.Function

Description

Notes

• Functions are coded as functional relations (in particular, functions are sets)
• Extensional equality of functions coincedes with extensional equality of sets.

Synopsis

Preliminary

data ExSnd f a whereSource

Existential quantification over the first component of a pair

Constructors

 ExSnd :: ((a, ex) :∈: f) -> ExSnd f a

Instances

 Fact (:~>: dom cod f -> :∈: a dom -> ExSnd f a)

type Total dom f = forall a. (a :∈: dom) -> ExSnd f aSource

Totality

type Sval f = forall a b1 b2 r. ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> rSource

Single-valuedness (CPS)

Functions

data dom :~>: cod whereSource

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

 (cod' ~ cod'_copy, Fact (:~>: dom cod f)) => Fact (:⊆: cod cod'_copy -> :~>: dom cod' f) Fact (:⊆: dom cod -> :~>: dom cod (Incl dom cod)) Fact (:∈: x cod -> :~>: dom cod (Const dom x)) Fact (:~~>: dom cod (Lower f) -> :~>: dom cod f) Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) Fact (:~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> :==: (:○: (:○: g f) f1) (:○: g (:○: f f1))) Fact (:~>: dom cod f -> :⊆: (Image f (Preimage f set)) set) Fact (:~>: dom cod f -> :⊆: set dom -> :⊆: set (Preimage f (Image f set))) Fact (:~>: dom cod f -> Injective f -> :~>: (Image f dom) dom (Inv f)) Fact (:~>: total base bun -> :~>: base total f -> :==: (:○: bun f) (Id base) -> Section bun f) Fact (:~>: total base bun -> :~>: base total f -> Section bun f -> :==: (:○: bun f) (Id base)) Fact (:~>: dom cod f -> :~~>: dom cod (Lower f)) Fact (:~>: d c f -> :==: (:○: f (Id d)) f) Fact (:~>: d c f -> :==: (:○: (Id c) f) f) Fact (:~>: dom cod f -> :==: (Image f (:∪: s1 s2)) (:∪: (Image f s1) (Image f s2))) Fact (:~>: dom cod f -> :~>: dom2 cod f -> :==: dom dom2) Fact (:~>: dom cod f -> :∈: (a, b) f -> :∈: b cod) Fact (:~>: dom cod f -> :∈: (a, b) f -> :∈: a dom) Fact (:~>: d c f' -> :==: f f' -> :∈: (x, y) f -> :∈: (x, y') f' -> :=: y y') Fact (:~>: s t f1 -> :~>: (Equaliser f1 f2) s (EqualiserIncl s f1 f2)) Fact (:~>: s0 s g -> :~>: s t f1 -> :==: (:○: f1 g) (:○: f2 g) -> :~>: s0 (Equaliser f1 f2) g) Fact (:~>: s t f1 -> :⊆: (Equaliser f1 f2) s) Fact (:~>: dom cod f -> :⊆: cod cod' -> :~>: dom cod' f) Fact (:~>: dom cod f -> :~>: dom cod' f' -> :⊆: f f' -> :==: f f') Fact (:~>: dom cod f -> :∈: a dom -> ExSnd f a) Fact (:~>: dom cod f -> :∈: pair f -> :∈: pair (:×: dom cod)) Fact (:~>: dom cod f -> :⊆: f (:×: dom cod)) Fact (:~>: dom cod f -> :∈: (a, b1) f -> :∈: (a, b2) f -> :=: b1 b2) Fact (:~>: s2 s3 g -> :~>: s1 s2 f -> :~>: s1 s3 (:○: g f)) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :~>: dom (:×: cod1 cod2) (:***: f1 f2)) (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 aSource

Functions are total

totalCPS :: (dom :~>: cod) f -> (a :∈: dom) -> (forall totalCPS_y. ((a, totalCPS_y) :∈: f) -> totalCPS_return) -> totalCPS_returnSource

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 :=: b2Source

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 -> b2Source

Perform coercion using the single-valuedness

svalCPS :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> (b1 ~ b2 => r) -> rSource

Functions are single-valued (CPS version)

svalCPS' :: (dom :~>: cod) f -> ((a, b1) :∈: f) -> ((a, b2) :∈: f) -> ((b1 :=: b2) -> r) -> rSource

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_returnSource

inDom :: (dom :~>: cod) f -> ((a, b) :∈: f) -> a :∈: domSource

If `f a = b`, then `a` is in the domain of `f`

inCod :: (dom :~>: cod) f -> ((a, b) :∈: f) -> b :∈: codSource

If `f a = b`, then `b` is in the codomain of `f`

domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2Source

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) fSource

raiseFunCPS :: (dom :~~>: cod) lf -> (forall f. lf ~ Lower f => (dom :~>: cod) f -> r) -> rSource

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 whereSource

Image of a set under the function

Constructors

 Image :: (a :∈: s) -> ((a, b) :∈: f) -> Image f s b

Instances

 Fact (:~>: dom cod f -> :⊆: (Image f (Preimage f set)) set) Fact (:~>: dom cod f -> :⊆: set dom -> :⊆: set (Preimage f (Image f set))) Fact (:~>: dom cod f -> Injective f -> :~>: (Image f dom) dom (Inv f)) Fact (:~>: dom cod f -> :==: (Image f (:∪: s1 s2)) (:∪: (Image f s1) (Image f s2)))

imageCod :: (dom :~>: cod) f -> Image f s :⊆: codSource

Every image is a subset of every possible codomain

setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) fSource

The full image is a codomain

adjustCod :: (dom :~>: cod) f -> (Image f dom :⊆: cod') -> (dom :~>: cod') fSource

Change the codomain by proving that the full image is included in the new codomain

extendCod :: (dom :~>: cod) f -> (cod :⊆: cod') -> (dom :~>: cod') fSource

Enlargen the codomain

imageMonotonic :: (s1 :⊆: s2) -> Image f s1 :⊆: Image f s2Source

imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom)Source

fullImageOfInclusion :: (dom :⊆: cod) -> Image (Incl dom cod) dom :==: domSource

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 whereSource

Inclusion function of a subset

Inclusions do know their codomain (somewhat arbitrary design decision)

Constructors

 Incl :: dom a -> Incl dom cod (a, a)

Instances

 Fact (Injective (Incl dom cod)) Fact (:⊆: dom cod -> :~>: dom cod (Incl dom cod)) Fact (:⊆: dom cod) => Fact (:~>: dom cod (Incl dom cod))

type Id dom = Incl dom domSource

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 whereSource

Composition

Constructors

 Compo :: ((b, c) :∈: g) -> ((a, b) :∈: f) -> (g :○: f) (a, c)

Instances

 Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) Fact (:~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> :==: (:○: (:○: g f) f1) (:○: g (:○: f f1))) Fact (:~>: total base bun -> :~>: base total f -> :==: (:○: bun f) (Id base) -> Section bun f) Fact (:~>: total base bun -> :~>: base total f -> Section bun f -> :==: (:○: bun f) (Id base)) Fact (:~>: d c f -> :==: (:○: f (Id d)) f) Fact (:~>: d c f -> :==: (:○: (Id c) f) f) Fact (:~>: s0 s g -> :~>: s t f1 -> :==: (:○: f1 g) (:○: f2 g) -> :~>: s0 (Equaliser f1 f2) g) Fact (:~>: s2 s3 g -> :~>: s1 s2 f -> :~>: s1 s3 (:○: g f)) (Fact (:~>: s2 s3 g), Fact (:~>: s1 s2 f)) => Fact (:~>: s1 s3 (:○: g f))

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) :==: fSource

`Id` is a left identity for composition

compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: fSource

`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 whereSource

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

Instances

 Fact (:~>: s t f1 -> :~>: (Equaliser f1 f2) s (EqualiserIncl s f1 f2)) Fact (:~>: s0 s g -> :~>: s t f1 -> :==: (:○: f1 g) (:○: f2 g) -> :~>: s0 (Equaliser f1 f2) g) Fact (:~>: s t f1 -> :⊆: (Equaliser f1 f2) s)

type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) sSource

Inclusion of the equaliser into the domain of the parallel functions

equaliserSubset :: (s :~>: t) f1 -> Equaliser f1 f2 :⊆: sSource

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) gSource

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 whereSource

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)) Fact (:~>: dom cod f -> Injective f -> :~>: (Image f dom) dom (Inv f))

injective :: forall f a1 a2 b. Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> a1 :=: a2Source

Preimages

data Preimage f s whereSource

Constructors

 Preimage :: ((a, b) :∈: f) -> (b :∈: s) -> Preimage f s a

Instances

 Fact (:~>: dom cod f -> :⊆: (Image f (Preimage f set)) set) Fact (:~>: dom cod f -> :⊆: set dom -> :⊆: set (Preimage f (Image f set)))

preimage_Image :: (dom :~>: cod) f -> (set :⊆: dom) -> set :⊆: Preimage f (Image f set)Source

image_Preimage :: (dom :~>: cod) f -> Image f (Preimage f set) :⊆: setSource

Binary product projections, target tupling

data Fst s1 s2 whereSource

Constructors

 Fst :: (a :∈: s1) -> (b :∈: s2) -> Fst s1 s2 ((,) ((,) a b) a)

Instances

 Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) Fact (:~>: (:×: s1 s2) s1 (Fst s1 s2))

data Snd s1 s2 whereSource

Constructors

 Snd :: (a :∈: s1) -> (b :∈: s2) -> Snd s1 s2 ((,) ((,) a b) b)

Instances

 Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) Fact (:~>: (:×: s1 s2) s2 (Snd s1 s2))

data f1 :***: f2 whereSource

Analogous to `***`

Constructors

 :***: :: ((,) a b1 :∈: f1) -> ((,) a b2 :∈: f2) -> (f1 :***: f2) (a, (,) b1 b2)

Instances

 Fact (:~>: dom (:×: cod1 cod2) f -> :==: (:***: (:○: (Fst cod1 cod2) f) (:○: (Snd cod1 cod2) f)) f) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Snd cod1 cod2) (:***: f1 f2)) f2) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :==: (:○: (Fst cod1 cod2) (:***: f1 f2)) f1) Fact (:~>: dom cod1 f1 -> :~>: dom cod2 f2 -> :~>: dom (:×: cod1 cod2) (:***: f1 f2)) (Fact (:~>: dom cod1 f1), Fact (:~>: dom cod2 f2)) => Fact (:~>: dom (:×: cod1 cod2) (:***: f1 f2))

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)) :==: f1Source

snd_tupling :: (dom :~>: cod1) f1 -> (dom :~>: cod2) f2 -> (Snd cod1 cod2 :○: (f1 :***: f2)) :==: f2Source

tupling_eta :: (dom :~>: (cod1 :×: cod2)) f -> ((Fst cod1 cod2 :○: f) :***: (Snd cod1 cod2 :○: f)) :==: fSource

Particular functions

data HaskFun whereSource

The type-level function:

HaskFun(a,b) = (a -> b)

Constructors

 HaskFun :: HaskFun ((,) ((,) a b) (a -> b))

Instances

 Fact (Injective HaskFun) (a_copy ~ a, b_copy ~ b) => Fact (:∈: ((a_copy, b_copy), a -> b) HaskFun) Fact (:~>: (:×: Univ Univ) FunctionType HaskFun)

data KleisliHom m whereSource

The type-level function:

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

Constructors

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

Instances

 Fact (Injective (KleisliHom m)) (a1 ~ a, b1 ~ b, m1 ~ m) => Fact (:∈: ((a1, b1), a -> m1 b) (KleisliHom m)) Fact (:~>: (:×: Univ Univ) (KleisliType m) (KleisliHom m))

Conversions type constructors <-> type-level functions

data Graph f whereSource

Graph of a `(* -> *)` type constructor

Constructors

 Graph :: Graph f (a, f a)

Instances

 Fact (Injective (Graph f)) a ~ a_copy => Fact (:∈: (a_copy, f a) (Graph f)) Fact (:~>: Univ Univ (Graph f))

graphCPS :: (pair :∈: Graph f) -> (forall a. pair ~ (a, f a) => r) -> rSource

Type constructors are injective

data ToTyCon f x Source

Constructors

 forall y . ToTyCon ((x, y) :∈: f) y

introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f xSource

elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x, z) :∈: f) -> zSource

NB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness

toTCG :: f x -> ToTyCon (Graph f) xSource

fromTCG :: ToTyCon (Graph f) x -> f xSource

data BiGraph f whereSource

Graph of a `(* -> * -> *)` type constructor

Constructors

 BiGraph :: BiGraph f ((a, b), f a b)

Instances

 Fact (Injective (BiGraph f)) (a ~ a_copy, b ~ b_copy) => Fact (:∈: ((a_copy, b_copy), f a b) (BiGraph f)) Fact (:~>: (:×: Univ Univ) Univ (BiGraph f))

Type constructors are injective

Example of an extensional equation between functions

Constant functions

data Const dom x whereSource

Constructors

 Const :: (a :∈: dom) -> Const dom x (a, x)

Instances

 Fact (Ex dom -> :==: (Const dom x) (Const dom' x') -> :=: x x') Fact (:∈: x cod -> :~>: dom cod (Const dom 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 whereSource

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 whereSource

Expresses that `f` is a section of `bundleMap`

Constructors

 Section :: (forall x y. ((x, y) :∈: f) -> (y, x) :∈: bundleMap) -> Section bundleMap f

Instances

 Fact (:~>: total base bun -> :~>: base total f -> :==: (:○: bun f) (Id base) -> Section bun f) Fact (:~>: total base bun -> :~>: base total f -> Section bun f -> :==: (:○: bun f) (Id base))

idLemma :: (dom :~>: dom) f -> (forall x y. ((x, y) :∈: f) -> x :=: y) -> Id dom :==: fSource

Lemma for proving a function equal to the identity

section_CompoId :: (total :~>: base) bun -> (base :~>: total) f -> Section bun f -> (bun :○: f) :==: Id baseSource

Is section ==> composition is id

compoId_Section :: (total :~>: base) bun -> (base :~>: total) f -> ((bun :○: f) :==: Id base) -> Section bun fSource

Composition is id ==> is section

Inverses

data Inv f whereSource

Constructors

 Inv :: ((a, b) :∈: f) -> Inv f (b, a)

Instances

 Fact (:~>: dom cod f -> Injective f -> :~>: (Image f dom) dom (Inv f)) Fact (:==: (Inv (Id dom)) (Id dom))

invInv :: (dom :~>: cod) f -> Inv (Inv f) :==: fSource

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 domSource