3.1#HoTT-3.1. Prove that if 𝐴≃𝐵 and 𝐴 is a set, then so is 𝐵.Solution by RanolPAs the problem said, we have:•𝑒:𝐴≃𝐵•𝑓:isSet(𝐴)And we need to check inhabitant of 𝑔:isSet(𝐵), which is by definition:𝑔:∏(𝑥,𝑦:𝐵)∏(𝑝,𝑞:𝑥=𝑦)(𝑝=𝑞)and we’ll define this function as follows:Let ℎ=ap𝑒−1𝑔(𝑥,𝑦,𝑝,𝑞):≡(apℎ)−1(𝑓(𝑒−1(𝑥),𝑒−1(𝑦),ℎ(𝑝),ℎ(𝑞)))by Lemma 3.3.5. isSet(𝐵) is mere propositionand because of inhabitant of 𝑔:isSet(𝐵),isSet(𝐵)≃𝟏.∎
3.2#HoTT 3.2. Prove that if A and B are sets, then so is A + B.Solution by kiwiyouWe want to construct:𝗂𝗌𝖲𝖾𝗍𝐴+𝐵:𝗂𝗌𝖲𝖾𝗍(𝐴)→𝗂𝗌𝖲𝖾𝗍(𝐵)→𝗂𝗌𝖲𝖾𝗍(𝐴+𝐵)Proof outline:1.Using encode-decode method, suggest a type family 𝖼𝗈𝖽𝖾(𝑥,𝑦)≃(𝑥=𝐴+𝐵𝑦)2.Prove 𝗂𝗌𝖯𝗋𝗈𝗉(𝖼𝗈𝖽𝖾(𝑥,𝑦))3.Prove 𝖼𝗈𝖽𝖾(𝑥,𝑦)≃(𝑥=𝐴+𝐵𝑦)4.Prove 𝗂𝗌𝖲𝖾𝗍(𝐴+𝐵) using univalence and transport1. Definition of 𝖼𝗈𝖽𝖾(𝑥,𝑦)𝑥=𝐴+𝐵𝑦 is hard to handle directly since there are two degenerate cases: 𝗂𝗇𝗅=𝗂𝗇𝗋 and 𝗂𝗇𝗋=𝗂𝗇𝗅. We use 𝖼𝗈𝖽𝖾(𝑥,𝑦) to rule them out.𝖼𝗈𝖽𝖾:∏𝑥,𝑦:𝐴+𝐵𝒰︀𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎′)):≡(𝑎=𝐴𝑎′)𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗋(𝑏′)):≡(𝑏=𝐵𝑏′)𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗋(𝑏′)):≡𝟎𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗅(𝑎′)):≡𝟎We omit 𝟎 cases from now on.We define 𝖾𝗇𝖼𝗈𝖽𝖾 with path induction on 𝑥 and 𝑦.𝖾𝗇𝖼𝗈𝖽𝖾:∏𝑥,𝑦:𝐴+𝐵(𝑥=𝑦)→𝖼𝗈𝖽𝖾(𝑥,𝑦)𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝗋𝖾𝖿𝗅𝗂𝗇𝗅(𝑎)):≡𝗋𝖾𝖿𝗅𝑎𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗋(𝑏),𝗋𝖾𝖿𝗅𝗂𝗇𝗋(𝑏)):≡𝗋𝖾𝖿𝗅𝑏𝖽𝖾𝖼𝗈𝖽𝖾 needs case analysis.𝖽𝖾𝖼𝗈𝖽𝖾:∏𝑥,𝑦:𝐴+𝐵𝖼𝗈𝖽𝖾(𝑥,𝑦)→(𝑥=𝐴+𝐵𝑦)𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎′),𝑐):≡𝖺𝗉𝗂𝗇𝗅(𝑐)𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗋(𝑏′),𝑐):≡𝖺𝗉𝗂𝗇𝗋(𝑐)2. Construction of 𝗂𝗌𝖯𝗋𝗈𝗉(𝖼𝗈𝖽𝖾(𝑥,𝑦))𝗂𝗌𝖯𝗋𝗈𝗉(𝖼𝗈𝖽𝖾(𝑥,𝑦))≡∏𝑝,𝑞:𝖼𝗈𝖽𝖾(𝑥,𝑦)(𝑝=𝑞)The type seems a bit obscure, but case analysis on 𝑥 and 𝑦 reveals it is actually simple.𝗂𝗌𝖯𝗋𝗈𝗉𝖼𝗈𝖽𝖾:∏𝑢:𝗂𝗌𝖲𝖾𝗍(𝐴)∏𝑣:𝗂𝗌𝖲𝖾𝗍(𝐵)∏𝑥,𝑦:𝐴+𝐵∏𝑝,𝑞:𝖼𝗈𝖽𝖾(𝑥,𝑦)(𝑝=𝑞)𝗂𝗌𝖯𝗋𝗈𝗉𝖼𝗈𝖽𝖾(𝑢,𝑣,𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎′),𝑝,𝑞):≡𝑢(𝑎,𝑎′,𝑝,𝑞)𝗂𝗌𝖯𝗋𝗈𝗉𝖼𝗈𝖽𝖾(𝑢,𝑣,𝗂𝗇𝗋(𝑏),𝗂𝗇𝗋(𝑏′),𝑝,𝑞):≡𝑣(𝑏,𝑏′,𝑝,𝑞)3. 𝖼𝗈𝖽𝖾(𝑥,𝑦) and (𝑥=𝐴+𝐵𝑦) are equivalentTo use univalence and transport, we need equivalence.Forward direction: when 𝑥≡𝗂𝗇𝗅(𝑎) and 𝑦≡𝗂𝗇𝗅(𝑎′), 𝖼𝗈𝖽𝖾(𝑥,𝑦)≡(𝑎=𝑎′). do a path induction with 𝑎≡𝑎′, 𝑐≡𝗋𝖾𝖿𝗅𝑎:𝖾𝗇𝖼𝗈𝖽𝖾(𝑥,𝑦,𝖽𝖾𝖼𝗈𝖽𝖾(𝑥,𝑦,𝑐))≡𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝗋𝖾𝖿𝗅𝑎))≡𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝖺𝗉𝗂𝗇𝗅(𝗋𝖾𝖿𝗅𝑎))≡𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝗋𝖾𝖿𝗅𝗂𝗇𝗅(𝑎))≡𝗋𝖾𝖿𝗅𝑎≡𝑐The case 𝑥≡𝗂𝗇𝗋(𝑏) and 𝑦≡𝗂𝗇𝗋(𝑏′) is symmetric.Backward direction: path induction with 𝑎=𝑎′, 𝑝≡𝗋𝖾𝖿𝗅𝗂𝗇𝗅(𝑎):𝖽𝖾𝖼𝗈𝖽𝖾(𝑥,𝑦,𝖾𝗇𝖼𝗈𝖽𝖾(𝑥,𝑦,𝑝))≡𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝖾𝗇𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝗋𝖾𝖿𝗅𝗂𝗇𝗅(𝑎)))≡𝖽𝖾𝖼𝗈𝖽𝖾(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎),𝗋𝖾𝖿𝗅𝑎)≡𝖺𝗉𝗂𝗇𝗅(𝗋𝖾𝖿𝗅𝑎)≡𝗋𝖾𝖿𝗅𝗂𝗇𝗅(𝑎)≡𝑝4. Construction of 𝗂𝗌𝖲𝖾𝗍(𝐴+𝐵)𝗂𝗌𝖲𝖾𝗍𝐴+𝐵(𝑢,𝑣,𝑥,𝑦):≡𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝗂𝗌𝖯𝗋𝗈𝗉(𝗎𝖺(𝗌𝗎𝗆𝗆𝗈𝗇𝖼𝗈𝖽𝖾(𝑥,𝑦)≃(𝑥=𝑦)))(𝗂𝗌𝖯𝗋𝗈𝗉𝖼𝗈𝖽𝖾(𝑢,𝑣,𝑥,𝑦))Sanity check:•𝗎𝖺(𝗌𝗎𝗆𝗆𝗈𝗇𝖼𝗈𝖽𝖾(𝑥,𝑦)≃(𝑥=𝑦)) is of type 𝖼𝗈𝖽𝖾(𝑥,𝑦)=𝒰︀(𝑥=𝑦).•𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝗂𝗌𝖯𝗋𝗈𝗉(□:𝖼𝗈𝖽𝖾(𝑥,𝑦)=𝒰︀(𝑥=𝑦)) is of type 𝗂𝗌𝖯𝗋𝗈𝗉(𝖼𝗈𝖽𝖾(𝑥,𝑦))→𝗂𝗌𝖯𝗋𝗈𝗉(𝑥=𝑦).•𝗂𝗌𝖯𝗋𝗈𝗉𝖼𝗈𝖽𝖾(𝑢,𝑣,𝑥,𝑦) is of type ∏𝑝,𝑞:𝖼𝗈𝖽𝖾(𝑥,𝑦)(𝑝=𝑞)≡𝗂𝗌𝖯𝗋𝗈𝗉(𝖼𝗈𝖽𝖾(𝑥,𝑦)).•𝗂𝗌𝖲𝖾𝗍𝐴+𝐵(𝑢,𝑣,𝑥,𝑦) is of type 𝗂𝗌𝖯𝗋𝗈𝗉(𝑥=𝑦).•𝗂𝗌𝖲𝖾𝗍𝐴+𝐵(𝑢,𝑣) is of type ∏𝑥,𝑦:𝐴+𝐵𝗂𝗌𝖯𝗋𝗈𝗉(𝑥=𝑦)≡𝗂𝗌𝖲𝖾𝗍(𝐴+𝐵).∎
3.4#HoTT-3.4. Show that 𝐴 is a mere proposition if and only if 𝐴→𝐴 is contractible.Solution by RanolP1.(⟹) 𝐴→𝐴 is contractible → 𝐴 is mere propositionSince there’s 𝑒:isContr(𝐴→𝐴), and by definition it is,𝑒:∑𝑐:𝐴→𝐴∏𝑥:𝐴→𝐴(𝑐=𝑥)so we can get 𝑓:≡snd𝑒By definition, isProp(𝐴)≡∏𝑥,𝑦:𝐴(𝑥=𝑦) and we can define its element.answer:isProp(𝐴)answer 𝑥 𝑦:≡happly((𝑓(𝜆_.𝑥)−1⋅𝑓(𝜆_.𝑦)),𝑥)∎2.(⟸) 𝐴 is mere proposition → 𝐴→𝐴 is contractibleGiven 𝑓:isProp(𝐴) we can construct answeranswer:≡(id,𝜆𝑥.funext(𝜆𝑎.𝑓(id(𝑎),𝑥(𝑎))))∎
3.5#HoTT-3.5. Show that isProp(𝐴)≃(𝐴→isContr(𝐴)).Solution by finalchild𝑓:≡(𝐻:isProp𝐴)↦(𝑎:𝐴)↦(𝑎,(𝑏:𝐴)↦𝐻𝑎𝑏)𝑔:≡(𝐻:𝐴→isContr𝐴)↦(𝑎:𝐴)↦(𝑏:𝐴)↦(pr2(𝐻𝑎)𝑎)−1▪(pr2(𝐻𝑎)𝑏)Prove that 𝑔 is a quasi-inverse of 𝑓.Since isProp𝐴 is a mere proposition, by function extensionality,𝑔⚬𝑓=idisProp𝐴Since isContr𝐴 is a mere proposition, by function extensionality,𝑓⚬𝑔=id𝐴→isContr𝐴
3.7#HoTT 3.7. More generally, show that if 𝐴 and 𝐵 are mere propositions and ¬(𝐴×𝐵), then 𝐴+𝐵 is also a mere proposition.Solution by kiwiyouWe need:𝗌𝗎𝗆-𝗂𝗌𝖯𝗋𝗈𝗉:𝗂𝗌𝖯𝗋𝗈𝗉(𝐴)→𝗂𝗌𝖯𝗋𝗈𝗉(𝐵)→¬(𝐴×𝐵)→𝗂𝗌𝖯𝗋𝗈𝗉(𝐴+𝐵)Let ℎ𝐴:𝗂𝗌𝖯𝗋𝗈𝗉(𝐴), ℎ𝐵:𝗂𝗌𝖯𝗋𝗈𝗉(𝐵), ℎ¬:¬(𝐴×𝐵). Let 𝗌𝗎𝗆-𝗂𝗌𝖯𝗋𝗈𝗉(ℎ𝐴,ℎ𝐵,ℎ¬):≡𝑓. We define 𝑓 by cases on its arguments:𝑓:∏𝑥,𝑦:𝐴+𝐵𝑥=𝑦𝑓(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗅(𝑎′)):≡𝖺𝗉𝗂𝗇𝗅(ℎ𝐴(𝑎,𝑎′))𝑓(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗋(𝑏′)):≡𝖺𝗉𝗂𝗇𝗋(ℎ𝐵(𝑏,𝑏′))𝑓(𝗂𝗇𝗅(𝑎),𝗂𝗇𝗋(𝑏)):≡𝗂𝗇𝖽𝟎(ℎ¬(𝑎,𝑏))𝑓(𝗂𝗇𝗋(𝑏),𝗂𝗇𝗅(𝑎)):≡𝗂𝗇𝖽𝟎(ℎ¬(𝑎,𝑏))∎
3.11#HoTT 3.11. Show that it is not the case that for all 𝐴:𝒰︀ we have ‖𝐴‖→𝐴. (However, there can be particular types for which ‖𝐴‖→𝐴. Exercise 3.8 implies that qinv(𝑓) is such.)Solution by RanolPGiven 𝜀:∏𝐴:𝒰︀‖𝐴‖→𝐴,we have apd as follows:Given𝑃:𝐴→𝒰︀and𝑓:∏𝑥:𝐴𝑃(𝑥)apd𝑓:∏𝑝:𝑥=𝑦(𝑝∗(𝑓(𝑥))=𝑓(𝑦))Let’s define𝑃(𝐴):≡‖𝐴‖→𝐴so we can use equality ¬:𝟐≃𝟐 to get ua(¬):𝟐=𝟐:𝑝:≡apd𝜀(ua(¬)):((ua(¬)∗)(𝜀(𝟐)))=𝜀(𝟐)and happly on it using ⋆:‖𝟐‖happly(𝑝,⋆):((ua(¬)∗)(𝜀(𝟐)(⋆)))=𝜀(𝟐)(⋆)so, WLOG we can assume that 𝜀(𝟐)(⋆)=1𝟐 sohapply(𝑝,⋆):((ua(¬)∗)(1𝟐))=1𝟐and since ua(¬)∗=¬, we have:happly(𝑝,⋆):¬(1𝟐)=1𝟐which is contradiction.
3.12#HoTT 3.12. Show that if LEM holds, then for all 𝐴:𝒰 we have ‖(‖𝐴‖→𝐴)‖.Solution by finalchildBy LEM, ‖𝐴‖+¬‖𝐴‖. Casework.On case ‖𝐴‖, by recursion principle of ‖𝐴‖, it suffices to assume 𝑎:𝐴 and prove with |⋅↦𝑎|:‖‖𝐴‖→𝐴‖.On case ¬‖𝐴‖, ‖𝐴‖ contradicts the assumption, thus ‖𝐴‖→𝐴 by explosion. It follows that ‖‖A‖→A‖.
3.14#HoTT 3.14. Show that assuming LEM, the double negation ¬¬𝐴 has the same recursion principle as the propositional truncation ‖𝐴‖ but with a propositional computation rule rather than a judgmental one. In other words, prove that assuming LEM, if 𝐵 is a mere proposition and we have 𝑓:𝐴→𝐵, then there is an induced 𝑔:¬¬𝐴→𝐵 such that 𝑔(|𝑎|)=𝑓(𝑎) for all 𝑎:𝐴. Deduce that (assuming LEM) we have ¬¬𝐴≃‖𝐴‖. Thus, under LEM, the propositional truncation can be defined rather than taken as a separate type former.Solution by kiwiyouAssume𝖫𝖤𝖬:∏𝑃:Prop𝒰︀(𝑃+¬𝑃).Fix 𝐵:Prop𝒰︀ and 𝑓:𝐴→𝐵. We must build𝗋𝖾𝖼¬¬𝐴(𝐵,𝑓):¬¬𝐴→𝐵.So take 𝑔:¬¬𝐴 and try to produce an element of 𝐵.What data do we have?1.𝑓:𝐴→𝐵 only turns an 𝐴 into a 𝐵.2.𝑔:¬¬𝐴 is ((𝐴→𝟎)→𝟎); it does not give 𝐴.3.We do not have 𝖫𝖤𝖬(𝐴), and even with it this route is not needed.Therefore we cannot directly manufacture 𝐵 from 𝑓 and 𝑔. The only classical handle is to decide 𝐵 itself:𝖫𝖤𝖬(𝐵):𝐵+¬𝐵.This is why the eliminator must split on 𝐵+¬𝐵.1.If 𝐵 holds, we return it via id𝐵.2.If ℎ:¬𝐵, then ℎ∘𝑓:¬𝐴, so 𝑔(ℎ∘𝑓):𝟎. From this contradiction, ex-falso gives an element of 𝐵.Hence the proof line is exactly𝗋𝖾𝖼¬¬𝐴(𝐵,𝑓):≡𝜆𝑔.𝗋𝖾𝖼𝐵+¬𝐵(𝐵,id𝐵,𝜆ℎ.𝗋𝖾𝖼𝟎(𝐵,𝑔(ℎ∘𝑓)),𝖫𝖤𝖬(𝐵)).Let𝜂:𝐴→¬¬𝐴𝜂(𝑎):≡𝜆𝑢.𝑢(𝑎).Then for each 𝑎:𝐴 we have a propositional computation rule𝗋𝖾𝖼¬¬𝐴(𝐵,𝑓)(𝜂(𝑎))=𝑓(𝑎),by case analysis on 𝖫𝖤𝖬(𝐵): the 𝗂𝗇𝗅 case is from 𝗂𝗌𝖯𝗋𝗈𝗉(𝐵), and the 𝗂𝗇𝗋 case is absurd.Define𝑓:¬¬𝐴→‖𝐴‖𝑓:≡𝗋𝖾𝖼¬¬𝐴(‖𝐴‖,|−|),and𝑔:‖𝐴‖→¬¬𝐴𝑔:≡𝗋𝖾𝖼‖𝐴‖(¬¬𝐴,𝜆𝑎.𝜆𝑢.𝑢(𝑎)).Now 𝗊𝗂𝗇𝗏(𝑓) is immediate. We need∏𝑥:¬¬𝐴(𝑔(𝑓(𝑥))=𝑥) and ∏𝑦:‖𝐴‖(𝑓(𝑔(𝑦))=𝑦).Since both types are mere propositions,𝗂𝗌𝖯𝗋𝗈𝗉(¬¬𝐴),𝗂𝗌𝖯𝗋𝗈𝗉(‖𝐴‖)we can set𝛼(𝑥):≡𝗂𝗌𝖯𝗋𝗈𝗉(¬¬𝐴)(𝑔(𝑓(𝑥)),𝑥),and𝛽(𝑦):≡𝗂𝗌𝖯𝗋𝗈𝗉(‖𝐴‖)(𝑓(𝑔(𝑦)),𝑦).Hence 𝗊𝗂𝗇𝗏(𝑓), so¬¬𝐴≃‖𝐴‖.Therefore, under LEM, propositional truncation is definable from double negation, with only propositional computation. ∎
3.15#HoTT-3.15.(i)Show that for any 𝐴:𝒰︀, the type∏𝑃:Prop𝒰︀((𝐴→𝑃)→𝑃)has the same recursion principle as ‖𝐴‖, at least relative to propositions in 𝒰︀, with the same judgmental computation rule.(ii)The type considered in the previous part does not lie in the same universe 𝒰︀, and its recursion principle only applies to propositions in 𝒰︀. Show that if we assume propositional resizing, we can define a type that does lie in the same universe 𝒰︀ and satisfies the same recursion principle as ‖𝐴‖, albeit with only a propositional computation rule. Thus, we can also define the propositional truncation in this case.Solution by Jihyeon Kim (김지현) (simnalamburt)(i)문제에 주어진 타입을 𝑇(𝐴)로 명명한다.𝑇(𝐴):≡∏𝑃:Prop𝒰︀((𝐴→𝑃)→𝑃)임의의 𝑎:𝐴 를 𝑇(𝐴)로 보내는 함수 𝜂를 아래와 같이 정의한다.𝜂:𝐴→𝑇(𝐴)𝜂(𝑎):≡𝜆(𝑃:Prop𝒰︀).𝜆(𝑓:𝐴→𝑃).𝑓(𝑎)이제 임의의 mere proposition 𝑃:Prop𝒰︀와 함수 𝑓:𝐴→𝑃 에 대해, 𝑇(𝐴)를 𝑃로 보내는 함수 rec𝑇(𝐴)(𝑃,𝑓)를 정의할 수 있다.rec𝑇(𝐴)(𝑃,𝑓):𝑇(𝐴)→𝑃rec𝑇(𝐴)(𝑃,𝑓)(𝑧):≡𝑧(𝑃)(𝑓)이때, 모든 𝑎:𝐴 에 대해 아래가 성립한다.rec𝑇(𝐴)(𝑃,𝑓)(𝜂(𝑎))≡𝜂(𝑎)(𝑃)(𝑓) … (β-reduction)≡𝑓(𝑎) … (β-reduction)이때, ‖𝐴‖의 recursion principle은 교재 117p와 같이 아래와 같이 정의되어있다.If 𝐵 is a mere proposition and we have 𝑓:𝐴→𝐵,then there is an induced 𝑔:‖𝐴‖→𝐵 such that 𝑔(|𝑎|)≡𝑓(𝑎) for all 𝑎:𝐴.— HoTT p.117따라서 임의의 𝑃:Prop𝒰︀와 𝑓:𝐴→𝑃에 대해𝑔:‖𝐴‖→𝑃rec𝑇(𝐴)(𝑃,𝑓):𝑇(𝐴)→𝑃가 존재하고, 모든 𝑎:𝐴에 대해𝑔(|𝑎|)≡𝑓(𝑎)rec𝑇(𝐴)(𝑃,𝑓)(𝜂(𝑎))≡𝑓(𝑎)가 성립하는것이다.|−|:𝐴→‖𝐴‖를𝜂:𝐴→𝑇(𝐴)로 바꾼 것과 정확히 같은 형태이며, 계산 규칙도 judgmental equality로 같다.(ii)먼저 (i)의 𝑇(𝐴)가 mere proposition임을 증명하겠다.•𝑃:Prop𝒰︀가 존재할 경우, Prop𝒰︀의 정의에 의해 𝜋2(𝑃):isProp(𝑃)가 존재한다.𝑃:Prop𝒰︀≡{𝐴:𝒰︀|isProp(𝐴)}≡∑𝐴:𝒰︀isProp(𝐴)𝜋2(𝑃):isProp(𝑃)•𝑃가 mere proposition이면, ((𝐴→𝑃)→𝑃)도 mere proposition이다.lemma:isProp(𝑃)→isProp((𝐴→𝑃)→𝑃)lemma(ℎ𝑃):≡𝜆(𝑓,𝑔:(𝐴→𝑃)→𝑃).funext(𝜆(𝑎:(𝐴→𝑃)).ℎ𝑃(𝑓(𝑎),𝑔(𝑎)))타입체크:ℎ𝑃:isProp(𝑃)≡∏𝑥,𝑦:𝑃(𝑥=𝑦)𝑎:𝐴→𝑃𝑓,𝑔:(𝐴→𝑃)→𝑃𝑓(𝑎),𝑔(𝑎):𝑃ℎ𝑃(𝑓(𝑎),𝑔(𝑎)):(𝑓(𝑎)=𝑔(𝑎))𝜆(𝑎:(𝐴→𝑃)).ℎ𝑃(𝑓(𝑎),𝑔(𝑎)):∏𝑎:(𝐴→𝑃)(𝑓(𝑎)=𝑔(𝑎))funext(𝜆(𝑎:(𝐴→𝑃)).ℎ𝑃(𝑓(𝑎),𝑔(𝑎))):(𝑓=𝑔)lemma(ℎ𝑃)≡𝜆(𝑓,𝑔:(𝐴→𝑃)→𝑃).funext(𝜆(𝑎:(𝐴→𝑃)).ℎ𝑃(𝑓(𝑎),𝑔(𝑎))):∏𝑓,𝑔:(𝐴→𝑃)→𝑃(𝑓=𝑔):≡isProp((𝐴→𝑃)→𝑃)•이때, ℎ𝑇(𝐴):isProp(𝑇(𝐴))를 찾을 수 있다.ℎ𝑇(𝐴):isProp(𝑇(𝐴))ℎ𝑇(𝐴):≡𝜆(𝑓,𝑔:𝑇(𝐴)).funext(𝜆(𝑃:Prop𝒰︀).lemma(𝜋2(𝑃))(𝑓(𝑃),𝑔(𝑃)))타입체크:𝑃:Prop𝒰︀𝑓,𝑔:𝑇(𝐴)≡∏𝑃:Prop𝒰︀((𝐴→𝑃)→𝑃)𝑓(𝑃),𝑔(𝑃):(𝐴→𝑃)→𝑃lemma:isProp(𝑃)→isProp((𝐴→𝑃)→𝑃)𝜋2(𝑃):isProp(𝑃)lemma(𝜋2(𝑃)):isProp((𝐴→𝑃)→𝑃)≡∏𝑥,𝑦:(𝐴→𝑃)→𝑃(𝑥=𝑦)lemma(𝜋2(𝑃))(𝑓(𝑃),𝑔(𝑃)):(𝑓(𝑃)=𝑔(𝑃))𝜆(𝑃:Prop𝒰︀).lemma(𝜋2(𝑃))(𝑓(𝑃),𝑔(𝑃)):∏𝑃:Prop𝒰︀(𝑓(𝑃)=𝑔(𝑃))funext(𝜆(𝑃:Prop𝒰︀).lemma(𝜋2(𝑃))(𝑓(𝑃),𝑔(𝑃))):(𝑓=𝑔)ℎ𝑇(𝐴)≡𝜆(𝑓,𝑔:𝑇(𝐴)).funext(𝜆(𝑃:Prop𝒰︀).lemma(𝜋2(𝑃))(𝑓(𝑃),𝑔(𝑃))):∏𝑓,𝑔:𝑇(𝐴)(𝑓=𝑔):≡isProp(𝑇(𝐴))따라서, 𝑇(𝐴)는 mere proposition이다.𝑇(𝐴)≡∏𝑃:Prop𝒰︀((𝐴→𝑃)→𝑃) 이므로, 𝑃:Prop𝒰︀에 의해 𝑇(𝐴)는 𝒰︀보다 한단계 더 큰 universe인 𝒰︀+에 속한다. 하지만 𝑇(𝐴)가 mere proposition이므로, propositional resizing axiom을 가정하면 𝑇(𝐴)와 동치인 타입 𝑇′(𝐴)를 𝒰︀ 안에서 잡을 수 있다.𝑇(𝐴):𝒰︀+𝑇′(𝐴):𝒰︀𝑒:𝑇′(𝐴)≃𝑇(𝐴)이제 𝑇(𝐴)의 𝜂,rec𝑇(𝐴)(𝑃,𝑓)를, 𝑇′(𝐴)의 𝜂′,rec′𝑇(𝐴)(𝑃,𝑓)로 옮기겠다.𝜂′:𝐴→𝑇′(𝐴)𝜂′(𝑎):≡𝑒−1(𝜂(𝑎))rec′𝑇(𝐴)(𝑃,𝑓):𝑇′(𝐴)→𝑃rec′𝑇(𝐴)(𝑃,𝑓)(𝑧):≡𝑒(𝑧)(𝑃)(𝑓)그러면 𝑎:𝐴 에 대해 아래가 성립한다.rec′𝑇(𝐴)(𝑃,𝑓)(𝜂′(𝑎))≡rec′𝑇(𝐴)(𝑃,𝑓)(𝑒−1(𝜂(𝑎))) … (β-reduction)≡𝑒(𝑒−1(𝜂(𝑎)))(𝑃)(𝑓) … (β-reduction)=𝜂(𝑎)(𝑃)(𝑓) … (equivalence)≡𝑓(𝑎) … (β-reduction)이때, path 𝑒(𝑒−1(𝑥))=𝑥 로 인해, 전체가 judgemental이 아닌 propositional equality이다.즉 𝑇′(𝐴):𝒰︀ 는 ‖𝐴‖와 비교했을때 계산 규칙이 propositional하게 같은 recursion principle을 가진다.
3.17#HoTT 3.17. Show that the rules for the propositional truncation given in §3.7 are sufficient to imply the following induction principle: for any type family 𝐵:‖𝐴‖→𝒰 such that each 𝐵(𝑥) is a mere proposition, if for every 𝑎:𝐴 we have 𝐵(|𝑎|), then for every 𝑥:‖𝐴‖ we have 𝐵(𝑥).Solution by finalchildWe are given ℎ:Π𝑎:𝐴𝐵(|𝑎|).Let ℎ′:≡(𝑎:𝐴)↦(|𝑎|,ℎ(𝑎)):𝐴→Σ𝑦:‖𝐴‖𝐵(𝑦). Note that Σ𝑦:‖𝐴‖𝐵(𝑦) is a mere proposition.Given 𝑥:‖𝐴‖, by the recursion principle on 𝑥:‖𝐴‖ with ℎ′, Σ𝑦:‖𝐴‖𝐵(𝑦). Destruct it to (𝑦,𝑖).Since 𝑥=𝑦, transport 𝑖 to prove 𝐵(𝑥).
3.18#HoTT-3.18. Show that the law of excluded middle (3.4.1) and the law of double negation (3.4.2) are logically equivalentLEM:≡∏𝐴:𝒰︀(isProp(𝐴)→(𝐴+¬𝐴)) ⋯ (3.4.1)LDN:≡∏𝐴:𝒰︀(isProp(𝐴)→(¬¬𝐴→𝐴)) ⋯ (3.4.2)Solution by Jihyeon Kim (김지현) (simnalamburt)(i)먼저 LEM→LDN 을 증명하겠다.lem:LEM 을 가정하자. 임의의 𝐴:𝒰︀, ℎ𝐴:isProp(𝐴) 에 대해 ¬¬𝐴→𝐴 를 만드는 함수 toLDN(lem)(𝐴)(ℎ𝐴)를 아래와 같이 정의할 수 있다.toLDN:LEM→LDNtoLDN(lem)(𝐴)(ℎ𝐴):≡𝜆(𝑢:¬¬𝐴).rec𝐴+¬𝐴(𝐴,𝜆𝑎.𝑎,𝜆𝑛.rec𝟎(𝐴,𝑢(𝑛)),lem(𝐴)(ℎ𝐴))타입체크:lem:LEM≡∏𝑋:𝒰︀(isProp(𝑋)→(𝑋+¬𝑋))𝐴:𝒰︀ℎ𝐴:isProp(𝐴)𝑢:¬¬𝐴≡(¬𝐴→𝟎)lem(𝐴):isProp(𝐴)→(𝐴+¬𝐴)lem(𝐴)(ℎ𝐴):𝐴+¬𝐴𝜆𝑎.𝑎:𝐴→𝐴𝑛:¬𝐴≡(𝐴→𝟎)𝑢(𝑛):𝟎rec𝟎(𝐴,𝑢(𝑛)):𝐴𝜆𝑛.rec𝟎(𝐴,𝑢(𝑛)):¬𝐴→𝐴rec𝐴+¬𝐴(𝐴,𝜆𝑎.𝑎,𝜆𝑛.rec𝟎(𝐴,𝑢(𝑛)),lem(𝐴)(ℎ𝐴)):𝐴𝜆(𝑢:¬¬𝐴).rec𝐴+¬𝐴(𝐴,𝜆𝑎.𝑎,𝜆𝑛.rec𝟎(𝐴,𝑢(𝑛)),lem(𝐴)(ℎ𝐴)):¬¬𝐴→𝐴toLDN(lem)(𝐴)(ℎ𝐴):¬¬𝐴→𝐴따라서, toLDN 은 LEM→LDN 의 witness 이다.(ii)다음으로 LDN→LEM 을 증명하겠다.ldn:LDN 을 가정하자. 임의의 𝐴:𝒰︀와 ℎ𝐴:isProp(𝐴)에 대해 𝐴+¬𝐴를 만들기 위해, 먼저 보조정리 세 개를 구성하겠다.•먼저 ¬𝐴가 mere proposition임을 보이자.isPropNot(𝐴):isProp(¬𝐴)isPropNot(𝐴):≡𝜆(𝑓,𝑔:¬𝐴).funext(𝜆𝑎.ind𝟎(𝑓(𝑎)))타입체크:𝐴:𝒰︀¬𝐴:𝐴→𝟎𝑓,𝑔:¬𝐴≡(𝐴→𝟎)𝑎:𝐴𝑓(𝑎):𝟎𝑔(𝑎):𝟎ind𝟎(𝑓(𝑎)):𝑓(𝑎)=𝑔(𝑎)𝜆𝑎.ind𝟎(𝑓(𝑎)):∏𝑎:𝐴(𝑓(𝑎)=𝑔(𝑎))funext(𝜆𝑎.ind𝟎(𝑓(𝑎))):𝑓=𝑔𝜆(𝑓,𝑔:¬𝐴).funext(𝜆𝑎.ind𝟎(𝑓(𝑎))):∏𝑓,𝑔:¬𝐴(𝑓=𝑔)isPropNot(𝐴):isProp(¬𝐴)•이제 𝐴+¬𝐴가 mere proposition임을 보이자.isPropDec:isProp(𝐴)→isProp(𝐴+¬𝐴)isPropDec(ℎ𝐴)(inl(𝑎),inl(𝑎′)):≡apinl(ℎ𝐴(𝑎,𝑎′))isPropDec(ℎ𝐴)(inl(𝑎),inr(𝑛)):≡ind𝟎(𝑛(𝑎))isPropDec(ℎ𝐴)(inr(𝑛),inl(𝑎)):≡ind𝟎(𝑛(𝑎))isPropDec(ℎ𝐴)(inr(𝑛),inr(𝑛′)):≡apinr(isPropNot(𝐴)(𝑛,𝑛′))타입체크:ℎ𝐴:isProp(𝐴)≡∏𝑥,𝑦:𝐴(𝑥=𝑦)𝑎,𝑎′:𝐴𝑛,𝑛′:¬𝐴ℎ𝐴(𝑎,𝑎′):𝑎=𝑎′apinl(ℎ𝐴(𝑎,𝑎′)):inl(𝑎)=inl(𝑎′)𝑛(𝑎):𝟎ind𝟎(𝑛(𝑎)):inl(𝑎)=inr(𝑛)ind𝟎(𝑛(𝑎)):inr(𝑛)=inl(𝑎)isPropNot(𝐴)(𝑛,𝑛′):𝑛=𝑛′apinr(isPropNot(𝐴)(𝑛,𝑛′)):inr(𝑛)=inr(𝑛′)isPropDec(ℎ𝐴):∏𝑥,𝑦:𝐴+¬𝐴(𝑥=𝑦):≡isProp(𝐴+¬𝐴)따라서, 𝐴+¬𝐴는 mere proposition이다.•마지막으로 ¬¬(𝐴+¬𝐴)를 보이자.nnem(𝐴):¬¬(𝐴+¬𝐴)nnem(𝐴):≡𝜆𝑘.𝑘(inr(𝜆𝑎.𝑘(inl(𝑎))))타입체크:𝐴:𝒰︀𝐴+¬𝐴:𝒰︀𝑘:¬(𝐴+¬𝐴)≡((𝐴+¬𝐴)→𝟎)𝑎:𝐴inl(𝑎):𝐴+¬𝐴𝑘(inl(𝑎)):𝟎𝜆𝑎.𝑘(inl(𝑎)):𝐴→𝟎≡¬𝐴inr(𝜆𝑎.𝑘(inl(𝑎))):𝐴+¬𝐴𝑘(inr(𝜆𝑎.𝑘(inl(𝑎)))):𝟎≡𝟎𝜆𝑘.𝑘(inr(𝜆𝑎.𝑘(inl(𝑎)))):¬(𝐴+¬𝐴)→𝟎nnem(𝐴):¬¬(𝐴+¬𝐴)이제 위의 세 보조정리를 사용해 LDN→LEM 의 witness를 직접 정의할 수 있다.toLEM:LDN→LEMtoLEM(ldn)(𝐴)(ℎ𝐴):≡ldn(𝐴+¬𝐴)(isPropDec(ℎ𝐴))(nnem(𝐴))타입체크:ldn:LDN≡∏𝑋:𝒰︀(isProp(𝑋)→(¬¬𝑋→𝑋))𝐴+¬𝐴:𝒰︀isPropDec(ℎ𝐴):isProp(𝐴+¬𝐴)nnem(𝐴):¬¬(𝐴+¬𝐴)ldn(𝐴+¬𝐴):isProp(𝐴+¬𝐴)→(¬¬(𝐴+¬𝐴)→(𝐴+¬𝐴))ldn(𝐴+¬𝐴)(isPropDec(ℎ𝐴)):¬¬(𝐴+¬𝐴)→(𝐴+¬𝐴)ldn(𝐴+¬𝐴)(isPropDec(ℎ𝐴))(nnem(𝐴)):𝐴+¬𝐴toLEM(ldn)(𝐴)(ℎ𝐴):𝐴+¬𝐴따라서, toLEM 은 LDN→LEM 의 witness 이다.결론적으로, toLDN 과 toLEM 이 존재하므로 LEM 과 LDN 은 논리적으로 동치이다. ∎
3.20#HoTT 3.20. Prove Lemma 3.11.9(ii): if 𝐴 is contractible with center 𝑎, then ∑(𝑥:𝐴)𝑃(𝑥) is equivalent to 𝑃(𝑎).Solution by kiwiyou(𝑎,𝜋):𝗂𝗌𝖢𝗈𝗇𝗍𝗋(𝐴)≡∑(𝑎:𝐴)∏(𝑥:𝐴)(𝑎=𝑥).Thus 𝜋(𝑥):𝑎=𝑥 for each 𝑥:𝐴.Use 𝜋(𝑥) to transport 𝑃(𝑥) into 𝑃(𝑎):𝜋(𝑥)−1∗:≡𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝑃(𝜋(𝑥)−1,−):𝑃(𝑥)→𝑃(𝑎)Define𝑓:(∑(𝑥:𝐴)𝑃(𝑥))→𝑃(𝑎)𝑓(𝑧):≡𝜋(𝗉𝗋1(𝑧))−1∗(𝗉𝗋2(𝑧))and𝑔:𝑃(𝑎)→∑(𝑥:𝐴)𝑃(𝑥)𝑔(𝑦):≡(𝑎,𝑦).1. Homotopy 𝑔∘𝑓∼idLemma 2.3.2 (Path lifting property). Let 𝑃:𝐴→𝒰︀ be a type family over 𝐴 and assume we have 𝑢:𝑃(𝑥) for some 𝑥:𝐴. Then for any 𝑝:𝑥=𝑦, we have 𝗅𝗂𝖿𝗍(𝑢,𝑝):(𝑥,𝑢)=(𝑦,𝑝∗(𝑢)) in ∑(𝑥:𝐴)𝑃(𝑥), such that 𝗉𝗋1(𝗅𝗂𝖿𝗍(𝑢,𝑝))=𝑝.Let 𝑧:∑(𝑥:𝐴)𝑃(𝑥). Apply path lifting to𝑢:≡𝗉𝗋2(𝑧):𝑃(𝗉𝗋1(𝑧)),𝑝:≡𝜋(𝗉𝗋1(𝑧))−1:𝗉𝗋1(𝑧)=𝑎.Then𝗅𝗂𝖿𝗍(𝗉𝗋2(𝑧),𝜋(𝗉𝗋1(𝑧))−1):(𝗉𝗋1(𝑧),𝗉𝗋2(𝑧))=(𝑎,𝜋(𝗉𝗋1(𝑧))−1∗(𝗉𝗋2(𝑧))).Taking inverse and unfolding 𝑓,𝑔 gives𝑔(𝑓(𝑧))≡(𝑎,𝜋(𝗉𝗋1(𝑧))−1∗(𝗉𝗋2(𝑧)))(𝛽-reduction)=(𝗉𝗋1(𝑧),𝗉𝗋2(𝑧))(path lifting)=𝑧.(Corollary 2.7.3.)Hence 𝑔∘𝑓 is homotopic to the identity on ∑(𝑥:𝐴)𝑃(𝑥).2. Homotopy 𝑓∘𝑔∼idLet 𝑦:𝑃(𝑎). We compute𝑓(𝑔(𝑦))≡𝑓((𝑎,𝑦))≡𝜋(𝑎)−1∗(𝑦).Lemma 2.3.5. If 𝑃:𝐴→𝒰︀ is defined by 𝑃(𝑥):≡𝐵 for a fixed 𝐵:𝒰︀, then for any 𝑥,𝑦:𝐴 and 𝑝:𝑥=𝑦 and 𝑏:𝐵 we have a path𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝐵𝑝(𝑏):𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝑃(𝑝,𝑏)=𝑏.Applying Lemma 2.3.5 to𝐵:≡𝑃(𝑎):𝒰︀,𝑝:≡𝜋(𝑎)−1:𝑎=𝑎,𝑏:≡𝑦:𝑃(𝑎).Then𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝑃(𝑎)𝜋(𝑎)−1(𝑦):𝜋(𝑎)−1∗(𝑦)=𝑦.𝑓(𝑔(𝑦))=𝑦 is inhabited, so 𝑓∘𝑔 is homotopic to the identity on 𝑃(𝑎).The two homotopies show that 𝑔 is a quasi-inverse of 𝑓, hence(∑(𝑥:𝐴)𝑃(𝑥))≃𝑃(𝑎).∎
3.21#HoTT 3.21. Prove that isProp(𝑃)≃(𝑃≃‖𝑃‖).Solution by finalchildNote that both isProp(𝑃) and 𝑃≃‖𝑃‖ are mere propositions. The latter is derived from equivalence being a dependent product of a function and its isequiv, both of which being mere propositions:isProp(𝑃→‖𝑃‖)Given𝑓:𝑃→‖𝑃‖, isProp(isequiv𝑓)Thus it suffices to show isProp(𝑃)↔(𝑃≃‖𝑃‖). Both sides being mere propositions automatically proves inverseness.Right direction is Lemma 3.9.1.Left direction: Given 𝑒:𝑃≃‖𝑃‖ and 𝑝1,𝑝2:𝑃, 𝑝1=𝑒−1(𝑒𝑝1)=𝑒−1(𝑒𝑝2)=𝑝2.
3.22#HoTT 3.22. As in classical set theory, the finite version of the axiom of choice is a theorem. Prove that the axiom of choice holds when 𝑋 is a finite type 𝖥𝗂𝗇(𝑛).Solution by kiwiyouFor a type 𝑋, let𝖠𝖢(𝑋):≡(∏𝑥:𝑋‖∑𝑎:𝐴(𝑥)𝑃(𝑥,𝑎)‖)→‖∑(𝑔:∏(𝑥:𝑋)𝐴(𝑥))∏(𝑥:𝑋)𝑃(𝑥,𝑔(𝑥))‖,where 𝐴:𝑋→𝒰︀ and 𝑃:∏𝑥:𝑋(𝐴(𝑥)→𝒰︀).We prove by induction on 𝑛:ℕ that for every𝐴:𝖥𝗂𝗇(𝑛)→𝒰︀and𝑃:∏𝑥:𝖥𝗂𝗇(𝑛)(𝐴(𝑥)→𝒰︀),there is𝖺𝖼𝖿𝗂𝗇𝑛(𝐴,𝑃):𝖠𝖢(𝖥𝗂𝗇(𝑛)).We use the definition𝖥𝗂𝗇(0):≡𝟎,𝖥𝗂𝗇(𝑛+1):≡𝖥𝗂𝗇(𝑛)+𝟏.Base CaseSince 𝖥𝗂𝗇(0):≡𝟎, it suffices to construct an element of 𝖠𝖢(𝟎). Let𝑓:∏𝑥:𝟎‖∑𝑎:𝐴(𝑥)𝑃(𝑥,𝑎)‖.By the induction principle of the empty type, define𝑔0:∏𝑥:𝟎𝐴(𝑥)andℎ0:∏𝑥:𝟎𝑃(𝑥,𝑔0(𝑥)).Therefore(𝑔0,ℎ0):∑(𝑔:∏(𝑥:𝟎)𝐴(𝑥))∏(𝑥:𝟎)𝑃(𝑥,𝑔(𝑥)),and hence𝖺𝖼𝖿𝗂𝗇0(𝐴,𝑃)(𝑓):≡|(𝑔0,ℎ0)|is an element of 𝖠𝖢(𝟎).Induction StepAssume𝖺𝖼𝖿𝗂𝗇𝑛:∏(𝐴:𝖥𝗂𝗇(𝑛)→𝒰︀)∏(𝑃:∏𝑦:𝖥𝗂𝗇(𝑛)(𝐴(𝑦)→𝒰︀))𝖠𝖢(𝖥𝗂𝗇(𝑛)).We must construct 𝖺𝖼𝖿𝗂𝗇𝑛+1.Let𝐴:𝖥𝗂𝗇(𝑛)+𝟏→𝒰︀,𝑃:∏𝑥:𝖥𝗂𝗇(𝑛)+𝟏(𝐴(𝑥)→𝒰︀),and suppose𝑓:∏𝑥:𝖥𝗂𝗇(𝑛)+𝟏‖∑𝑎:𝐴(𝑥)𝑃(𝑥,𝑎)‖.Define restricted families on 𝖥𝗂𝗇(𝑛) by𝐵(𝑦):≡𝐴(𝗂𝗇𝗅(𝑦)),𝑄(𝑦,𝑏):≡𝑃(𝗂𝗇𝗅(𝑦),𝑏).Then𝑓∘𝗂𝗇𝗅:∏𝑦:𝖥𝗂𝗇(𝑛)‖∑𝑏:𝐵(𝑦)𝑄(𝑦,𝑏)‖,so the induction hypothesis yields𝑢:≡𝖺𝖼𝖿𝗂𝗇𝑛(𝐵,𝑄)(𝑓∘𝗂𝗇𝗅):‖∑(𝑔𝑛:∏𝑦:𝖥𝗂𝗇(𝑛)𝐵(𝑦))∏(𝑦:𝖥𝗂𝗇(𝑛))𝑄(𝑦,𝑔𝑛(𝑦))‖.Also,𝑣:≡𝑓(𝗂𝗇𝗋(⋆)):‖∑𝑎:𝐴(𝗂𝗇𝗋(⋆))𝑃(𝗂𝗇𝗋(⋆),𝑎)‖.Let𝑇:≡‖∑(𝑔:∏𝑥:𝖥𝗂𝗇(𝑛)+𝟏𝐴(𝑥))∏(𝑥:𝖥𝗂𝗇(𝑛)+𝟏)𝑃(𝑥,𝑔(𝑥))‖.Since 𝑇 is a propositional truncation, it is a mere proposition. Therefore we may eliminate both 𝑢 and 𝑣 into 𝑇.Assume representatives(𝑔𝑛,ℎ𝑛):∑(𝑔𝑛:∏𝑦:𝖥𝗂𝗇(𝑛)𝐵(𝑦))∏(𝑦:𝖥𝗂𝗇(𝑛))𝑄(𝑦,𝑔𝑛(𝑦))and(𝑎,𝑝):∑𝑎:𝐴(𝗂𝗇𝗋(⋆))𝑃(𝗂𝗇𝗋(⋆),𝑎).Define𝑔:∏(𝑥:𝖥𝗂𝗇(𝑛)+𝟏)𝐴(𝑥)by coproduct recursion:𝑔(𝗂𝗇𝗅(𝑦)):≡𝑔𝑛(𝑦),𝑔(𝗂𝗇𝗋(⋆)):≡𝑎.Similarly defineℎ:∏(𝑥:𝖥𝗂𝗇(𝑛)+𝟏)𝑃(𝑥,𝑔(𝑥))by coproduct recursion:ℎ(𝗂𝗇𝗅(𝑦)):≡ℎ𝑛(𝑦),ℎ(𝗂𝗇𝗋(⋆)):≡𝑝.Then(𝑔,ℎ):∑(𝑔:∏(𝑥:𝖥𝗂𝗇(𝑛)+𝟏)𝐴(𝑥))∏(𝑥:𝖥𝗂𝗇(𝑛)+𝟏)𝑃(𝑥,𝑔(𝑥)),so|(𝑔,ℎ)|:𝑇.Hence, by two applications of the elimination principle for propositional truncation into the mere proposition 𝑇, we obtain𝖺𝖼𝖿𝗂𝗇𝑛+1(𝐴,𝑃)(𝑓):𝑇.Concretely, we first eliminate 𝑢, then eliminate 𝑣, and on representatives (𝑔𝑛,ℎ𝑛) and (𝑎,𝑝) we return |(𝑔,ℎ)|:𝑇.This completes the induction, and therefore 𝖠𝖢(𝖥𝗂𝗇(𝑛)) holds for every 𝑛:ℕ. ∎