Data.Linear.Inverse

This module is based on the content of the functional pearl
How to Take the Inverse of a Type
by Daniel Marshall and Dominic Orchard

Definitions

Inverse : Type -> Type

  Inverse is a shorthand for 'multiplicative skew inverse'

Totality: total
Visibility: export

mkInverse : (a -@ ()) -@ Inverse a

Totality: total
Visibility: export

divide : a -@ (Inverse a -@ ())

  And this is the morphism witnessing the multiplicative skew inverse

Totality: total
Visibility: export

doubleNegation : a -@ Inverse (Inverse a)

Totality: total
Visibility: export

maybeNeg : LMaybe a -@ (Inverse a -@ LMaybe (Inverse a))

  We only use the inverse of a if the LMaybe is actually Just.m

Totality: total
Visibility: export

lid : a -@ a

Totality: total
Visibility: public export

lcompose : (b -@ c) -@ ((a -@ b) -@ (a -@ c))

Totality: total
Visibility: public export

comap : (b -@ a) -@ (Inverse a -@ Inverse b)

Totality: total
Visibility: public export

comapId : (u : Inverse a) -> comap lid u = lid u

Totality: total
Visibility: export

comapComp : (u : Inverse a) -> comap (lcompose g f) u = lcompose (comap f) (comap g) u

Totality: total
Visibility: export

munit : () -@ Inverse ()

Totality: total
Visibility: export

mmult : Inverse a -@ (Inverse b -@ Inverse (LPair a b))

Totality: total
Visibility: export

Pow : Type -> INTEGER -> Type

Totality: total
Visibility: public export

zip : Pow a n -@ (Pow b n -@ Pow (LPair a b) n)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

powPositiveL : (m : Nat) -> (n : Nat) -> Pow a (cast (m + n)) -@ LPair (Pow a (cast m)) (Pow a (cast n))

Totality: total
Visibility: export

powPositiveR : (m : Nat) -> (n : Nat) -> Pow a (cast m) -@ (Pow a (cast n) -@ Pow a (cast (m + n)))

Totality: total
Visibility: export

powNegateL : (m : Nat) -> Pow a (negate (cast m)) -> Pow (Inverse a) (cast m)

Totality: total
Visibility: export

powNegateR : (m : Nat) -> Pow (Inverse a) (cast m) -> Pow a (negate (cast m))

Totality: total
Visibility: export

powNegativeL : (m : Nat) -> (n : Nat) -> Pow a (negate (cast (m + n))) -@ LPair (Pow a (negate (cast m))) (Pow a (negate (cast n)))

Totality: total
Visibility: export

powNegativeR : (m : Nat) -> (n : Nat) -> Pow a (negate (cast m)) -@ (Pow a (negate (cast n)) -@ Pow a (negate (cast (m + n))))

Totality: total
Visibility: export

powAnnihilate : (m : Nat) -> Pow a (cast m) -@ (Pow a (negate (cast m)) -@ ())

Totality: total
Visibility: export

powMinus : (m : Nat) -> (n : Nat) -> Pow a (cast m) -@ (Pow a (negate (cast n)) -@ Pow a (cast m - cast n))

Totality: total
Visibility: export