Mercurial > hg > Members > kono > Proof > category
changeset 634:5b0286e3aa32
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2017 17:17:17 +0900 |
| parents | 37fa9d3fab8c |
| children | f7cc0ec00e05 |
| files | freyd2.agda |
| diffstat | 1 files changed, 16 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Wed Jun 28 08:55:11 2017 +0900 +++ b/freyd2.agda Wed Jun 28 17:17:17 2017 +0900 @@ -299,8 +299,21 @@ ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a ee {a} {b} {f} {g} = equalizer-e comp f g preinitialEqu : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) → - IsEqualizer A ee (A [ arrow f o arrow ( piArrow x ) ] ) ( arrow ( piArrow y ) ) - preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (piArrow x) ] ) ( arrow ( piArrow y )) + IsEqualizer A ee (A [ arrow f o arrow ( preinitialArrow PI {x}) ] ) ( arrow ( preinitialArrow PI {y}) ) + preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI )) + pa : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) + → Hom ( K (Sets) A * ↓ U) (preinitialObj PI) + (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} ) + pa {x} {y} f = piArrow (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} ) + -- + -- e f + -- c -------→ a ---------→ b + -- ^ . ---------→ + -- | . g + -- |k . + -- | . h + -- d + -- comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b ) → ( K Sets A * ↓ U) [ ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ≈ preinitialArrow PI ] comm13 a b f = let open ≈-Reasoning A in begin @@ -309,7 +322,7 @@ arrow f o arrow ( preinitialArrow PI {{!!}}) ≈⟨ {!!} ⟩ arrow ( preinitialArrow PI {{!!}} ) - ∎ + ∎ comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [ FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ] comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin