1    λ(w : Type → Type)
 2  → λ(extract : ∀(a : Type) → w a → a)
 3  → λ(extend : ∀(a : Type) → ∀(b : Type) → ∀(f : w a → b) → w a → w b)
 4  →   { extract =
 5          extract
 6      , extend =
 7          extend
 8      , duplicate =
 9          λ(a : Type) → extend a (w a) ((./../Function/category).identity (w a))
10      , map =
11            λ(a : Type)
12          → λ(b : Type)
13          → λ(f : a → b)
14          → extend a b (λ(x : w a) → f (extract a x))
15      }
16    : ./Type w