scientific article; zbMATH DE number 7471707

MaRDI QIDQ5028473

Andrew Swan

Publication date: 9 February 2022

Full work available at URL: https://arxiv.org/abs/2010.01187

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

free groupshomotopy type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (1)

Formalizing free groups in Isabelle/HOL: the Nielsen-Schreier theorem and the conjugacy problem

Uses Software

• Cubical agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal Sets
• Nielsen‐Schreier and the Axiom of Choice
• Subgroups of a free group and the axiom of choice
• Eilenberg-MacLane spaces in homotopy type theory
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Syntax and models of Cartesian cubical type theory
• Higher Groups in Homotopy Type Theory
• Free Higher Groups in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)

This page was built for publication: