Mercurial > hg > Members > kono > Proof > category
changeset 511:b9c086bda3cc
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 19 Mar 2017 13:28:12 +0900 |
| parents | 5eb4b69bf541 |
| children | f19dab948e39 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 26 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Sun Mar 19 11:14:49 2017 +0900 +++ b/SetsCompleteness.agda Sun Mar 19 13:28:12 2017 +0900 @@ -122,7 +122,19 @@ ek=h {d} {h} {eq} = refl uniqueness : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h eq ≈ k' ] - uniqueness {d} refl = extensionality Sets ( λ x → {!!} ) + uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ x → + begin + k h fh=gh x + ≡⟨ {!!} ⟩ + elem (h x) ( ≡-cong ( λ y → y x ) fh=gh ) + ≡⟨ {!!} ⟩ + elem (equ (k' x)) {!!} + ≡⟨ {!!} ⟩ + k' x + ∎ + ) where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning open Functor @@ -163,19 +175,19 @@ open Slimit -SetsLimit : { c₂ : Level} → Limit Sets Sets Γ -SetsLimit { c₂} = record { - a0 = Slimit (Obj Sets) {!!} ΓMap - ; t0 = record { - TMap = λ i → λ lim → s-t0 lim {!!} - ; isNTrans = record { commute = {!!} } - } - ; isLimit = record { - limit = {!!} - ; t0f=t = {!!} - ; limit-uniqueness = {!!} - } - } where +-- SetsLimit : { c₂ : Level} → Limit Sets Sets Γ +-- SetsLimit { c₂} = record { +-- a0 = Slimit (Obj Sets) {!!} ΓMap +-- ; t0 = record { +-- TMap = λ i → λ lim → s-t0 lim {!!} +-- ; isNTrans = record { commute = {!!} } +-- } +-- ; isLimit = record { +-- limit = {!!} +-- ; t0f=t = {!!} +-- ; limit-uniqueness = {!!} +-- } +-- } where -- comm1 : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → s-t0 lim ? ) ] ≈ -- Sets [ (λ lim → s-t0 lim ?) o FMap (K Sets Sets (Slimit (Obj Sets) ΓObj (λ {a} {b} → ΓMap))) f ] ] -- comm1 {a} {b} {f} = {!!}