Mercurial > hg > Members > kono > Proof > category
diff freyd2.agda @ 693:984518c56e96
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 13 Nov 2017 12:39:30 +0900 |
| parents | 917e51be9bbf |
| children | 7a6ee564e3a8 |
line wrap: on
line diff
--- a/freyd2.agda Sun Nov 12 10:01:06 2017 +0900 +++ b/freyd2.agda Mon Nov 13 12:39:30 2017 +0900 @@ -12,19 +12,20 @@ ---------- -- +-- A is locally small complete and K{*}↓U has preinitial full subcategory, U is an adjoint functor +-- -- a : Obj A -- U : A → Sets -- U ⋍ Hom (a,-) -- --- maybe this is a part of local smallness -postulate ≈-≡ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y +-- A is localy small +postulate ≡←≈ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y import Relation.Binary.PropositionalEquality -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - ---- -- -- Hom ( a, - ) is Object mapping in Yoneda Functor @@ -48,10 +49,10 @@ } } where lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL + lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≡←≈ A idL lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≡←≈ A ( begin A [ A [ g o f ] o x ] ≈↑⟨ assoc ⟩ A [ g o A [ f o x ] ] @@ -59,7 +60,7 @@ ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) ∎ ) lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≡←≈ A ( begin A [ f o x ] ≈⟨ resp refl-hom eq ⟩ A [ g o x ] @@ -119,7 +120,7 @@ FMap Γ f o TMap t a₁ x ≈⟨⟩ ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x - ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ + ≈⟨ ≈←≡ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x ≈⟨⟩ ( TMap t b₁ * id1 Sets a ) x @@ -135,7 +136,7 @@ ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) (i : Obj I) → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] - t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin + t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≡←≈ A ( begin ( Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x ≈⟨⟩ FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) @@ -151,7 +152,7 @@ limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → Sets [ ψ a t ≈ f ] - limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin + limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≡←≈ A ( begin ψ a t x ≈⟨⟩ FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) @@ -159,7 +160,7 @@ limit (isLimit lim) b (ta a x t ) o id1 A b ≈⟨ idR ⟩ limit (isLimit lim) b (ta a x t ) - ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ + ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≈←≡ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ f x ∎ )) @@ -191,7 +192,7 @@ initObj : Obj (K A Sets * ↓ Yoneda A a) initObj = record { obj = a ; hom = λ x → id1 A a } comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x - comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin + comm2 b OneObj = let open ≈-Reasoning A in ≡←≈ A ( begin ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj ≈⟨⟩ FMap (Yoneda A a) (hom b OneObj) (id1 A a) @@ -228,7 +229,7 @@ ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) ≈⟨⟩ ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj - ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ + ≈⟨ ≈←≡ ( cong (λ k → k OneObj ) (comm f )) ⟩ ( Sets [ hom b o FMap (K A Sets *) (arrow f) ] ) OneObj ≈⟨⟩ hom b OneObj @@ -294,7 +295,7 @@ A [ f o arrow (initial In (ob A U a y)) ] ≡⟨⟩ A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ] - ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K A Sets * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ + ≡⟨ ≡←≈ A ( uniqueness In {ob A U b (FMap U f y) } (( K A Sets * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ arrow (initial In (ob A U b (FMap U f y) )) ≡⟨⟩ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y @@ -342,7 +343,7 @@ → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K A Sets *) y ] ) z iso0 x y OneObj = refl iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] - iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin + iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≡←≈ A ( begin ( Sets [ tmap1 x o tmap2 x ] ) y ≈⟨⟩ arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) @@ -397,7 +398,7 @@ B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ] unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin arrow (solution f) - ≈↑⟨ ≡-≈ ( cong (λ k → arrow (solution k)) ( ≈-≡ B ugη=f )) ⟩ + ≈↑⟨ ≈←≡ ( cong (λ k → arrow (solution k)) ( ≡←≈ B ugη=f )) ⟩ arrow (solution (B [ FMap U g o tmap-η a ] )) ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ g