1    λ(w : Type → Type)
2  →   { extract :
3          ∀(a : Type) → w a → a
4      , extend :
5          ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b
6      , duplicate :
7          ∀(a : Type) → w a → w (w a)
8      }
9    ⩓ ./../Functor/Type w