1    λ(f : Type → Type → Type)
 2  → { dimap :
 3          ∀(a : Type)
 4        → ∀(b : Type)
 5        → ∀(c : Type)
 6        → ∀(d : Type)
 7        → (a → b)
 8        → (c → d)
 9        → f b c
10        → f a d
11    , lmap :
12        ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → f b c → f a c
13    , rmap :
14        ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (b → c) → f a b → f a c
15    }