Mercurial > hg > Members > kono > Proof > category
diff freyd2.agda @ 691:917e51be9bbf
change argument of Limit and K
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 12 Nov 2017 09:56:40 +0900 |
| parents | 3d41a8edbf63 |
| children | 984518c56e96 |
line wrap: on
line diff
--- a/freyd2.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/freyd2.agda Sun Nov 12 09:56:40 2017 +0900 @@ -100,27 +100,27 @@ YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) - (Γ : Functor I A) (limita : Limit A I Γ) → - IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) + (Γ : Functor I A) (limita : Limit I A Γ) → + IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where - hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) - hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b) + hat0 : NTrans I Sets (K I Sets (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) + hat0 = LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b) haa0 : Obj Sets haa0 = FObj (Yoneda A b) (a0 lim) - ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ + ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) → NTrans I A (K I A b ) Γ ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → - A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] + A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K I A b) f ] ] commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin FMap Γ f o TMap t a₁ x ≈⟨⟩ ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ - ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x + ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x ≈⟨⟩ ( TMap t b₁ * id1 Sets a ) x ≈⟨⟩ @@ -128,15 +128,15 @@ ≈↑⟨ idR ⟩ TMap t b₁ x o id1 A b ≈⟨⟩ - TMap t b₁ x o FMap (K A I b) f + TMap t b₁ x o FMap (K I A b) f ∎ - ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) + ψ : (X : Obj Sets) ( t : NTrans I Sets (K I Sets X) (Yoneda A b ○ Γ)) → Hom Sets X (FObj (Yoneda A b) (a0 lim)) ψ 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 Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) - → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] + 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 - ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x + ( 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 )) ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] @@ -148,8 +148,8 @@ ≈⟨⟩ TMap t i x ∎ )) - limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → - ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → + 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 ψ a t x @@ -164,9 +164,9 @@ ∎ )) -YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) - (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) -YonedaFpreserveLimit A I b = record { +YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ) + (b : Obj A ) → LimitPreserve I A Sets (Yoneda A b) +YonedaFpreserveLimit I A b = record { preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim } @@ -181,14 +181,14 @@ KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) - → IsInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) + → IsInitialObject ( K A Sets * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { initial = λ b → initial0 b ; uniqueness = λ f → unique f } where commaCat : Category (c₂ ⊔ c₁) c₂ ℓ - commaCat = K Sets A * ↓ Yoneda A a - initObj : Obj (K Sets A * ↓ Yoneda A a) + commaCat = K A Sets * ↓ Yoneda A a + 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 @@ -200,13 +200,13 @@ ≈⟨ idR ⟩ hom b OneObj ∎ ) - comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ] + comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K A Sets *) (hom b OneObj) ] ] comm1 b = let open ≈-Reasoning Sets in begin FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ hom b ≈⟨⟩ - hom b o FMap (K Sets A *) (hom b OneObj) + hom b o FMap (K A Sets *) (hom b OneObj) ∎ initial0 : (b : Obj commaCat) → Hom commaCat initObj b @@ -214,12 +214,12 @@ arrow = hom b OneObj ; comm = comm1 b } -- what is comm f ? - comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) + comm-f : (b : Obj (K A Sets * ↓ (Yoneda A a))) (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] - ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ] + ≈ Sets [ hom b o FMap (K A Sets *) (arrow f) ] ] comm-f b f = comm f - unique : {b : Obj (K Sets A * ↓ Yoneda A a)} (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) - → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ] + unique : {b : Obj (K A Sets * ↓ Yoneda A a)} (f : Hom (K A Sets * ↓ Yoneda A a) initObj b) + → (K A Sets * ↓ Yoneda A a) [ f ≈ initial0 b ] unique {b} f = let open ≈-Reasoning A in begin arrow f ≈↑⟨ idR ⟩ @@ -229,7 +229,7 @@ ≈⟨⟩ ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ - ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj + ( Sets [ hom b o FMap (K A Sets *) (arrow f) ] ) OneObj ≈⟨⟩ hom b OneObj ∎ @@ -244,19 +244,19 @@ ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) - → Hom Sets (FObj (K Sets A *) b) (FObj U b) + → Hom Sets (FObj (K A Sets *) b) (FObj U b) ub A U b x OneObj = x ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) - → Obj ( K Sets A * ↓ U) + → Obj ( K A Sets * ↓ U) ob A U b x = record { obj = b ; hom = ub A U b x} fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a ) - → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) + → Hom ( K A Sets * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x } where fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y fArrowComm1 a b f x OneObj = refl fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → - Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ] + Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K A Sets *) f ] ] fArrowComm a b f x = extensionality Sets ( λ y → begin ( Sets [ FMap U f o hom (ob A U a x) ] ) y ≡⟨⟩ @@ -276,8 +276,8 @@ UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) - ( i : Obj ( K (Sets) A * ↓ U) ) - (In : IsInitialObject ( K (Sets) A * ↓ U) i ) + ( i : Obj ( K A Sets * ↓ U) ) + (In : IsInitialObject ( K A Sets * ↓ U) i ) → Representable A U (obj i) UisRepresentable A U i In = record { repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } @@ -294,7 +294,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 Sets A * ↓ 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 @@ -339,7 +339,7 @@ tmap2 b o FMap (Yoneda A (obj i)) f ∎ iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) - → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z + → ( 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 @@ -368,19 +368,19 @@ module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) (U : Functor A B ) - (i : (b : Obj B) → Obj ( K B A b ↓ U) ) - (In : (b : Obj B) → IsInitialObject ( K B A b ↓ U) (i b) ) + (i : (b : Obj B) → Obj ( K A B b ↓ U) ) + (In : (b : Obj B) → IsInitialObject ( K A B b ↓ U) (i b) ) where tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) tmap-η y = hom (i y) - sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U + sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K A B a) U sobj {a} {b} f = record {obj = b; hom = f } - solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f) + solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K A B a) U (i a) (sobj f) solution {a} {b} f = initial (In a) (sobj f) - ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) + ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K A B a ↓ U) ηf a b f = sobj ( B [ tmap-η b o f ] ) univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b)) @@ -388,7 +388,7 @@ univ {a} {b} f = let open ≈-Reasoning B in begin FMap U (arrow (solution f)) o tmap-η a ≈⟨ comm (initial (In a) (sobj f)) ⟩ - hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f))) + hom (sobj f) o FMap (K A B a) (arrow (initial (In a) (sobj f))) ≈⟨ idR ⟩ f ∎ @@ -402,7 +402,7 @@ ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ g ∎ where - comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ] + comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K A B a) g ] ] comm1 = let open ≈-Reasoning B in sym idR UM : UniversalMapping B A U