skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


  • Home
  • Search Results
  • Page 1 of 1

Search for: All records

Award ID contains: 2204304

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. ; (, Mathematical Structures in Computer Science)
    Abstract Consider a locally cartesian closed category with an object$$\mathbb{I}$$and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of$$\mathbb{I}$$defines a trivial fibration. Then the fibrations are also closed under pushforward. 
    more » « less
    Full Text Available 
  2. (, Bulletin of the London Mathematical Society)
    Abstract Many introductions tohomotopy type theoryand theunivalence axiomgloss over the semantics of this new formal system in traditional set‐based foundations. This expository article, written as lecture notes to accompany a three‐part mini course delivered at the Logic and Higher Structures workshop at CIRM‐Luminy, attempt to survey the state of the art, first presenting Voevodsky's simplicial model of univalent foundations and then touring Shulman's vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ‐topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning. 
    more » « less
  3. ; ; (, ACM)
    Full Text Available 
  4. ; ; ; (, Algebraic & Geometric Topology)
    Full Text Available 
  5. (, Notices of the American Mathematical Society)
    Full Text Available