napkin solutions > HoTT

Back to Chapter Selection

Table of Contents

  1. 1.2
  2. 1.6
  3. 1.8
  4. 1.10
  5. 1.12
  6. 1.13
  7. 1.15
  8. 2.2
  9. 2.3
  10. 2.6
  11. 2.8
  12. 2.9
  13. 2.14
  14. 2.18
  15. 3.1
  16. 3.2
  17. 3.4
  18. 3.5
  19. 3.7
  20. 3.11
  21. 3.12
  22. 3.14
  23. 3.15
  24. 3.17
  25. 3.18
  26. 3.20
  27. 3.22

1.2 #

HoTT-1.2. Derive the recursion principle for products rec𝐴×𝐵 using only the projections, and verify that the definitional equalities are valid. Do the same for Σ-types.Solution by RanolPThe exercise makes us define the recursor based on the projection of (maybe dependent) product types.1.rec𝐴×𝐵We have projections•pr1:𝐴×𝐵→𝐴•pr2:𝐴×𝐵→𝐵with the following defining equations•pr1((𝑎,𝑏)):≡𝑎•pr2((𝑎,𝑏)):≡𝑏Here, our goal is to definerec𝐴×𝐵:Π𝐶:𝒰︀(𝐴→𝐵→𝐶)→𝐴×𝐵→𝐶and the definition isrec𝐴×𝐵(𝐶,𝑔,(𝑎,𝑏)):≡𝑔(pr1((𝑎,𝑏)))(pr2((𝑎,𝑏)))We can verify that the recursor above has the desired property by doing 𝛽-reduction on pr1 and pr2.After the reduction, we get 𝑔(𝑎)(𝑏), correctly Church-encoding the product.∎2.recΣ𝑥:𝐴𝐵(𝑥)We have projections•pr1:(Σ𝑥:𝐴𝐵(𝑥))→𝐴•pr2:Π𝑝:Σ(𝑥:𝐴)𝐵(𝑥)𝐵(pr1(𝑝))with the following defining equations•pr1((𝑎,𝑏)):≡𝑎•pr2((𝑎,𝑏)):≡𝑏Here, our goal is to definerecΣ𝑥:𝐴𝐵(𝑥):Π(𝐶:𝒰︀)(Π(𝑥:𝐴)𝐵(𝑥)→𝐶)→(Σ(𝑥:𝐴)𝐵(𝑥))→𝐶and its definition isrecΣ𝑥:𝐴𝐵(𝑥)(𝐶,𝑔,(𝑎,𝑏)):≡𝑔(pr1((𝑎,𝑏)))(pr2((𝑎,𝑏)))Let’s verify that the definition concludes with the property we desired once more:By 𝛽-reducing on pr1 and pr2, we get recΣ𝑥:𝐴𝐵(𝑥)(𝐶,𝑔,(𝑎,𝑏)):≡𝑔(𝑎)(𝑏),and it correctly Church-encodes the dependent product.∎As shown above, the recursor can be defined with the projection functions of (maybe dependent) products.

1.6 #

HoTT 1.6. Show that if we define 𝐴×𝐵:≡∏𝑥:𝟐𝗋𝖾𝖼𝟐(𝒰︀,𝐴,𝐵,𝑥), then we can give a definition of 𝗂𝗇𝖽𝐴×𝐵 for which the definitional equalities stated in §1.5 hold propositionally (i.e. using equality types). (This requires the function extensionality axiom, which is introduced in §2.9.)𝗂𝗇𝖽𝐴×𝐵:∏𝐶:𝐴×𝐵→𝒰︀(∏(𝑥:𝐴)∏(𝑦:𝐵)𝐶((𝑥,𝑦)))→∏𝑥:𝐴×𝐵𝐶(𝑥)𝗂𝗇𝖽𝐴×𝐵(𝐶,𝑔,(𝑎,𝑏)):≡𝑔(𝑎)(𝑏)(§1.5)𝖿𝗎𝗇𝖾𝗑𝗍:(∏𝑥:𝐴(𝑓(𝑥)=𝑔(𝑥)))→(𝑓=𝑔)(§2.9)Solution by kiwiyouFrom definition of 𝐴×𝐵:≡∏𝑥:𝟐𝗋𝖾𝖼𝟐(𝒰︀,𝐴,𝐵,𝑥), we can natrally try defining our 𝗂𝗇𝖽𝐴×𝐵:𝗂𝗇𝖽′𝐴×𝐵(𝐶,𝑔,𝑥):≡𝑔(𝑥(0𝟐))(𝑥(1𝟐))Sadly, 𝗂𝗇𝖽′𝐴×𝐵 has a different type from 𝗂𝗇𝖽𝐴×𝐵 in §1.5:𝗂𝗇𝖽′𝐴×𝐵:∏𝐶:𝐴×𝐵→𝒰︀(∏(𝑥:𝐴)∏(𝑦:𝐵)𝐶((𝑥,𝑦)))→∏𝑥:𝐴×𝐵𝐶((𝑥(0𝟐),𝑥(1𝟐)))How can we get value of type ∏𝑥:𝐴×𝐵𝐶(𝑥) from that of type ∏𝑥:𝐴×𝐵𝐶((𝑥(0𝟐),𝑥(1𝟐)))?See this lemma, hidden in §2.3:Lemma 2.3.1 (Transport). Suppose that 𝑃 is a type family over 𝐴 and that 𝑝:𝑥=𝐴𝑦. Then there is a function 𝑝∗:𝑃(𝑥)→𝑃(𝑦).So if we have 𝑝:(𝑥(0𝟐),𝑥(1𝟐))=𝑥, we can transport 𝐶((𝑥(0𝟐),𝑥(1𝟐))) into 𝐶(𝑥). Let’s call this 𝑝 as 𝗎𝗇𝗂𝗊′𝐴×𝐵.𝗎𝗇𝗂𝗊′𝐴×𝐵:∏𝑥:𝐴×𝐵((𝑥(0𝟐),𝑥(1𝟐))=𝑥)Since we don’t have judgemental equality, it’s time for the function extensionality axiom.𝗎𝗇𝗂𝗊′𝐴×𝐵(𝑥):≡𝖿𝗎𝗇𝖾𝗑𝗍(𝗂𝗇𝖽𝟐(𝜆𝑦.((𝑥(0𝟐),𝑥(1𝟐))(𝑦)=𝑥(𝑦)),𝗋𝖾𝖿𝗅𝑥(0𝟐),𝗋𝖾𝖿𝗅𝑥(1𝟐)))Verify the type by case analysis:(𝜆𝑦.((𝑥(0𝟐),𝑥(1𝟐))(𝑦)=𝑥(𝑦))(0𝟐)≡((𝑥(0𝟐),𝑥(1𝟐))(0𝟐)=𝑥(0𝟐))≡((𝗂𝗇𝖽𝟐(𝗋𝖾𝖼𝟐(𝒰︀,𝐴,𝐵),𝑥(0𝟐),𝑥(1𝟐)))(0𝟐)=𝑥(0𝟐))≡(𝑥(0𝟐)=𝑥(0𝟐))⇒𝗋𝖾𝖿𝗅𝑥(0𝟐):(𝜆𝑦.((𝑥(0𝟐),𝑥(1𝟐))(𝑦)=𝑥(𝑦))(0𝟐)(𝜆𝑦.((𝑥(0𝟐),𝑥(1𝟐))(𝑦)=𝑥(𝑦))(1𝟐)≡((𝑥(0𝟐),𝑥(1𝟐))(1𝟐)=𝑥(1𝟐))≡((𝗂𝗇𝖽𝟐(𝗋𝖾𝖼𝟐(𝒰︀,𝐴,𝐵),𝑥(0𝟐),𝑥(1𝟐)))(1𝟐)=𝑥(1𝟐))≡(𝑥(1𝟐)=𝑥(1𝟐))⇒𝗋𝖾𝖿𝗅𝑥(1𝟐):(𝜆𝑦.((𝑥(0𝟐),𝑥(1𝟐))(𝑦)=𝑥(𝑦))(1𝟐)Finally, we have 𝗎𝗇𝗂𝗊′𝐴×𝐵(𝑥)∗:𝐶((𝑥(0𝟐),𝑥(1𝟐)))→𝐶(𝑥) to complete 𝗂𝗇𝖽′𝐴×𝐵. This is a new definition:𝗂𝗇𝖽′𝐴×𝐵:∏𝐶:𝐴×𝐵→𝒰︀(∏(𝑥:𝐴)∏(𝑦:𝐵)𝐶((𝑥,𝑦)))→∏𝑥:𝐴×𝐵𝐶(𝑥)𝗂𝗇𝖽′𝐴×𝐵(𝐶,𝑔,𝑥):≡𝗎𝗇𝗂𝗊′𝐴×𝐵(𝑥)∗(𝑔(𝑥(0𝟐))(𝑥(1𝟐)))Remaining question: 𝗂𝗇𝖽′𝐴×𝐵=𝗂𝗇𝖽𝐴×𝐵 holds?

1.8 #

HoTT-1.8. Define multiplication and exponentiation using recℕ. Verify that (ℕ,+,0,×,1) is a semiring using only indℕ. You will probably also need to use symmetry and transitivity of equality, Lemmas 2.1.1 and 2.1.2.Solution by finalchildDefinition of multiplication and exponentiationDefine multiplication and exponentiation as follows. This is just like how we defined add. Note that exponen­tiate has an extra step that reverses the order of parameters.multiply:≡recℕ(ℕ→ℕ,𝜆𝑛.0,𝜆𝑚.𝜆𝑔.𝜆𝑛.𝑛+𝑔(𝑛))exponentiate:≡𝜆𝑚.𝜆𝑛.recℕ(ℕ→ℕ,𝜆𝑚.1,𝜆𝑛.𝜆𝑔.𝜆𝑚.𝑚×𝑔(𝑚))(𝑛,𝑚)(ℕ,+,0,×,1) is a semiringNow we verify that (ℕ,+,0,×,1) is a semiring. Note that summon(𝑇) is a notation for summoning a known proof that becomes type 𝑇 with appropriate arguments.(ℕ,+,0) is a commutative monoidProve 𝑖+𝑗+𝑘=𝑖+(𝑗+𝑘) with induction.assoc+:∏𝑖,𝑗,𝑘:ℕ𝑖+𝑗+𝑘=𝑖+(𝑗+𝑘)assoc+:≡indℕ(𝜆(𝑖:ℕ).∏𝑗,𝑘:ℕ𝑖+𝑗+𝑘=𝑖+(𝑗+𝑘),assoc+,0,assoc+,s)assoc+,0:∏𝑗,𝑘:ℕ0+𝑗+𝑘=0+(𝑗+𝑘)assoc+,0(𝑗,𝑘):≡refl𝑗+𝑘assoc+,s:∏𝑖:ℕ(∏𝑗,𝑘:ℕ𝑖+𝑗+𝑘=𝑖+(𝑗+𝑘))→succ(𝑖)+𝑗+𝑘=succ(𝑖)+(𝑗+𝑘)assoc+,s(ℎ,𝑖,𝑗,𝑘):≡apsucc(ℎ(𝑗,𝑘))Prove that 0 is the identity of (ℕ,+).𝜆𝑖.refl𝑖:∏𝑖:ℕ0+𝑖=𝑖indℕ(𝜆(𝑖:ℕ). 𝑖+0=𝑖,refl0,𝜆𝑖.𝜆ℎ.apsucc(ℎ)):∏𝑖:ℕ𝑖+0=𝑖Prove 𝑖+𝑗=𝑗+𝑖 with double induction.commut+:∏𝑖,𝑗:ℕ𝑖+𝑗=𝑗+𝑖commut+:indℕ(𝜆(𝑖:ℕ).∏𝑗:ℕ𝑖+𝑗=𝑗+𝑖,commut+,0,commut+,s)commut+,0:∏𝑗:ℕ0+𝑗=𝑗+0commut+,0(𝑗):≡summon(𝑗+0=𝑗))−1commut+,s:∏𝑖:ℕ(∏𝑗:ℕ𝑖+𝑗=𝑗+𝑖)→∏𝑗:ℕsucc(𝑖)+𝑗=𝑗+succ(𝑖)commut+,s(𝑖,ℎ1):≡indℕ(𝜆(𝑗:ℕ).succ(𝑖)+𝑗=𝑗+succ(𝑖),summon(succ(𝑖)+0=succ(𝑖)),commut_inner(𝑖,ℎ1))commut_inner:∏𝑖:ℕ(∏𝑗:ℕ𝑖+𝑗=𝑗+𝑖)→∏𝑗:ℕ(succ(𝑖)+𝑗=𝑗+succ(𝑖))→succ(𝑖)+succ(𝑗)=succ(𝑗)+succ(𝑖)Prove commut_inner(𝑖,ℎ1,𝑗,ℎ2) with the composition of three equalities:succ(𝑖+succ(𝑗))=succ2(𝑗+𝑖)(byℎ1)=succ2(𝑖+𝑗)(byℎ1)=succ(𝑗+succ(𝑖))(byℎ2)commut_inner(𝑖,ℎ1,𝑗,ℎ2):≡apsucc(ℎ1(succ(𝑗)))⋅apsucc2(ℎ1(𝑗))−1⋅apsucc(ℎ2)Axioms on ×Prove that 1 is the identity of (ℕ,×).𝜆𝑖.summon(𝑖+0=𝑖):∏𝑖:ℕ1×𝑖=𝑖indℕ(𝜆(𝑖:ℕ). 𝑖×1=𝑖,refl0,𝜆𝑖.𝜆ℎ.apsucc(ℎ)):∏𝑖:ℕ𝑖×1=𝑖Prove 0 annihilates multiplication.𝜆𝑖.refl0:∏𝑖:ℕ0×𝑖=0indℕ(𝜆(𝑖:ℕ). 𝑖×0=0,refl0,𝜆𝑖.𝜆ℎ.ℎ):∏𝑖:ℕ𝑖×0=0Prove distribution.distrbl:∏𝑖,𝑗,𝑘:ℕ𝑖×(𝑗+𝑘)=𝑖×𝑗+𝑖×𝑘distrbl:≡indℕ(𝜆(𝑖:ℕ).∏𝑗,𝑘:ℕ𝑖×(𝑗+𝑘)=𝑖×𝑗+𝑖×𝑘,distrbl0,distrbls)distrbl0:∏𝑗,𝑘:ℕ0×(𝑗+𝑘)=0×𝑗+0×𝑘distrbl0(𝑗,𝑘):≡refl0distrbls:∏𝑖:ℕ(∏𝑗,𝑘:ℕ𝑖×(𝑗+𝑘)=𝑖×𝑗+𝑖×𝑘)→∏𝑗,𝑘:ℕsucc(𝑖)×(𝑗+𝑘)=succ(𝑖)×𝑗+succ(𝑖)×𝑘Prove distrbl𝑠(𝑖,ℎ,𝑗,𝑘) by the composition of equalities:𝑗+𝑘+𝑖×(𝑗+𝑘)=𝑗+𝑘+(𝑖×𝑗+𝑖×𝑘)(byℎ)=𝑗+(𝑘+𝑖×𝑗+𝑖×𝑘)(byassoc+)=𝑗+(𝑖×𝑗+𝑘+𝑖×𝑘)(bycommut+)=𝑗+(𝑖×𝑗+(𝑘+𝑖×𝑘))(byassoc+)=𝑗+𝑖×𝑗+(𝑘+𝑖×𝑘)(byassoc+)I omit the explicit term for this composition. The components are just ℎ, commut+ and assoc+ wrapped with ap.distribr:∏𝑖,𝑗,𝑘:ℕ(𝑖+𝑗)×𝑘=𝑖×𝑘+𝑗×𝑘distribr:≡indℕ(𝜆(𝑖:ℕ).∏𝑗,𝑘:ℕ(𝑖+𝑗)×𝑘=𝑖×𝑘+𝑗×𝑘,distribr0,distribrs)distribr0:∏𝑗,𝑘:ℕ(0+𝑗)×𝑘=0×𝑘+𝑗×𝑘distribr0(𝑗,𝑘):≡refl𝑗×𝑘distribrs:∏𝑖:ℕ(∏𝑗,𝑘:ℕ(𝑖+𝑗)×𝑘=𝑖×𝑘+𝑗×𝑘)→∏𝑗,𝑘:ℕ(succ(𝑖)+𝑗)×𝑘=succ(𝑖)×𝑘+𝑗×𝑘Prove distribr𝑠(𝑖,ℎ,𝑗,𝑘) by the composition of equalities:𝑘+(𝑖+𝑗)×𝑘=𝑘+(𝑖×𝑘+𝑗×𝑘)(byℎ)=𝑘+𝑖×𝑘+𝑗×𝑘(byassoc+)Prove 𝑖×𝑗×𝑘=𝑖×(𝑗×𝑘) with induction.assoc×:∏𝑖,𝑗,𝑘:ℕ𝑖×𝑗×𝑘=𝑖×(𝑗×𝑘)assoc×:≡indℕ(𝜆(𝑖:ℕ).∏𝑗,𝑘:ℕ𝑖×𝑗×𝑘=𝑖×(𝑗×𝑘),assoc×,0,assoc×,s)assoc×,0:∏𝑗,𝑘:ℕ0×𝑗×𝑘=0×(𝑗×𝑘)assoc×,0(𝑗,𝑘):≡refl0assoc×,s:∏𝑖:ℕ(∏𝑗,𝑘:ℕ𝑖×𝑗×𝑘=𝑖×(𝑗×𝑘))→succ(𝑖)×𝑗×𝑘=succ(𝑖)×(𝑗×𝑘)Prove assoc×,s(𝑖,ℎ) by the composition of equalities:(𝑗+𝑖×𝑗)×𝑘=𝑗×𝑘+𝑖×𝑗×𝑘(bydistribr)=𝑗×𝑘+𝑖×(𝑗×𝑘)(byℎ)Therefore, (ℕ,+,0,×,1) is a semiring.

1.10 #

HoTT-1.10. Show that the Ackermann function ack:ℕ→ℕ→ℕ is definable using only recℕ satisfying the following equations:ack(0,𝑛)≡succ(𝑛)ack(succ(𝑚),0)≡ack(𝑚,1)ack(succ(𝑚),succ(𝑛))≡ack(𝑚,ack(succ(𝑚),𝑛))Solution by finalchildack:≡recℕ(ℕ→ℕ,succ,𝜆(𝑚:ℕ). 𝜆(𝑓:ℕ→ℕ). recℕ(ℕ,𝑓(1),𝜆(𝑛:ℕ). 𝜆(𝑐:ℕ). 𝑓(𝑐)))Verify the equations:ack(0)≡succack(succ(𝑚))≡recℕ(ℕ,ack(𝑚,1),𝜆(𝑛:ℕ). 𝜆(𝑐:ℕ). ack(𝑚,𝑐))Thusack(0,𝑛)≡succ(𝑛)ack(succ(𝑚),0)≡ack(𝑚,1)ack(succ(𝑚),succ(𝑛))≡(𝜆(𝑛:ℕ). 𝜆(𝑐:ℕ). ack(𝑚,𝑐))(𝑛,ack(succ(𝑚),𝑛))≡ack(𝑚,ack(succ(𝑚),𝑛))Note that we folded some instances of recursive calls implicitly.

1.12 #

HoTT-1.12. Using the propositions as types interpretation, derive the following tautologies.(i) If 𝐴, then (if 𝐵 then 𝐴).(ii) If 𝐴, then not (not 𝐴).(iii) If (not 𝐴 or not 𝐵), then not (𝐴 and 𝐵).Solution by Jineon Baek (백진언) (xtalclr)𝖨:𝐴→(𝐵→𝐴)𝖨:≡𝜆(𝑎:𝐴).(𝜆(𝑏:𝐵).𝑎)In words: Assume evidence 𝑎 of 𝐴. Then assuming the evidence 𝑏 of 𝐵, the statement 𝐴 is true because 𝑎 is an evidence of 𝐴.𝖨𝖨:𝐴→((𝐴→𝟎)→𝟎)𝖨𝖨:≡𝜆(𝑎:𝐴).(𝜆(𝑛:(𝐴→𝟎)).𝑛(𝑎))In words: Assume evidence 𝑎 of 𝐴. Assuming the evidence 𝑛 of not 𝐴, we get contradiction by evidence 𝑎 of 𝐴 and 𝑛 of not 𝐴. So it is impossible that not 𝐴.𝖨𝖨𝖨:((𝐴→𝟎)+(𝐵→𝟎))→(𝐴×𝐵)→𝟎𝖨𝖨𝖨:≡𝜆𝑥.𝗋𝖾𝖼(𝐴→𝟎)+(𝐵→𝟎)((𝐴×𝐵)→𝟎,𝖼𝖺𝗌𝖾𝑎,𝖼𝖺𝗌𝖾𝑏,𝑥) where𝖼𝖺𝗌𝖾𝑎:(𝐴→𝟎)→(𝐴×𝐵)→𝟎𝖼𝖺𝗌𝖾𝑎:≡𝜆(𝑐:𝐴→𝟎).𝜆(𝑝:𝐴×𝐵).𝑐(𝗉𝗋1(𝑝))𝖼𝖺𝗌𝖾𝑏:(𝐵→𝟎)→(𝐴×𝐵)→𝟎𝖼𝖺𝗌𝖾𝑏:≡𝜆(𝑐:𝐵→𝟎).𝜆(𝑝:𝐴×𝐵).𝑐(𝗉𝗋2(𝑝))In words: Assume we are given either a evidence of not 𝐴 or a evidence of not 𝐵.•First assume the evidence 𝑐 of not 𝐴. Then that both 𝐴 and 𝐵 are true is impossible: since the evidence 𝑝 of both 𝐴 and 𝐵 gives the evidence 𝗉𝗋1(𝑝) of 𝐴, we get contradiction by evidence 𝗉𝗋1(𝑝) of 𝐴 and 𝑐 of not 𝐴.•Now assume the evidence 𝑐 of not 𝐵. Then that both 𝐴 and 𝐵 are true is impossible: since the evidence 𝑝 of both 𝐴 and 𝐵 gives the evidence 𝗉𝗋2(𝑝) of 𝐵, we get contradiction by evidence 𝗉𝗋2(𝑝) of 𝐵 and 𝑐 of not 𝐵.So in either case, that both 𝐴 and 𝐵 are true is impossible. So it is not that both 𝐴 and 𝐵 holds.Solution by Jihyeon Kim (김지현) (simnalamburt)𝖨𝖨𝖨2:((𝐴→𝟎)+(𝐵→𝟎))→(𝐴×𝐵)→𝟎𝖨𝖨𝖨2(𝗂𝗇𝗅(𝗇𝖺)):≡𝜆𝑝.𝗇𝖺(𝗉𝗋1(𝑝))𝖨𝖨𝖨2(𝗂𝗇𝗋(𝗇𝖻)):≡𝜆𝑝.𝗇𝖻(𝗉𝗋2(𝑝))In words: Assume we are given evidence 𝑥:(¬𝐴+¬𝐵) that either ¬𝐴 holds or ¬𝐵 holds.To show ¬(𝐴×𝐵), let 𝑝:𝐴×𝐵 be evidence that both 𝐴 and 𝐵 hold. We proceed by cases on 𝑥.•If 𝑥 is 𝗂𝗇𝗅(𝗇𝖺) with 𝗇𝖺:¬𝐴, then from 𝑝:𝐴×𝐵 we get 𝗉𝗋1(𝑝):𝐴. Applying 𝗇𝖺 to 𝗉𝗋1(𝑝) yields 0.•If 𝑥 is 𝗂𝗇𝗋(𝗇𝖻) with 𝗇𝖻:¬𝐵, then from 𝑝:𝐴×𝐵 we get 𝗉𝗋2(𝑝):𝐵. Applying 𝗇𝖻 to 𝗉𝗋2(𝑝) yields 0.In either case, assuming 𝐴×𝐵 leads to a 0. Therefore, from (¬𝐴+¬𝐵) we conclude ¬(𝐴×𝐵).

1.13 #

HoTT 1.13. Using propositions-as-types, derive the double negation of the principle of excluded middle, i.e. prove not (not (P or not P)).Solution by kiwiyouWe need to find a witness of the type not (not (P or not P)).¬¬𝖫𝖤𝖬:∏𝑃:𝒰︀((𝑃+(𝑃→𝟎))→𝟎)→𝟎¬¬𝖫𝖤𝖬:≡𝜆𝑃. (□:((𝑃+(𝑃→𝟎))→𝟎)→𝟎)Our first hole must get a function of type (𝑃+(𝑃→𝟎))→𝟎 and derive a contradiction.¬¬𝖫𝖤𝖬:≡𝜆𝑃. 𝜆𝑓. (□:𝟎)We must use 𝑓 to derive a contradiction as we cannot prove a contradiction directly. Note that 𝑓 derives a contradiction from a witness of either 𝑃 or 𝑃→𝟎. 𝑃 is not inhabited yet, so we can try constructing a function of type 𝑃→𝟎.¬¬𝖫𝖤𝖬:≡𝜆𝑃. 𝜆𝑓. 𝑓(𝗂𝗇𝗋(□:𝑃→𝟎))Our hole now must receive a witness of 𝑃 and derive a contradiction. This time 𝑓 can receive a witness of 𝑃.¬¬𝖫𝖤𝖬:≡𝜆𝑃. 𝜆𝑓. 𝑓(𝗂𝗇𝗋(𝜆𝑝. 𝑓(𝗂𝗇𝗅(𝑝))))∎

1.15 #

HoTT-1.15. Show that the indiscernibility of identicals follows from path induction.Path induction:ind=𝐴:∏𝐶:Π(𝑥,𝑦:𝐴)(𝑥=𝐴𝑦)→𝒰︀(Π(𝑥:𝐴)𝐶(𝑥,𝑥,refl𝑥))→∏(𝑥,𝑦:𝐴)∏(𝑝:𝑥=𝐴𝑦)𝐶(𝑥,𝑦,𝑝)with equalityind=𝐴(𝐶,𝑐,𝑥,𝑥,refl𝑥):≡𝑐(𝑥)Indiscernibility of identicals: for every family𝐶:𝐴→𝒰︀there is a function𝑓:∏(𝑥,𝑦:𝐴)∏(𝑝:𝑥=𝐴𝑦)𝐶(𝑥)→𝐶(𝑦)such that𝑓(𝑥,𝑥,refl𝑥):≡id𝐶(𝑥)Solution by RanolPHole Notation (□:𝜏). To show the reasoning step, we’ll present a hole notation, which displays the current goal(s) typed 𝜏. The hole may be untyped if it’s too obvious or annoying to write explicitly. On the reasoning step, we’ll replace hole(s) and may introduce new hole(s).The goal is to construct such 𝑓. Let’s solve step-by-step.Given type family 𝐶:𝐴→𝒰︀,𝑓:≡□:∏(𝑥,𝑦:𝐴)∏(𝑝:𝑥=𝐴𝑦)𝐶(𝑥)→𝐶(𝑦)≡ind=𝐴(□)(□):∏(𝑥,𝑦:𝐴)∏(𝑝:𝑥=𝐴𝑦)𝐶(𝑥)→𝐶(𝑦)≡ind=𝐴(𝜆𝑥.𝜆𝑦.𝜆𝑝.𝐶(𝑥)→𝐶(𝑦))(□:Π(𝑥:𝐴)𝐶(𝑥)→𝐶(𝑥))≡ind=𝐴(𝜆𝑥.𝜆𝑦.𝜆𝑝.𝐶(𝑥)→𝐶(𝑦))(𝜆𝑥.(□:𝐶(𝑥)→𝐶(𝑥)))≡ind=𝐴(𝜆𝑥.𝜆𝑦.𝜆𝑝.𝐶(𝑥)→𝐶(𝑦))(𝜆𝑥.id𝐶(𝑥))Let’s verify 𝑓(𝑥,𝑥,refl𝑥)≡id𝐶(𝑥).𝑓(𝑥,𝑥,refl𝑥)≡ind=𝐴(𝜆𝑥.𝜆𝑦.𝜆𝑝.𝐶(𝑥)→𝐶(𝑦))(𝜆𝑥.id𝐶(𝑥))(𝑥,𝑥,refl𝑥)≡(𝜆𝑥.id𝐶(𝑥))(𝑥)≡id𝐶(𝑥)So, the indicernibility of identicals can be derived from the path induction.∎

2.2 #

HoTT-2.2. Show that the three equalities of proofs constructed in the previous exercise form a commutative triangle. In other words, if the three definitions of concatenation are denoted by (𝑝 ▪1 𝑞), (𝑝 ▪2 𝑞), and (𝑝 ▪3 𝑞), then the concatenated equality(𝑝 ▪1 𝑞)=(𝑝 ▪2 𝑞)=(𝑝 ▪3 𝑞)is equal to the equality (𝑝 ▪1 𝑞)=(𝑝 ▪3 𝑞).Solution by finalchild𝑒12 𝑥 𝑦 𝑝 𝑧 𝑞:(𝑝 ▪1 𝑞)=(𝑝 ▪2 𝑞)𝑒23 𝑥 𝑦 𝑝 𝑧 𝑞:(𝑝 ▪2 𝑞)=(𝑝 ▪3 𝑞)𝑒13 𝑥 𝑦 𝑝 𝑧 𝑞:(𝑝 ▪1 𝑞)=(𝑝 ▪3 𝑞)Goal: for all 𝑥, 𝑦, 𝑝, 𝑧, 𝑞,(𝑒12 𝑥 𝑦 𝑝 𝑧 𝑞) ▪ (𝑒23 𝑥 𝑦 𝑝 𝑧 𝑞)=𝑒13 𝑥 𝑦 𝑝 𝑧 𝑞By induction on 𝑝 and 𝑞, the goal becomes(𝑒12 𝑥 𝑥 refl𝑥 𝑥 refl𝑥) ▪ (𝑒23 𝑥 𝑥 refl𝑥 𝑥 refl𝑥)=𝑒13 𝑥 𝑥 refl𝑥 𝑥 refl𝑥which isreflrefl𝑥 ▪ reflrefl𝑥=reflrefl𝑥which is true, judgementally.

2.3 #

HoTT-2.3. Give a fourth, different, proof of Lemma 2.1.2, and prove that it is equal to the others.Lemma 2.1.2. For every type 𝐴 and every 𝑥,𝑦,𝑧:𝐴, there is a function(𝑥=𝑦)→(𝑦=𝑧)→(𝑥=𝑧)Solution by Jihyeon Kim (김지현) (simnalamburt)𝑥,𝑦,𝑧:𝐴 이고 𝑝:𝑥=𝑦, 𝑞:𝑦=𝑧 라 하자. Type family 𝑃:𝐴→𝒰︀ 를 𝑃(𝑤)≡(𝑥=𝑤) 로 정의하면, 𝑝:𝑃(𝑦) 가 된다. 이제 transport를 이용한 네 번째 경로 연결(concatenation)을 다음과 같이 정의하자.𝑝⋅4𝑞:𝑥=𝑧𝑝⋅4𝑞:≡transport𝑃(𝑞,𝑝)이제 이 정의가 기존의 경로 연결 𝑝⋅𝑞 와 같음을 보여야 한다. 즉, 다음을 증명해야 한다.𝑝⋅4𝑞=𝑝⋅𝑞𝑞 에 대한 경로 귀납(path induction)을 사용하자. 𝑧 를 𝑦 로, 𝑞 를 refl𝑦 로 가정하면 충분하다.1.좌변: transport의 정의에 의해, 경로가 refl 일 때 transport 함수는 항등 함수(identity function)와 정의상 같다(definitionally equal).𝑝⋅4refl𝑦≡transport𝑃(refl𝑦,𝑝)≡𝑝2.우변: 기존 경로 연결의 우측 단위 법칙(right unit law)에 의해 다음이 성립한다.𝑝⋅refl𝑦=𝑝따라서 𝑞≡refl𝑦 일 때 𝑝=𝑝 가 되어 등식이 성립하므로, path induction에 의해 모든 𝑞 에 대해 𝑝⋅4𝑞=𝑝⋅𝑞 이다.

2.6 #

HoTT-2.6. Prove that if 𝑝:𝑥=𝑦, then the function (𝑝 ▪ –):(𝑦=𝑧)→(𝑥=𝑧) is an equivalence.Solution by finalchildWe have a quasi-inverse given by (𝑟:𝑥=𝑧)↦𝑝−1 ▪ 𝑟.We prove the properties needed:((𝑟:𝑥=𝑧)↦𝑝−1 ▪ 𝑟)∘((𝑞:𝑦=𝑧)↦𝑝 ▪ 𝑞)≡((𝑞:𝑦=𝑧)↦𝑝−1 ▪ (𝑝 ▪ 𝑞))∼id𝑦=𝑧((𝑞:𝑦=𝑧)↦𝑝 ▪ 𝑞)∘((𝑟:𝑥=𝑧)↦𝑝−1 ▪ 𝑟)≡((𝑟:𝑥=𝑧)↦𝑝 ▪ (𝑝−1 ▪ 𝑟))∼id𝑥=𝑧

2.8 #

HoTT-2.8. State and prove an analogue of Theorem 2.6.5 for coproductsQuotation of §2.6pair=:(pr1(𝑥)=pr1(𝑦))×(pr2(𝑥)=pr2(𝑦))→(𝑥=𝑦)⋯Finally, we consider the functoriality of ap under cartesian products. Suppose given types 𝐴,𝐵,𝐴′,𝐵′ and functions 𝑔:𝐴→𝐴′ and ℎ:𝐵→𝐵′; then we can define a function 𝑓:𝐴×𝐵→𝐴′×𝐵′ by 𝑓(𝑥):≡(𝑔(pr1𝑥),ℎ(pr2𝑥)).Theorem 2.6.5. In the above situation, given 𝑥,𝑦:𝐴×𝐵 and 𝑝:pr1𝑥=pr1𝑦 and 𝑞:pr2𝑥=pr2𝑦, we have𝑓(pair=(𝑝,𝑞))=𝑓(𝑥)=𝑓(𝑦)pair=(𝑔(𝑝),ℎ(𝑞)))Solution by RanolPThe core property of the theorem above is followings are same:•apply(𝐴→𝐴′and𝐵→𝐵′) then compose(𝐴′and𝐵′→𝐴′×𝐵′)•compose(𝐴and𝐵→𝐴×𝐵) then apply(𝐴×𝐵→𝐴′×𝐵′).Thus, the analogue for coproducts is followings are same:•apply(𝐴→𝐴′or𝐵→𝐵′) then compose(𝐴′or𝐵′→𝐴′+𝐵′)•compose(𝐴or𝐵→𝐴+𝐵) then apply(𝐴+𝐵→𝐴′+𝐵′).Suppose given types 𝐴,𝐵,𝐴′,𝐵′ and functions 𝑔:𝐴→𝐴′ and ℎ:𝐵→𝐵′ then we can define a function 𝑓:𝐴+𝐵→𝐴′+𝐵′ by case analysis:𝑓(inl(𝑎)):≡inl(𝑔(𝑎))𝑓(inr(𝑏)):≡inr(ℎ(𝑏))In above situation1.Given 𝑎,𝑎′:𝐴 and 𝑝:𝑎=𝑎′, we haveap𝑓(apinl(𝑝))=apinl(ap𝑔(𝑝))Proof. by path induction on 𝑝,ap𝑓(apinl(refl𝑎))=apinl(ap𝑔(refl𝑎))ap𝑓(reflinl(𝑎))=apinl(refl𝑔(𝑎))reflinl(𝑔(𝑎))=reflinl(𝑔(𝑎))2.Given 𝑏,𝑏′:𝐵 and 𝑝:𝑏=𝑏′, we haveap𝑓(apinr(𝑝))=apinr(apℎ(𝑝))Proof. by path induction on 𝑝,ap𝑓(apinr(refl𝑏))=apinr(apℎ(refl𝑏))ap𝑓(reflinr(𝑏))=apinr(reflℎ(𝑏))reflinr(ℎ(𝑏))=reflinr(ℎ(𝑏))

2.9 #

HoTT-2.9. Prove that coproducts have the expected universal property,(𝐴+𝐵→𝑋)≃(𝐴→𝑋)×(𝐵→𝑋).Can you generalize this to an equivalence involving dependent functions?Solution by Jihyeon Kim (김지현) (simnalamburt)먼저 비의존 함수(non-dependent function) 버전을 증명하자.두 함수 split (forward, →)와 join (backward, ←)을 다음과 같이 정의한다.split:(𝐴+𝐵→𝑋)→(𝐴→𝑋)×(𝐵→𝑋)split(ℎ):≡(ℎ∘inl,ℎ∘inr)join:(𝐴→𝑋)×(𝐵→𝑋)→(𝐴+𝐵→𝑋)join((𝑔,ℎ)):≡rec𝐴+𝐵(𝑋,𝑔,ℎ)이제 두 함수가 서로 역함수(inverse)임을 보이자.1.split∘join∼id: 임의의 𝑥 에 대하여, by induction on 𝑥, (𝑔,ℎ)≡𝑥split(join((𝑔,ℎ)))≡(join((𝑔,ℎ))∘inl,join((𝑔,ℎ))∘inr)≡(𝜆𝑎.𝑔(𝑎),𝜆𝑏.ℎ(𝑏))≡(𝑔,ℎ)(by η-conversion)So, split(join((𝑔,ℎ)))=(𝑔,ℎ).2.join∘split∼id: 임의의 𝑓:𝐴+𝐵→𝑋 에 대하여, 모든 𝑥:𝐴+𝐵 에서 join(split(𝑓))(𝑥)=𝑓(𝑥) 임을 𝑥 에 대한 귀납법으로 보인다.•𝑥≡inl(𝑎) 일 때: join(split(𝑓))(inl(𝑎))≡(𝑓∘inl)(𝑎)≡𝑓(inl(𝑎))•𝑥≡inr(𝑏) 일 때: join(split(𝑓))(inr(𝑏))≡(𝑓∘inr)(𝑏)≡𝑓(inr(𝑏))점별로(pointwise) 같으므로, 함수 외연성(function extensionality)에 의해 join(split(𝑓))=𝑓 이다.다음으로, 이를 의존 함수(dependent function) 버전으로 일반화하자.임의의 Type family 𝑃:𝐴+𝐵→𝒰︀ 에 대하여 다음이 성립한다.(Π𝑥:𝐴+𝐵𝑃(𝑥))≃(Π𝑎:𝐴𝑃(inl(𝑎)))×(Π𝑏:𝐵𝑃(inr(𝑏)))증명 구조는 위와 완전히 동일하다.splitΠ(ℎ):≡(𝜆𝑎.ℎ(inl(𝑎)),𝜆𝑏.ℎ(inr(𝑏)))joinΠ(𝑔,ℎ):≡ind𝐴+𝐵(𝜆𝑥.𝑋,𝑔,ℎ)1.splitΠ(joinΠ(𝑔,ℎ)) 는 정의에 따라 (𝑔,ℎ) 로 계산된다(definitionally equal).2.joinΠ(splitΠ(𝑓)) 는 𝑥 가 inl(𝑎) 일 때와 inr(𝑏) 일 때 모두 𝑓(𝑥) 와 같으므로, 함수 외연성에 의해 𝑓 와 같다.

2.14 #

HoTT 2.14. Suppose we add to type theory the equality reflection rule which says that if there is an element 𝑝:𝑥=𝑦, then in fact 𝑥≡𝑦. Prove that for any 𝑝:𝑥=𝑥, we have 𝑝≡𝗋𝖾𝖿𝗅𝑥. (This implies that every type is a set in the sense to be introduced in §3.1; see §7.2.)Solution by kiwiyouWe can have this strange claim under equality reflection rule:𝗌𝗍𝗋𝖺𝗇𝗀𝖾:∏𝑥,𝑦:𝐴∏𝑞:𝑥=𝑦𝑞=𝑥=𝑦𝗋𝖾𝖿𝗅𝑥Then we can prove this with path induction. We can inhabit 𝗌𝗍𝗋𝖺𝗇𝗀𝖾:𝗌𝗍𝗋𝖺𝗇𝗀𝖾(𝑥,𝑥,𝗋𝖾𝖿𝗅𝑥)≡𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅𝑥𝗌𝗍𝗋𝖺𝗇𝗀𝖾:≡𝗂𝗇𝖽=𝐴(𝜆𝑥,𝑦:𝐴. 𝜆𝑞:𝑥=𝑦. 𝑞=𝑥=𝑦𝗋𝖾𝖿𝗅𝑥,𝜆𝑥:𝐴. 𝗋𝖾𝖿𝗅𝗋𝖾𝖿𝗅𝑥)So finally, given 𝑝:𝑥=𝑥, we have 𝗌𝗍𝗋𝖺𝗇𝗀𝖾(𝑥,𝑥,𝑝):𝑝=𝗋𝖾𝖿𝗅𝑥, which is also, by equality reflection rule:𝑝≡𝗋𝖾𝖿𝗅𝑥∎

2.18 #

HoTT-2.18. State and prove a version of Lemma 2.4.3 for dependent functions.Lemma 2.4.3. Suppose 𝐻:𝑓∼𝑔 is a homotopy between functions 𝑓,𝑔:𝐴→𝐵 and let 𝑝:𝑥=𝐴𝑦. Then we have𝐻(𝑥)▪𝑔(𝑝)=𝑓(𝑝)▪𝐻(𝑦)Solution by Jihyeon Kim (김지현) (simnalamburt)일단 Lemma 2.4.3의 의존버전을 정의해보자.비 의존버전 Lemma 2.4.3에 등장하는 항들의 타입을 모두 나열하면 아래와 같다.𝐴,𝐵:𝒰︀𝑓,𝑔:𝐴→𝐵𝑥,𝑦:𝐴𝑝:𝑥=𝐴𝑦𝐻:𝑓∼𝑔ap𝑓:(𝑥=𝐴𝑦)→𝑓(𝑥)=𝐵𝑓(𝑦)𝑓(𝑝)≡ap𝑓(𝑝):𝑓(𝑥)=𝐵𝑓(𝑦)ap𝑔:(𝑥=𝐴𝑦)→𝑔(𝑥)=𝐵𝑔(𝑦)𝑔(𝑝)≡ap𝑔(𝑝):𝑔(𝑥)=𝐵𝑔(𝑦)𝐻(𝑥):𝑓(𝑥)=𝐵𝑔(𝑥)𝐻(𝑦):𝑓(𝑦)=𝐵𝑔(𝑦)𝐻(𝑥)▪ap𝑔(𝑝):𝑓(𝑥)=𝐵𝑔(𝑦)ap𝑓(𝑝)▪𝐻(𝑦):𝑓(𝑥)=𝐵𝑔(𝑦)위를 모두 의존버전으로 옮기면 아래와 같다.𝐴:𝒰︀𝑃:𝐴→𝒰︀𝑓,𝑔:∏𝑥:𝐴𝑃(𝑥)𝑥,𝑦:𝐴𝑝:𝑥=𝐴𝑦𝐻:∏𝑥:𝐴(𝑓(𝑥)=𝑃(𝑥)𝑔(𝑥))𝑝∗≡transport𝑃(𝑝,−):𝑃(𝑥)→𝑃(𝑦)apd𝑓:∏𝑥,𝑦:𝐴∏𝑝:𝑥=𝐴𝑦(𝑝∗(𝑓(𝑥))=𝑃(𝑦)𝑓(𝑦))apd𝑓(𝑝):𝑝∗(𝑓(𝑥))=𝑃(𝑦)𝑓(𝑦)apd𝑔:∏𝑥,𝑦:𝐴∏𝑝:𝑥=𝐴𝑦(𝑝∗(𝑔(𝑥))=𝑃(𝑦)𝑔(𝑦))apd𝑔(𝑝):𝑝∗(𝑔(𝑥))=𝑃(𝑦)𝑔(𝑦)𝐻(𝑥):𝑓(𝑥)=𝑃(𝑥)𝑔(𝑥)𝐻(𝑦):𝑓(𝑦)=𝑃(𝑦)𝑔(𝑦)𝑝∗(𝐻(𝑥))≡aptransport𝑃(𝑝,−)(𝐻(𝑥)):𝑝∗(𝑓(𝑥))=𝑃(𝑦)𝑝∗(𝑔(𝑥))𝑝∗(𝐻(𝑥))▪apd𝑔(𝑝):𝑝∗(𝑓(𝑥))=𝑃(𝑦)𝑔(𝑦)apd𝑓(𝑝)▪𝐻(𝑦):𝑝∗(𝑓(𝑥))=𝑃(𝑦)𝑔(𝑦)약간 설명을 하자면, 비의존 버전의 Lemma 2.4.3에서 ap𝑓(𝑝),ap𝑔(𝑝) 가 하던 역할은 의존 버전에서는 apd𝑓(𝑝),apd𝑔(𝑝) 가 한다. 이때, 𝐻(𝑥):𝑓(𝑥)=𝑃(𝑥)𝑔(𝑥) 는 fiber 𝑃(𝑥) 안의 path이므로, fiber 𝑃(𝑦) 안의 path인 apd𝑔(𝑝) 와 곧바로 합성할 수 없다. 따라서 𝑝∗ 를 써서 𝐻(𝑥) 를 fiber 𝑃(𝑦) 안의 path로 먼저 옮긴 뒤 합성해야한다.따라서 다음이 의존함수 버전의 Lemma 2.4.3 이다.∏𝑥,𝑦:𝐴∏𝑝:𝑥=𝐴𝑦(𝑝∗(𝐻(𝑥))▪apd𝑔(𝑝)=apd𝑓(𝑝)▪𝐻(𝑦))이제 증명하자. 𝑝 에 대한 path induction을 사용하면 𝑝≡refl𝑥 인 경우만 보면 충분하다.이 경우 𝑝∗ 는 항등 함수이고, apd𝑓(refl𝑥)=refl𝑓(𝑥), apd𝑔(refl𝑥)=refl𝑔(𝑥) 이다.𝑝∗(𝐻(𝑥))▪apd𝑔(𝑝)=𝐻(𝑥)▪refl𝑔(𝑥)=𝐻(𝑥)이고,apd𝑓(𝑝)▪𝐻(𝑦)=apd𝑓(refl𝑥)▪𝐻(𝑥)=refl𝑓(𝑥)▪𝐻(𝑥)=𝐻(𝑥)이므로 양변이 같다.따라서 모든 𝑥,𝑦:𝐴 와 𝑝:𝑥=𝑦 에 대해𝑝∗(𝐻(𝑥))▪apd𝑔(𝑝)=apd𝑓(𝑝)▪𝐻(𝑦)가 성립한다. ∎

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.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 𝑛:ℕ. ∎