Mercurial > hg > Members > kono > Proof > category
changeset 631:7be3eb96310c
introduce fArrow
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Jun 2017 21:58:55 +0900 |
| parents | d2fc6fb58e0e |
| children | d36ff598a063 |
| files | freyd2.agda |
| diffstat | 1 files changed, 34 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Mon Jun 26 21:23:24 2017 +0900 +++ b/freyd2.agda Mon Jun 26 21:58:55 2017 +0900 @@ -268,7 +268,36 @@ ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U) ob b x = record { obj = b ; hom = ub b x} piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b - piArrow b = SFSFMap← SFS ( preinitialArrow PI ) + piArrow b = SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} ) + fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y + fArrowComm1 a b f x OneObj = begin + FMap U f ( ub a x OneObj ) + ≡⟨⟩ + FMap U f x + ≡⟨⟩ + ub b (FMap U f x) OneObj + ∎ where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning + fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → + Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ] + fArrowComm a b f x = extensionality Sets ( λ y → begin + ( Sets [ FMap U f o hom (ob a x) ] ) y + ≡⟨⟩ + FMap U f ( hom (ob a x) y ) + ≡⟨⟩ + FMap U f ( ub a x y ) + ≡⟨ fArrowComm1 a b f x y ⟩ + ub b (FMap U f x) y + ≡⟨⟩ + hom (ob b (FMap U f x)) y + ≡⟨⟩ + ( Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ) y + ∎ ) where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning + fArrow : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) ) + fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x } tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b) tmap1 b x = arrow ( piArrow ( ob b x ) ) preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ] @@ -281,6 +310,10 @@ ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y ≡⟨⟩ A [ f o arrow (piArrow (ob a y)) ] + ≡⟨⟩ + A [ arrow ( fArrow a b f y ) o arrow (piArrow (ob a y)) ] + ≡⟨⟩ + arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y ) o (piArrow (ob a y)) ] ) ≡⟨ {!!} ⟩ arrow (piArrow (ob b (FMap U f y) )) ≡⟨⟩