Wellfounded trees and dependent polynomial functors

DOI10.1007/978-3-540-24849-1_14MaRDI QIDQ5712306zbMATH OpenOpenAlexFDO

Authors Nicola Gambino, Martin Hyland

Publication date 23 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98246, http://eprints.whiterose.ac.uk/113158/1/gambino-hyland.pdf

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• Polynomial functors and trees
• Functorial invariants of trees and their cones
• Trees, functional equations, and combinatorial Hopf algebras
• Non-wellfounded trees in homotopy type theory
• Power-set functors and saturated trees
• Rooted trees, strong cofinality and ample generics
• Tree-functors, determinacy and bisimulations
• Trees, set compositions and the twisted descent algebra
• Inductive algebras for trees
• Some Wellfounded Trees in UniMath

Cited in

(41)

• Wellfounded trees in categories
• On semiflexible, flexible and pie algebras
• A formalized general theory of syntax with bindings: extended version
• The simplicial model of univalent foundations (after Voevodsky)
• The universal exponentiable arrow
• Actads
• Combining effects: sum and tensor
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Containers: Constructing strictly positive types
• A coalgebraic view of bar recursion and bar induction
• Some Wellfounded Trees in UniMath
• Constructive membership predicates as index types
• C-systems defined by universe categories: presheaves
• Polynomial functors and trees
• Data types with symmetries and polynomial functors over groupoids
• Polynomial functors and polynomial monads
• Directed containers as categories
• Dependent inductive and coinductive types are fibrational dialgebras
• Canonicity and homotopy canonicity for cubical type theory
• On Church’s thesis in cubical assemblies
• Quotients, inductive types, and quotient inductive types
• Variations on inductive-recursive definitions
• Representing continuous functions between greatest fixed points of indexed containers
• W-types in setoids
• Monads in double categories
• Indexed containers
• The essence of ornaments
• 2-Dimensional Directed Type Theory
• Decomposing Comonad Morphisms.
• scientific article; zbMATH DE number 7649955 (Why is no real title available?)
• Constructing initial algebras using inflationary iteration
• GADTs, functoriality, parametricity: pick two
• A topological counterpart of well-founded trees in dependent type theory
• Functorial aggregation
• GADTs are not (even partial) functors
• Universal algebra in UniMath
• Distributive laws of monadic containers
• Formalising inductive and coinductive containers
• Oracle modalities
• Non-well-founded trees in categories
• Polynomial functors and opetopes

This page was built for publication: Wellfounded trees and dependent polynomial functors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5712306)