Mercurial > hg > Members > kono > Proof > category
diff freyd.agda @ 484:fcae3025d900
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 |
line wrap: on
line diff
--- a/freyd.agda Sat Mar 11 10:51:12 2017 +0900 +++ b/freyd.agda Sat Mar 11 16:38:08 2017 +0900 @@ -49,7 +49,7 @@ initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A A) (SFS : SmallFullSubcategory A ) → - (PI : PreInitial A (SFSF SFS )) → { a0 : Obj A } → HasInitialObject A (limit-c comp (SFSF SFS)) + (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS)) initialFromPreInitialFullSubcategory A comp SFS PI = record { initial = initialArrow ; uniqueness = λ a f → lemma1 a f @@ -58,35 +58,35 @@ F = SFSF SFS FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b FMap← = SFSFMap← SFS - a0 : Obj A - a0 = limit-c comp F - lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ) + a00 : Obj A + a00 = limit-c comp F + lim : ( Γ : Functor A A ) → Limit A A Γ lim Γ = isLimit comp Γ - u : NTrans A A (K A A a0) F - u = T0 ( lim F ) + u : NTrans A A (K A A a00) F + u = t0 ( lim F ) equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g equ f g = Complete.isEqualizer comp f g ep : {a b : Obj A} → {f g : Hom A a b} → Obj A ep {a} {b} {f} {g} = equalizer-p comp f g ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a ee {a} {b} {f} {g} = equalizer-e comp f g - f : {a : Obj A} → Hom A a0 (FObj F (preinitialObj PI {a} ) ) + f : {a : Obj A} → Hom A a00 (FObj F (preinitialObj PI {a} ) ) f {a} = TMap u (preinitialObj PI {a} ) - initialArrow : ∀( a : Obj A ) → Hom A a0 a + initialArrow : ∀( a : Obj A ) → Hom A a00 a initialArrow a = A [ preinitialArrow PI {a} o f ] - equ-fi : { a : Obj A} → {f' : Hom A a0 a} → + equ-fi : { a : Obj A} → {f' : Hom A a00 a} → IsEqualizer A ee ( A [ preinitialArrow PI {a} o f ] ) f' equ-fi {a} {f'} = equ ( A [ preinitialArrow PI {a} o f ] ) f' - 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 ] + 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 ] e=id {e} uce=uc = let open ≈-Reasoning (A) in begin e ≈↑⟨ limit-uniqueness (lim F) e ( λ {i} → uce=uc ) ⟩ - limit (lim F) a0 u - ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( λ {i} → idR ) ⟩ - id1 A a0 + limit (lim F) a00 u + ≈⟨ limit-uniqueness (lim F) (id1 A a00) ( λ {i} → idR ) ⟩ + id1 A a00 ∎ - kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a0} → A [ A [ TMap u c o + kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ] ≈ TMap u c ] kfuc=uc {c} {k1} {p} = let open ≈-Reasoning (A) in @@ -99,13 +99,13 @@ ≈↑⟨ 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 a0) (FMap← (TMap u c o p o preinitialArrow PI)) + TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI)) ≈⟨⟩ - TMap u c o id1 A a0 + TMap u c o id1 A a00 ≈⟨ 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 : Obj A} → {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ] kfuc=1 {k1} {p} = e=id ( kfuc=uc ) -- if equalizer has right inverse, f = g lemma2 : (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) @@ -129,14 +129,14 @@ ≈⟨ idR ⟩ g ∎ - lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ] + lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ] lemma1 a f' = let open ≈-Reasoning (A) in sym ( begin initialArrow a ≈⟨⟩ preinitialArrow PI {a} o f - ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a0} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) + ≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o f ]} {f'} } (equ-fi ) (kfuc=1 {ep} {ee} ) ⟩ f' ∎ )