Mercurial > hg > Members > kono > Proof > category

comparison freyd.agda @ 484:fcae3025d900

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Limit pu a0 and t0 in record definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Mar 2017 16:38:08 +0900
parents 65e6906782bb
children c257347a27f3
comparison
equal deleted inserted replaced
483:265f13adf93b 484:fcae3025d900
47 open IsEqualizer 47 open IsEqualizer
48 48
49 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 49 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
50 (comp : Complete A A) 50 (comp : Complete A A)
51 (SFS : SmallFullSubcategory A ) → 51 (SFS : SmallFullSubcategory A ) →
52 (PI : PreInitial A (SFSF SFS )) → { a0 : Obj A } → HasInitialObject A (limit-c comp (SFSF SFS)) 52 (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
53 initialFromPreInitialFullSubcategory A comp SFS PI = record { 53 initialFromPreInitialFullSubcategory A comp SFS PI = record {
54 initial = initialArrow ; 54 initial = initialArrow ;
55 uniqueness = λ a f → lemma1 a f 55 uniqueness = λ a f → lemma1 a f
56 } where 56 } where
57 F : Functor A A 57 F : Functor A A
58 F = SFSF SFS 58 F = SFSF SFS
59 FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 59 FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b
60 FMap← = SFSFMap← SFS 60 FMap← = SFSFMap← SFS
61 a0 : Obj A 61 a00 : Obj A
62 a0 = limit-c comp F 62 a00 = limit-c comp F
63 lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ) 63 lim : ( Γ : Functor A A ) → Limit A A Γ
64 lim Γ = isLimit comp Γ 64 lim Γ = isLimit comp Γ
65 u : NTrans A A (K A A a0) F 65 u : NTrans A A (K A A a00) F
66 u = T0 ( lim F ) 66 u = t0 ( lim F )
67 equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g 67 equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g
68 equ f g = Complete.isEqualizer comp f g 68 equ f g = Complete.isEqualizer comp f g
69 ep : {a b : Obj A} → {f g : Hom A a b} → Obj A 69 ep : {a b : Obj A} → {f g : Hom A a b} → Obj A
70 ep {a} {b} {f} {g} = equalizer-p comp f g 70 ep {a} {b} {f} {g} = equalizer-p comp f g
71 ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a 71 ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a
72 ee {a} {b} {f} {g} = equalizer-e comp f g 72 ee {a} {b} {f} {g} = equalizer-e comp f g
73 f : {a : Obj A} → Hom A a0 (FObj F (preinitialObj PI {a} ) ) 73 f : {a : Obj A} → Hom A a00 (FObj F (preinitialObj PI {a} ) )
74 f {a} = TMap u (preinitialObj PI {a} ) 74 f {a} = TMap u (preinitialObj PI {a} )
75 initialArrow : ∀( a : Obj A ) → Hom A a0 a 75 initialArrow : ∀( a : Obj A ) → Hom A a00 a
76 initialArrow a = A [ preinitialArrow PI {a} o f ] 76 initialArrow a = A [ preinitialArrow PI {a} o f ]
77 equ-fi : { a : Obj A} → {f' : Hom A a0 a} → 77 equ-fi : { a : Obj A} → {f' : Hom A a00 a} →
78 IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f' 78 IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f'
79 equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f' 79 equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f'
80 e=id : {e : Hom A a0 a0} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a0 ] 80 e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u c o e ] ≈ TMap u c ] ) → A [ e ≈ id1 A a00 ]
81 e=id {e} uce=uc = let open ≈-Reasoning (A) in 81 e=id {e} uce=uc = let open ≈-Reasoning (A) in
82 begin 82 begin
83 e 83 e
84 ≈↑⟨ limit-uniqueness (lim F) e ( λ {i} → uce=uc ) ⟩ 84 ≈↑⟨ limit-uniqueness (lim F) e ( λ {i} → uce=uc ) ⟩
85 limit (lim F) a0 u 85 limit (lim F) a00 u
86 ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( λ {i} → idR ) ⟩ 86 ≈⟨ limit-uniqueness (lim F) (id1 A a00) ( λ {i} → idR ) ⟩
87 id1 A a0 87 id1 A a00
88 ∎ 88 ∎
89 kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a0} → A [ A [ TMap u c o 89 kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o
90 A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ] 90 A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]
91 ≈ TMap u c ] 91 ≈ TMap u c ]
92 kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in 92 kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in
93 begin 93 begin
94 TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) )) 94 TMap u c o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI) ))
97 ≈⟨ assoc ⟩ 97 ≈⟨ assoc ⟩
98 (TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI) 98 (TMap u c o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI)
99 ≈↑⟨ car ( full→ SFS ) ⟩ 99 ≈↑⟨ car ( full→ SFS ) ⟩
100 FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI) 100 FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
101 ≈⟨ nat u ⟩ 101 ≈⟨ nat u ⟩
102 TMap u c o FMap (K A A a0) (FMap← (TMap u c o p o preinitialArrow PI)) 102 TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI))
103 ≈⟨⟩ 103 ≈⟨⟩
104 TMap u c o id1 A a0 104 TMap u c o id1 A a00
105 ≈⟨ idR ⟩ 105 ≈⟨ idR ⟩
106 TMap u c 106 TMap u c
107 ∎ 107 ∎
108 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 ] 108 kfuc=1 : {k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ]
109 kfuc=1 {k1} {p} = e=id ( kfuc=uc ) 109 kfuc=1 {k1} {p} = e=id ( kfuc=uc )
110 -- if equalizer has right inverse, f = g 110 -- if equalizer has right inverse, f = g
111 lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) 111 lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b )
112 {e : Hom A c a } {e' : Hom A a c } ( equ : IsEqualizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] ) 112 {e : Hom A c a } {e' : Hom A a c } ( equ : IsEqualizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
113 → A [ f ≈ g ] 113 → A [ f ≈ g ]
127 ≈⟨ cdr inv-e ⟩ 127 ≈⟨ cdr inv-e ⟩
128 g o id1 A a 128 g o id1 A a
129 ≈⟨ idR ⟩ 129 ≈⟨ idR ⟩
130 g 130 g
131 ∎ 131 ∎
132 lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ] 132 lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ]
133 lemma1 a f' = let open ≈-Reasoning (A) in 133 lemma1 a f' = let open ≈-Reasoning (A) in
134 sym ( 134 sym (
135 begin 135 begin
136 initialArrow a 136 initialArrow a
137 ≈⟨⟩ 137 ≈⟨⟩
138 preinitialArrow PI {a} o f 138 preinitialArrow PI {a} o f
139 ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a0} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) 139 ≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi )
140 (kfuc=1 {ep} {ee} ) ⟩ 140 (kfuc=1 {ep} {ee} ) ⟩
141 f' 141 f'
142 ∎ ) 142 ∎ )
143 143
144 144