Mercurial > hg > Members > kono > Proof > category

changeset 1093:4bef1ec9d385

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 Mon, 17 May 2021 09:31:44 +0900
parents 9f967d9312f1
children bcaa8f66ec09
files src/ToposIL.agda
diffstat 1 files changed, 1 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Mon May 17 01:19:00 2021 +0900
+++ b/src/ToposIL.agda	Mon May 17 09:31:44 2021 +0900
@@ -78,6 +78,7 @@
 
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
 
+
   -- functional completeness
   FC0 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
   FC0 = {a b : Obj A}  (t : Topos A c) ( φ : Poly a (Ω t) b) → Functional-completeness φ