Mercurial > hg > Members > kono > Proof > category
changeset 483:265f13adf93b
add NIC
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Mar 2017 10:51:12 +0900 |
| parents | fd752ad25ac0 |
| children | fcae3025d900 |
| files | freyd1.agda |
| diffstat | 1 files changed, 45 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd1.agda Sat Mar 11 01:35:06 2017 +0900 +++ b/freyd1.agda Sat Mar 11 10:51:12 2017 +0900 @@ -32,11 +32,14 @@ } } open Complete - open CommaObj open CommaHom open Limit +-- F : A → C +-- G : A → C +-- + FIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I A FIA {I} Γ = record { FObj = λ x → obj (FObj Γ x ) ; @@ -53,7 +56,6 @@ id1 A (obj (FObj Γ x)) ∎ - 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 { @@ -64,6 +66,47 @@ 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 ) +NIC : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) + (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) ) +NIC {I} Γ c ta = record { + TMap = λ x → FMap G (TMap ta x ) + ; isNTrans = record { commute = comm1 } + } where + comm1 : {a b : Obj I} {f : Hom I a b} → + C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] + comm1 {a} {b} {f} = let open ≈-Reasoning (C) in begin + FMap (G ○ FIA Γ) f o FMap G (TMap ta a) + ≈↑⟨ distr G ⟩ + FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] ) + ≈⟨ fcong G ( nat ta ) ⟩ + FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] ) + ≈⟨ distr G ⟩ + FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f ) + ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩ + FMap G (TMap ta b) o id1 C (FObj G (obj c)) + ≈⟨⟩ + FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f + ∎ + + +NIComma : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) + (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) ) → NTrans I CommaCategory ( K CommaCategory I c ) Γ +NIComma {I} Γ c ta = record { + TMap = λ x → record { + arrow = TMap ta x + ; comm = comm1 x + } + ; isNTrans = record { commute = {!!} } + } where + comm1 : ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] + comm1 x = let open ≈-Reasoning (C) in begin + FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) + ≈⟨ {!!} ⟩ + hom (FObj Γ x) o FMap F (TMap ta x) + ∎ + + + commaLimit : { I : Category c₁ c₂ ℓ } → ( Complete A I) → ( Γ : Functor I CommaCategory ) → Obj CommaCategory commaLimit {I} comp Γ = record { obj = limit-c comp (FIA Γ)