Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OPair.agda @ 376:6c72bee25653

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, 20 Jul 2020 16:28:12 +0900
parents 17adeeee0c2a
children 6dcea4c7cba1
comparison
equal deleted inserted replaced
375:8cade5f660bd 376:6c72bee25653
154 lemma | tri< a ¬b ¬c = {!!} 154 lemma | tri< a ¬b ¬c = {!!}
155 lemma | tri≈ ¬a b ¬c = next< {!!} {!!} 155 lemma | tri≈ ¬a b ¬c = next< {!!} {!!}
156 lemma | tri> ¬a ¬b c = {!!} 156 lemma | tri> ¬a ¬b c = {!!}
157 157
158 _⊗_ : (A B : HOD) → HOD 158 _⊗_ : (A B : HOD) → HOD
159 A ⊗ B = Union ( Replace B (λ b _ → Replace A (λ a _ → < a , b > ) )) 159 A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
160 160
161 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > 161 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b >
162 product→ {A} {B} {a} {b} A∋a B∋b = {!!} 162 product→ {A} {B} {a} {b} A∋a B∋b = {!!}
163 163
164 record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p ) : Set (suc n) where 164 record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p ) : Set (suc n) where