Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

2010-05-01から1ヶ月間の記事一覧

CLTT p45 Exercises 1.3.1 (i) の証明の一部 (2)

前回の続き。only if を示します。 Categorical Logic and Type Theory, Volume 141 (Studies in Logic and the Foundations of Mathematics) まず、(u,f)がカルテシアンなので、(u,π'):(I,Y)→(J,Y)とIに関して、以下を可換にするようなj:I×Y→Xが存在します…

CLTT p45 Exercises 1.3.1 (i) の証明の一部

CLTT読書会のまとめです。1.3.1の(i)の"if"の証明を酒井さんが解いて下さったので、その図を載せときます。まず、示さなきゃいけないのは、問題文のようなhが与えられたとき、(u,f)がCartesianであること。つまり、以下の図の青字のような任意の(v,g):(K,Z)→…