4
data Functor : Set₁ where
6
_|x|_ : Functor → Functor → Functor
8
record _×_ (A B : Set) : Set where
14
[_] : Functor → Set → Set
16
[ F |x| G ] X = [ F ] X × [ G ] X
18
data µ_ (F : Functor) : Set where
19
<_> : [ F ] (µ F) → µ F
21
mapFold : ∀ {X} F G → ([ G ] X → X) → [ F ] (µ G) → [ F ] X
22
mapFold |Id| G φ < x > = φ (mapFold G G φ x)
23
mapFold (F1 |x| F2 ) G φ (x , y) = mapFold F1 G φ x , mapFold F2 G φ y
b'\\ No newline at end of file'