Homotopy Type Theory transport > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Idea

Definition

Given a type $A$, a judgment $z:{𝒯}_{𝒰}(A)⊢B(z)\mathrm{type}$ z:\mathcal{T}_\mathcal{U}(A) z:A \vdash B(z)\ \mathrm{type}, terms $x:A$ and $y:A$, and an identity $p:(x =_A y)$, there are transport functions $\overrightarrow{\mathrm{tr}}_{B}^{p}:B(x) \to B(y)$ and $\overleftarrow{\mathrm{tr}}_{B}^{p}:B(y) \to B(x)$, such that for all $\mathrm{<span><del\; class="diffmod">\; u</del><ins\; class="diffmod">\; v</ins></span>}:B(\mathrm{<span><del\; class="diffmod">\; x</del><ins\; class="diffmod">\; y</ins></span>})$ u:B(x) v:B(y) , the$\overleftarrow{\mathrm{tr}}_{B}^{p}(\overrightarrow{\mathrm{tr}}_{B}^{p}(u)) = u$fiber and of for all$v{\overrightarrow{\mathrm{tr}}}_B^p:B(y)$ v:B(y) \overrightarrow{\mathrm{tr}}_{B}^{p} , at${\overrightarrow{\mathrm{tr}}}_B^p({\overleftarrow{\mathrm{tr}}}_B^p(v))=v$ \overrightarrow{\mathrm{tr}}_{B}^{p}(\overleftarrow{\mathrm{tr}}_{B}^{p}(v)) = v is contractible, and for all $u:B(x)$, the fiber of $\overleftarrow{\mathrm{tr}}_{B}^{p}$ at $u$ is contractible.

See also

• identity type
• dependent identity type?

References

HoTT book