Mercurial > hg > Members > kono > Proof > category

changeset 471:36d13c7182c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 06 Mar 2017 17:23:10 +0900
parents c375d8f93a2c
children f62e72e81c7f
files discrete.agda limit-to.agda
diffstat 2 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Mon Mar 06 15:45:51 2017 +0900
+++ b/discrete.agda	Mon Mar 06 17:23:10 2017 +0900
@@ -92,6 +92,7 @@
 
 -- Category with no arrow but identity
 
+-- It looks like only one obj
 record DiscreteObj  {c₁  : Level }  :  Set c₁ 
    where
 
--- a/limit-to.agda	Mon Mar 06 15:45:51 2017 +0900
+++ b/limit-to.agda	Mon Mar 06 17:23:10 2017 +0900
@@ -253,7 +253,7 @@
                  id (FObj Γ b)  o qi a
                 ≈⟨ idL ⟩
                    qi  a 
-                ≈⟨⟩
+                ≈⟨⟩  -- only a = b case in discrete category
                    qi  b 
                 ≈↑⟨ idR ⟩
                    qi  b o id q