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 exponentiate 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.∎