Mercurial > hg > Members > kono > Proof > category
changeset 637:946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jul 2017 00:12:38 +0900 |
| parents | 3e663c7f88c4 |
| children | a07b95e92933 |
| files | freyd2.agda |
| diffstat | 1 files changed, 8 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Fri Jun 30 23:36:54 2017 +0900 +++ b/freyd2.agda Sat Jul 01 00:12:38 2017 +0900 @@ -344,17 +344,16 @@ ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f ≈⟨⟩ tmap2 b o FMap (Yoneda A (obj i)) f - ∎ + ∎ + iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) + → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z + iso0 x y OneObj = refl iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin ( Sets [ tmap1 x o tmap2 x ] ) y ≈⟨⟩ arrow ( initial In (ob x (( FMap U y ) ( hom i OneObj ) ))) - ≈↑⟨ uniqueness In {!!} ⟩ - arrow (fArrow y {!!} ) - ≈⟨ {!!} ⟩ - arrow (fArrow y (hom i OneObj) ) - ≈⟨⟩ + ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩ y ∎ )) iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ] @@ -362,7 +361,9 @@ ( Sets [ tmap2 x o tmap1 x ] ) y ≡⟨⟩ ( FMap U ( arrow ( initial In (ob x y ) )) ) ( hom i OneObj ) - ≡⟨ {!!} ⟩ + ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob x y ) )) ⟩ + hom (ob x y) OneObj + ≡⟨⟩ y ∎ ) ) where open import Relation.Binary.PropositionalEquality