Theorems about dependent products

Paths

Paths p : f = g in a function type ∀ x:X, P x are equivalent to functions taking values in path types, H : ∀ x:X, f x = g x, or concisely, H : f == g. This equivalence, however, is just the combination of apD10 and function extensionality funext, and as such, path_forall, et seq. are given in the Overture: Now we show how these things compute.

The identification of the path space of a dependent function space, up to equivalence, is of course just funext.

Path algebra

Transport

The concrete description of transport in sigmas and pis is rather trickier than in the other types. In particular, these cannot be described just in terms of transport in simpler types; they require the full Id-elim rule by way of "dependent transport" transportD. In particular this indicates why "transport" alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory). A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually?

A special case of transport_forall where the type P does not depend on A, and so it is just a fixed type B.

Maps on paths

The action of maps given by application.

The action of maps given by lambda.

Dependent paths

Usually, a dependent path over p:x1=x2 in P:A→Type between y1:P x1 and y2:P x2 is a path transport P p y1 = y2 in P x2. However, when P is a function space, these dependent paths have a more convenient description: rather than transporting the argument of y1 forwards and backwards, we transport only forwards but on both sides of the equation, yielding a "naturality square".

Functorial action

The functoriality of ∀ is slightly subtle: it is contravariant in the domain type and covariant in the codomain, but the codomain is dependent on the domain.

Some special cases appear when one or the other of the maps are equivalences.

If f0 is an equivalence, then we can simply apply functor_forall to its inverse. However, in this case it is sometimes more convenient to place the substitution on the other side of f1.

Since there's a nontrivial transport here, it's useful to have a computation lemma.

Equivalences

If *both* maps in functor_forall are equivalences, then so is the output.

Similarly, we have a version of functor_forall_equiv that acts on on equivalences both upstairs and downstairs.

Functoriality on logical equivalences

At least over a fixed base

Two variable versions for function extensionality.

Truncatedness: any dependent product of n-types is an n-type: see contr_forall and istrunc_forall in Basics.Trunc.

Contractibility: A product over a contractible type is equivalent to the fiber over the center.

Symmetry of curried arguments

Using the standard Haskell name for this, as it’s a handy utility function. Note: not sure if P will usually be deducible, or whether it would be better explicit.