Mercurial > hg > Members > kono > Proof > HyperReal

comparison src/logic.agda @ 17:02847b697be9

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 Thu, 08 Jul 2021 08:40:51 +0900
parents f094694aeec5
children
comparison
equal deleted inserted replaced
16:cd52a72d4fca 17:02847b697be9
71 true <=> true = true 71 true <=> true = true
72 false <=> false = true 72 false <=> false = true
73 _ <=> _ = false 73 _ <=> _ = false
74 74
75 open import Relation.Binary.PropositionalEquality 75 open import Relation.Binary.PropositionalEquality
76
77 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
78 field
79 fun← : S → R
80 fun→ : R → S
81 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
82 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
83
84 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
85 injection R S f = (x y : R) → f x ≡ f y → x ≡ y
86
76 87
77 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 88 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
78 ¬t=f true () 89 ¬t=f true ()
79 ¬t=f false () 90 ¬t=f false ()
80 91