4.4#HoTT 4.4 (The unstable octahedral axiom). Suppose 𝑓:𝐴→𝐵 and 𝑔:𝐵→𝐶 and 𝑏:𝐵.(i)Show that there is a natural map 𝖿𝗂𝖻𝑔∘𝑓(𝑔(𝑏))→𝖿𝗂𝖻𝑔(𝑔(𝑏)) whose fiber over (𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏)) is equivalent to 𝖿𝗂𝖻𝑓(𝑏).(ii)Show that 𝖿𝗂𝖻𝑔∘𝑓(𝑐)≃∑(𝑤:𝖿𝗂𝖻𝑔(𝑐))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤).Solution by kiwiyouWe solve (ii) first and (i) next.Defineℎ:𝖿𝗂𝖻𝑔∘𝑓(𝑔(𝑏))→𝖿𝗂𝖻𝑔(𝑔(𝑏))ℎ((𝑎,𝑝)):≡(𝑓(𝑎),𝑝)as our desired map.Theorem 1. ℎ is natural.𝗉𝗋1ℎ𝑓id𝗉𝗋1𝑔𝖿𝗂𝖻𝑔∘𝑓(𝑔(𝑏))𝐴𝐶𝖿𝗂𝖻𝑔(𝑔(𝑏))𝐵𝐶This square commutes by definition: for (𝑎,𝑝):𝖿𝗂𝖻𝑔∘𝑓(𝑔(𝑏)),(𝗉𝗋1∘ℎ)((𝑎,𝑝))≡𝑓(𝑎)≡(𝑓∘𝗉𝗋1)(𝑎,𝑝).Applying 𝑔 to either side gives the same point of 𝐶, namely (𝑔∘𝑓)(𝑎).Theorem 2. For every 𝑐:𝐶,𝖿𝗂𝖻𝑔∘𝑓(𝑐)≃∑(𝑤:𝖿𝗂𝖻𝑔(𝑐))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤).First,∑(𝑤:𝖿𝗂𝖻𝑔(𝑐))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤):≡∑(𝑦,𝑝):𝖿𝗂𝖻𝑔(𝑐)𝖿𝗂𝖻𝑓(𝑦)≡∑(𝑦,𝑝):𝖿𝗂𝖻𝑔(𝑐)∑𝑎:𝐴(𝑓(𝑎)=𝑦)≡∑𝑎:𝐴∑𝑦:𝐵∑𝑞:𝑓(𝑎)=𝑦(𝑔(𝑦)=𝑐).Fix 𝑎:𝐴. Consider the family𝑄𝑎((𝑦,𝑞)):≡(𝑔(𝑦)=𝑐)on (𝑦,𝑞):∑𝑦:𝐵(𝑓(𝑎)=𝑦).Note that the base ∑𝑦:𝐵(𝑓(𝑎)=𝑦) is contractible with center (𝑓(𝑎),𝗋𝖾𝖿𝗅𝑓(𝑎)) using the left universal property of identity types.Lemma 3.11.9. Let 𝑃:𝐴→𝒰︀ be a type family.(ii) if 𝐴 is contractible with center 𝑎, then ∑(𝑥:𝐴)𝑃(𝑥) is equivalent to 𝑃(𝑎).Applying the lemma with𝐴:≡∑𝑦:𝐵(𝑓(𝑎)=𝑦),𝑎:≡(𝑓(𝑎),𝗋𝖾𝖿𝗅𝑓(𝑎)),𝑃(𝑥):≡𝑄𝑎(𝑥)gives us∑𝑦:𝐵∑𝑞:𝑓(𝑎)=𝑦(𝑔(𝑦)=𝑐)≃𝑄𝑎(𝑓(𝑎),𝗋𝖾𝖿𝗅𝑓(𝑎))≡(𝑔(𝑓(𝑎))=𝑐).Therefore∑(𝑤:𝖿𝗂𝖻𝑔(𝑐))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤)≃∑𝑎:𝐴(𝑔(𝑓(𝑎))=𝑐)≡𝖿𝗂𝖻𝑔∘𝑓(𝑐).∎Theorem 3. 𝖿𝗂𝖻ℎ((𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏)))≃𝖿𝗂𝖻𝑓(𝑏).Apply Theorem 2 with 𝑐:≡𝑔(𝑏):𝖿𝗂𝖻𝑔∘𝑓(𝑔(𝑏))≃∑(𝑤:𝖿𝗂𝖻𝑔(𝑔(𝑏)))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤).Under this equivalence, the map ℎ is exactly the first projection𝗉𝗋1:(∑(𝑤:𝖿𝗂𝖻𝑔(𝑔(𝑏)))𝖿𝗂𝖻𝑓(𝗉𝗋1𝑤))→𝖿𝗂𝖻𝑔(𝑔(𝑏)),since both maps send (𝑎,𝑝) to (𝑓(𝑎),𝑝).Hence𝖿𝗂𝖻ℎ((𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏)))≃𝖿𝗂𝖻𝗉𝗋1((𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏))).Lemma 4.8.1. For any type family 𝐵:𝐴→𝒰︀, the fiber of 𝗉𝗋1:(∑(𝑥:𝐴)𝐵(𝑥))→𝐴 over 𝑎:𝐴 is equivalent to 𝐵(𝑎):𝖿𝗂𝖻𝗉𝗋1(𝑎)≃𝐵(𝑎)Applying the lemma with𝐴:≡𝖿𝗂𝖻𝑔(𝑔(𝑏)),𝑎:≡(𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏)),𝐵(𝑥):≡𝖿𝗂𝖻𝑓(𝗉𝗋1𝑥)gives us𝖿𝗂𝖻𝗉𝗋1((𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏)))≃𝖿𝗂𝖻𝑓(𝗉𝗋1((𝑏,𝗋𝖾𝖿𝗅𝑔(𝑏))))≡𝖿𝗂𝖻𝑓(𝑏).∎