Mercurial > hg > Members > kono > Proof > category
changeset 457:0ba86e29f492
limit-to and discrete clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Mar 2017 18:30:58 +0900 |
| parents | 4d97955ea419 |
| children | fd79b6d9f350 |
| files | discrete.agda limit-to.agda |
| diffstat | 2 files changed, 156 insertions(+), 741 deletions(-) [+] |
line wrap: on
line diff
--- a/discrete.agda Thu Mar 02 17:41:20 2017 +0900 +++ b/discrete.agda Thu Mar 02 18:30:58 2017 +0900 @@ -4,14 +4,6 @@ module discrete where open import Relation.Binary.Core -open import Relation.Nullary -open import Data.Empty -open import Data.Unit -open import Data.Maybe -open import cat-utility -open import HomReasoning - -open Functor data TwoObject {c₁ : Level} : Set c₁ where t0 : TwoObject @@ -25,6 +17,8 @@ --- 0 1 --- -----→ --- g +-- +-- missing arrows are constrainted by TwoHom data data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where id-t0 : TwoHom t0 t0 @@ -57,21 +51,19 @@ {g : (TwoHom {c₁} {c₂ } b c )} → {h : (TwoHom {c₁} {c₂ } a b )} → ( f × (g × h)) ≡ ((f × g) × h ) -assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with f | g | h -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} | id-t0 | id-t0 | id-t0 = refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-f | id-t0 | id-t0 = refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} | arrow-g | id-t0 | id-t0 = refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-f | id-t0 = refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} | id-t1 | arrow-g | id-t0 = refl -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-f = refl -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} | id-t1 | id-t1 | arrow-g = refl -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} | id-t1 | id-t1 | id-t1 = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl +assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl +assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = id-t0 TwoId {_} {_} t1 = id-t1 -open import Relation.Binary open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ @@ -90,17 +82,15 @@ } } where identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f - identityL {c₁} {c₂} {a} {b} {f} with f - identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl - identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl - identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl - identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl + identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl + identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl + identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl + identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f - identityR {c₁} {c₂} {_} {_} {f} with f - identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl - identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl - identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl - identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl + identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl + identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl + identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl + identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = @@ -116,190 +106,3 @@ ( i × g ) ∎ -indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A -indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { - FObj = λ a → fobj a - ; FMap = λ {a} {b} f → fmap {a} {b} f - ; isFunctor = record { - identity = λ{x} → identity x - ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} - ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} - } - } where - T = TwoCat {c₁} {c₂} - fobj : Obj T → Obj A - fobj t0 = a - fobj t1 = b - fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) - fmap {t0} {t0} id-t0 = id1 A a - fmap {t1} {t1} id-t1 = id1 A b - fmap {t0} {t1} arrow-f = f - fmap {t0} {t1} arrow-g = g - ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom - identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] - identity t0 = let open ≈-Reasoning A in refl-hom - identity t1 = let open ≈-Reasoning A in refl-hom - distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → - A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] - distr1 {a} {b} {c} {f} {g} with f | g - distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL - distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin - id1 A b - ≈↑⟨ idL ⟩ - id1 A b o id1 A b - ∎ - distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin - fmap (comp arrow-f id-t0) - ≈⟨⟩ - fmap arrow-f - ≈↑⟨ idR ⟩ - fmap arrow-f o id1 A a - ∎ - distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin - fmap (comp arrow-g id-t0) - ≈⟨⟩ - fmap arrow-g - ≈↑⟨ idR ⟩ - fmap arrow-g o id1 A a - ∎ - distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-f) - ≈⟨⟩ - fmap arrow-f - ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-f - ∎ - distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-g) - ≈⟨⟩ - fmap arrow-g - ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-g - ∎ - ---- Equalizer ---- f ---- e -----→ ---- c -----→ a b ---- ^ / -----→ ---- |k h g ---- | / ---- | / ^ ---- | / | ---- |/ | Γ ---- d _ | ---- |\ | ---- \ K af ---- \ -----→ ---- \ t0 t1 ---- -----→ ---- ag ---- ---- - -open Complete -open Limit -open NTrans - -equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) -> - Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a -equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = ? -- TMap (limit-u comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0 - -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (comp : Complete A (TwoCat {c₁} {c₂} ) ) - → {a b : Obj A} (f g : Hom A a b ) - → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] ) - → IsEqualizer A (equlimit A f g comp ) f g -lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { - fe=ge = fe=ge - ; k = λ {d} h fh=gh → k {d} h fh=gh - ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh - ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' - } where - I = TwoCat {c₁} {c₂} - Γ : Functor I A - Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g - c = limit-c comp Γ - k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x) - nmap x d h with x - ... | t0 = h - ... | t1 = A [ f o h ] - commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] - → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] - commute1 {x} {y} {f'} d h fh=gh with f' - commute1 {t0} {t1} {f'} d h fh=gh | arrow-f = let open ≈-Reasoning A in begin - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t1} {f'} d h fh=gh | arrow-g = let open ≈-Reasoning A in begin - g o h - ≈↑⟨ fh=gh ⟩ - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t0} {f'} d h fh=gh | id-t0 = let open ≈-Reasoning A in begin - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o id1 A d - ∎ - commute1 {t1} {t1} {f'} d h fh=gh | id-t1 = let open ≈-Reasoning A in begin - id1 A b o ( f o h ) - ≈⟨ idL ⟩ - f o h - ≈↑⟨ idR ⟩ - ( f o h ) o id1 A d - ∎ - nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ - nat1 d h fh=gh = record { - TMap = λ x → nmap x d h ; - isNTrans = record { - commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh - } - } - e = equlimit A f g comp - eqlim = isLimit comp Γ (nat1 c e fe=ge ) - k {d} h fh=gh = limit eqlim d (nat1 d h fh=gh ) - ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] - ek=h d h fh=gh = let open ≈-Reasoning A in begin - e o k h fh=gh - ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0} ⟩ - h - ∎ - uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) - ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → - A [ A [ TMap (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ] - uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin - (nmap t0 c e ) o k' - ≈⟨⟩ - e o k' - ≈⟨ ek'=h ⟩ - h - ≈⟨⟩ - nmap t0 d h - ∎ - uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin - (nmap t1 c e ) o k' - ≈⟨⟩ - (f o e ) o k' - ≈↑⟨ assoc ⟩ - f o ( e o k' ) - ≈⟨ cdr ek'=h ⟩ - f o h - ≈⟨⟩ - TMap (nat1 d h fh=gh) t1 - ∎ - uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → - ( k' : Hom A d c ) - → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] - uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin - k h fh=gh - ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ - k' - ∎ -
--- a/limit-to.agda Thu Mar 02 17:41:20 2017 +0900 +++ b/limit-to.agda Thu Mar 02 18:30:58 2017 +0900 @@ -6,423 +6,14 @@ open import cat-utility open import HomReasoning open import Relation.Binary.Core -open import Data.Maybe -open Functor - - - --- If we have limit then we have equalizer ---- two objects category ---- ---- f ---- -----→ ---- 0 1 ---- -----→ ---- g - - - -data TwoObject {c₁ : Level} : Set c₁ where - t0 : TwoObject - t1 : TwoObject - --- constrainted arrow --- we need inverse of f to complete cases -data Arrow {c₁ c₂ : Level } ( t00 t11 : TwoObject {c₁} ) : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where - id-t0 : Arrow t00 t11 t00 t00 - id-t1 : Arrow t00 t11 t11 t11 - arrow-f : Arrow t00 t11 t00 t11 - arrow-g : Arrow t00 t11 t00 t11 - inv-f : Arrow t00 t11 t11 t00 - -record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set c₂ where - field - hom : Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) - -open TwoHom - --- arrow composition - - -comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 b c ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) → Maybe ( Arrow {c₁} {c₂} t0 t1 a c ) -comp {_} {_} {_} {_} {_} nothing _ = nothing -comp {_} {_} {_} {_} {_} (just _ ) nothing = nothing -comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-f ) = just arrow-f -comp {_} {_} {t0} {t1} {t1} (just id-t1 ) ( just arrow-g ) = just arrow-g -comp {_} {_} {t1} {t1} {t1} (just id-t1 ) ( just id-t1 ) = just id-t1 -comp {_} {_} {t1} {t1} {t0} (just inv-f ) ( just id-t1 ) = just inv-f -comp {_} {_} {t0} {t0} {t1} (just arrow-f ) ( just id-t0 ) = just arrow-f -comp {_} {_} {t0} {t0} {t1} (just arrow-g ) ( just id-t0 ) = just arrow-g -comp {_} {_} {t0} {t0} {t0} (just id-t0 ) ( just id-t0 ) = just id-t0 -comp {_} {_} {t1} {t0} {t0} (just id-t0 ) ( just inv-f ) = just inv-f -comp {_} {_} {_} {_} {_} (just _ ) ( just _ ) = nothing - - -_×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → ( TwoHom {c₁} {c₂} b c ) → ( TwoHom {c₁} {c₂} a b ) → ( TwoHom {c₁} {c₂} a c ) -_×_ {c₁} {c₂} {a} {b} {c} f g = record { hom = comp {c₁} {c₂} {a} {b} {c} (hom f) (hom g ) } - - -_==_ : ∀{ c₁ c₂ a b } → Rel (Maybe (Arrow {c₁} {c₂} t0 t1 a b )) (c₂) -_==_ = Eq _≡_ - -map2hom : ∀{ c₁ c₂ } → {a b : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} t0 t1 a b ) → TwoHom {c₁} {c₂ } a b -map2hom {_} {_} {t1} {t1} (just id-t1) = record { hom = just id-t1 } -map2hom {_} {_} {t0} {t1} (just arrow-f) = record { hom = just arrow-f } -map2hom {_} {_} {t0} {t1} (just arrow-g) = record { hom = just arrow-g } -map2hom {_} {_} {t0} {t0} (just id-t0) = record { hom = just id-t0 } -map2hom {_} {_} {_} {_} _ = record { hom = nothing } - -record TwoHom1 {c₁ c₂ : Level} (a : TwoObject {c₁} ) (b : TwoObject {c₁} ) : Set c₂ where - field - Map : TwoHom {c₁} {c₂ } a b - iso-Map : Map ≡ map2hom ( hom Map ) - -open TwoHom1 - -==refl : ∀{ c₁ c₂ a b } → ∀ {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == x -==refl {_} {_} {_} {_} {just x} = just refl -==refl {_} {_} {_} {_} {nothing} = nothing - -==sym : ∀{ c₁ c₂ a b } → ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == y → y == x -==sym (just x≈y) = just (≡-sym x≈y) -==sym nothing = nothing - -==trans : ∀{ c₁ c₂ a b } → ∀ {x y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } → - x == y → y == z → x == z -==trans (just x≈y) (just y≈z) = just (≡-trans x≈y y≈z) -==trans nothing nothing = nothing - -==cong : ∀{ c₁ c₂ a b c d } → ∀ {x y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → - (f : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) → Maybe (Arrow {c₁} {c₂} t0 t1 c d ) ) → x == y → f x == f y -==cong { c₁} {c₂} {a} {b } {c} {d} {nothing} {nothing} f nothing = ==refl -==cong { c₁} {c₂} {a} {b } {c} {d} {just x} {just .x} f (just refl) = ==refl - - -module ==-Reasoning {c₁ c₂ : Level} where - - infixr 2 _∎ - infixr 2 _==⟨_⟩_ _==⟨⟩_ - infix 1 begin_ - - - data _IsRelatedTo_ {c₁ c₂ : Level} {a b : TwoObject {c₁} } (x y : (Maybe (Arrow {c₁} {c₂} t0 t1 a b ))) : - Set c₂ where - relTo : (x≈y : x == y ) → x IsRelatedTo y - - begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → - x IsRelatedTo y → x == y - begin relTo x≈y = x≈y - - _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y z : Maybe (Arrow {c₁} {c₂} t0 t1 a b ) } → - x == y → y IsRelatedTo z → x IsRelatedTo z - _ ==⟨ x≈y ⟩ relTo y≈z = relTo (==trans x≈y y≈z) - - - _==⟨⟩_ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) {y : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} - → x IsRelatedTo y → x IsRelatedTo y - _ ==⟨⟩ x≈y = x≈y - - _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )) → x IsRelatedTo x - _∎ _ = relTo ==refl - - --- TwoHom1Eq : {c₁ c₂ : Level } {a b : TwoObject {c₁} } {f g : ( TwoHom1 {c₁} {c₂ } a b)} → --- hom (Map f) == hom (Map g) → f == g --- TwoHom1Eq = ? - - --- f g h --- d <- c <- b <- a --- --- It can be proved without Arrow constraints - -assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } - {f : (TwoHom {c₁} {c₂ } c d )} → - {g : (TwoHom {c₁} {c₂ } b c )} → - {h : (TwoHom {c₁} {c₂ } a b )} → - hom ( f × (g × h)) == hom ((f × g) × h ) -assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with hom f | hom g | hom h -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t0} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just _ | nothing | _ = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | just id-t0 = ==refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | just id-t0 = ==refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | just id-t0 = ==refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | just id-t0 = ==refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | just id-t0 = ==refl -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-f = ==refl -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just arrow-g = ==refl -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | just id-t1 = ==refl --- remaining all failure case (except inf-f case ) -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t0} {f} {g} {h} | just id-t0 | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} {f} {g} {h} | just id-t1 | just id-t1 | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t0} {t0} {f} {g} {h} | just id-t0 | just inv-f | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-f | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} {f} {g} {h} | just arrow-g | just id-t0 | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-f | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t0} {t1} {t1} {f} {g} {h} | just id-t1 | just arrow-g | nothing = nothing -assoc-× {c₁} {c₂} {t0} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t0} {f} {g} {h} | just inv-f | just id-t1 | nothing = nothing -assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing -assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing -assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing -assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | nothing = nothing -assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-f) | (just id-t0) = nothing -assoc-× {_} {_} {t0} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just arrow-g) | (just id-t0) = nothing -assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just _) = nothing -assoc-× {_} {_} {t0} {t1} {t0} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = nothing -assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-f) = nothing -assoc-× {_} {_} {t0} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just arrow-g) = nothing -assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just inv-f) = ==refl -assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just inv-f) = nothing -assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just inv-f) = nothing -assoc-× {_} {_} {t1} {t0} {t1} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing -assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-f) | (just _) = nothing -assoc-× {_} {_} {t1} {t0} {t1} {t1} {_} {_} {_} | (just id-t1) | (just arrow-g) | (just _) = nothing -assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just id-t0) | (just inv-f) | (just id-t1) = ==refl -assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just inv-f) | (just id-t1) = ==refl -assoc-× {_} {_} {t1} {t1} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just inv-f) | (just id-t1) = ==refl -assoc-× {_} {_} {t1} {t1} {t1} {t0} {_} {_} {_} | (just inv-f) | (just id-t1) | (just id-t1) = ==refl - - - -TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) -TwoId {_} {_} t0 = record { hom = just id-t0 } -TwoId {_} {_} t1 = record { hom = just id-t1 } - -open import maybeCat - --- identityL {c₁} {c₂} {_} {b} {nothing} = let open ==-Reasoning {c₁} {c₂} in --- begin --- (TwoId b × nothing) --- ==⟨ {!!} ⟩ --- nothing --- ∎ - -open import Relation.Binary -TwoCat : {c₁ c₂ ℓ : Level } → Category c₁ c₂ c₂ -TwoCat {c₁} {c₂} {ℓ} = record { - Obj = TwoObject {c₁} ; - Hom = λ a b → ( TwoHom {c₁} {c₂ } a b ) ; - _o_ = λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ; - _≈_ = λ x y → hom x == hom y ; - Id = λ{a} → TwoId {c₁ } { c₂} a ; - isCategory = record { - isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ; - identityL = λ{a b f} → identityL {c₁} {c₂ } {a} {b} {f} ; - identityR = λ{a b f} → identityR {c₁} {c₂ } {a} {b} {f} ; - o-resp-≈ = λ{a b c f g h i} → o-resp-≈ {c₁} {c₂ } {a} {b} {c} {f} {g} {h} {i} ; - associative = λ{a b c d f g h } → assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} - } - } where - identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) == hom f - identityL {c₁} {c₂} {_} {_} {f} with hom f - identityL {c₁} {c₂} {t0} {t0} {_} | nothing = nothing - identityL {c₁} {c₂} {t0} {t1} {_} | nothing = nothing - identityL {c₁} {c₂} {t1} {t0} {_} | nothing = nothing - identityL {c₁} {c₂} {t1} {t1} {_} | nothing = nothing - identityL {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl - identityL {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl - identityL {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl - identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl - identityL {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl - identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ( f × TwoId A ) == hom f - identityR {c₁} {c₂} {_} {_} {f} with hom f - identityR {c₁} {c₂} {t0} {t0} {_} | nothing = nothing - identityR {c₁} {c₂} {t0} {t1} {_} | nothing = nothing - identityR {c₁} {c₂} {t1} {t0} {_} | nothing = nothing - identityR {c₁} {c₂} {t1} {t1} {_} | nothing = nothing - identityR {c₁} {c₂} {t1} {t0} {_} | just inv-f = ==refl - identityR {c₁} {c₂} {t1} {t1} {_} | just id-t1 = ==refl - identityR {c₁} {c₂} {t0} {t0} {_} | just id-t0 = ==refl - identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-f = ==refl - identityR {c₁} {c₂} {t0} {t1} {_} | just arrow-g = ==refl - o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → - hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g ) - o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = - let open ==-Reasoning {c₁} {c₂ } in begin - hom ( h × f ) - ==⟨⟩ - comp (hom h) (hom f) - ==⟨ ==cong (λ x → comp ( hom h ) x ) f==g ⟩ - comp (hom h) (hom g) - ==⟨ ==cong (λ x → comp x ( hom g ) ) h==i ⟩ - comp (hom i) (hom g) - ==⟨⟩ - hom ( i × g ) - ∎ - -record Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where - field - nil : {a b : Obj A } → Hom A a b - nil-id : {a : Obj A } → A [ nil {a} {a} ≈ id1 A a ] -- too strong but we need this - nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ] ≈ nil {a} {c} ] - nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ] ≈ nil {a} {c} ] - -open Nil - -justFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → Nil A → Functor (MaybeCat A ) A -justFunctor{c₁} {c₂} {ℓ} A none = record { - FObj = λ a → fobj a - ; FMap = λ {a} {b} f → fmap {a} {b} f - ; isFunctor = record { - identity = λ{x} → identity {x} - ; distr = λ {a} {b} {c} {f} {g} → distr2 {a} {b} {c} {f} {g} - ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} - } - } where - MA = MaybeCat A - fobj : Obj MA → Obj A - fobj = λ x → x - fmap : {x y : Obj MA } → Hom MA x y → Hom A x y - fmap {x} {y} f with MaybeHom.hom f - fmap {x} {y} _ | nothing = nil none - fmap {x} {y} _ | (just f) = f - identity : {x : Obj MA} → A [ fmap (id1 MA x) ≈ id1 A (fobj x) ] - identity = let open ≈-Reasoning (A) in refl-hom - distr2 : {a : Obj MA} {b : Obj MA} {c : Obj MA} {f : Hom MA a b} {g : Hom MA b c} → A [ fmap (MA [ g o f ]) ≈ A [ fmap g o fmap f ] ] - distr2 {a} {b} {c} {f} {g} with MaybeHom.hom f | MaybeHom.hom g - distr2 | nothing | nothing = let open ≈-Reasoning (A) in sym ( nil-idR none ) - distr2 | nothing | just ga = let open ≈-Reasoning (A) in sym ( nil-idR none ) - distr2 | just fa | nothing = let open ≈-Reasoning (A) in sym ( nil-idL none ) - distr2 | just f | just g = let open ≈-Reasoning (A) in refl-hom - ≈-cong : {a : Obj MA} {b : Obj MA} {f g : Hom MA a b} → MA [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f} {g} eq with MaybeHom.hom f | MaybeHom.hom g - ≈-cong {a} {b} {f} {g} nothing | nothing | nothing = let open ≈-Reasoning (A) in refl-hom - ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq - --- indexFunctor' : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) --- → ( obj→ : Obj A → TwoObject {c₁} ) --- → ( hom→ : { a b : Obj A } → Hom A a b → Arrow t0 t0 (obj→ a) (obj→ b) ) --- → ( { x y : Obj A } { h i : Hom A x y } → A [ h ≈ i ] → hom→ h ≡ hom→ i ) --- → Functor A A --- this one does not work on fmap ( g o f ) ≈ ( fmap g o fmap f ) --- because g o f can be arrow-f when g is arrow-g --- ideneity and ≈-cong are easy - - -indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂} {c₂} ) A -indexFunctor {c₁} {c₂} {ℓ} A none a b f g = record { - FObj = λ a → fobj a - ; FMap = λ {a} {b} f → fmap {a} {b} f - ; isFunctor = record { - identity = λ{x} → identity {x} - ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} - ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} - } - } where - I = TwoCat {c₁} {c₂} {ℓ} - fobj : Obj I → Obj A - fobj t0 = a - fobj t1 = b - fmap : {x y : Obj I } → (TwoHom {c₁} {c₂} x y ) → Hom A (fobj x) (fobj y) - fmap {x} {y} h with hom h - fmap {t0} {t0} h | just id-t0 = id1 A a - fmap {t1} {t1} h | just id-t1 = id1 A b - fmap {t0} {t1} h | just arrow-f = f - fmap {t0} {t1} h | just arrow-g = g - fmap {_} {_} h | _ = nil none - open ≈-Reasoning A - ≈-cong : {a : Obj I} {b : Obj I} {f g : Hom I a b} → I [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f1} {g1} f≈g with hom f1 | hom g1 - ≈-cong {t0} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom - ≈-cong {t0} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom - ≈-cong {t1} {t0} {f1} {g1} nothing | nothing | nothing = refl-hom - ≈-cong {t1} {t1} {f1} {g1} nothing | nothing | nothing = refl-hom - ≈-cong {t0} {t0} {f1} {g1} (just refl) | just id-t0 | just id-t0 = refl-hom - ≈-cong {t1} {t1} {f1} {g1} (just refl) | just id-t1 | just id-t1 = refl-hom - ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-f | just arrow-f = refl-hom - ≈-cong {t0} {t1} {f1} {g1} (just refl) | just arrow-g | just arrow-g = refl-hom - ≈-cong {t1} {t0} {f1} {g1} (just refl) | just inv-f | just inv-f = refl-hom - identity : {x : Obj I} → A [ fmap ( id1 I x ) ≈ id1 A (fobj x) ] - identity {t0} = refl-hom - identity {t1} = refl-hom - distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → - A [ fmap (I [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] - distr1 {a1} {b1} {c1} {f1} {g1} with hom g1 | hom f1 - distr1 {t0} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t0} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t1} {t0} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t1} {t0} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t1} {t1} {t0} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t1} {t1} {t1} {f1} {g1} | nothing | nothing = sym ( nil-idR none ) - distr1 {t0} {t0} {t0} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none ) - distr1 {t0} {t0} {t1} {f1} {g1} | nothing | just id-t0 = sym ( nil-idL none ) - distr1 {t1} {t1} {t0} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none ) - distr1 {t1} {t1} {t1} {f1} {g1} | nothing | just id-t1 = sym ( nil-idL none ) - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none ) - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-f = sym ( nil-idL none ) - distr1 {t0} {t1} {t1} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none ) - distr1 {t0} {t1} {t0} {f1} {g1} | nothing | just arrow-g = sym ( nil-idL none ) - distr1 {t1} {t0} {t0} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none ) - distr1 {t1} {t0} {t1} {f1} {g1} | nothing | just inv-f = sym ( nil-idL none ) - distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none ) - distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | nothing = sym ( nil-idR none ) - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none ) - distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | nothing = sym ( nil-idR none ) - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none ) - distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-f | nothing = sym ( nil-idR none ) - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none ) - distr1 {t1} {t0} {t1} {f1} {g1} | just arrow-g | nothing = sym ( nil-idR none ) - distr1 {t0} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none ) - distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | nothing = sym ( nil-idR none ) - distr1 {t0} {t0} {t0} {f1} {g1} | just id-t0 | just id-t0 = sym idL - distr1 {t1} {t0} {t0} {f1} {g1} | just id-t0 | just inv-f = sym idL - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-f | just id-t0 = sym idR - distr1 {t0} {t0} {t1} {f1} {g1} | just arrow-g | just id-t0 = sym idR - distr1 {t1} {t1} {t1} {f1} {g1} | just id-t1 | just id-t1 = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-f = sym idL - distr1 {t0} {t1} {t1} {f1} {g1} | just id-t1 | just arrow-g = sym idL - distr1 {t1} {t1} {t0} {f1} {g1} | just inv-f | just id-t1 = sym ( nil-idL none ) - distr1 {t0} {t1} {t0} {_} {_} | (just inv-f) | (just _) = sym ( nil-idL none ) - distr1 {t1} {t0} {t1} {_} {_} | (just arrow-f) | (just _) = sym ( nil-idR none ) - distr1 {t1} {t0} {t1} {_} {_} | (just arrow-g) | (just _) = sym ( nil-idR none ) - +open import discrete --- Equalizer --- f --- e -----→ ---- c -----→ a b +--- c -----→ a b A --- ^ / -----→ --- |k h g --- | / @@ -432,150 +23,173 @@ --- d _ | --- |\ | --- \ K af ---- \ -----→ ---- \ t0 t1 +--- \ -----→ +--- \ t0 t1 I --- -----→ --- ag --- --- +open Complete open Limit +open NTrans -I' : {c₁ c₂ ℓ : Level} → Category c₁ c₂ c₂ -I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ} +-- Functor : TwoCat -> A -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( none : Nil A ) - (lim : ( Γ : Functor (I' {c₁} {c₂} {ℓ}) A ) → {a0 : Obj A } - {u : NTrans I' A ( K A I' a0 ) Γ } → Limit A I' Γ a0 u ) -- completeness - → {a b c : Obj A} (f g : Hom A a b ) - → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → IsEqualizer A e f g -lim-to-equ {c₁} {c₂} {ℓ } A none lim {a} {b} {c} f g e fe=ge = record { - fe=ge = fe=ge - ; k = λ {d} h fh=gh → k {d} h fh=gh - ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh - ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' - } where - open ≈-Reasoning A - I : Category c₁ c₂ c₂ - I = I' {c₁} {c₂} {ℓ} +IndexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A +IndexFunctor {c₁} {c₂} {ℓ} A a b f g = record { + FObj = λ a → fobj a + ; FMap = λ {a} {b} f → fmap {a} {b} f + ; isFunctor = record { + identity = λ{x} → identity x + ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} + ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} + } + } where + T = TwoCat {c₁} {c₂} + fobj : Obj T → Obj A + fobj t0 = a + fobj t1 = b + fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) + fmap {t0} {t0} id-t0 = id1 A a + fmap {t1} {t1} id-t1 = id1 A b + fmap {t0} {t1} arrow-f = f + fmap {t0} {t1} arrow-g = g + ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] + ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom + identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] + identity t0 = let open ≈-Reasoning A in refl-hom + identity t1 = let open ≈-Reasoning A in refl-hom + distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → + A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] + distr1 {t0} {t0} {t0} {id-t0 } { id-t0 } = let open ≈-Reasoning A in sym-hom idL + distr1 {t1} {t1} {t1} { id-t1 } { id-t1 } = let open ≈-Reasoning A in begin + id1 A b + ≈↑⟨ idL ⟩ + id1 A b o id1 A b + ∎ + distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin + fmap (comp arrow-f id-t0) + ≈⟨⟩ + fmap arrow-f + ≈↑⟨ idR ⟩ + fmap arrow-f o id1 A a + ∎ + distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin + fmap (comp arrow-g id-t0) + ≈⟨⟩ + fmap arrow-g + ≈↑⟨ idR ⟩ + fmap arrow-g o id1 A a + ∎ + distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin + fmap (comp id-t1 arrow-f) + ≈⟨⟩ + fmap arrow-f + ≈↑⟨ idL ⟩ + id1 A b o fmap arrow-f + ∎ + distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin + fmap (comp id-t1 arrow-g) + ≈⟨⟩ + fmap arrow-g + ≈↑⟨ idL ⟩ + id1 A b o fmap arrow-g + ∎ + +--- Nat for Limit +-- +-- Nat : K -> IndexFunctor +-- + +open Functor + +IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (comp : Complete A (TwoCat {c₁} {c₂} ) ) + → {a b : Obj A} (f g : Hom A a b ) + (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → + NTrans (TwoCat {c₁} {c₂}) A (K A (TwoCat {c₁} {c₂}) d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g) +IndexNat {c₁} {c₂} {ℓ} A comp {a} {b} f g d h fh=gh = record { + TMap = λ x → nmap x d h ; + isNTrans = record { + commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh + } + } where + I = TwoCat {c₁} {c₂} Γ : Functor I A - Γ = indexFunctor {c₁} {c₂} {ℓ} A none a b f g + Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x) - nmap x d h with x - ... | t0 = h - ... | t1 = A [ f o h ] + nmap t0 d h = h + nmap t1 d h = A [ f o h ] commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] - commute1 {x} {y} {f'} d h fh=gh with hom f' - commute1 {t0} {t0} {f'} d h fh=gh | nothing = begin - nil none o h - ≈⟨ car ( nil-id none ) ⟩ + commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin + f o h + ≈↑⟨ idR ⟩ + (f o h ) o id1 A d + ∎ + commute1 {t0} {t1} {arrow-g} d h fh=gh = let open ≈-Reasoning A in begin + g o h + ≈↑⟨ fh=gh ⟩ + f o h + ≈↑⟨ idR ⟩ + (f o h ) o id1 A d + ∎ + commute1 {t0} {t0} {id-t0} d h fh=gh = let open ≈-Reasoning A in begin id1 A a o h ≈⟨ idL ⟩ h ≈↑⟨ idR ⟩ h o id1 A d ∎ - commute1 {t0} {t1} {f'} d h fh=gh | nothing = begin - nil none o h - ≈↑⟨ car ( nil-idL none ) ⟩ - (nil none o f ) o h - ≈⟨ car ( car ( nil-id none ) ) ⟩ - (id1 A b o f ) o h - ≈⟨ car idL ⟩ - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t1} {t0} {f'} d h fh=gh | nothing = begin - nil none o ( f o h ) - ≈⟨ assoc ⟩ - ( nil none o f ) o h - ≈⟨ car ( nil-idL none ) ⟩ - nil none o h - ≈⟨ car ( nil-id none ) ⟩ -- nil-id is need here - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o id1 A d - ∎ - commute1 {t1} {t1} {f'} d h fh=gh | nothing = begin - nil none o ( f o h ) - ≈⟨ car ( nil-id none ) ⟩ - id1 A b o ( f o h ) - ≈⟨ idL ⟩ - f o h - ≈↑⟨ idR ⟩ - ( f o h ) o id1 A d - ∎ - commute1 {t1} {t0} {f'} d h fh=gh | just inv-f = begin - nil none o ( f o h ) - ≈⟨ assoc ⟩ - ( nil none o f ) o h - ≈⟨ car ( nil-idL none ) ⟩ - nil none o h - ≈⟨ car ( nil-id none ) ⟩ - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o id1 A d - ∎ - commute1 {t0} {t1} {f'} d h fh=gh | just arrow-f = begin - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t1} {f'} d h fh=gh | just arrow-g = begin - g o h - ≈↑⟨ fh=gh ⟩ - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t0} {f'} d h fh=gh | just id-t0 = begin - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o id1 A d - ∎ - commute1 {t1} {t1} {f'} d h fh=gh | just id-t1 = begin + commute1 {t1} {t1} {id-t1} d h fh=gh = let open ≈-Reasoning A in begin id1 A b o ( f o h ) ≈⟨ idL ⟩ f o h ≈↑⟨ idR ⟩ ( f o h ) o id1 A d ∎ - nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ - nat1 d h fh=gh = record { - TMap = λ x → nmap x d h ; - isNTrans = record { - commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh - } - } - eqlim = lim Γ {c} {nat1 c e fe=ge } + + +lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (comp : Complete A (TwoCat {c₁} {c₂} ) ) + → {a b : Obj A} (f g : Hom A a b ) {e : Hom A (limit-c comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) a } + → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) + → IsEqualizer A e f g +lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g {e} fe=ge = record { + fe=ge = fe=ge + ; k = λ {d} h fh=gh → k {d} h fh=gh + ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh + ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' + } where + I = TwoCat {c₁} {c₂} + Γ : Functor I A + Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g + c = limit-c comp Γ k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k {d} h fh=gh = limit eqlim d (nat1 d h fh=gh ) + nat0 = IndexNat A comp f g + eqlim = isLimit comp Γ (nat0 c e fe=ge ) + k {d} h fh=gh = limit eqlim d (nat0 d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] - ek=h d h fh=gh = begin + ek=h d h fh=gh = let open ≈-Reasoning A in begin e o k h fh=gh - ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0} ⟩ + ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh} {t0} ⟩ h ∎ - uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ nmap i c e o k' ] ≈ nmap i d h ] - uniq-nat {t0} d h k' ek'=h = begin - nmap t0 c e o k' + uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) + ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → + A [ A [ TMap (nat0 c e fe=ge ) i o k' ] ≈ TMap (nat0 d h fh=gh) i ] + uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin + TMap (nat0 c e fe=ge ) t0 o k' ≈⟨⟩ e o k' ≈⟨ ek'=h ⟩ h ≈⟨⟩ - nmap t0 d h + TMap (nat0 d h fh=gh) t0 ∎ - uniq-nat {t1} d h k' ek'=h = begin - nmap t1 c e o k' + uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin + TMap (nat0 c e fe=ge ) t1 o k' ≈⟨⟩ (f o e ) o k' ≈↑⟨ assoc ⟩ @@ -583,16 +197,14 @@ ≈⟨ cdr ek'=h ⟩ f o h ≈⟨⟩ - nmap t1 d h + TMap (nat0 d h fh=gh) t1 ∎ uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → ( k' : Hom A d c ) - → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] - uniquness d h fh=gh k' ek'=h = begin + → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] + uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin k h fh=gh - ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩ + ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ k' ∎ - -