# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1617929462 -32400
# Node ID aa3ec90f5b7890681c4ac2147181db8459d397dc
# Parent  35a3d5b194b746efb8b7d6017066a000fe6c045f
...

diff -r 35a3d5b194b7 -r aa3ec90f5b78 src/ToposIL.agda
--- a/src/ToposIL.agda	Fri Apr 09 09:50:58 2021 +0900
+++ b/src/ToposIL.agda	Fri Apr 09 09:51:02 2021 +0900
@@ -34,8 +34,8 @@
          -- { x ∈ a | φ x } : P a
          select : {a b : Obj A}  (α : Hom A (CCC.１ c) (P a) ) → ( (x :  Hom A  (CCC.１ c) a ) →  Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
-     _|-_  : {a : Obj A} (p : Hom A (CCC.１ c) Ω ) → Set ℓ
-     _|-_  {a} p = A [ p ≈  ⊤ ] 
+     |-_  : {a : Obj A} (p : Hom A (CCC.１ c) Ω ) → Set ℓ
+     |-_  {a} p = A [ p ≈  ⊤ ] 
   
 --             ○ b
 --       b -----------→ 1