On planarity of graphs in homotopy type theory
type: Item
instance of: scholarly article
title: On planarity of graphs in homotopy type theory
author: Jonathan Prieto-Cubides
author: Håkon Robbestad Gylterud
published in: Mathematical Structures in Computer Science
publication date: 2024-10-16T00:00:00Z
Mathematics Subject Classification ID: 03-XX
Mathematics Subject Classification ID: 05-XX
zbMATH DE Number: 7927454
zbMATH Keywords: planarity
zbMATH Keywords: combinatorial maps
zbMATH Keywords: univalent mathematics
zbMATH Keywords: formalisation of mathematics
MaRDI profile type: Publication
cites work: Univalent Foundations and the Equivalence Principle
cites work: A Higher Structure Identity Principle
cites work: The four color proof suffices
cites work: Q4390601
cites work: Type Theory and Homotopy
cites work: Univalence as a principle of logic
cites work: Higher-Dimensional Algebra VII: Groupoidification
cites work: Digraphs
cites work: Q4484332
cites work: Eliminating dependent pattern matching without K
cites work: Isomorphism is equality
cites work: Graph Theory
cites work: Q6099604
cites work: Graph theory in Coq: minors, treewidth, and isomorphisms
cites work: Tests and Proofs for Enumerative Combinatorics
cites work: An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
cites work: Functional specification and prototyping with oriented combinatorial maps
cites work: Graphs on Surfaces
cites work: The Four Colour Theorem: Engineering of a Formal Proof
cites work: Q3757929
cites work: A combinatorial condition for planar graphs.
cites work: Embeddings of infinite graphs
cites work: The embeddings of a graph—A survey
cites work: Homotopy Type Theory: Univalent Foundations of Mathematics
cites work: Non-separable and planar graphs.
cites work: Q3024892
DOI: 10.1017/S0960129524000100
description: scientific article; zbMATH DE number 7927454