Mercurial > hg > Members > kono > Proof > category
diff freyd.agda @ 441:61550782be4a
preinital full subcategory done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Aug 2016 15:11:17 +0900 |
| parents | ff36c500962e |
| children | 87600d338337 |
line wrap: on
line diff
--- a/freyd.agda Tue Aug 30 14:22:47 2016 +0900 +++ b/freyd.agda Tue Aug 30 15:11:17 2016 +0900 @@ -81,7 +81,22 @@ kfuc=uc : {c k1 : Obj A} -> {p : Hom A k1 a0} -> A [ A [ TMap u c o A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ] ≈ TMap u c ] - kfuc=uc {k1} {c} = {!!} + kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in + begin + TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) )) + ≈⟨ cdr assoc ⟩ + TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI)) + ≈⟨ assoc ⟩ + (TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI) + ≈↑⟨ car ( full→ SFS ) ⟩ + FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI) + ≈⟨ nat u ⟩ + TMap u c o FMap (K A A (limit-c comp F)) (FMap← (TMap u c o p o preinitialArrow PI)) + ≈⟨⟩ + TMap u c o id1 A (limit-c comp F) + ≈⟨ idR ⟩ + TMap u c + ∎ kfuc=1 : {k1 : Obj A} -> {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ] kfuc=1 {k1} {p} = e=id ( kfuc=uc ) -- if equalizer has right inverse, f = g @@ -98,8 +113,7 @@ f o ( e o e' ) ≈⟨ assoc ⟩ ( f o e ) o e' - ≈⟨ car ( fe=ge equ ) ⟩ - ( g o e ) o e' + ≈⟨ car ( fe=ge equ ) ⟩ ( g o e ) o e' ≈↑⟨ assoc ⟩ g o ( e o e' ) ≈⟨ cdr inv-e ⟩