<div class="chatlog__message-group"> <div id="chatlog__message-container-408012577185202197" class="chatlog__message-container" data-message-id="408012577185202197"> <div class="chatlog__message"> <div class="chatlog__message-aside"><img class="chatlog__avatar" src="https://cdn.discordapp.com/avatars/293624673265123328/accd07acc220a18568ba46a6e9ede18a.png?size=512" alt="Avatar" loading="lazy"></div> <div class="chatlog__message-primary"> <div class="chatlog__header"><span class="chatlog__author" style="color:rgb(17,128,106)" title="koher" data-user-id="293624673265123328">koher</span> <a href="/channels/400483073743126558?category=archived&channel=math&message_id=408014753869332491"><span class="chatlog__timestamp" title="Tuesday, January 30, 2018 9:36 PM"></span></a><a href="#chatlog__message-container-408012577185202197">1/30/2018 9:36 PM</a></div> <div class="chatlog__content chatlog__markdown"><span class="chatlog__markdown-preserve">それは違うか。自己射と恒等射が区別されているから、なんらかの方法で射の <code class="chatlog__markdown-pre chatlog__markdown-pre--inline">=</code> を定義しないといけないのか。</span></div> </div> </div> </div> <div id="chatlog__message-container-408013361486364682" class="chatlog__message-container" data-message-id="408013361486364682"> <div class="chatlog__message"> <div class="chatlog__message-aside"> <div class="chatlog__short-timestamp" title="Tuesday, January 30, 2018 9:39 PM">9:39 PM</div> </div> <div class="chatlog__message-primary"> <div class="chatlog__content chatlog__markdown"><span class="chatlog__markdown-preserve">プログラミング言語における型を対象、(副作用のない)関数を射とみなした圏を考えたとき、型が同じであることを対象の equality と考えると <code class="chatlog__markdown-pre chatlog__markdown-pre--inline">(T) -> T</code> な関数は複数考えられてしまうし、関数のオプジェクトが同一であることと考えると複数の恒等関数が作れてしまうからダメだし、挙動が同じなら <code class="chatlog__markdown-pre chatlog__markdown-pre--inline">=</code> が成り立つとかにしないといけない?</span> <span class="chatlog__edited-timestamp" title="Tuesday, January 30, 2018 11:35 PM">(edited)</span></div> </div> </div> </div> <div id="chatlog__message-container-408014753869332491" class="chatlog__message-container" data-message-id="408014753869332491"> <div class="chatlog__message"> <div class="chatlog__message-aside"> <div class="chatlog__short-timestamp" title="Tuesday, January 30, 2018 9:44 PM">9:44 PM</div> </div> <div class="chatlog__message-primary"> <div class="chatlog__content chatlog__markdown"><span class="chatlog__markdown-preserve"><code class="chatlog__markdown-pre chatlog__markdown-pre--multiline nohighlight">これらの公理から、各対象に対して恒等射はただ一つ存在することが示せる。</code> これも、一つであることを示すには二つの射が同じものかどうかを判定できないといけないから、暗黙的に <code class="chatlog__markdown-pre chatlog__markdown-pre--inline">射: Equatable</code> と仮定されている?</span></div> </div> </div> </div> </div>