Mercurial > hg > Members > kono > Proof > category
changeset 633:37fa9d3fab8c
add equalizer
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2017 08:55:11 +0900 |
| parents | d36ff598a063 |
| children | 5b0286e3aa32 |
| files | freyd2.agda |
| diffstat | 1 files changed, 12 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Tue Jun 27 10:29:06 2017 +0900 +++ b/freyd2.agda Wed Jun 28 08:55:11 2017 +0900 @@ -240,7 +240,7 @@ --- K{*}↓U has preinitial full subcategory then U is representable +-- A is complete and K{*}↓U has preinitial full subcategory then U is representable open SmallFullSubcategory open PreInitial @@ -292,14 +292,23 @@ preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ] ≈ Sets [ ub a x o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ] preinitComm a x = comm (piArrow (ob a x )) + equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g + equ f g = Complete.isEqualizer comp f g + ep : {a b : Obj A} → {f g : Hom A a b} → Obj A + ep {a} {b} {f} {g} = equalizer-p comp f g + 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 )) 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 arrow ( ( K Sets A * ↓ U) [ f o preinitialArrow PI ] ) ≈⟨⟩ - arrow f o arrow ( preinitialArrow PI ) + arrow f o arrow ( preinitialArrow PI {{!!}}) ≈⟨ {!!} ⟩ - 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 ))) ]