Type.Function

Notes

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

Preliminary

data ExSnd f a where

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 a

Totality

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

Single-valuedness (CPS)

Functions

data dom :~>: cod where

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)

Functions are relations

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

Functions are total

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

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

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

Perform coercion using the single-valuedness

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

Functions are single-valued (CPS version)

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

rel :: (dom :~>: cod) f -> (pair :∈: f) -> pair :∈: (dom :×: cod)

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

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

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

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

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

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

The domain of a function is uniquely determined

Set of functions

type :~~>: dom cod = Lower1 (dom :~>: cod)

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)

raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f

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

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

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 :⊆: cod

Every image is a subset of every possible codomain

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

The full image is a codomain

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

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

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

Enlargen the codomain

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)

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'

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'

funEq with the inclusion argument flipped

equal_f :: (d :~>: c) f' -> (f :==: f') -> ((x, y) :∈: f) -> ((x, y') :∈: f') -> y :=: y'

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'

Perform coercion using a function equality

isFun_congruence :: (d :~>: c) f -> (f :==: f') -> (d :~>: c) f'

Inclusion functions, identity, composition

data Incl dom cod where

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 dom

Identity function on dom

inclusionIsFun :: (dom :⊆: cod) -> (dom :~>: cod) (Incl dom cod)

Inclusion is a function

idIsFun :: (dom :~>: dom) (Id dom)

Id is a function

data g :○: f where

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)

The composition is a function

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

Id is a left identity for composition

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

Id is a right identity for composition

compo_assoc :: :~>: s2 cod g -> :~>: s21 s2 f -> :~>: dom s21 f1 -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1))

Equalisers

data Equaliser f1 f2 where

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

Inclusion of the equaliser into the domain of the parallel functions

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

The equaliser is a subset of the domain of the parallel functions

equaliserIsFun :: (s :~>: t) f1 -> (Equaliser f1 f2 :~>: s) (EqualiserIncl s f1 f2)

The equaliser inclusion is a function

equaliserUni :: (s0 :~>: s) g -> (s :~>: t) f1 -> ((f1 :○: g) :==: (f2 :○: g)) -> (s0 :~>: Equaliser f1 f2) g

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

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

inclusion_Injective :: Injective (Incl dom cod)

Preimages

data Preimage f s where

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)

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

Binary product projections, target tupling

data Fst s1 s2 where

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 where

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 where

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)

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

Particular functions

data HaskFun where

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)

haskFunIsFun :: ((Univ :×: Univ) :~>: FunctionType) HaskFun

haskFunInjective :: Injective HaskFun

data KleisliHom m where

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

kleisliHomIsFun :: ((Univ :×: Univ) :~>: KleisliType m) (KleisliHom m)

kleisliHomInjective :: Injective (KleisliHom m)

Conversions type constructors <-> type-level functions

data Graph f where

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

graphIsFun :: (Univ :~>: Univ) (Graph f)

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

graphInjective :: Injective (Graph f)

Type constructors are injective

imageGraphList :: [a] :∈: Image (Graph []) Univ

data ToTyCon f x

Constructors

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

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

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

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

data BiGraph f where

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

biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f)

biGraphInjective :: Injective (BiGraph f)

Type constructors are injective

biGraph_eq_HaskFun :: BiGraph (->) :==: HaskFun

Example of an extensional equation between functions

Constant functions

data Const dom x where

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)

constEq :: Ex dom -> (Const dom x :==: Const dom' x') -> x :=: x'

Dependent product

data Π fam f where

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

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

Lemma for proving a function equal to the identity

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

Is section ==> composition is id

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

Composition is id ==> is section

Inverses

data Inv f where

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

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)

An injective function has an inverse, with domain the image

invId :: Inv (Id dom) :==: Id dom