Mercurial > hg > Members > kono > Proof > category

changeset 1044:aa3ec90f5b78

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 Fri, 09 Apr 2021 09:51:02 +0900
parents 35a3d5b194b7
children 139d58917093
files src/ToposIL.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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