Iso.idr

Isomorphisms

Propositional equality is not the only notion of equality that we will use. Isomorphisms play a big role in relating two constructs without relying on strict propositional equality. We start by defining isomorphisms of types and expand the definition to any preorder relation on a carrier.

Definition

An Isomorphism between two types $a,b\in Type$ is given by two maps $to:a\to b$ and $from:b\to a$ and proofs that they are inverses of each other.

record (≅) (left, right : Type) where
  constructor MkIso
  to : left -> right
  from : right -> left
  0 toFrom : (x : right) -> to (from x) === x
  0 fromTo : (x : left) -> from (to x) === x

We establish a couple of properties on isomorphisms that are crucial in using isomorphisms.

Proposition

Isomorphisms are reflexive. That is, given a type $a\in Type$ there is always an isomorphism $a\cong a$.

identity : (0 x : Type) -> x ≅ x
identity x = MkIso
  id
  id
  (\_ => Refl)
  (\_ => Refl)

Proposition

Isomorphisms are symetric, given an isomorphism $a\cong b$ we can obtain the isomorphism $b\cong a$

• code replace this by sym

symIso : x ≅ y -> y ≅ x
symIso (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

Proposition

Isomorphisms are transitive. That is, given ismorphisms $a\cong b$ and $b\cong c$ we obtain an isomorphism $a\cong c$.

• code replace this by trans or maybe |\cong>.

transIso : {0 x, y, z : Type} -> x ≅ y -> y ≅ z -> x ≅ z
transIso iso1 iso2 =
  MkIso
    (iso2.to . iso1.to)
    (iso1.from . iso2.from)
    (\v => cong iso2.to (iso1.toFrom (iso2.from v)) `trans` iso2.toFrom v)
    (\v => trans (cong iso1.from (iso2.fromTo (iso1.to v))) (iso1.fromTo v))

Proposition

Isomorphisms form an equivalence relation.

export
Reflexive Type (≅) where
  reflexive = identity _
 
export
Transitive Type (≅) where
  transitive = transIso
 
export
Symmetric Type (≅) where
  symmetric = symIso
 
export
Equivalence Type (≅) where

Equalities between isomorphisms

Isomorphisms themselves are interesting structures to study. To prove facts about them we need a notion of equality between isomorphisms. We define it as an equality between the two maps. That definition is enough as we do not need to prove anything about the coherence condtions since, by uniqueness of identity proofs~\ref{def:uip}, they are all the same.

• move into its own module Data.Iso.Eq

Definition

Ismorphism equality is given by equality of their $to$ and $from$ maps.

public export
record IsoEq (i1, i2 : left ≅ right) where
  constructor MkIsoEq
  0 eqTo : (x : left) -> i1.to x === i2.to x
  0 eqFrom : (x : right) -> i1.from x === i2.from x

Proposition

We can convert from Isomorphism equality into propositional equality.

isoEqToEq : IsoEq a b -> a === b

Proposition

Isomorphism equality is reflexive.

• replace this by identity : a -> IsoEq a a

export
reflIsoEq : IsoEq a a
reflIsoEq = MkIsoEq
  (\_ => Refl)
  (\_ => Refl)

Proposition

Isomorphism equality is symmetric.

export
symIsoEq : IsoEq a b -> IsoEq b a
symIsoEq (MkIsoEq et tf) = MkIsoEq (\x => sym (et x)) (\x => sym (tf x))

Proposition

Isomorphism equality is transitive.

export
trans : IsoEq a b -> IsoEq b c -> IsoEq a c

Using isomorphism equality we can start proving facts about isomoprhisms, for example the fact that transitivity of isomorphisms is associative.

Lemma

Transitivity of isomorphisms is associative.

export
transIsoAssoc : {0 a, b, c, d : Type} ->
                 (f : a ≅ b) -> (g : b ≅ c) -> (h : c ≅ d) ->
                 (f `transIso` (g `transIso` h)) `IsoEq`
                 ((f `transIso` g) `transIso` h)
transIsoAssoc f g h = MkIsoEq (\x => Refl) (\_ => Refl)

Lemma

The identity isomorphism is neutral wrt to transitivity of isomorphisms.

export
isoIdRight : (f : a ≅ b) -> transIso f (identity b) `IsoEq` f
isoIdRight (MkIso to from toFrom fromTo) = MkIsoEq (\_ => Refl) (\_ => Refl)
 
export
isoIdLeft : (f : a ≅ b) -> transIso (identity a) f `IsoEq` f
isoIdLeft (MkIso to from toFrom fromTo) = MkIsoEq (\_ => Refl) (\_ => Refl)

Lemma

There is an isomorphism between any two uninhabited types.

IsoVoid : (u1 : Uninhabited a) => (u2 : Uninhabited b) => a ≅ b
IsoVoid = MkIso absurd absurd  (\x => absurd x) (\x => absurd x)

• check how much of this is necessary