Mercurial > hg > Members > kono > Proof > category

diff src/CCCGraph.agda @ 995:1d365952dde4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Mar 2021 23:02:33 +0900
parents 485bc7560a75
children d89f2c8cf0f4
line wrap: on
line diff
--- a/src/CCCGraph.agda	Sat Mar 06 19:11:01 2021 +0900
+++ b/src/CCCGraph.agda	Sat Mar 06 23:02:33 2021 +0900
@@ -95,6 +95,14 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+--             h
+
 data II  {c : Level } : Set c where
      true : II
      false : II