/dada/colambek

Copy path to clipboard

Source

let B =
https://sellout.github.io/dhall-bhat/package.dhall sha256:67617847fca913d17863ad857224cd9b3904297bb15a9674146d5e120c5ff08a

in λ(t : Type) →
λ(base : Type → Type) →
λ(functor : B.Functor.Type base) →
λ(ana : ∀(a : Type) → (a → base a) → a → t) →
λ(project : tbase t) →
ana (base t) (functor.map t (base t) project)