Mercurial > hg > Members > kono > Proof > category
changeset 962:9cf91e773517
give up burroni
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Feb 2021 21:31:38 +0900 |
| parents | 0719e76cd3b8 |
| children | 50d8750d32c0 |
| files | src/equalizer.agda |
| diffstat | 1 files changed, 15 insertions(+), 51 deletions(-) [+] |
line wrap: on
line diff
--- a/src/equalizer.agda Mon Feb 22 21:21:30 2021 +0900 +++ b/src/equalizer.agda Mon Feb 22 21:31:38 2021 +0900 @@ -332,9 +332,8 @@ -- Bourroni equations gives an Equalizer -- -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 { +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 { fe=ge = fe=ge1 ; k = k1 ; ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; @@ -372,54 +371,19 @@ -- | . 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 = - begin - k1 {d} h eq - ≈⟨⟩ - γ bur f g h o δ bur (f o h) (g o h) eq - ≈⟨ 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 )))) - ≈↑⟨ assoc ⟩ - γ 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 ))))) - ≈⟨ cdr assoc ⟩ - γ 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 )))) - ≈⟨ cdr (car pq=1) ⟩ - γ bur f g (α bur f g o k' ) o (id1 A _ o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g )))) - ≈⟨ cdr idL ⟩ - γ bur f g (α bur f g o k' ) o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))) - ≈⟨ b4 bur f g ⟩ - 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')) (α 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) (α 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 ))) - ∎ - + postulate + 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 = +-- begin +-- k1 {d} h eq +-- ≈⟨⟩ +-- γ bur f g h o δ bur (f o h) (g o h) eq +-- ≈⟨ ? ⟩ -- without locality, we cannot simply replace h with (α bur f g o k' +-- γ bur f g (α bur f g o k' ) o (δ bur ( f o ( α bur f g o k' )) ( g o ( α bur f g o k' )) (f1=gh (b1 bur f g ))) +-- ≈⟨ b4 bur f g ⟩ +-- k' +-- ∎ -- end