Mercurial > hg > Members > kono > Proof > category
diff freyd1.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 | 372205f40ab0 |
| children |
line wrap: on
line diff
--- a/freyd1.agda Sun Nov 12 01:29:47 2017 +0900 +++ b/freyd1.agda Sun Nov 12 09:56:40 2017 +0900 @@ -51,13 +51,13 @@ --- Get a nat on A from a nat on CommaCategory -- NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) - (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ) + (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K I CommaCategory c ) Γ ) → NTrans I A ( K I A (obj c) ) (FIA Γ) NIA {I} Γ c ta = record { TMap = λ x → arrow (TMap ta x ) ; isNTrans = record { commute = comm1 } } where comm1 : {a b : Obj I} {f : Hom I a b} → - A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ] + A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K I A (obj c)) f ] ] comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) @@ -67,19 +67,19 @@ -- LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) - → Limit C I (G ○ (FIA Γ)) + → ( glimit : LimitPreserve I A C G ) + → Limit I C (G ○ (FIA Γ)) LimitC {I} comp Γ glimit = plimit glimit (climit comp (FIA Γ)) tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) + → NTrans I C (K I C (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) tu {I} comp Γ = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where commute : {a b : Obj I} {f : Hom I a b} → C [ C [ FMap (G ○ (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ] - ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ] + ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ] ] commute {a} {b} {f} = let open ≈-Reasoning (C) in begin FMap (G ○ (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a )) ≈⟨⟩ @@ -95,7 +95,7 @@ ≈⟨⟩ hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ) f o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ))) ))) ⟩ - hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] )) + hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K I A (a0 (climit comp (FIA Γ)))) f ] )) ≈⟨⟩ hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] )) ≈⟨ cdr ( distr F ) ⟩ @@ -103,14 +103,14 @@ ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩ hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ)))) ≈⟨ assoc ⟩ - ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f + ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ∎ limitHom : { I : Category c₁ c₂ ℓ } → (comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) + → ( glimit : LimitPreserve I A C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) )) limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) + → ( glimit : LimitPreserve I A C G ) → Obj CommaCategory commaLimit {I} comp Γ glimit = record { obj = limit-c comp (FIA Γ) @@ -119,8 +119,8 @@ commaNat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) - → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit)) Γ + → ( glimit : LimitPreserve I A C G ) + → NTrans I CommaCategory (K I CommaCategory (commaLimit {I} comp Γ glimit)) Γ commaNat {I} comp Γ glimit = record { TMap = λ x → record { arrow = TMap ( limit-u comp (FIA Γ ) ) x @@ -129,10 +129,10 @@ ; isNTrans = record { commute = comm2 } } where comm1 : (x : Obj I ) → - C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] + C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] comm1 x = let open ≈-Reasoning (C) in begin - FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) + FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ≈⟨⟩ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) ≈⟨⟩ @@ -146,23 +146,23 @@ ∎ comm2 : {a b : Obj I} {f : Hom I a b} → CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ] - ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ] + ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K I CommaCategory (commaLimit comp Γ glimit)) f ] ] comm2 {a} {b} {f} = let open ≈-Reasoning (A) in begin FMap (FIA Γ) f o TMap (limit-u comp (FIA Γ)) a ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ))) ⟩ - TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f + TMap (limit-u comp (FIA Γ)) b o FMap (K I A (limit-c comp (FIA Γ))) f ∎ gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) - → (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → - NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) + → (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → + NTrans I C (K I C (FObj F (obj a))) (G ○ FIA Γ) gnat {I} Γ a t = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ] ; isNTrans = record { commute = λ {x y f} → comm1 x y f } } where comm1 : (x y : Obj I) (f : Hom I x y ) → C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ] - ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K C I (FObj F (obj a))) f ] ] + ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K I C (FObj F (obj a))) f ] ] comm1 x y f = let open ≈-Reasoning (C) in begin FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x )) ≈⟨⟩ @@ -180,12 +180,12 @@ ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A))) ⟩ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ≈↑⟨ idR ⟩ - ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K C I (FObj F (obj a))) f + ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K I C (FObj F (obj a))) f ∎ comma-a0 : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) comma-a0 {I} comp Γ glimit a t = record { arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) ; comm = comm1 @@ -243,7 +243,7 @@ ∎ comma-t0f=t : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) (i : Obj I ) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) (i : Obj I ) → CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ] comma-t0f=t {I} comp Γ glimit a t i = let open ≈-Reasoning (A) in begin TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) @@ -252,7 +252,7 @@ ∎ comma-uniqueness : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) + → ( glimit : LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a) Γ ) → ( f : Hom CommaCategory a (commaLimit comp Γ glimit)) → ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat { I} comp Γ glimit ) i o f ] ≈ TMap t i ] ) → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] @@ -263,9 +263,9 @@ ∎ hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) - → ( glimit : LimitPreserve A I C G ) + → ( glimit : LimitPreserve I A C G ) → ( Γ : Functor I CommaCategory ) - → Limit CommaCategory I Γ + → Limit I CommaCategory Γ hasLimit {I} comp glimit Γ = record { a0 = commaLimit {I} comp Γ glimit ; t0 = commaNat { I} comp Γ glimit ;