About: Inductive type

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Class of coinductive types in intuitionistic type theories

Property	Value
dbo:description	class of coinductive types in intuitionistic type theories (en)
dbo:wikiPageExternalLink	http://www.cs.swan.ac.uk/~csetzer/slides/dybjer60thBirthdayGothenburgJune2013/dybjer60thBirthdayGothenburgJune2013.pdf http://homotopytypetheory.org/book/ https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/ https://web.archive.org/web/20141114172626/http:/www.cs.swan.ac.uk/~csetzer/slides/lisbon2012/setzerLisbon2012InductionInductionInduction.pdf
dbo:wikiPageWikiLink	dbr:Tree_(graph_theory) dbr:Natural_deduction dbr:Peano_axioms dbr:Universe_(mathematics) dbr:Intuitionistic_type_theory dbr:Number dbr:Parity_(mathematics) dbr:Coinduction dbr:Type_theory dbr:Dual_(category_theory) dbr:Initial_algebra dbr:Arity dbr:Isomorphism dbr:Coq dbr:Data_structure dbr:Dependent_type dbr:Structural_induction dbc:Type_theory dbr:Well-founded_relation dbr:Successor_function dbr:Natural_number dbr:Curry–Howard_correspondence dbr:Homotopy_type_theory dbr:Polynomial_functor_(type_theory) dbr:Structural_recursion dbr:Induction-induction dbr:Relation_(mathematics) dbr:Polynomial_functor dbr:Induction-recursion_(type_theory) dbr:Stream_(computer_science) dbr:Univalence_axiom dbr:Impredicative
dbp:wikiPageUsesTemplate	dbt:Cite_book dbt:! dbt:Reflist dbt:Math dbt:Var dbt:More_citations_needed dbt:Distinguish dbt:Mvar
dct:subject	dbc:Type_theory
rdfs:label	Inductive type (en)
owl:differentFrom	dbr:Inductive_data_type
owl:sameAs	freebase:Inductive type wikidata:Inductive type dbpedia-global:Inductive type
prov:wasDerivedFrom	wikipedia-en:Inductive_type?oldid=1282897928&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Inductive_type
is dbo:wikiPageRedirects of	dbr:W-type dbr:W_type
is dbo:wikiPageWikiLink of	dbr:Type_M dbr:Coq dbr:Recursive_data_type dbr:Inductive_data_type dbr:Agda_(programming_language) dbr:List_(abstract_data_type) dbr:Mutual_Induction dbr:Lean_(proof_assistant) dbr:Constructive_set_theory dbr:Polynomial_functor_(type_theory) dbr:W-type dbr:W_type
is foaf:primaryTopic of	wikipedia-en:Inductive_type