fact: Fixpoint induced_map (t : Tree) : A := match t with | generator x => h x | node o arg => op A o (fun i => induced_map (arg i)) end.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian