unimath/typetheory

The mathematical study of type theories, in univalent foundations

TypeTheory: the mathematical study of type theories, in univalent foundations

Code on C-systems, D-systems, categories with families, comprehension categories, saturation, and the like.

Compilation

Prerequisites

The Coq code depends on the UniMath library, available from http://github.com/UniMath/UniMath. To compile UniMath, follow the installation instructions given there.

You will also need to make UniMath’s coq binaries available for compiling this library. The simplest way is to install them as the default Coq on your system, by calling, from within the UniMath toplevel directory,

$ make install 

and then adding them to your $PATH, either temporarily by running

$ PATH=$PATH:`pwd`/sub/coq/bin/

or permanently by modifying your shell configuration file (usually ~/.bash_profile or similar):

echo "export PATH=\"`pwd`/sub/coq/bin/:\$PATH\"" >> ~/.bash_profile

Alternatively, if you do not want to make UniMath’s Coq your default, you can add an alias for its directory to your shell config file by calling (from within the UniMath toplevel directory)

echo "export UNIBIN=\"`pwd`/sub/coq/bin/\"" >> ~/.bash_profile

and then give the option COQBIN=$UNIBIN when compiling this library.

Compilation of UniMath/TypeTheory

If you have UniMath’s Coq in your path (as per the first suggestion above), then our library can be built just with make from within the toplevel directory.

Otherwise, you need to pass the location of the UniMath coqc binary by hand, as e.g. make COQBIN="~/src/UniMath/sub/coq/bin/" or make COQBIN=$UNIBIN.

Similarly, to use these files in Proof General, you must make sure the correct coqtop is called. This may be either permanently set in the option coq-prog-name, or prompted for at each invocation by setting proof-prog-name-ask.

Contents

The contents of this library are split into several "packages" (subdirectories). We give an overview of the packages and refer to each package's README for details.

NOTE: this table of contents is not automatically updated, and may often be out of sync with the development.

• Auxiliary/
  • General background definitions and results, that could be upstreamed into UniMath/UniMath
• RelUniv/
  • Definition and basic development of relative universe structures
• CompCats/
  • Basic development of comprehension categories (though UniMath itself contains the basic definition)
• TypeCat/
  • Definition and basic development of type-categories, including splitness, the (2-)category of type-categories, and extra logical structure on them
• CwF/
  • Definition and basic development of categories with families, using the Fiore–Aowdey approach with representable (more precisely, represented) maps
  • An equivalence between families structures and relative universe structures on Yoneda
  • Construction of a function from families structures on a category to families structures on its Rezk completion
• CwF_TypeCat/
  • Comparisons between CwF’s and split type-categories; specifically:
    • equivalence of types between families structures and split type structures, as presented in Ahrens–Lumsdaine–Voevodsky 2017
    • equivalence of categories between families structures and split type structures
• OtherDefs/
  • Various other categorical structures used in the study of type theory, not yet developed here enough to warrant separate packages
• Categories/
  • Background constructions and results on categories; might be upstreamed to UniMath/CategoryTheory
• Instances/
  • concrete examples of the categorical structures considered
  • so far, only the result that presheaves form a type-category
• Csystems/
  • the implementation of Vladimir Voevodsky's notion of C system
• Bsystems/
  • the implementation of Vladimir Voevodsky's notion of B system
• Cubical/
  • To be documented
• Initiality/
  • the interpretation from the syntax of a small type theory into suitably-structured CwA’s
  • (incomplete) the syntactic CwA of the type theory, and its initiality
• TypeConstructions/
  • To be documented
• Articles/
  • files corresponding to articles whose content is formalised here, linking results named in the articles to their formalisation in this development

typetheory's Issues

PR#224 not yet fully satisfying

As argued by @nmvdw in the discussion about PR 1582 of UniMath, the inclusion of material from PAdics is not even needed.

CI broken due to missing system packages for OPAM

Build failure in the Travis CI here (on PR benediktahrens#1) seems to be due to an Opam dependency issue:

The following system packages will first need to be installed:
    libipc-system-simple-perl libstring-shellquote-perl

<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
Let opam run your package manager to install the required system packages?
(answer 'n' for other options) [Y/n] 

No output has been received in the last 10m0s, this potentially indicates a stalled build or something wrong with the build itself.

I guess this could be fixed either by installing them explicitly, or by giving opam --confirm-level=unsafe-yes? If this is a quick fix for someone more experienced with Travis scripts than me (@DanGrayson ?), that’d be great — otherwise I can try to figure it out later this week.

Fix typo to re-establish compatibility with UniMath/UniMath

See UniMath/UniMath#1756 corrected by @rmatthes

Compilation broken due to changes in UniMath/UniMath

COQC TypeTheory/Auxiliary/CategoryTheoryImports.v
File "./TypeTheory/Auxiliary/CategoryTheoryImports.v", line 18, characters 15-50:
Error: Unable to locate library UniMath.CategoryTheory.equivalences.

This is the relevant change: UniMath/UniMath#1118
This also means that part of Auxiliary/Auxiliary.v can be removed.

Reorganise library structure: consistently use topic-based packages, not project-based?

Several times recently I’ve found the current organisation of the library causing obstacles in development/refactoring; I think it’s slightly overdue for a bit of larger-scale reorganisation.

Currently, the grouping of files into packages is rather ad hoc, following several different ideas. In particular, several packages correspond to particular research projects/papers, or at least started out that way. A typical example of the tensions this causes: The ALV1 package contains the definition and some core development of split type-categories. This gets imported, and further developed, in several other packages — at least Initiality, ALV2, and OtherDefs. These each import it separately, so there’s a fair bit of near-duplicated material on split type-cats, which it would be good to consolidate. But where should it get consolidated? The natural place would be in the same file (or at least the same package) as the core development of split type-cats. But that conflicts with the current naming scheme and documentation, which suggests that ALV1 is meant to contain the material of the paper Ahrens–Lumsdaine–Voevodsky 2017.

Generally: project-based packages conflict badly with other organisational demands. Organising packages by topic (like some of the present packages, and like all/most of UniMath) works much better. The main benefit of project-based packages is that they help papers based on contributions to this library to showcase their contributions. But that can be alternately accomplished by files like those in the Articles package, which summarise a contribution without making demands on the overall organisation.

So, briefly, I propose:

• the packages that are project-based should be dissolved, and reorganised into more consistently topic-based packages;
• the topic-based structure may also be reorganised to better fit the current state of the material;
• projects whose packages are dissolved should (either now or later) get files in the Article package.

Figuring out the full details is I think best done by trying it out and making a draft PR — it’s difficult to foresee exactly how the reorganisation will work — and I plan to take a crack at that soon. This issue is just to float the idea initially, and get advance input from other contributors — do others agree this sounds good, or at least potentially so (pending a concrete draft PR)? And are there other large-scale considerations I haven’t mentioned here, that should be kept in mind for the reorganisation?

Upstreaming some of the material in `Auxiliary` to UniMath/UniMath?

Great work was done by @peterlefanulumsdaine in #202 regarding organization of auxiliary material in Auxiliary.

Question: would some of the material from Auxiliary fit well into UniMath/UniMath? The advantages of upstreaming such material are:

1. It would be easier to find and use in other libraries (though I am not aware of any development outside UniMath/UniMath and UniMath/TypeTheory).
2. Material in U/U (but not in U/T) is regularly checked for compatibility with Coq development versions.

Upstreaming would not make the work of #202 superfluous - on the contrary, the good organization of the material makes it feasible at all to discuss the possibility of upstreaming, and would make upstreaming much easier.

Change name and of arguments in `functor_over`, `nat_trans_over`, etc

• change for consistency with def’n of [mor_disp], etc
• also call them just [disp_functor], etc (the “over” doesn’t make so much sense if the functor in the base is not the first argument)

CI broken, due to recent package dependencies in UniMath

As noted in UniMath/UniMath#1396, the CategoryTheory package now depends (mutually) on Bicategories and SubstitutionSystems. This breaks our CI (see eg here), which currently attempts to build a subset of packages including CategoryTheory but not the other two (see here).

It looks like this ought to be easily fixable, by just adding Bicategories and SubstitutionSystems to the list of packages in our CI job. Testing that locally I’m getting some strange build problems, so I’m not quite sure whether it’s work or the fix will be more complicated — but I’ll issue a PR with that simple fix, to test whether it actually works on Github.

Topological spaces as an example of displayed cats

Improve compilation instructions in README

explain that

• location of Coq binaries needs to be given manually (by PATH or locally)
• UniMath files are found automatically after make install if using the right Coq binaries

Consolidate CategoryTheory imports

Add a file Auxiliary.CategoryTheory_Imports or similar, which re-exports the modules (10 or so) that are needed throughout our library

Refactor definition of the codomain displayed cat

Should be a Sigma-construction in two steps:

• first, the disp cat over C whose fibers are all C (which itself should be instance of more general “constant displayed cat”, which in turn should be pulling back C seen as a disp cat over 1 along the functor C –> 1)
• (the total cat of this will be just C^2, but we give it as a total cat to make the next step possible)
• second, the displayed arrow category over the total cat of the previous one;
• then, the sigma of this pair of displayed cats gives the codomain displayed cat

Compilation error after updating Coq version

The following error occurs:

COQC TypeTheory/Initiality/SplitTypeCat_Contextual.v
File "./TypeTheory/Initiality/SplitTypeCat_Contextual.v", line 228, characters 17-67:
Error:
In environment
C : split_typecat
Γ0 : C
Γ : C
The term "∃! AA : extension Γ0, ext_extension Γ0 AA = Γ" has type 
"UU" while it is expected to have type "hProp".

make[1]: *** [build/CoqMakefile.make:678: TypeTheory/Initiality/SplitTypeCat_Contextual.vo] Error 1

@peterlefanulumsdaine : could you take a look?

File `Bsystems/lBsystems_work` unlisted, stale, and very unclear status — salvage, delete, …?

FAO @rmatthes : I was just checking the repo for any .v-files not listed in packages (at the request of @benediktahrens), and found there is one unlisted file, TypeTheory/Bsystems/lBsystems_work. It seems to be a code fragment without any context; it was only touched once, in July 2017, when @rmatthes initialised the Bsystems package in commit af46fa3 with message:

very light modification of Vladimir Voevodsky's implementation of B-systems

just to ensure that it compiles within the TypeTheory repository
the file lBsystems_work.v does not compile and is therefore not mentioned in the file list
(anyway, its contents has an unclear status)

Having dead code in the development is bad, so if nothing in this file is still wanted, then I suggest we delete it — it clearly has historical interest, but anyone who is interested in seeing VV’s original work should be looking back to the original version of the package anyway. Or if there’s something in that that we genuinely still want in future, then could someone clean up this file to get it compiling (or at least as some of it), and add it to the package list so it doesn’t stale further?

Remove dependency on Coq.Init.Logic

After merging #234 two files still unfortunately imports Coq.Init.Logic:

• Initiality/Interpretation.v
• TypeCat/General.v

It's currently unclear to me if it's easy to fix or requires a more involved patch, so I'm creating this issue both as a reminder and an invitation to anyone who feels inspired to give it a try.

Most fixes related to removing Coq.Init.Logic has been replacing trivial or auto with try apply idpath, but if you're (un?)lucky you get one of the rare cases where a rewrite is performed using eq_refl and then all bets are off.

Slow type-checking: replace `admitted` by proof

File https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v contains admitted statements:

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 44 in 9242475

  use weqimplimpl; apply admit_slow_proof.

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 90 in 9242475

  - intros X Y. apply admit_slow_proof. (* refine (pr2 (idweq _)). *)

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 91 in 9242475

  - admit. (* refine (pr2 DiscCompCat_DiscCompCatDef_weq). *)

Fragments or complete proofs are there, but do not type-check in a reasonable amount of time, or at all.

The admitted statements should be proved.

For some background, see also #202 (comment)

Build fails with Coq 8.16.0

There's an error when building TypeTheory with Coq 8.16.0. The error message is:

File "./TypeTheory/TypeTheory/Auxiliary/SetsAndPresheaves.v", line 117, characters 8-16:
Error:
In environment
C : category
F : preShv C
c : C
A : F c
c' : C
f : C ⟦ c', c ⟧
The term "# (F : C^op ⟶ HSET_univalent_category) f A" has type
 "pr1hSet (F c')" while it is expected to have type
"pr1hSet (?F ?c)".

I remeber encountering this problem a couple of months ago maybe, so I don't think it's a recent change that caused it. I took a look at the lemma in SetsAndPresheaves.v that fails but I couldn't make heads or tails of what's causing the error.

It fails on this version of Coq:

$ coqc --version
The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.1

and I verified that TypeTheory compiles with the following versions: 8.13.2, 8.14.0, 8.14.1, 8.15.0, 8.15.1, 8.15.2.

Replace all uses of `cancel_postcomposition` by `maponpaths_2`

Implement mechanism to conveniently specify full subcategories as displayed categories

such as the subcategory of monad algebras (of functor algebras)

Move the repository into the UniMath organization

Here is a link on how to do it:
https://help.github.com/articles/transferring-a-repository-owned-by-your-personal-account/

It seems that the steps are:

• making the repo public
• transfer it to the UniMath organization

This will keep the code, but also the issues intact. If we don't want that, we can decide to just move the code, or to clean the issues before the move (check inhowfar that is possible).

Add careful refs for definitions in `OtherDefs` files

Make sure each definition of a structure is carefully referenced — citation to somewhere giving that precise form of the definition, where possible.

Add lemma: any disp cat over a univalent cat is an isofibration

Consolidate notations

Several notations are repeatedly defined multiple times in the library. TODO: consolidate these into a file Auxiliary/Notations.v, probably also subsuming current Auxiliary/UnicodeNotations.v.

Adapt Travis configuration to new version of Coq

until then, builds will fail

Add algebras for a functor + a monad as example of displayed cats

This can go as a 2-step construction:

• algs for a functor as a disp cat over the original cat;
• algs for a monad as a disp cat over the algs for the underling functor; then, their sigma, to get them displayed over the original cat

Remove material that has been upstreamed to UniMath/UniMath

This includes

• Comprehension categories UniMath/UniMath#1125
• Composites and inverses of equivalences of categories UniMath/UniMath#1118

Rename identifiers for categories to adhere to convention suggested by VV

see UniMath/UniMath#362 (comment)

Put notations in scope or make them local

as suggested by Anders

Naming: structure vs property

In Fibrations.v, it reads
"We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven."
So is_fibration is actually a structure, but its name sounds like it is a property.

We had a discussion in UniMath about that [1], where I asked not to do any renaming.

But maybe new notions could observe the convention suggested there?

[1] UniMath/UniMath#214

Remove duplicate definition `CwF_structure`

CwF_structure is also defined in CwF_RelUnivYoneda. That def is obsolete, should be replaced everywhere by the new def from ..._defs

Compilation Failure with coq 8.7

I get an error when trying to compile TypeTheory with coq 8.7

File "./TypeTheory/ALV1/CwF_def.v", line 180, characters 10-25:
Error:
In environment
C : category
pp : mor_total (preShv C)
Γ : C
A : (Ty pp) Γ : hSet
x : (∑ (ΓAπ : map_into Γ) (te : cwf_tm_of_ty pp (# (Ty pp) (pr2 ΓAπ) A)),
     isPullback (yy A) pp (# (yoneda C (homset_property C)) (pr2 ΓAπ))
       (yy (pr1 te)) (cwf_square_comm (pr2 te))) →
    ?Y
Unable to unify
 "∑ f : (∑ y, ?M203 y) → ∑ (x0 : ?X) (p : ?M202 x0), ?M203 (x0,, p), isweq f"
with "∑ f : ?P x → isweq x, isweq f".

Provide export wrapper file

Provide a summary file which re-exports the whole library (or perhaps individual packages?), for easier wholesale importing by others.

Attribution for def of rel univ strux

Give attribution for this by the def, as for other definitions.

Build system (opam) seems to require changes

Our travis build system uses opam, which seems to require changes to the setup.

The complete log is here: https://api.travis-ci.org/v3/job/657119034/log.txt

@peterlefanulumsdaine @DanGrayson : would you be willing to investigate?

(The same problem affects UniMath/largecatmodules.)

Travis build failure

COQC TypeTheory/Csystems/hSet_ltowers.v
File "./TypeTheory/Csystems/hSet_ltowers.v", line 438, characters 2-14:
Error:
Found no subterm matching "internal_paths_rew_r BB 
                             (ftn m (ft X)) ((ft ∘ ftn m) X)
                             (λ l : BB, Y = l) eq 
                             (ftn_ft m X)" in the current goal.
build/CoqMakefile.make:715: recipe for target 'TypeTheory/Csystems/hSet_ltowers.vo' failed
make[1]: *** [TypeTheory/Csystems/hSet_ltowers.vo] Error 1
build/CoqMakefile.make:338: recipe for target 'all' failed
make: *** [all] Error 2
The command "make" exited with 2.

Complete log here: https://travis-ci.org/github/UniMath/TypeTheory/builds/768029040

Could this stem from recent reorganization by @peterlefanulumsdaine ? (No finger pointing, but the changes done could indicate what fix is required here.)

TypeTheory does not compile with Coq 8.10

File "./TypeTheory/Initiality/Typing.v", line 63, characters 2-275:
Error:
Anomaly
"Ill-formed template inductive declaration: not polymorphic on any universe."
Please report at http://coq.inria.fr/bugs/.

---

COQC TypeTheory/ALV1/CwF_Defs_Equiv.v
does not compile either because use fails somewhere

does not compile with Coq 8.20 release candidate 1

In CI, it was visible that Coq dev (an alpha version of Coq 8.21) does not compile this satellite, but it is even worse.

The first error message is:

coqc TypeTheory/TypeTheory/Auxiliary/Auxiliary.{glob,vo} (exit 1) File "./TypeTheory/TypeTheory/Auxiliary/Auxiliary.v", line 15, characters 0-43: Error: Universe inconsistency. Cannot enforce UU.u0 <= PartA.cast.u1 because PartA.cast.u1 <= PartA.cast.u0 < UU.u0.

Clarify referencing/attributions of main defs of CwF’s, split type cats

We currently just reference the exact forms we follow. Keep that, but also mention the originators of the definitions those were based on. (i.e. Dybjer for CwF’s, Cartmell &c. for split type cats).

Anomaly detected during compilation

After compiling and installing the current UniMath library and installing it, I get the following with Debian 9 (the current version is Debian 10):

COQC TypeTheory/Initiality/InterpretationLemmas.v
Finished transaction in 6.397 secs (6.372u,0.019s) (successful)
Finished transaction in 3.817 secs (3.774u,0.039s) (successful)
File "./TypeTheory/Initiality/InterpretationLemmas.v", line 387, characters 2-11:
Error:
Anomaly
"File "interp/impargs.ml", line 388, characters 15-21: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

build/CoqMakefile.make:715: recipe for target 'TypeTheory/Initiality/InterpretationLemmas.vo' failed
make[1]: *** [TypeTheory/Initiality/InterpretationLemmas.vo] Error 129
build/CoqMakefile.make:338: recipe for target 'all' failed
make: *** [all] Error 2

Can someone please confirm this with their proper installation?

Ralph

Document `CwF_SplitTypeCat_Defs` better

Explain more clearly in opening docs of this file how we are building up CwF’s etc. out of object-extension structures etc.

TypeTheory does not compile with current UniMath

mv .coq_makefile_output build/CoqMakefile.make
COQDEP VFILES
COQC TypeTheory/Auxiliary/CategoryTheoryImports.v
COQC TypeTheory/Auxiliary/Auxiliary.v
File "./TypeTheory/Auxiliary/Auxiliary.v", line 31, characters 34-45:
Error: The reference dirprodpair was not found in the current environment.
make[1]: *** [TypeTheory/Auxiliary/Auxiliary.vo] Error 1
make: *** [all] Error 2

The problem is UniMath/UniMath#1216.

Make code quality/cleaning pass over files

Before making public, would be good to have a rough quality/cleanup pass over all files (at least all of ALV1). Doesn’t need to be too thorough, but should at least:

• make sure all terminology/naming conventions are up-to-date and consistent;
• make sure all names are somewhat meaningful
• remove obsolete code and comments

To make sure we’ve had at least one pair of eyes (preferably two) over each file before going public, mark below when you’ve checked a file.

File	BA	PLL	VV
Auxiliary/Auxiliary.v
Auxiliary/CategoryTheoryImports.v
Auxiliary/UnicodeNotations.v
ALV1/CwF_RelUnivYoneda.v	2016-10-06	2016-10-07
ALV1/CwF_SplitTypeCat_Cats_Standalone.v
ALV1/CwF_SplitTypeCat_Defs.v		2016-10-05
ALV1/CwF_SplitTypeCat_Equivalence.v
ALV1/CwF_SplitTypeCat_Maps.v		2016-10-10
ALV1/RelativeUniverses.v	2016-10-06	2016-10-07
ALV1/RelUnivYonedaCompletion.v	2016-10-06	2016-10-07
ALV1/Summary.v	2016-10-06
ALV2/CwF_SplitTypeCat_Cats.v
ALV2/CwF_SplitTypeCat_Equiv_Cats.v
ALV2/CwF_SplitTypeCat_Equiv_Comparison.v
ALV2/CwF_SplitTypeCat_Univalent_Cats.v
Categories/category_FAM.v
Categories/category_of_elements.v
Categories/ess_alg_categories.v
Categories/ess_and_gen_alg_cats.v
Displayed_Cats/Auxiliary.v
Displayed_Cats/Constructions.v
Displayed_Cats/Core.v
Displayed_Cats/Equivalences.v
Displayed_Cats/Examples.v

CI: Build instructions for Coq and UniMath need to be updated

From https://github.com/UniMath/TypeTheory/actions/runs/3222458407/jobs/5271547506:

~/work/TypeTheory ~/work/TypeTheory/TypeTheory
Cloning into 'UniMath'...
/home/runner/work/TypeTheory/UniMath
Already on 'master'
Your branch is up to date with 'origin/master'.
commit 1966eac142152fa9d13dca25f94a74d8060eaf4c
Merge: 59ea66c6 ffdb427e
Author: Benedikt Ahrens <[email protected]>
Date:   Mon Oct 10 11:52:20 2022 -0400

    Merge pull request #1230 from olynch/master
    
    Created Normal Subgroups section.

--- making .coq_makefile_input
git submodule update --init sub/coq
Submodule 'sub/coq' (https://github.com/coq/coq.git) registered for path 'sub/coq'
Cloning into '/home/runner/work/TypeTheory/UniMath/sub/coq'...
Submodule path 'sub/coq': checked out '70765ee1eb2c5f1085a2c2da6a39adcac4f89b9f'
--- making sub/coq/config/coq_config.ml because of sub/coq/configure.ml
cd sub/coq && ./configure -coqide "no" -with-doc no -prefix /home/runner/work/TypeTheory/UniMath
Dune could not be found, please ensure you have a working OCaml enviroment
Makefile:79: .coq_makefile_output.conf: No such file or directory
make: *** [Makefile:247: sub/coq/config/coq_config.ml] Error 1
Error: Process completed with exit code 2.

Provide summary/overview file

…to serve as readable entry point for the library, especially for readers arriving from the paper. (Probably base this on current ALV1/Tests.v.)

Consistentise terminology: cartesian generators, qq-morphisms, etc.