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𝑓(𝑝)▪𝐻(𝑦)가 성립한다. ∎