# Homotopy type theory, Edition: version 28 Aug 2012 by Egbert Rijke By Egbert Rijke

Similar mathematics_1 books

Arithmétique et travaux pratiques cycle d'observation classe de sixième

Manuel de mathématiques, niveau sixième. Cet ouvrage fait partie de l. a. assortment Lebossé-Hémery dont les manuels furent à l’enseignement des mathématiques ce que le Bled et le Bescherelle furent à celui du français.

Additional resources for Homotopy type theory, Edition: version 28 Aug 2012

Sample text

IdP(x) . σ ○ ρ. σ ○ ρ ○ τ. It is immediate that there are homotopies hom(τ,σ ) ↝ hom(σ ,P′ ) ○ hom(Q,τ) hom(τ,σ ) ↝ hom(Q′ ,τ) ○ hom(σ ,P). 5 (Yoneda lemma). Assuming function extensionality we have: for any dependent type P over A and any a ∶ A there is an equivalence αP,a ∶ hom(Y(a),P) ≃ P(a) 54 for each a ∶ A and P ∶ A → Type. The equivalences αP,a are natural in the sense that the diagram hom(Y(a),P) αP,a hom(Y(p), σ ) hom(Y(a′ ),P′ ) P(a) σ (p) αP′ ,a′ commutes for every p ∶ a ↝ a′ and σ ∶ hom(P,P′ ).

Then we have an equivalence hFiber(proj1 ,a) ≃ P(a) for any term a of A. P ROOF. ⟨⟨a,u⟩,ida ⟩ ∶ P(a) → hFiber(proj1 ,a). We have to verify that ϕ ○ ψ ∼ idmap and that ψ ○ ϕ ∼ idmap. For the first, suppose that u ∶ P(a). Then we have that ϕ(ψ(u)) = ϕ(⟨⟨a,u⟩,ida ⟩ = ida ⋅ u = u so we even get that ϕ ○ ψ = idmapP(a) . ψ(ϕ(⟨⟨x,u⟩, p⟩)) ↝ ⟨⟨x,u⟩, p⟩ ψ(ϕ(⟨⟨x,u⟩, p⟩)) = ⟨⟨a, p ⋅ u⟩,ida ⟩. A path from ⟨⟨a, p ⋅ u⟩,ida ⟩ to ⟨⟨x,u⟩, p⟩ is found using path induction over p. 3 Equivalences of total spaces and fiberwise equivalences In this final subsection of the section about equivalences we will show that if τ ∶ ∏(x ∶ A), P(x) → Q(x) is a transformation from P to Q, then τ induces an equivalence between the total spaces whenever τ(x) is an equivalence for each x ∶ A.

Similarly, we find Θ′ −1 (ηP ) ∶ hom(F ′ P,FP). To prove that Θ′ −1 (ηP ) ○ Θ−1 (ηP′ ) ↝ idFP , note that it suffices to show that Θ(Θ′ −1 (ηP ) ○ Θ−1 (ηP′ )) ↝ ηP . This is just the same calculation as in the categorical argument: Θ(Θ′ −1 (ηP ) ○ Θ−1 (ηP′ )) ↝ ηP ↝ GΘ′ −1 (ηP ) ○ ηP′ = GΘ′ −1 (ηP ) ○ Θ′ (idF ′ P ) ↝ Θ′ (Θ′ −1 (ηP ) ○ idF ′ P ) ↝ ηP The proof that there is a homotopy Θ−1 (η ′ ) ○ Θ′ −1 (ηP ) ∼ id is similar. Θ′ −1 (ηP ) follows from the naturality of Θ, Θ′ , η and η ′. 8. Suppose that F,G ∶ (B → Type) → (A → Type) have right adjoints RF and RG respectively.