# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488449044 -32400
# Node ID fd79b6d9f350fd112df1408bba564add9b6b67e3
# Parent  0ba86e29f4924b501ea3430dcebf7414e590b6b5
fix comment

diff -r 0ba86e29f492 -r fd79b6d9f350 discrete.agda
--- 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
 ---       -----→
diff -r 0ba86e29f492 -r fd79b6d9f350 limit-to.agda
--- 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 {