1樓：nasqum
隨手瞎答乙個吧，我其實也不確定。。。
我猜你的問題是，有了idtoeqv以後，為什麼不定義乙個反向的postulate，這樣的話就有了乙個雙射，而是定義univalence，僅僅變成乙個equivalence relation
如果問題是這樣的話那大概是因為 isomorphism這個條件實在太強了實際用起來派不上什麼用處，用equivlanece relation更靈活，而isomorphism只是一種特殊的equivalence。
至於怎麼定義equivalence呢，第四章有很多，一般大家都比較喜歡adjoint equivalence
2樓：Anqur
我認為 isomorphism 是很 meta 的東西.
拿 inductive types 舉例, 其本質是 initial -algebras 沒毛病, 但其代數 (其中 是範疇 中的物件, 是態射 ) 中的這個 是個 isomorphism, 即 能表示自然數 的 successor, 且存在乙個逆 表示 的 predecessor.
那麼後面的事情我們都知道了: 為了 pattern matching on data, 為了實現 looping functions, 為了表達 inductive types, 我們需要更好的 data encoding 方法, 如 Church encoding, Scott encoding, Parigot encoding. 然後基於這些 encoding, 繼續定義我們在型別論中所需要的 algebra, 如:
我想要 primitive recursion, 我可以基於 Parigot encoding 實現 primitive recursive -algebra, 即三元組 .
我想要方便寫 case, 我可以基於 Scott encoding 實現 -algebra with case, 即三元組 .
啊交換圖懶得畫了...
web為什麼不直接用tcp協議？
Archeus 瀏覽器需要提供乙個安全沙箱,在使用網路協議上就需要加入一些諸如跨域等限制.如果瀏覽器提供建立裸TCP鏈結的能力,那麼當你開啟網頁的時候,該網頁的指令碼就可以利用TCP協議訪問內網的資源. luoxn28 web可以直接使用TCP進行通訊，但是為什麼使用websocket來通訊呢 注意...
為什麼RCNN用SVM做分類而不直接用CNN全連線之後softmax輸出？
月臻 究其原因一句話就是 SVM和對預訓練的網路做調優兩個階段使用的正負樣本標準不同 下面談下作者的整個思路 剛開始只是用了ImageNet 預訓練了CNN，並用提取的特徵訓練了SVMs，此時用正負樣本標記方法的IoU閾值為0.3 小於0.3的為負樣本，正樣本為嚴格的Ground Truth 後來剛...
林沖當時為什麼不直接用寶刀殺了高俅？
董培 林沖根本不願意殺高俅，這是大前提。好多人受電視劇集影響，覺得林沖是乙個血性的好漢，實際上並非如此。就連後來在梁山，高俅被俘虜，林沖對高俅也只是怒目而視，並沒有衝上去殺他。林沖其實是乙個理性到冷血的人物，他知道什麼人可以得罪，什麼人不可以得罪，而高俅，就是他不可以得罪的人，畢竟是太尉，能左右他的...