Mercurial > hg > Members > kono > Proof > category
view freyd1.agda @ 643:5eb746702732
add more lemma
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 03 Jul 2017 12:20:26 +0900 |
| parents | 5c7908202d5a |
| children | 372205f40ab0 |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor A C ) where open import cat-utility open import HomReasoning open Functor open import Comma1 F G -- open import freyd CommaCategory -- we don't need this yet open import Category.Cat -- Functor composition open NTrans open Complete open CommaObj open CommaHom open Limit open IsLimit -- -- -- F : A → C -- G : A → C -- -- if A is complete and G preserve limit, Comma Category F↓G is complete -- i.e. it has limit for Γ : I → F↓G -- -- -- --- Get a functor Functor I A from a functor I CommaCategory --- FIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I A FIA {I} Γ = record { FObj = λ x → obj (FObj Γ x ) ; FMap = λ {a} {b} f → arrow (FMap Γ f ) ; isFunctor = record { identity = identity ; distr = IsFunctor.distr (isFunctor Γ) ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ) }} where identity : {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A (obj (FObj Γ x)) ] identity {x} = let open ≈-Reasoning (A) in begin arrow (FMap Γ (id1 I x)) ≈⟨ IsFunctor.identity (isFunctor Γ) ⟩ id1 A (obj (FObj Γ x)) ∎ --- 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 Γ) 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 ] ] comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta ) open LimitPreserve -- Limit on A from Γ : I → CommaCategory -- LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve A I C G ) → Limit C I (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 Γ)) 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 ] ] 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 )) ≈⟨⟩ FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a )) ≈⟨ assoc ⟩ (FMap G (arrow (FMap Γ f ) ) o hom (FObj Γ a)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) ≈⟨ car ( comm (FMap Γ f)) ⟩ (hom (FObj Γ b) o FMap F (arrow (FMap Γ f)) ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) ≈↑⟨ assoc ⟩ hom (FObj Γ b) o ( FMap F (arrow (FMap Γ f)) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) a ) ) ≈↑⟨ cdr (distr F) ⟩ hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f) o TMap (t0 ( climit comp (FIA Γ))) a ] ) ) ≈⟨⟩ 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 id1 A (limit-c comp (FIA Γ)) ] )) ≈⟨ cdr ( distr F ) ⟩ hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ)))) ≈⟨ 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 ∎ 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 Γ) )) 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 ) → Obj CommaCategory commaLimit {I} comp Γ glimit = record { obj = limit-c comp (FIA Γ) ; hom = limitHom comp Γ glimit } 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)) Γ commaNat {I} comp Γ glimit = record { TMap = λ x → record { arrow = TMap ( limit-u comp (FIA Γ ) ) x ; comm = comm1 x } ; 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 [ 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 (commaLimit comp Γ glimit) ≈⟨⟩ FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) ≈⟨⟩ TMap (t0 ( LimitC comp Γ glimit )) x o limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) ≈⟨ t0f=t ( isLimit ( LimitC comp Γ glimit ) ) ⟩ TMap (tu comp Γ) x ≈⟨⟩ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ∎ 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 ] ] 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 ∎ 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 Γ) 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 ] ] 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 )) ≈⟨⟩ FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x )) ≈⟨ assoc ⟩ (FMap G (FMap (FIA Γ) f) o ( hom (FObj Γ x))) o FMap F (TMap (NIA Γ a t) x ) ≈⟨ car ( comm (FMap Γ f) ) ⟩ ( hom (FObj Γ y) o FMap F (FMap (FIA Γ) f )) o FMap F (TMap (NIA Γ a t) x ) ≈↑⟨ assoc ⟩ hom (FObj Γ y) o ( FMap F (FMap (FIA Γ) f ) o FMap F (TMap (NIA Γ a t) x )) ≈↑⟨ cdr (distr F) ⟩ hom (FObj Γ y) o ( FMap F ( A [ FMap (FIA Γ) f o TMap (NIA Γ a t) x ]) ) ≈⟨ cdr ( fcong F ( IsNTrans.commute ( isNTrans ( NIA Γ a t )))) ⟩ hom (FObj Γ y) o ( FMap F ( A [ TMap (NIA Γ a t) y o id1 A (obj a) ]) ) ≈⟨ 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 ∎ 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) comma-a0 {I} comp Γ glimit a t = record { arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) ; comm = comm1 } where comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ] ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ] comm1 = let open ≈-Reasoning (C) in begin FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ≈↑⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin TMap (t0 (LimitC comp Γ glimit)) i o ( FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ) ≈⟨ assoc ⟩ ( TMap (t0 (LimitC comp Γ glimit)) i o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a ≈⟨⟩ ( FMap G ( TMap (limit-u comp (FIA Γ )) i ) o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a ≈↑⟨ car ( distr G ) ⟩ FMap G ( A [ TMap (limit-u comp (FIA Γ )) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) o hom a ≈⟨ car ( fcong G ( t0f=t (isLimit (climit comp (FIA Γ ))))) ⟩ FMap G (arrow (TMap t i)) o hom a ≈⟨ comm ( TMap t i) ⟩ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ≈⟨⟩ TMap (gnat Γ a t) i ∎ ) ⟩ limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) (gnat Γ a t ) ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin TMap (t0 (LimitC comp Γ glimit )) i o ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) ≈⟨ assoc ⟩ ( TMap (t0 (LimitC comp Γ glimit )) i o ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) )) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ≈⟨ car ( t0f=t ( isLimit (LimitC comp Γ glimit )) ) ⟩ TMap (tu comp Γ ) i o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ≈⟨⟩ ( hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ≈↑⟨ assoc ⟩ hom ( FObj Γ i ) o ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) ≈↑⟨ cdr ( distr F ) ⟩ hom ( FObj Γ i ) o FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ≈⟨⟩ TMap (gnat Γ a t ) i ∎ ) ⟩ limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ≈⟨⟩ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ∎ 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 ) → 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 ) ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) ) ⟩ TMap (NIA {I} Γ a t ) i ∎ 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) Γ ) → ( 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 ] comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) t=f ⟩ arrow f ∎ hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) → ( glimit : LimitPreserve A I C G ) → ( Γ : Functor I CommaCategory ) → Limit CommaCategory I Γ hasLimit {I} comp glimit Γ = record { a0 = commaLimit {I} comp Γ glimit ; t0 = commaNat { I} comp Γ glimit ; isLimit = record { limit = λ a t → comma-a0 comp Γ glimit a t ; t0f=t = λ {a t i } → comma-t0f=t comp Γ glimit a t i ; limit-uniqueness = λ {a} {t} {f} t=f → comma-uniqueness {I} comp Γ glimit a t f t=f } }