Mercurial > hg > Members > kono > Proof > category
changeset 961:0719e76cd3b8
... locality
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Feb 2021 21:21:30 +0900 |
| parents | 062974e39cc7 |
| children | 9cf91e773517 |
| files | src/equalizer.agda |
| diffstat | 1 files changed, 33 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/src/equalizer.agda Sun Feb 21 21:39:01 2021 +0900 +++ b/src/equalizer.agda Mon Feb 22 21:21:30 2021 +0900 @@ -332,8 +332,9 @@ -- Bourroni equations gives an Equalizer -- -lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g -lemma-equ2 {a} {b} f g bur = record { +lemma-equ2 : {a b : Obj A} (f g : Hom A a b) → ( bur : Burroni ) → (≡←≈ : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g ) + → IsEqualizer A {equ bur f g} {a} {b} (α bur f g ) f g +lemma-equ2 {a} {b} f g bur ≡←≈ = record { fe=ge = fe=ge1 ; k = k1 ; ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; @@ -362,6 +363,15 @@ ≈⟨ idR ⟩ h ∎ + +-- e f +-- c -------→ a ---------→ b +-- ^ . ---------→ +-- | . g +-- |k . +-- | . h +-- d + uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → A [ A [ (α bur f g ) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] uniqueness1 {d} {h} {eq} {k'} ek=h = @@ -369,7 +379,7 @@ k1 {d} h eq ≈⟨⟩ γ bur f g h o δ bur (f o h) (g o h) eq - ≈⟨ cdr {!!} ⟩ + ≈⟨ cdr lemma1 ⟩ γ bur f g h o (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))) ≈⟨ car {!!} ⟩ (γ bur f g (α bur f g o k' ) o p ) o (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))) @@ -385,12 +395,30 @@ k' ∎ where open ≈-Reasoning A + lemma0 : A [ A [ f o ( α bur f g o k' ) ] ≈ A [ g o ( α bur f g o k' ) ] ] + lemma0 = begin f o ( α bur f g o k' ) ≈⟨ cdr ek=h ⟩ f o h ≈⟨ eq ⟩ + g o h ≈↑⟨ cdr ek=h ⟩ + g o ( α bur f g o k' ) ∎ p : Hom A (equ bur (f o h) (g o h)) (equ bur (f o ( α bur f g o k'))(g o ( α bur f g o k'))) - p = γ bur (f o ( α bur f g o k')) (g o ( α bur f g o k')) (id1 A _) o δ bur {!!} {!!} {!!} o {!!} + p = β bur (f o ( α bur f g o k')) (g o ( α bur f g o k')) (α bur (f o h) (g o h)) (f1=g1 lemma0 _) q : Hom A (equ bur (f o ( α bur f g o k'))(g o ( α bur f g o k'))) (equ bur (f o h) (g o h)) - q = γ bur (f o h) (g o h) (id1 A _) o δ bur {!!} {!!} {!!} o {!!} + q = β bur (f o h) (g o h) (α bur (f o ( α bur f g o k')) (g o ( α bur f g o k'))) (f1=g1 eq _) pq=1 : A [ A [ p o q ] ≈ id1 A _ ] pq=1 = {!!} + lemma2 : A [ (p o (δ bur (f o h) (g o h) eq )) ≈ δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )) ] + lemma2 = {!!} + lemma1 : A [ δ bur (f o h) (g o h) eq ≈ (q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))) ] + lemma1 = begin + δ bur (f o h) (g o h) eq + ≈⟨ {!!} ⟩ + ((γ bur ( f o h)( g o h) (α bur (f o (α bur f g o k')) (g o (α bur f g o k')))) + o δ bur ((f o h) o α bur (f o ( α bur f g o k') ) (g o ( α bur f g o k')) ) + ((g o h) o α bur (f o ( α bur f g o k') ) (g o ( α bur f g o k')) ) + (f1=g1 eq _ ) ) + o (δ bur (f o (α bur f g o k')) (g o (α bur f g o k')) (f1=gh (b1 bur f g))) + ≈⟨⟩ + q o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))) + ∎ -- end