Here's a request for some new material in the HoTT file on equivalences that might be a fun exercise for someone.

In the section on Invertible maps we define a type has-inverse and later in the section Invertible map data we define map-inverse-has-inverse. It would be nice to define has-inverse-map-inverse-has-inverse showing that this map has an inverse (proving that having an inverse is symmetric).

Then it would be great to apply to this to prove that section-is-equiv and retraction-is-equiv are equivalences. One of these will likely be easier than the other by the particular method we used to show that equivalences are invertible maps. But not we have homotopy-section-retraction-is-equiv showing that the two maps are homotopic, so once one is an equivalence the other is as well by is-equiv-homotopy or is-equiv-rev-homotopy.

I'm happy to chat about this further.

• Example 8.14 (#29)
• Lemma 8.15

The notion of orthogonality from BW23 is formalized in #76.

It satisfies many desirable closure properties:

• In the left argument:
  • isomorphism of shape-pairs
  • composition
  • left cancellation
  • right cancellation with retraction
  • pushout product
  • crossing with a shape
  • exact pushout
  • retracts
• in the right argument:
  • equivalence of maps
  • composition
  • right cancellation
  • left cancellation with section
  • exponentiation
  • pullback
  • retracts
• and many more

Many terms in 08-families-of-maps.rzk.md seem to be named using an outdated naming scheme.

For example the name total-equiv-family-of-equiv is written "conclusion-last" and is used for what I believe should be called is-fiberwise-equiv-is-total-equiv or is-family-of-equiv-is-equiv-total-map or some variation thereof.

Some names follow the "conclusion-first" paradigm, but mix up equiv and is-equiv.
For example family-equiv-total-equiv takes a family of maps and an is-equiv (total-map), but returns not fiberwise is-equiv, but rather actual fiberwise equivalences Equiv. It should probably be called something like family-equiv-is-equiv-total-map.

I was a bit scared to just run off on my own and try to clean up the document, since a) it is long and b) probably many other things rely on it.

So what is the best policy for this? As a preliminary measure, one could add properly named synonyms for the most important "outward facing" terms so that at least the dirt is contained until one can do a proper project-wide cleaning.

Should be straightforward, except definitions in Rzk would likely have to be duplicated for different concrete dimensions.

• Proposition 8.21
• Theorem 8.26
• Proposition 8.27

Depends on #22.

• Definition 9.3
• Remark 9.4

Right now the the new file 04a on right orthogonality does not appear in the web directory. This is an easy fix but at the same time I propose we renumber them to get rid of the a.

One easy to implement change would be to move 03-simplicial-type-theory to 02-simplicial-type-theory and 04-extension-types to 03-extension-types and 04a-right-orthogonality to 04-right-orthogonality. This could be implemented immediately as it should not create conflicts with the open pull requests.

This also leaves the numbers 00 and 01 open for later similar moves. What do we think @jonweinb and @fizruk and @TashiWalde?

Let A : U and C : A -> U and s t : total-type A C.
I observed that applying first-path-Sigma to a term of the form (eq-pair p q) : s = t
(where p : first s = first t and q : s' = t is a path from the transported term) does not strictly compute to p.

See issue #61, where first-path-\Sigma-eq-pair cannot simply be implemented as refl.

It might be a bit unreasonable to ask such a strict computation rule for every pair (p,q), but I was expecting this to hold at least when p is refl. To my surprise, even this computation rule fails with the current implementations.

#def first-path-Σ-eq-pair-refl
-- does not type-check!
  ( A : U)
  ( B : A → U)
  ( a : A)
  ( b b' :  B a)
  ( q : b = b')
  : first-path-Σ A B (a,b) (a,b') (eq-pair A B (a,b) (a,b') (refl, q)) = refl
  :=
    refl

Is it possible to re-implement first-path-\Sigma satisfying at least strict computation for terms of the form (eq-pair refl q)?

The term is-right-orthogonal-to-shape-× says that left orthogonality of shape inclusions is preserved when crossing with another shape.

The current implementation has two problems that should be addressed:

• It is very verbose and essentially duplicates the same construction twice. It should be refactored by introducing and relying on cofibration-product-functorial. For comparison, see how is-right-orthogonal-to-shape-pushout is constructed by relying on cofibration-union-functorial.

• It relies on naiveextext. Is this really necessary?

The first one is purely cosmetic, so not very important. But the second should really be resolved, since it impacts every other result that uses this basic operation.

Should be straightforward.

The proof of naturality of the Yoneda lemma in a : A should be improved to calculate how the covariant family in the domain acts on morphisms f : hom A a b.

• Theorem 8.30 (see #45)
• Theorem 8.31

Perhaps, it could be automatic?

Should be fairly straightforward, following the proof in the paper.

I'm working on this currently, namely the equivalence stipulated in [BW23, Section 2.4].

Should be straightforward.

All of these should be straightforward.

• Proposition 8.18
• Corollary 8.19
• Corollary 8.20

Should be relatively straightforward. Depends on #20.

Requires some work with transports, but otherwise should be straightforward.

Should be straightforward, no HoTT preliminaries required.

Should be straightforward.

• Definition 5.19 (inner anodyne)
• Proposition 5.20
• Proposition 5.21
• Corollary 5.22

Might require extra HoTT definitions.

I spoke just now with Matthias Hutzler who plans to work on this issue, which I'll describe here.

In the contractibility file we define WeakFunExt. We should show that FunExt implies WeakFunExt and conversely.

We might consider cutting all the code

"

For future reference we add a variable we can assume.

#assume weakfunext : WeakFunExt

Whenever a definition (implicitly) uses function extensionality, we write
#!rzk uses (weakfunext).

#def call-weakfunext uses (weakfunext)
  ( A : U )
  ( C : A → U)
  ( f : (a : A) → is-contr (C a) )
  : (is-contr ( (a : A) → C a ))
  := weakfunext A C f

"

because we don't actually use the function call-weakfunext. We shouldn't state assumptions of either funext or weakfunext while demonstrating they are logically equivalent. Instead the goal is to fill in a proof of the following

#def weakfunext-funext
   (funext : FunExt)
   : WeakFunExt
   := ???

and conversely.

We now have various logically equivalent definitions of is-prop here. It would be great to apply the various notions to prove that various types are propositions.

For instance, for any type A we can show that is-contr A implies is-prop A. A proof should be called is-prop-is-contr.

But also, for any type A, whether or not is-contr A holds, is-prop (is-contr A), i.e., is-contr A is a proposition. The agda-unimath library calls this is-property-is-contr.

Again for any f : A -> B, is-equiv A B f is a proposition. This might be called is-property-is-equiv.

There are lots of other types we should be able to prove are properties, in both the HoTT and sHoTT libraries, but let's start with just a few to settle on good style.

This should be split into sub-issues.

• Section 11.1 (Notions of adjunction) #32
  • Definition 11.1 (transposing adjunction)
  • Definition 11.2 (quasi-diagrammatic adjunction)
  • Definition 11.3 (half-adjoint diagrammatic adjunction)
  • Constructions 11.4, 11.5, and unnumbered diagrams right after
  • Definition 11.6 (bi-diagrammatic adjunction)
• Section 11.2 (Adjunctions between Segal types)
  • Definition 11.7 (quasi-transposing adjunction)
  • Theorem 11.8
  • Corollary 11.12
  • Theorem 11.13
  • Theorem 11.14
  • Corollary 11.21
  • Corollary 11.22
• Section 11.3 (Adjunctions between Rezk types)
  • Theorem 11.23

This one would particularly benefit from the literate style, providing the category-theoretic version of the proof from the paper in the text.

Consider (a special case of) cofibration-composition, which for a fixed shape inclusion psi subset chi and any type A produces an equivalence
(chi -> A) -> Sigma ( s : psi -> A ) (chi -> A [ extending s ]) .

This equivalence is functorial in the sense that for each f : B -> A, it yields a map of maps from (chi -> B) -> (chi ->A) to Sigma_s (\ chi -> B [extending s]) -> Sigma_s (\ chi -> A [extending s]).

One can say ad hoc what this means in this special case (and probably in every other special case of interest), as I have done with the term cofibration-composition-functorial in #79 .

It would be desirable to:

1. Introduce the general concept of a functorial map and a functorial equivalence. Note that even after making everything in the above description dependent, the general case of cofibration-composition cannot just be expressed directly as such a natural transformation, since the map depends on the choice of an additional piece of data ( the a:\phi -> A). I don't quite know what the most generalized version of functoriality should therefore be; only that my implementation of cofibration-composition-functorial should be an instance of it.
2. There are many other functions in the library which should really be defined as functorial maps. One should add corresponding instances.

The last point might be out of reach at the moment, but I'll add it nonetheless in case anyone has any ideas about it.

3 ) Investigate if a map T A -> S A which is defined for all types A (maybe depending on some additional data d : D(A)) is automatically functorial in A. I suspect this might be true assuming some version of directed univalence. Then one might be able to reduce this question to the corresponding question about natural transformations into the universe (viewed as a Rezk type). If I understand correctly, there one gets naturality for free.

• Definition 8.28
• Proposition 8.29

In #57, inner anodyne maps are defined via unique lifting against Segal types C.

• Define the notion of inner fibrations C -> A (including the possibility that A and C are not Segal).

• Prove the stronger unique lifting property of inner anodyne maps against all inner fibrations.

If this turns out not to be possible, we should strenghten the definition of inner anodyne.

Should be straightforward, no HoTT preliminaries required.

In #50, limits are definined as terminal cones.

Implement an alternative (a priori stronger) characterization of limits:

• Define cocone not as a single Sigma type, but as a type family cone : (f : A -> B) -> (b : B) -> U.
• Define the canonical composition map cone-precomp b x : cone f x -> hom B b x -> cone f b.
• Define limit (f : A->B) := Sigma ( x: X, c : cone f x ), (b : B) -> is-equiv (cone-precomp b x c)
• Alternatively, if one wants to avoid inputting the composition map (which would require a Segal type),
  one could directly ask for an equivalence of dependent types (b:B) -> Equiv (hom B b x) (cone f b)
  and then show that for a Segal type this equivalence needs to be given by composition.

For a few things I want to do, it will be useful to have the statement that equivalences are embeddings in the HoTT section of the library. I'm working on this now.

Perhaps, we should maintain a list of contributors in a single place and refer to it from wherever we have a list at the moment.

• Axiom 4.6
• Construction 4.7 (ext-htpy-eq)
• Proposition 4.8
  • (i)
  • (ii) (ExtExt is defined but is not connected to the definition of Axiom 4.6)
• Proposition 4.10
• Proposition 4.11
• Proposition 4.12 (currently only instances of the proposition for specific n can be stated in Rzk)

May require extra definitions in the HoTT part.

Should be straightforward by path induction.

@TashiWalde makes a good point that renaming terms such as is-covariant-representable-is-segal to is-covariant-hom-is-segal would be both shorter and more in line with our style guide. I'd be happy to implement this change throughout.

One challenge is that section 8 involves both covariant and contravariant versions of hom. The term is-contravariant-hom-is-segal is no problem but we might have to be careful with the names for a few auxiliary terms, eg the current dhom-representable and dhom-contra-representable.

Now that the formalization of right orthogonality and its closure properties is well underway (#81), it is time to start the analogous story for LARI/RARI-orthogonality.

• Formalize strict left and right adjoint sections / reflectors / coreflectors / LARI/RARI - maps.
• Formalize the corresponding notion of orthogonality.
• Formalize closure properties...

• Construction 10.5 (iso-eq)
• Definition 10.6 (is-rezk)
• Lemma 10.7 (compute-covariant-transport-of-hom-family-iso-eq-is-segal)
• Lemma 10.8 (compute-ap-hom-of-iso-eq)
• Proposition 10.9
  • depends on #23
    • which depends on #22
• Proposition 10.10