Mercurial > hg > Members > kono > Proof > category
changeset 1018:4b517d46e987
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 24 Mar 2021 23:15:22 +0900 |
| parents | 90224a662c4e |
| children | 501e016bf877 |
| files | src/CCC.agda src/CCCSets.agda src/ToposEx.agda src/equalizer.agda |
| diffstat | 4 files changed, 105 insertions(+), 104 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Tue Mar 23 17:58:57 2021 +0900 +++ b/src/CCC.agda Wed Mar 24 23:15:22 2021 +0900 @@ -186,7 +186,7 @@ -- pull back on -- -- iso ○ b --- e ⇐====⇒ b -----------→ 1 +-- e ⇐====⇒ b -----------→ 1 m ∙ f ≈ m ∙ g → f ≈ g -- | | | -- | m | | ⊤ -- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) @@ -210,54 +210,12 @@ field char-uniqueness : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ] - ker-iso : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono ))) + ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ]) ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a ker h = equalizer (Ker h) - mm : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → A [ A [ equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ] ≈ m ] - mm m mono = IsoL.L≈iso (ker-iso m mono) - fe=ge : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → A [ A [ char m mono o m ] ≈ A [ A [ ⊤ o CCC.○ c a ] o m ] ] - fe=ge {a} {b} m mono = begin - char m mono o m ≈↑⟨ cdr (mm m mono) ⟩ - char m mono o (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ assoc ⟩ - (char m mono o equalizer (Ker (char m mono))) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer (Ker (char m mono))) ) ⟩ - (( ⊤ o CCC.○ c a) o equalizer (Ker (char m mono)) ) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈↑⟨ assoc ⟩ - ( ⊤ o CCC.○ c a) o (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ cdr (mm m mono) ⟩ - ( ⊤ o CCC.○ c a) o m ∎ where open ≈-Reasoning A - ek=h : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → {d : Obj A} {h : Hom A d a} - {eq : A [ A [ char m mono o h ] ≈ A [ A [ ⊤ o CCC.○ c a ] o h ] ]} → - A [ A [ m o (A Category.o Iso.≅← (IsoL.iso-L (ker-iso m mono))) (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ] ≈ h ] - ek=h {a} {b} m mono {d} {h} {eq} = begin - m o ( Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈↑⟨ car (mm m mono) ⟩ - (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) o ( Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈↑⟨ assoc ⟩ - _ o (Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o ( Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq )) ≈⟨ cdr assoc ⟩ - equalizer (Ker (char m mono)) o ((Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o Iso.≅← (IsoL.iso-L (ker-iso m mono))) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈⟨ cdr (car (Iso.iso← (IsoL.iso-L (ker-iso m mono)))) ⟩ - equalizer (Ker (char m mono)) o (id1 A _ o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈⟨ cdr idL ⟩ - equalizer (Ker (char m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker (char m mono))) ⟩ - h ∎ where open ≈-Reasoning A - uniqueness : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → {d : Obj A} {h : Hom A d a} - {eq : A [ A [ char m mono o h ] ≈ A [ A [ ⊤ o CCC.○ c a ] o h ] ]} - {k' : Hom A d b} → A [ A [ m o k' ] ≈ h ] - → A [ (A Category.o Iso.≅← (IsoL.iso-L (ker-iso m mono))) (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ≈ k' ] - uniqueness {a} {b} m mono {d} {h} {eq} {k'} eqk = begin - Iso.≅← (IsoL.iso-L (ker-iso m mono)) o (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer (Ker (char m mono))) ( begin - equalizer (Ker (char m mono)) o ((Iso.≅→ (IsoL.iso-L (ker-iso m mono))) o k' ) ≈⟨ assoc ⟩ - (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) o k' ≈⟨ car (mm m mono) ⟩ - m o k' ≈⟨ eqk ⟩ - h ∎ )) ⟩ - Iso.≅← (IsoL.iso-L (ker-iso m mono)) o ( Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o k' ) ≈⟨ assoc ⟩ - (Iso.≅← (IsoL.iso-L (ker-iso m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ) o k' ≈⟨ car (Iso.iso→ (IsoL.iso-L (ker-iso m mono)) )⟩ - id1 A _ o k' ≈⟨ idL ⟩ - k' ∎ where open ≈-Reasoning A - mequ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Equalizer A (char m mono) (A [ ⊤ o (CCC.○ c a) ]) - mequ {a} {b} m mono = record { equalizer-c = b ; equalizer = m ; isEqualizer = record { - fe=ge = fe=ge m mono - ; k = λ {d} h fh=gh → A [ Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h fh=gh ] - ; ek=h = ek=h m mono - ; uniqueness = uniqueness m mono - } } char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ] char-m=⊤ {a} {b} m mono = begin - char m mono o m ≈⟨ fe=ge m mono ⟩ + char m mono o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono) ⟩ (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩ ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩ ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A
--- a/src/CCCSets.agda Tue Mar 23 17:58:57 2021 +0900 +++ b/src/CCCSets.agda Wed Mar 24 23:15:22 2021 +0900 @@ -20,8 +20,10 @@ -- Sets is a CCC -import Axiom.Extensionality.Propositional -postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ +open import SetsCompleteness hiding (ki1) + +-- import Axiom.Extensionality.Propositional +-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ data One {c : Level } : Set c where OneObj : One -- () in Haskell ( or any one object set ) @@ -108,11 +110,11 @@ true : Bool false : Bool -data Tker {c : Level} {a : Set c} ( f : a → Bool {c} ) : Set c where - isTrue : (x : a ) → f x ≡ true → Tker f +-- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where +-- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g -irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' -irr refl refl = refl +-- irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' +-- irr refl refl = refl topos : {c : Level } → Topos (Sets {c}) sets topos {c} = record { @@ -121,43 +123,26 @@ ; Ker = tker ; char = tchar ; isTopos = record { - char-uniqueness = λ {a} {b} {h} m mono → {!!} -- extensionality Sets ( λ x → uniq h m mono x ) - ; ker-iso = {!!} + char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x ) + ; ker-m = imequ } } where tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ]) tker {a} h = record { - equalizer-c = Tker h - ; equalizer = etker - ; isEqualizer = record { - fe=ge = extensionality Sets ( λ x → e-eq x ) - ; k = k - ; ek=h = λ {d} {h1} {eq} → extensionality Sets ( λ x → refl ) - ; uniqueness = λ {d} {h1} {eq} {k'} ek=h → extensionality Sets ( λ x → uniq h1 eq k' ek=h x ) - } - } where - etker : Hom Sets ( Tker h ) a - etker (isTrue x eq) = x - e-eq : (x : Tker h ) → h ( etker x ) ≡ true - e-eq (isTrue x eq ) = eq - k : {d : Obj Sets} (h₁ : Hom Sets d a) → - Sets [ Sets [ h o h₁ ] ≈ Sets [ Sets [ (λ _ → true) o CCC.○ sets a ] o h₁ ] ] → - Hom Sets d (Tker h) - k {d} h1 hf=hg x = isTrue (h1 x) ( cong ( λ k → k x) hf=hg ) - tker-cong : (x y : Tker h ) → etker x ≡ etker y → x ≡ y - tker-cong ( isTrue x eq ) (isTrue .x eq' ) refl = cong ( λ ee → isTrue x ee ) ( irr eq eq' ) - uniq : {d : Obj Sets} (h1 : Hom Sets d a) -- etker (k h1 eq x) ≡ etker (k' x) - (eq : Sets [ Sets [ h o h1 ] ≈ Sets [ Sets [ (λ _ → true) o (λ _ → OneObj) ] o h1 ] ]) - (k' : Hom Sets d (Tker h)) (ek=h : Sets [ Sets [ etker o k' ] ≈ h1 ]) (x : d) → k h1 eq x ≡ k' x - uniq h1 eq k' ek=h x with cong (λ j → j x) ek=h -- etker (k h1 eq x) ≡ etker (k' x) - ... | t = tker-cong (k h1 eq x) (k' x) (sym t) - kiso : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsoL Sets m (Equalizer.equalizer (tker (λ x → true))) - kiso {a} {b} m mono = record { iso-L = record { - ≅→ = λ x → isTrue (m x) refl ; ≅← = ki1 ; iso→ = {!!} ; iso← = {!!} } ; iso≈L = {!!} } where - ki1 : Hom Sets (Equalizer.equalizer-c (tker (λ x → true))) b - ki1 (isTrue x eq) = {!!} + equalizer-c = sequ a Bool h (λ _ → true) + ; equalizer = λ e → equ e + ; isEqualizer = SetsIsEqualizer _ _ _ _ } tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a Bool tchar {a} {b} m mono x = true + selem : {a : Obj (Sets {c})} → (x : sequ a Bool (λ x₁ → true) (λ _ → true)) → a + selem (elem x eq) = x + imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true) o CCC.○ sets a ]) + imequ {a} {b} m mono = record { + fe=ge = extensionality Sets ( λ x → refl ) + ; k = λ h eq → {!!} + ; ek=h = {!!} + ; uniqueness = {!!} + } uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x uniq {a} {b} h m mono x = begin true ≡⟨⟩
--- a/src/ToposEx.agda Tue Mar 23 17:58:57 2021 +0900 +++ b/src/ToposEx.agda Wed Mar 24 23:15:22 2021 +0900 @@ -78,39 +78,25 @@ ; π2 = ○ b ; isPullback = record { commute = IsTopos.char-m=⊤ (Topos.isTopos t) m mono - ; pullback = λ {d} {p1} {p2} eq → f← o k p1 p2 eq + ; pullback = λ {d} {p1} {p2} eq → k p1 p2 eq ; π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC)) ; uniqueness = uniq } } where - f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) - f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) - k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono))) - k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq ) + k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d b + k p1 p2 eq = IsEqualizer.k (IsTopos.ker-m (isTopos t) m mono) p1 (mh=⊤ (char t m mono) p1 p2 eq ) lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) - → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 + → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (k p1 p2 eq ) ≈ p1 lemma3 {d} p1 p2 eq = begin - m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩ - (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-iso (isTopos t) m mono )) ⟩ - equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩ + m o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (IsTopos.ker-m (isTopos t) m mono) ⟩ p1 ∎ uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １) (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) → - A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → f← o k π1' π2' eq ≈ p' + A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → k π1' π2' eq ≈ p' uniq {d} p p1 p2 eq pe1 pe2 = begin - f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness (isEqualizer (Ker t (char t m mono))) lemma4) ⟩ - f← o (f→ o p ) ≈⟨ assoc ⟩ - (f← o f→ ) o p ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono ))) ⟩ - id1 A _ o p ≈⟨ idL ⟩ - p ∎ where - lemma4 : A [ A [ equalizer (Ker t (char t m mono)) o (f→ o p) ] ≈ p1 ] - lemma4 = begin - equalizer (Ker t (char t m mono)) o (f→ o p) ≈⟨ assoc ⟩ - (equalizer (Ker t (char t m mono)) o f→ ) o p ≈⟨ car (IsoL.L≈iso (IsTopos.ker-iso (isTopos t) m mono )) ⟩ - m o p ≈⟨ pe1 ⟩ - p1 ∎ where - + k p1 p2 eq ≈⟨ IsEqualizer.uniqueness (IsTopos.ker-m (isTopos t) m mono) pe1 ⟩ + p ∎ δmono : {b : Obj A } → Mono A < id1 A b , id1 A b > δmono = record {
--- a/src/equalizer.agda Tue Mar 23 17:58:57 2021 +0900 +++ b/src/equalizer.agda Wed Mar 24 23:15:22 2021 +0900 @@ -166,6 +166,61 @@ j ∎ + +equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) + → (m : Hom A c a) + → ( ker-iso : IsoL A m (equalizer equ) ) + → IsEqualizer A m f g +equalizerIso {a} {b} {c} f g equ m ker-iso = record { + fe=ge = fe-ge + ; k = λ {d} h eq → A [ Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ] + ; ek=h = ek=h1 + ; uniqueness = uniqueness1 } where + ker : Hom A ( equalizer-c equ ) a + ker = equalizer equ + mm : A [ A [ equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso ) ] ≈ m ] + mm = IsoL.L≈iso ker-iso + fe-ge : A [ A [ f o m ] ≈ A [ g o m ] ] + fe-ge = begin + f o m ≈↑⟨ cdr mm ⟩ + f o (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ assoc ⟩ + (f o equalizer equ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer equ) ) ⟩ + (g o equalizer equ ) o Iso.≅→ (IsoL.iso-L ker-iso) ≈↑⟨ assoc ⟩ + g o (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) ≈⟨ cdr mm ⟩ + g o m ∎ where open ≈-Reasoning A + ek=h1 : {d : Obj A} {h : Hom A d a} + {eq : A [ A [ f o h ] ≈ A [ g o h ] ]} → + A [ A [ m o (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ] ≈ h ] + ek=h1 {d} {h} {eq} = begin + m o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ car mm ⟩ + (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈↑⟨ assoc ⟩ + _ o (Iso.≅→ (IsoL.iso-L ker-iso) o ( Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq )) ≈⟨ cdr assoc ⟩ + equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso) o Iso.≅← (IsoL.iso-L ker-iso)) o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr (car (Iso.iso← (IsoL.iso-L ker-iso))) ⟩ + equalizer equ o (id1 A _ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ) ≈⟨ cdr idL ⟩ + equalizer equ o IsEqualizer.k (Equalizer.isEqualizer equ) h eq ≈⟨ IsEqualizer.ek=h (isEqualizer equ) ⟩ + h ∎ where open ≈-Reasoning A + 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 [ m o k' ] ≈ h ] + → A [ (A Category.o Iso.≅← (IsoL.iso-L ker-iso)) (IsEqualizer.k (isEqualizer equ) h eq) ≈ k' ] + uniqueness1 {d} {h} {eq} {k'} eqk = begin + Iso.≅← (IsoL.iso-L ker-iso) o (IsEqualizer.k (isEqualizer equ) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer equ) ( begin + equalizer equ o ((Iso.≅→ (IsoL.iso-L ker-iso)) o k' ) ≈⟨ assoc ⟩ + (equalizer equ o Iso.≅→ (IsoL.iso-L ker-iso)) o k' ≈⟨ car mm ⟩ + m o k' ≈⟨ eqk ⟩ + h ∎ )) ⟩ + Iso.≅← (IsoL.iso-L ker-iso) o ( Iso.≅→ (IsoL.iso-L ker-iso) o k' ) ≈⟨ assoc ⟩ + (Iso.≅← (IsoL.iso-L ker-iso) o Iso.≅→ (IsoL.iso-L ker-iso) ) o k' ≈⟨ car (Iso.iso→ (IsoL.iso-L ker-iso) )⟩ + id1 A _ o k' ≈⟨ idL ⟩ + k' ∎ where open ≈-Reasoning A + mequ : Equalizer A f g + mequ = record { equalizer-c = c ; equalizer = m ; isEqualizer = record { + fe=ge = fe-ge + ; k = λ {d} h fh=gh → A [ Iso.≅← (IsoL.iso-L ker-iso) o IsEqualizer.k (Equalizer.isEqualizer equ) h fh=gh ] + ; ek=h = ek=h1 + ; uniqueness = uniqueness1 + } } + -------------------------------- -- -- If we have two equalizers on c and c', there are isomorphic pair h, h' @@ -325,6 +380,23 @@ open ≈-Reasoning A h : Hom A d a h = equalizer (eqa f g) o j +-- cong-γ1 : {a b c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → +-- A [ k (ieqa f g ) {_} ( A [ h o (equalizer1 ( ieqa (A [ f o h ] ) (A [ g o h ] ) )) ] ) (lemma-equ4 {a} {b} {d} f g h ) +-- ≈ A [ k (ieqa f g ) {_} ( A [ h' o (equalizer1 ( ieqa (A [ f o h' ] ) (A [ g o h' ] ) )) ] ) (lemma-equ4 {a} {b} {d} f g h' ) o {!!} ] ] +-- cong-γ1 {a} {b} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin +-- k (ieqa f g ) {_} ( A [ h o (equalizer1 ( ieqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h ) +-- ≈⟨ uniqueness (ieqa f g) {!!} ⟩ +-- {!!} -- k (ieqa f g ) {_} ( A [ h' o (equalizer1 ( ieqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {d} f g h' ) +-- ∎ +-- cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (ieqa f f ) (id1 A a) (f1=f1 f) ≈ +-- A [ {!!} o k (ieqa f' f' ) (id1 A a) (f1=f1 f') ] ] +-- cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in +-- begin +-- k (ieqa f f ) (id a) (f1=f1 f) +-- ≈⟨ uniqueness (ieqa f f) {!!} ⟩ +-- {!!} -- k (ieqa f' f' ) (id a) (f1=f1 f') +-- ∎ + --------------------------------