Mercurial > hg > Members > kono > Proof > category

changeset 458:fd79b6d9f350

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Mar 2017 19:04:04 +0900
parents 0ba86e29f492
children 9d24fb809746
files discrete.agda limit-to.agda
diffstat 2 files changed, 6 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Thu Mar 02 18:30:58 2017 +0900
+++ b/discrete.agda	Thu Mar 02 19:04:04 2017 +0900
@@ -9,8 +9,8 @@
    t0 : TwoObject
    t1 : TwoObject
 
--- If we have limit then we have equalizer
----  two objects category
+---
+---  two objects category  ( for limit to equalizer proof )
 ---
 ---          f
 ---       -----→
--- a/limit-to.agda	Thu Mar 02 18:30:58 2017 +0900
+++ b/limit-to.agda	Thu Mar 02 19:04:04 2017 +0900
@@ -10,7 +10,9 @@
 open import discrete
 
 
----  Equalizer
+---  Equalizer  from Limit ( 2->A functor Γ and  Nat :  K ->　Γ)
+---
+---
 ---                     f
 ---          e       -----→
 ---     c -----→  a         b     A
@@ -34,7 +36,7 @@
 open Limit
 open NTrans
 
--- Functor : TwoCat -> A
+-- Functor Γ : TwoCat -> A
 
 IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} {c₂})  A
 IndexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {