Univalent Type Theorems: Models, Equalities, and Coherence

Abstract

During the performance period of the grant, the PI, the PRDAs Karol Szumilo and Sina Hazratpour and the PIs PhD students developed research along three connected lines of enquiry: algebraic models of homotopy type theory, constructive models of univalent foundations, and connections between homotopy type theory and higher categories. Their research led to several key results, including a partial solution to the open problem of definining a constructive version of the simplicial model of univalent foundations. These results have already been used by researchers in the area and have been presented in several papers and preprints. The work has also opened up new research directions, such as a higher-categorical version of exact completions.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 02, 2021
Accession Number
AD1154739

Entities

People

  • Nicola Gambino

Organizations

  • University of Leeds

Tags

DTIC Thesaurus Topics

  • Air Force
  • Air Force Research Laboratories
  • Buildings And Structures
  • Christianity
  • Computer Science
  • Department Of Defense
  • Information Operations
  • Language
  • Logic
  • Mathematical Logic
  • Mathematics
  • Scientific Research
  • Set Theory
  • Students
  • Teamwork
  • Theorems
  • Topoi
  • Topology
  • Two Dimensional
  • Universities

Fields of Study

  • Mathematics

Readers

  • Graph Algorithms and Convex Optimization.
  • Research Science/Academic Research
  • Theoretical Analysis.