TypeTheory.ALV1.CwF_Defs_Equiv Part of the TypeTheory library (Ahrens, Lumsdaine, Voevodsky, 2015–present). The main result of this file is an equivalence weq_cwf'_cwf_structure between the canonical definition of CwF-structures on a precategory C and the regrouped definition based on object-extension structures. A cwf'_structure on C is

• a triple (Ty, (◂ + π)) (the object-extension structure)
• a triple (Tm, pp, Q) where
  • Tm is a presheaf,
  • pp is a morphism of presheaves Tm -> Ty
  • te is a term, for any Γ : C and A : Ty(Γ), te A : Tm (Γ◂A)
• such (te A) has the desired type, and square are pbs

Parentheses are ( (Ty, (◂ + π)), ( (Tm,(pp,Q)), props) ) Meanwhile, a cwf_structure on C consists of a morphism pp : Ty --> Tm of presheaves together with, for each Γ:C and A : Ty Γ, a representation of the fiber of Tm over A, which we will inspect in more detail below. So the three differences, in the order we will tackle them, are:

• ordering: moving the morphism pp to the front;
• distributing ∏ over ∑: a single quantification over Γ, A on the outside, vs. quantifying within each component;
• re-association of the components within the fiber-representation

Definition of an intermediate structure

We start by reordering the components of cwf'_structure, so that like cwf_structure, the morphism of presheaves comes first: ( (Ty, Tm, pp), ( ((◂ + π) , Q), props ) ) We name the intermediate structure produced as follows:

• the type of triples (Ty,Tm,pp) is just mor_total (preShv C);
• the type of triples (◂ + π, Q) is called rep1_data;
• the axioms are called rep1_axioms.

A pair rep1_data, rep1_axioms is called rep1, and we define cwf1_structure as the type of pairs of a mor_total and a rep1 on it. The equivalence weq_cwf'_cwf1_structure : cwf'_structure C ≃ cwf1_structure C is given just (!) by shuffling components. It remains then to give an equivalence cwf1_structure C ≃ cwf_structure C. Since pp is at the front in both of these, it suffices to give, for each (Ty,Tm,pp) : mor_total (preShv C) , an equivalence between the remaining structure, weq_rep1_representation : rep1 pp ≃ cwf_representation pp .

Equivalence between cwf'_structure and intermediate cwf1_structure

Equivalence between cwf_structure and intermediate

As per the outline above, it now remains to construct, for a given morphism pp : Tm --> Ty in preShv pp , an equivalence rep1 pp ≃ cwf_representation pp . Recall: a rep1 pp consists of:

• rep1_data, a triple (◂ + π, Q) as in a CwF, so
  • ◂ + π : for each Γ:C and A : Ty Γ, an object Γ ◂ A : C , and projection π : Γ ◂ A -> Γ
  • Q : for each Γ, A, a tm te : Tm (Γ ◂ A)
• some axioms, rep1_axioms.

a representation of pp is a function giving, for each Γ : C and f : Yo Γ -> Ty,

• an object and map f^*Γ -> Γ in C ;
• a term of appropriate type;
• such that the induced square of presheaves is a pullback.

The equivalence between these goes in two steps, essentially:

• distributing the quantification over Γ, A to the outside;
• reassociating the sigma-types.

For distributing the quantification, we go via an intermediate defind notion rep2_data.

Main result: equivalence between cwf_structure C and cwf'_structure C