Skip to content

CoqHott/univalent_parametricity

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Univalent Parametricity

Univalent Parametricity for Effective Transport

The repository contains the companion code of the article "The Marriage of Univalence and Parametricity"

A previous version of this work has been published at ICFP'18 "Equivalences for Free: Univalent Parametricity for Effective Transport"

Structure

  • ./theories contains the core development with type classes described in Section 5

  • ./examples contains examples of the use of univalent parametricity

  • ./translation contains the univalent parametricity translation (Fig 3) and associated proofs

Compilation

Hereafter, "the main development" denotes the directories theories/ and examples/.

You need Coq 8.13 to compile the main development. To compile the file in the translation/ directory, you need the hoqc compiler (the HoTT version of Coq provided by the HoTT Library -- available at https://github.com/HoTT/HoTT).

To compile the main development:

set $COQBIN to the path where coqc is (export COQBIN=/.../bin/), or have Coq 8.13 in your path. Then, in the / directory, run:

make

To compile translation/ run (requires hoqc):

hoqc translation/Translation.v

directory ./theories

This is the core development with type classes described in Section 5. The structure of the files follows more or less the structure of the paper.

  • HoTT.v contains several definitions from the HoTT library; the point of this file is so that the main development is independent from hoqc.

Note that HoTT.v contains one admit (hprop_isequiv), which corresponds to a standard result in the HoTT library, but whose proof was too laborious to be added independently to this distribution.

  • HoTT_axioms.v contains the definition of the univalence and functional extensionality axioms.

  • UR.v contains the definition of the univalent logical relation using type classes.

  • URTactics.v provides a bunch of tactics for automation of typeclass resolution

  • FP.v contains the proof that constructors of Coq enjoy the fundamental property of the univalent logical relation.

  • ADT.v contains tactics to automatize proofs that abstract data types are univalent.

  • Record.v contains tactics to automatize proofs that record types are univalent.

  • Transportable.v contains instances of the Transportable type class that allows for more computational rewriting.

directory ./examples

  • Vector.v is a copy-paste from Coq's standard library with the only modification that it uses universe polymorphism.

  • Examples.v presents examples, most of them in the paper.

  • MoreInductive.v deals with more examples of inductive types.

directory ./translation

  • Translation.v is a file showing the correctness of the univalent parametricity translation (Fig 3) using a deep embedding

About

Univalent Parametricity for Effective Transport

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published