Mercurial > hg > Members > kono > Proof > category
changeset 642:53f2a11474ee
on going ..
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 03 Jul 2017 08:41:01 +0900 |
| parents | c65d08d85092 |
| children | 5eb746702732 |
| files | freyd2.agda |
| diffstat | 1 files changed, 11 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Mon Jul 03 07:26:58 2017 +0900 +++ b/freyd2.agda Mon Jul 03 08:41:01 2017 +0900 @@ -299,10 +299,19 @@ ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i} ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where + revUub : (pi : FObj U (obj (preinitialObj PI)) ) → pi ≡ (hom (preinitialObj PI) OneObj) + revUub _ = {!!} + revU' : (a : Obj (K Sets A * ↓ U)) + → Sets [ Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) o hom (preinitialObj PI) ] ≈ hom a ] + revU' a = let open ≈-Reasoning Sets in begin + FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) o hom (preinitialObj PI) + ≈⟨ comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ⟩ + hom a + ∎ revU : (a : Obj (K Sets A * ↓ U)) → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ] - revU a = extensionality Sets ( λ (pi : FObj U (obj (preinitialObj PI)) ) → ( begin - FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) pi + revU a = extensionality Sets ( λ (upi : FObj U (obj (preinitialObj PI)) ) → ( begin + FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) upi ≡⟨ {!!} ⟩ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj) ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩