Mercurial > hg > Members > kono > Proof > category
changeset 679:20bdd2f5f708
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Nov 2017 16:33:37 +0900 |
| parents | 867ea41b331c |
| children | 5d894993477f |
| files | pullback.agda |
| diffstat | 1 files changed, 32 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Sun Nov 05 13:22:59 2017 +0900 +++ b/pullback.agda Sun Nov 05 16:33:37 2017 +0900 @@ -409,34 +409,45 @@ equ = isEqualizer ( equ-ε prod eqa ) proj = pi ( prod (FObj Γ) ) prodΓ = isIProduct ( prod (FObj Γ) ) - open import Relation.Binary.Core - import Relation.Binary.PropositionalEquality - postulate extensionality : {c : Level} {U : Set c} {x y : Obj A } {f g : U → Hom A x y } → ( ∀ (u : U) → A [ f u ≈ g u ] ) → ( λ u → f u ) ≡ ( λ u → g u ) - comm : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → - A [ A [ iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ]) - o iproduct prodΓ (TMap t) ] - ≈ A [ iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u)) - o iproduct prodΓ (TMap t) ] ] - comm a t = let open ≈-Reasoning (A) in begin - iproduct (isIProduct (prod Fcod)) (λ u → ( FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u))) o iproduct prodΓ (TMap t) - ≈⟨ car ( ip-cong (isIProduct (prod Fcod)) ( extensionality ( λ u → begin - FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) - ≈⟨ ? ⟩ - pi (prod (FObj Γ)) (hom-k u) - ∎ - ))) ⟩ - iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u)) o iproduct prodΓ (TMap t) + f : Hom A p0 (iprod (prod Fcod)) + f = (iproduct (isIProduct (prod Fcod)) (λ u → pi (prod (FObj Γ)) (hom-k u ))) + g : Hom A p0 (iprod (prod Fcod)) + g = (iproduct (isIProduct (prod Fcod)) (λ u → A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u ) ] )) + comm1 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod) + → A [ A [ FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ] ≈ pi (prod (FObj Γ)) (hom-k u) ] + comm1 a t u = let open ≈-Reasoning (A) in begin + FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) + ≈⟨ {!!} ⟩ + FMap Γ (hom u) o ( TMap t (hom-j u) o {!!} ) + ≈⟨ assoc ⟩ + (FMap Γ (hom u) o TMap t (hom-j u) ) o {!!} + ≈⟨ car (IsNTrans.commute (isNTrans t )) ⟩ + (TMap t (hom-k u) o id1 A a ) o {!!} + ≈⟨ car idR ⟩ + TMap t (hom-k u) o {!!} + ≈⟨ {!!} ⟩ + pi (prod (FObj Γ)) (hom-k u) + ∎ + comm2 : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → (u : homprod {c₁} ) + → A [ A [ FMap Γ (hom u) o TMap t (hom-j u) ] ≈ A [ TMap t (hom-k u) o id1 A a ] ] + comm2 a t u = IsNTrans.commute (isNTrans t ) + fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → + A [ A [ g o iproduct prodΓ (TMap t) ] ≈ A [ f o iproduct prodΓ (TMap t) ] ] + fh=gh a t = let open ≈-Reasoning (A) in begin + g o iproduct prodΓ (TMap t) + ≈⟨ car ( ip-cong (isIProduct (prod Fcod)) (comm1 a t ) ) ⟩ + f o iproduct prodΓ (TMap t) ∎ limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim - limit1 a t = let open ≈-Reasoning (A) in k equ (iproduct prodΓ (TMap t) ) ( comm a t ) + limit1 a t = k equ (iproduct prodΓ (TMap t) ) ( fh=gh a t ) t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → A [ A [ TMap (limit-ε prod eqa ) i o limit1 a t ] ≈ TMap t i ] t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin TMap (limit-ε prod eqa ) i o limit1 a t ≈⟨⟩ - ( ( proj i ) o e ) o k equ (iproduct prodΓ (TMap t) ) (comm a t) + ( ( proj i ) o e ) o k equ (iproduct prodΓ (TMap t) ) (fh=gh a t) ≈↑⟨ assoc ⟩ - proj i o ( e o k equ (iproduct prodΓ (TMap t) ) (comm a t ) ) + proj i o ( e o k equ (iproduct prodΓ (TMap t) ) (fh=gh a t ) ) ≈⟨ cdr ( ek=h equ) ⟩ proj i o iproduct prodΓ (TMap t) ≈⟨ pif=q prodΓ ⟩ @@ -448,7 +459,7 @@ limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin limit1 a t ≈⟨⟩ - k equ (iproduct prodΓ (TMap t) ) (comm a t) + k equ (iproduct prodΓ (TMap t) ) (fh=gh a t) ≈⟨ IsEqualizer.uniqueness equ ( begin e o f ≈↑⟨ ip-uniqueness prodΓ ⟩