iを階数、A,B:U(i)を型、f:A→Bを関数とする。
- -型LInv(f):U(i)をRecord{∣inv:B→A,is-linv:inv∘f∼id∣}と定義する。
- -型RInv(f):U(i)をRecord{∣inv:B→A,is-rinv:f∘inv∼id∣}と定義する。
- -型IsBiinv(f):U(i)をRecord{∣linv:LInv(f),rinv:RInv(f)∣}と定義する。
IsBiinv(f)の要素がある時、
fは
両側可逆(biinvertible)であると言う。