Mercurial > hg > Members > kono > Proof > category

comparison limit-to.agda @ 352:f589e71875ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Dec 2014 22:16:20 +0900
parents 1306fbc8290b
children d255a929815f
comparison
equal deleted inserted replaced
351:1306fbc8290b 352:f589e71875ea
34 unique-obj : ∀{two : Two } → obj← ( obj two ) ≡ two 34 unique-obj : ∀{two : Two } → obj← ( obj two ) ≡ two
35 unique-obj1 : ∀{i : Obj I } → obj ( obj← i ) ≡ i 35 unique-obj1 : ∀{i : Obj I } → obj ( obj← i ) ≡ i
36 unique-map : ∀{two : Two } → map← ( map two ) ≡ two 36 unique-map : ∀{two : Two } → map← ( map two ) ≡ two
37 unique-map1 : ∀{f : Hom I (obj t0) (obj t1) } → map ( map← f ) ≡ f 37 unique-map1 : ∀{f : Hom I (obj t0) (obj t1) } → map ( map← f ) ≡ f
38 38
39
40 open Limit 39 open Limit
41 open TwoCat 40 open TwoCat
41
42 record two-Γ {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
43 (a b : Obj A) (f g : Hom A a b )
44 (two : Two) (twocat : TwoCat I two ) (Γ : Functor I A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
45 field
46 a0 : FObj Γ (obj twocat t0 ) ≡ a
47 b0 : FObj Γ (obj twocat t1 ) ≡ b
48 f0 : A [ FMap Γ (map twocat t0 ) ≈ f ]
49 g0 : A [ FMap Γ (map twocat t0 ) ≈ g ]
42 50
43 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) 51 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
44 (two : Two ) 52 (two : Two )
45 (twocat : TwoCat I two) 53 (twocat : TwoCat I two)
54 (Γ : Functor I A)
46 (lim : ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness 55 (lim : ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
47 → {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g 56 → {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
48 lim-to-equ {c₁} A I two twocat lim {a} {b} {c} f g e fe=ge = record { 57 lim-to-equ {c₁} A I two twocat Γ lim {a} {b} {c} f g e fe=ge = record {
49 fe=ge = fe=ge 58 fe=ge = fe=ge
50 ; k = λ {d} h fh=gh → k {d} h fh=gh 59 ; k = λ {d} h fh=gh → k {d} h fh=gh
51 ; ek=h = λ {d} {h} {fh=gh} → {!!} 60 ; ek=h = λ {d} {h} {fh=gh} → {!!}
52 ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!} 61 ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
53 } where 62 } where
54 Γobj : Two {c₁} → Obj A
55 Γobj t0 = a
56 Γobj t1 = b
57 Γmap : Two {c₁} → Hom A a b
58 Γmap t0 = f
59 Γmap t1 = g
60 Γ : Functor I A
61 Γ = record {
62 FObj = λ x → Γobj (obj← twocat x) ;
63 FMap = λ f → {!!} ;
64 isFunctor = record {
65 ≈-cong = {!!} ;
66 identity = {!!} ;
67 distr = {!!}
68 }
69 }
70 nat : (d : Obj A) → NTrans I A (K A I d) Γ 63 nat : (d : Obj A) → NTrans I A (K A I d) Γ
71 nat d = record { 64 nat d = record {
72 TMap = λ x → {!!} ; 65 TMap = λ x → {!!} ;
73 isNTrans = record { 66 isNTrans = record {
74 commute = {!!} 67 commute = {!!}