Mercurial > hg > Members > kono > Proof > category
changeset 613:afddfebea797
t0f=t0 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Jun 2017 22:36:54 +0900 |
| parents | f924056bf08a |
| children | e6be03d94284 |
| files | freyd2.agda |
| diffstat | 1 files changed, 8 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Tue Jun 13 10:15:24 2017 +0900 +++ b/freyd2.agda Tue Jun 13 22:36:54 2017 +0900 @@ -153,14 +153,14 @@ t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ) x ≈⟨⟩ - (FMap (HomA A b) ( TMap (t0 lim) i)) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) - ≈⟨ {!!} ⟩ - FMap (HomA A b) (A [ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ]) (id1 A b ) - ≈⟨ ? ⟩ - FMap (HomA A b) (TMap t i x) (id1 A b ) - ≈⟨ {!!} ⟩ - {!!} o TMap t i x - ≈⟨ idL ⟩ + FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) + ≈⟨⟩ + TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) + ≈⟨ cdr idR ⟩ + TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) + ≈⟨ t0f=t (isLimit lim) ⟩ + TMap (ta a x t) i + ≈⟨⟩ TMap t i x ∎ ))