import FormalLab.Bridges.LinearLogicAndResourceSemantics import FormalLab.Bridges.MonoidalClosedCategories import FormalLab.Bridges.RecursiveTypeSemantics /-! # 全問題の解答：論理・計算・意味論 ## 第75章：モノイダル閉圏——内部hom・評価・自己豊穣化 ### 問題1：評価射からhom同値の一意性を再構成する #### ヒント 内部hom `[A,B]` と評価 `ev:[A,B]⊗A→B` に対する普遍射Λfを書きます。 #### 解答 各 `f:X⊗A→B` に一意な `Λf:X→[A,B]` があり、`(Λf⊗id_A)≫ev=f` を満たすなら `Hom(X,[A,B])≅Hom(X⊗A,B)` を得ます。順方向はgを `(g⊗id)≫ev` へ、逆はΛ。方程式が片方の逆、一意性がもう片方の 逆を与えます。Xについての自然性はテンソルの関手性と媒介射の一意性から従います。 内部演算を定義するとき、評価射と普遍性をAPIの中心に置けばカリー化を派生できます。 ### 問題2：内部カリー化同型の二重評価を追跡する #### ヒント `[A⊗B,C]≅[A,[B,C]]` を、両辺から二回評価して同じ射へ送ることで構成します。 #### 解答 `[A⊗B,C]⊗A⊗B` を結合子で並べ替え、一度の評価でCへ送る射をAについてカリー化し、さらに必要な内部化を行うと `[A⊗B,C]→[A,[B,C]]` を得ます。逆向きは `[A,[B,C]]⊗A⊗B` でまず内側[B,C]を評価し、次にBを評価してCへ送り、 A⊗Bについてカリー化します。二方向の合成は同じ二重評価射を持つため一意性から恒等です。 多引数線形写像のカリー化を、内部homの反復とモノイダル整合性で管理します。 ### 問題3：内部合成から通常の射の合成を回収する #### ヒント 内部合成 `comp:[B,C]⊗[A,B]→[A,C]` と、射fを単位からの点 `I→[A,B]` として使います。 #### 解答 通常の射 `f:A→B` は随伴で名前 `⌜f⌝:I→[A,B]` に対応します。f,gの名前を単位同型 `I≅I⊗I` の後に並べ、内部合成へ送ると `I→[A,C]` を得ます。この点を評価してunnamingするとg∘fになります。 内部合成自体は `[B,C]⊗[A,B]⊗A` で右の評価、左の評価を順に行う射の転置です。 自己豊穣化では圏の射・恒等・合成をhom対象内の点・単位・内部合成として統一します。 ### 問題4：デカルト構造が弱化と縮約を生むことを示す #### ヒント 積単位の終性と積の対角を、文脈テンソル上の自然なcomonoid構造として使います。 #### 解答 デカルト積では各Xに破棄 `!_X:X→1` と複製 `Δ_X:X→X×X` が自然にあります。!は変数を使わない弱化、Δは同じ変数を 二箇所へ供給する縮約を意味します。これらは余単位・余乗法をなし、可換comonoid法則を積の普遍性から満たします。 一般モノイダル圏ではこの自然な構造がなく、線形な資源使用が保たれます。 指数様相は選ばれた対象へcomonoid構造を復元し、線形世界内で限定的な弱化・縮約を許します。 ### 問題5：組紐によって左右の閉性を移す #### ヒント 右テンソル `(-)⊗A` と左テンソル `A⊗(-)` を組紐 `β:X⊗A≅A⊗X` で自然同型にします。 #### 解答 組紐付きモノイダル圏で `(-)⊗A` が右随伴 `[A,-]` を持つなら、`A⊗(-)` は組紐を介して同じ関手に自然同型です。 したがってhom同型 `Hom(A⊗X,B)≅Hom(X⊗A,B)≅Hom(X,[A,B])` が得られ、左テンソルにも右随伴が存在します。組紐がなければ左右の テンソルは別関手で、一方の閉性から他方は従いません。 非対称モノイダル圏では左内部homと右内部homを別記し、それぞれの評価射を追跡します。 ### 問題6：左随伴としてのテンソルが余極限を保つことを導く #### ヒント 閉性から `(-)⊗A` が左随伴であるため、一般定理「左随伴は余極限を保つ」を適用します。 #### 解答 図式Dの余極限Lに対し、`Hom(L⊗A,B)≅Hom(L,[A,B])`。Lの普遍性で右辺はDの各対象から[A,B]への整合射族に対応し、 再び閉性で各 `D j⊗A→B` の整合族に対応します。これは `D(-)⊗A` の余極限からBへの射の分類なので、L⊗Aがその余極限です。 従ってテンソルは余積・余等化子など存在するすべての余極限を保存します。 テンソル積が直和や商と可換する公式を、個別計算でなく随伴性から導けます。 ## 第76章：線形論理・線形型——仮定を資源として追跡する ### 問題1：弱化と縮約が導出をどこで止めるか調べる #### ヒント 線形文脈では各仮定をちょうど一度使い、未使用と二重使用の最初の規則適用を探します。 #### 解答 `x:A,y:B⊢x:A` はyを捨てる弱化がなければ導出できません。`x:A⊢(x,x):A⊗A` はテンソル導入で文脈を二分する際、xを 両枝へ置く縮約が必要なので導出不能です。一方 `x:A,y:B⊢(x,y):A⊗B` は文脈を `{x}` と `{y}` に分割して導出できます。 失敗は結論の値ではなく、導出木の葉へ資源を一対一に割り当てられない箇所として診断します。 ファイルハンドルやセッション型のAPIで、破棄・複製できない値の使用を同じ資源勘定で検査します。 ### 問題2：β簡約が資源使用を保存する条件を示す #### ヒント 線形ラムダ `λx.t` ではt中のxがちょうど一回現れることを代入時に使います。 #### 解答 適用 `(λx.t) u` の型付けでは、ラムダ側の文脈Γと引数側の文脈Δが互いに素で、tはΓとxを各一度使い、uはΔを各一度 使います。β簡約 `t[x:=u]` はt中の唯一のx出現をuで置き換えるため、Δの資源は一度だけ挿入され、Γの資源も保持されます。 xが0回ならuの資源が消え、2回なら複製されるので保存しません。線形代入補題が型保存と資源保存を同時に述べます。 量的型理論では「一度」を半環の使用量へ一般化し、代入で使用量が乗法・加法に従うことを証明します。 ### 問題3：シーケント規則を圏の射へ逐語的に翻訳する #### ヒント シーケント `A₁,…,Aₙ⊢B` を射 `A₁⊗…⊗Aₙ→B` と読みます。 #### 解答 恒等公理は `id_A:A→A`、cutは射の合成です。テンソル右規則は二つの文脈射をテンソルして `Γ⊗Δ→A⊗B` を作ります。線形含意右規則は `Γ⊗A→B` のカリー化 `Γ→[A,B]`、左規則は評価射とテンソル・合成を 組み合わせます。交換は組紐で表し、弱化・縮約に対応する自然射は一般モノイダル閉圏にはありません。 新しい結合子の意味論を設計するとき、導入・除去規則がどの普遍射を要求するか逐語的に読み取ります。 ### 問題4：乗法的結合子と加法的結合子を反例で分ける #### ヒント テンソル導入は文脈を分割し、with導入は同じ文脈から二成分を作る点を比較します。 #### 解答 `A⊗B` を作るには資源をΓ,Δへ分割し、一方でA、他方でBを作ります。加法的積 `A&B` は同じΓからAとBの両方を作り、 利用時にどちらか一方を選びます。単一資源x:Aから `A&A` は二つの導出が同じxを共有するため作れますが、`A⊗A` はxを 二分できず作れません。逆にテンソル対は両成分を同時に保持し、withは一度の観察で選択されるため意味が異なります。 積・和という集合論的名称だけで判断せず、資源配分を定める証明規則から結合子を識別します。 ### 問題5：余モナドと線形指数余モナドの差を列挙する #### ヒント 通常の余モナド法則に加え、`!A` が自然な可換comonoidを持つためのデータを挙げます。 #### 解答 余モナドには関手!、余単位 `der:!A→A`、余乗法 `dig:!A→!!A` と二単位・結合法則があります。線形指数余モナドにはさらに `weak:!A→I`、`contr:!A→!A⊗!A` という自然な可換comonoid構造、!のモノイダル性、der/digとの整合性が必要です。 通常の余モナドだけでは!Aを自由に捨てたり複製したりできず、線形論理の指数規則を解釈できません。 「指数様相」と呼ぶ構造について、単なる余モナドより強いSeely型の条件をどこまで仮定するか明記します。 ### 問題6：LNL随伴から指数様相を構成する #### ヒント デカルト閉圏Cと対称モノイダル閉圏Lのモノイダル随伴 `F:C⇄L:G` から `!=FG` を作ります。 #### 解答 F⊣GよりL上に余モナド `!=F∘G` が誘導され、余単位は随伴の余単位、余乗法はFηGです。Cはデカルトなので各GXに 対角と終対象への射があります。Fの強モノイダル構造でこれらをLへ運ぶと、!Xに縮約 `!X→!X⊗!X` と弱化 `!X→I` が 得られます。自然性とcomonoid法則はCのデカルト構造とFの整合性から従います。 非線形値をG側へ移しFで線形世界へ戻す型付けを、LNL言語の二文脈として実装できます。 ## 第77章：モナドと計算効果——値から計算を分離して合成する ### 問題1：三つの具体モナドを同じ法則で比較する #### ヒント 例外、状態、非決定性についてreturnとbindを定義し、三法則を同じ表へ置きます。 #### 解答 例外は `T A=E+A`、状態は `T A=S→A×S`、非決定性は `T A=List A`。returnはそれぞれ成功注入、状態不変の値、単一要素列です。 bindは例外なら短絡し、状態なら次状態を渡し、Listなら各候補への結果を連結します。左単位はreturn後のbind、右単位は returnへのbind、結合律は計算列の再括弧付けで、各効果のデータ演算の単位・結合法則へ還元されます。 新しい効果をモナド化するとき、型構成だけでなくreturn/bindと三法則の証拠を同じ比較表で設計します。 ### 問題2：値呼び適用の表示をstrengthから構成する #### ヒント 関数計算 `T(A→B)` と引数計算 `T A` を順に結び、純粋な適用をT内へ持ち上げます。 #### 解答 値呼びではまずmfを実行してfを得て、次にmaを実行してaを得てreturn(f a)します。圏論的にはstrength `A⊗TB→T(A⊗B)` とモナドの強度から二計算を `T((A→B)×A)` へまとめ、`T ev` で `T B` へ送ります。順序付き効果では mfとmaを交換できないため、左・右strengthと評価順を固定します。 言語の評価順をdenotationに反映するには、モナドだけでなく積との相互作用を表すstrengthを検査します。 ### 問題3：ChoiceTreeの自由性を証明する #### ヒント 戻り値、効果操作、選択節点を持つ木から、同じ演算を備えた任意の代数へfoldします。 #### 解答 ChoiceTree Aはreturn葉、シグネチャの効果節点、選択分岐で自由に生成されます。任意の解釈代数Xと値写像f:A→Xに対し、 木帰納で葉をf、効果節点を指定演算、選択をXの選択演算へ送るfoldを作ります。構成子との可換性を満たす他の写像hは、 木帰納法で各節点においてfoldと一致します。従って構造保存写像は一意です。 自由モナドを効果構文とし、ハンドラを代数準同型またはfoldとして定義できます。 ### 問題4：例外ハンドラをEilenberg–Moore代数として調べる #### ヒント 例外モナド `T A=E+A` の代数 `a:E+A→A` を成功・例外の場合へ分けます。 #### 解答 単位則から成功値について `a(inr x)=x`。従って代数は各例外eへ回復値 `h(e):A` を選ぶ関数で決まります。結合法則は 入れ子の例外処理を一度で処理することと一致します。代数準同型fは `f(h_A e)=h_B e` を満たす回復値保存写像です。 ただし例外を別の効果計算へ再送するハンドラは同じ圏上のEM代数でなく、モナド間射や相対代数が必要です。 ハンドラの返り先が純粋値か別効果かを区別し、適切な代数概念を選びます。 ### 問題5：効果の層順序を状態と例外で比較する #### ヒント `StateT S (Except E)` と `ExceptT E (State S)` の型を展開し、失敗時の状態が観察可能か調べます。 #### 解答 前者は概ね `S→E+(A×S)` で、失敗すると最終状態を返さないため更新が巻き戻る解釈です。後者は `S→(E+A)×S` で、失敗しても状態を保持できます。同じ状態・例外の二効果でも変換子の順序で観察が変わります。両者の交換には モナド間の分配法則が必要で、一般には自然同型ではありません。 効果スタックの順序を実装都合で選ばず、例外時のcommit/rollbackなど意図する意味論から決めます。 ### 問題6：表示の健全性とadequacyを分ける #### ヒント 操作的等式から意味の等式への向きと、意味が観察結果を十分に反映する逆向きを別々に述べます。 #### 解答 健全性は `t→*v` または `t≡u` なら `⟦t⟧=⟦v⟧` または `⟦t⟧=⟦u⟧` という意味保存です。adequacyは例えば 閉じたBool計算の表示がtrueの意味なら操作的にもtrueへ到達する、という観察の反映です。健全でもすべての項を一要素へ送る 自明モデルはadequateでありません。完全抽象性はさらに表示等式と文脈同値の一致を要求し、adequacyより強いです。 意味論の正当性を主張するとき、型保存・健全性・adequacy・完全抽象性を別の定理として証拠化します。 ## 第78章：トポスと圏論的論理——部分対象を真理値で分類する ### 問題1：`Type` の単射から特性述語を構成する #### ヒント 単射m:S→Xの像への所属を `χ_m:X→Prop` とし、真を分類する射との引戻しを作ります。 #### 解答 `χ_m(x)≔∃s:S,m s=x` と定めます。真射 `true:Unit→Prop` はTrueを選びます。χ_mに沿う引戻しは `Σx:X,χ_m(x)`、すなわち像の証人付き要素です。写像 `s↦⟨m s,⟨s,rfl⟩⟩` は単射性を使ってSとの同型を与え、引戻し正方形が mを回収します。部分対象を像同型まで扱うことで任意のmonoを述語が分類します。 データ型の部分集合を特性関数へ変換し、包含射と述語の相互変換を普遍性として扱います。 ### 問題2：分類子と表現可能性の二方向を再構成する #### ヒント Ωとtrueが部分対象関手 `Sub(-)` を表す自然同型 `Sub(X)≅Hom(X,Ω)` を与えることを示します。 #### 解答 分類子からはmono mを一意な特性射χ_mへ送り、引戻しの合成則によりXについて自然です。逆に自然な全単射があれば、 Ωで恒等射に対応する部分対象 `true:1↪Ω` を普遍元として取ります。任意χ:X→Ωに対応する部分対象は自然性によりtrueのχに沿う 引戻しです。二方向の逆法則が分類射の存在一意性を与えます。 「構造を分類する対象」を、対応する構造の反変関手の表現可能性として探します。 ### 問題3：前層の特性篩を要素ごとに計算する #### ヒント 部分前層S⊆Fと要素x∈F(c)に対し、どの射f:d→cで制限x|_fがS(d)へ入るか集めます。 #### 解答 `χ_c(x)={f:d→c | F(f)(x)∈S(d)}` と定めます。fが属しg:e→dなら、部分前層の制限閉性から `F(g)(F(f)x)=F(f∘g)x∈S(e)` なので篩です。x自体がS(c)に属すことと恒等射がχ_c(x)に属すこと、すなわちχ_c(x)が最大篩で あることは同値です。再制限すると篩の引戻しになるためχは自然変換です。 前層トポスの真理値が単なるBoolでなく「どの将来の制限で真になるか」を記録する篩であることを読み取れます。 ### 問題4：冪対象の所属関係から部分対象族を回収する #### ヒント 冪対象P(A)=Ω^Aの評価射を真理値として、普遍的所属部分対象を定義します。 #### 解答 評価 `ev:Ω^A×A→Ω` のtrueに沿う引戻しを `∈_A↪P(A)×A` とします。射 `χ:X→P(A)` はカリー化を戻すと `X×A→Ω` になり、その分類する部分対象はXで添字付けられたAの部分対象族です。逆に部分対象R↪X×Aの特性射をカリー化して χ_Rを得ます。指数随伴と分類子の二つの全単射を合成して対応を構成します。 関係、述語族、集合値写像を冪対象への一つの射として相互変換できます。 ### 問題5：排中律が失敗する局所的な真理値を調べる #### ヒント 位相空間の開集合Heyting代数で、否定を内部として `¬U=int(X\U)` と計算します。 #### 解答 実数上の開集合 `U=(0,∞)` を取ると、内部否定は `¬U=(-∞,0)`。和 `U∨¬U=R\{0}` は全体Rでなく、排中律が失敗します。 二重否定は `¬¬U=(0,∞)=U` ですが、別の稠密開集合では二重否定が全体へ広がることもあります。内部真理値は開集合で、 補集合が開とは限らないためBoolean代数でなくHeyting代数になります。 層・前層モデル内で古典原理を使う前に、ΩがBooleanである追加条件を確認します。 ### 問題6：二種類のトポスと保存される論理を比較する #### ヒント 初等トポスの有限極限・指数・分類子と、Grothendieckトポスの層圏表示・余極限構造を比較します。 #### 解答 初等トポスは有限極限、デカルト閉性、部分対象分類子を持ち、高階直観主義論理を解釈します。Grothendieckトポスは小さいサイト上の 層圏と同値で、初等トポス構造に加えて小余極限、生成族、特定のexactnessを持ちます。幾何学的射の逆像は有限極限と任意余極限を 保つため、有限極限・任意和・存在量化で作る幾何学的論理を保存しますが、一般の含意や全称量化は必ずしも保存しません。 論理式をモデル間で移す際、真理保存を期待する断片が幾何学的かを構文から判定します。 ## 第79章：再帰型の意味論——構文・近似・関手不動点を接続する ### 問題1：始鎖の最初の五段階を完全に記述する #### ヒント 始対象0から `0→F0→F²0→…` を、`F X=1+A×X` について展開します。 #### 解答 `X₀=0`、`X₁=1`、`X₂=1+A`、`X₃=1+A+A²`、`X₄=1+A+A²+A³` です。接続射は短い有限リストを同じリストとして次段へ 埋め込みます。各X_nは長さn未満のAリストを表し、鎖の余極限はすべての有限リスト `List A`。Fがこのω余極限を保存すれば 誘導構造射 `F(List A)→List A` が始代数になります。 構文木の深さ有限近似を始鎖として計算し、全有限構文の帰納型を余極限で構成できます。 ### 問題2：不動点同型から始性が従わない反例を強化する #### ヒント F=Id以外に、`F X=1+X` が複数の不動点を持つ集合または領域の例を使います。 #### 解答 無限集合Xでは `1+X≅X` が成立するものが多く、例えばNとZはいずれも不動点同型を持ちます。しかしSetで `1+X` の始代数はNで、 構造はzero/succです。Zへ任意の不動点同型を入れても、すべての代数への一意な準同型が従うわけではありません。同じ台Nでも 構造射を異なる全単射に替えると始性を失い得ます。対象同型だけでなく構造射と普遍性が必要です。 再帰ドメイン方程式の解を選ぶとき、初期解・最小解・代数的compactnessなど選択原理を明記します。 ### 問題3：`1+X` の終解に無限要素を加える #### ヒント 余代数 `X→1+X` は停止または次状態を返すので、振舞いは有限停止時間か永久継続です。 #### 解答 終余代数の台を `N∞=N∪{∞}` とします。構造射outは0を停止側へ、n+1を継続してnへ、∞を継続して∞へ送ります。任意の余代数状態xは、 最初に停止するまでの有限ステップ数nがあればnへ、永遠に継続すれば∞へ送られます。この振舞写像はoutと可換し、各観察段階を 保存する射は同じ停止時間を返すしかないため一意です。始代数Nには∞がありません。 部分計算を有限結果と発散の和としてではなく、終余代数の尽きない振舞いとして捉えられます。 ### 問題4：負の再帰出現の向きを型で追跡する #### ヒント 型式 `X→A` に写像f:X→Yを作用させようとし、必要になる射の向きを調べます。 #### 解答 共変関手ならf:X→Yから `(X→A)→(Y→A)` が必要ですが、関数をY上へ延長する標準的方法はありません。前合成で得られるのは `(Y→A)→(X→A)` で向きが逆です。従ってXが矢印の始域に一回現れる型演算子は反変で、通常の自己関手不動点として始代数を 構成できません。二回の負出現は形式上共変でも、strict positivityや連続性は別途検査が必要です。 混合分散の再帰型には双関手、反変関手対、逆極限法など適切な意味論を選びます。 ### 問題5：有限燃料とKleene反復を接続する #### ヒント 再帰機能Fと底⊥から `Fⁿ⊥` をn燃料の意味と対応させます。 #### 解答 燃料0の評価器はすべて未定義⊥、燃料n+1は本体を一段展開し再帰呼出しへnを渡します。その表示は近似列 `x₀=⊥,x_{n+1}=F x_n` と一致します。Fがω連続なら上限 `x=sup_n x_n` はFの最小不動点です。有限ステップで値vへ到達する入力は あるn以降x_nでvとなり、発散入力はすべての有限近似で⊥のままです。 実装可能な燃料付きインタプリタを、領域理論の最小不動点意味論に対する有限観測として正当化できます。 ### 問題6：操作的意味論と表示的意味論の境界を監査する #### ヒント 構文・一歩関係・評価と、意味領域・解釈関数・不動点を別の欄へ置き、接続定理を列挙します。 #### 解答 操作的側は項、値、評価文脈、簡約列、停止・発散を定めます。表示的側は領域と順序、型構成子の関手、項の連続写像、再帰の最小不動点を 定めます。両者の接続は型付けの意味健全性、簡約に対する不変性、停止結果の一致、adequacy、必要なら完全抽象性です。表示値が存在する だけで操作的停止は従わず、簡約保存だけでモデルが観察を十分区別するとも限りません。 意味論実装の保証を報告するとき、検査済みの橋定理だけを主張し、adequacyや完全抽象性を推測で補いません。 -/ namespace FormalLab.Appendix.Solutions.Chapter075Exercise002 open _root_.CategoryTheory open _root_.CategoryTheory.MonoidalCategory open _root_.CategoryTheory.MonoidalClosed #check ihomCurry #check ihomUncurry #check uncurry_uncurry_ihomCurry end FormalLab.Appendix.Solutions.Chapter075Exercise002 namespace FormalLab.Appendix.Solutions.Chapter075Exercise005 open _root_.CategoryTheory open scoped MonoidalCategory universe u v variable {C : Type u} [_root_.CategoryTheory.Category.{v} C] [_root_.CategoryTheory.MonoidalCategory C] [_root_.CategoryTheory.BraidedCategory C] [_root_.CategoryTheory.MonoidalClosed C] #check _root_.CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight example (A : C) : (_root_.CategoryTheory.MonoidalCategory.tensorRight A).IsLeftAdjoint := inferInstance end FormalLab.Appendix.Solutions.Chapter075Exercise005 namespace FormalLab.Appendix.Solutions.Chapter076Exercise003 open _root_.CategoryTheory open _root_.CategoryTheory.MonoidalCategory open scoped MonoidalCategory open FormalLab.Bridges.MonoidalClosedCategories open FormalLab.Bridges.LinearLogicAndResourceSemantics universe u v variable {C : Type u} [_root_.CategoryTheory.Category.{v} C] [_root_.CategoryTheory.MonoidalCategory C] [_root_.CategoryTheory.SymmetricCategory C] [_root_.CategoryTheory.MonoidalClosed C] variable {A B Γ Δ D : C} def interpretLinearImplicationLeft (argument : Γ ⟶ A) (continuation : B ⊗ Δ ⟶ D) : internalHom A B ⊗ (Γ ⊗ Δ) ⟶ D := (α_ (internalHom A B) Γ Δ).inv ≫ ((𝟙 (internalHom A B)) ⊗ₘ argument) ▷ Δ ≫ interpretApplication A B ▷ Δ ≫ continuation end FormalLab.Appendix.Solutions.Chapter076Exercise003 namespace FormalLab.Appendix.Solutions.Chapter079Exercise004 def precompose {X Y : Type} (f : X → Y) : (Y → Bool) → (X → Bool) := fun predicate ↦ predicate ∘ f def postcompose {X Y : Type} (f : X → Y) : (Bool → X) → (Bool → Y) := fun family ↦ f ∘ family def doubleContravariant {X Y : Type} (f : X → Y) : ((X → Bool) → Bool) → ((Y → Bool) → Bool) := fun observer predicate ↦ observer (predicate ∘ f) theorem precompose_comp {X Y Z : Type} (f : X → Y) (g : Y → Z) : precompose (g ∘ f) = precompose f ∘ precompose g := rfl theorem postcompose_comp {X Y Z : Type} (f : X → Y) (g : Y → Z) : postcompose (g ∘ f) = postcompose g ∘ postcompose f := rfl theorem doubleContravariant_comp {X Y Z : Type} (f : X → Y) (g : Y → Z) : doubleContravariant (g ∘ f) = doubleContravariant g ∘ doubleContravariant f := rfl end FormalLab.Appendix.Solutions.Chapter079Exercise004