Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/OPair.agda @ 1096:55ab5de1ae02
recovery
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 23 Dec 2022 12:54:05 +0900 |
parents | a5f8084b8368 |
children | 9dcbf3524a5c |
line wrap: on
line diff
--- a/src/OPair.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/OPair.agda Fri Dec 23 12:54:05 2022 +0900 @@ -166,8 +166,7 @@ A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) )) product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b > -product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >))) - ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where +product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2 } where lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >))) lemma1 = replacement← B b B∋b lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)