Mercurial > hg > Members > kono > Proof > category
changeset 431:a15f52456c78
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 26 Mar 2016 15:51:30 +0900 |
| parents | 46c057cb3d82 |
| children | 688066ac172e |
| files | limit-to.agda maybeCat.agda |
| diffstat | 2 files changed, 78 insertions(+), 78 deletions(-) [+] |
line wrap: on
line diff
--- a/limit-to.agda Sat Mar 26 15:47:46 2016 +0900 +++ b/limit-to.agda Sat Mar 26 15:51:30 2016 +0900 @@ -16,9 +16,9 @@ --- two objects category --- --- f ---- ------> +--- -----→ --- 0 1 ---- ------> +--- -----→ --- g @@ -29,7 +29,7 @@ -- 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 +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 @@ -45,7 +45,7 @@ -- 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 : ∀ {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 @@ -59,14 +59,14 @@ 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 : 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₂) +_==_ : ∀{ 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 : ∀{ 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 } @@ -80,21 +80,21 @@ open TwoHom1 -==refl : ∀{ c₁ c₂ a b } -> ∀ {x : Maybe (Arrow {c₁} {c₂} t0 t1 a b )} → x == x +==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 : ∀{ 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 ) } → +==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 } → ∀ {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 @@ -223,7 +223,7 @@ -TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) -> (TwoHom {c₁} {c₂ } a a ) +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 } @@ -237,19 +237,19 @@ -- ∎ open import Relation.Binary -TwoCat : {c₁ c₂ ℓ : Level } -> Category c₁ c₂ c₂ +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 ; + _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} + 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 @@ -281,9 +281,9 @@ hom ( h × f ) ==⟨⟩ comp (hom h) (hom f) - ==⟨ ==cong (\ x -> comp ( hom h ) x ) f==g ⟩ + ==⟨ ==cong (λ x → comp ( hom h ) x ) f==g ⟩ comp (hom h) (hom g) - ==⟨ ==cong (\ x -> comp x ( hom g ) ) h==i ⟩ + ==⟨ ==cong (λ x → comp x ( hom g ) ) h==i ⟩ comp (hom i) (hom g) ==⟨⟩ hom ( i × g ) @@ -291,31 +291,31 @@ 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 ] - 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} ] + nil : {a b : Obj A } → Hom A a b + nil-id : {a : Obj A } → A [ nil {a} {a} ≈ id1 A a ] + 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₂ ℓ : 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} + 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 + 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 : {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 @@ -329,21 +329,21 @@ ≈-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 ) -> Functor (TwoCat {c₁} {c₂} {c₂} ) A +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} + 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 : 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 : 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 @@ -412,27 +412,27 @@ --- Equalizer --- f ---- e ------> ---- c ------> a b ---- ^ / ------> +--- e -----→ +--- c -----→ a b +--- ^ / -----→ --- |k h g --- | / --- | / ^ --- | / | --- |/ | Γ --- d _ | ---- |\ | ---- \ K af ---- \ ------> ---- \ t0 t1 ---- ------> +--- |λ | +--- λ K af +--- λ -----→ +--- λ t0 t1 +--- -----→ --- ag --- --- open Limit -I' : {c₁ c₂ ℓ : Level} -> Category c₁ c₂ c₂ +I' : {c₁ c₂ ℓ : Level} → Category c₁ c₂ c₂ I' {c₁} {c₂} {ℓ} = TwoCat {c₁} {c₂} {ℓ} lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( none : Nil A ) @@ -451,11 +451,11 @@ I = I' {c₁} {c₂} {ℓ} Γ : Functor I A Γ = indexFunctor {c₁} {c₂} {ℓ} A none 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 : 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 ] ] + ... | 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 hom f' commute1 {t0} {t0} {f'} d h fh=gh | nothing = begin @@ -543,19 +543,19 @@ 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 + commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh } } eqlim = lim Γ {c} {nat1 c e fe=ge } 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 ) - 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 : 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 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 ) -> A [ A [ e o k' ] ≈ h ] -> A [ A [ nmap i c e o k' ] ≈ nmap i d 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' ≈⟨⟩ @@ -576,12 +576,12 @@ ≈⟨⟩ nmap t1 d h ∎ - uniquness : (d : Obj A ) (h : Hom A d a ) -> ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) -> + 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' ] + → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] uniquness d h fh=gh k' ek'=h = begin k h fh=gh - ≈⟨ limit-uniqueness eqlim {d} {nat1 d h fh=gh } {k'} ( \{i} -> uniq-nat {i} d h k' ek'=h ) ⟩ + ≈⟨ limit-uniqueness eqlim {d} {nat1 d h fh=gh } {k'} ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩ k' ∎
--- a/maybeCat.agda Sat Mar 26 15:47:46 2016 +0900 +++ b/maybeCat.agda Sat Mar 26 15:51:30 2016 +0900 @@ -18,16 +18,16 @@ open MaybeHom -_+_ : { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b c : Obj A } → MaybeHom A b c → MaybeHom A a b → MaybeHom A a c +_+_ : { c₁ c₂ ℓ : Level} → { A : Category c₁ c₂ ℓ } → {a b c : Obj A } → MaybeHom A b c → MaybeHom A a b → MaybeHom A a c _+_ {x} {y} {z} {A} {a} {b} {c} f g with hom f | hom g _+_ {_} {_} {_} {A} {a} {b} {c} f g | nothing | _ = record { hom = nothing } _+_ {_} {_} {_} {A} {a} {b} {c} f g | _ | nothing = record { hom = nothing } _+_ {_} {_} {_} {A} {a} {b} {c} _ _ | (just f) | (just g) = record { hom = just ( A [ f o g ] ) } -MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) -> MaybeHom A a a +MaybeHomId : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } (a : Obj A ) → MaybeHom A a a MaybeHomId {_} {_} {_} {A} a = record { hom = just ( id1 A a) } -_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } -> Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) +_[_≡≡_] : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → Rel (Maybe (Hom A a b)) (c₂ ⊔ ℓ) _[_≡≡_] A = Eq ( Category._≈_ A ) @@ -37,20 +37,20 @@ infixr 2 _≡≡⟨_⟩_ _≡≡⟨⟩_ infix 1 begin_ - ≡≡-refl : {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ] + ≡≡-refl : {a b : Obj A } → {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ] ≡≡-refl {_} {_} {just x} = just refl-hom where open ≈-Reasoning (A) ≡≡-refl {_} {_} {nothing} = nothing - ≡≡-sym : {a b : Obj A } -> {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ] + ≡≡-sym : {a b : Obj A } → {x y : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ x ] ≡≡-sym (just x≈y) = just (sym x≈y) where open ≈-Reasoning (A) ≡≡-sym nothing = nothing - ≡≡-trans : {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ] + ≡≡-trans : {a b : Obj A } → {x y z : Maybe ( Hom A a b ) } → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ] ≡≡-trans (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z) where open ≈-Reasoning (A) ≡≡-trans nothing nothing = nothing - ≡≡-cong : ∀{ a b c d } -> ∀ {x y : Maybe (Hom A a b )} → - (f : Maybe (Hom A a b ) -> Maybe (Hom A c d ) ) -> x ≡ y → A [ f x ≡≡ f y ] + ≡≡-cong : ∀{ a b c d } → ∀ {x y : Maybe (Hom A a b )} → + (f : Maybe (Hom A a b ) → Maybe (Hom A c d ) ) → x ≡ y → A [ f x ≡≡ f y ] ≡≡-cong {a} {b } {c} {d} {nothing} {nothing} f refl = ≡≡-refl ≡≡-cong {a} {b } {c} {d} {just x} {just .x} f refl = ≡≡-refl @@ -76,27 +76,27 @@ -MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) +MaybeCat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category c₁ (ℓ ⊔ c₂) (ℓ ⊔ c₂) MaybeCat { c₁} {c₂} {ℓ} ( A ) = record { Obj = Obj A ; Hom = λ a b → MaybeHom A a b ; _o_ = _+_ ; _≈_ = λ a b → _[_≡≡_] { c₁} {c₂} {ℓ} A (hom a) (hom b) ; - Id = \{a} -> MaybeHomId a ; + Id = λ {a} → MaybeHomId a ; isCategory = record { isEquivalence = let open ≡≡-Reasoning (A) in record {refl = ≡≡-refl ; trans = ≡≡-trans ; sym = ≡≡-sym } ; - identityL = \{a b f} -> identityL {a} {b} {f} ; - identityR = \{a b f} -> identityR {a} {b} {f}; - o-resp-≈ = \{a b c f g h i} -> o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; - associative = \{a b c d f g h } -> associative {a } { b } { c } { d } { f } { g } { h } + identityL = λ {a b f} → identityL {a} {b} {f} ; + identityR = λ {a b f} → identityR {a} {b} {f}; + o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; + associative = λ {a b c d f g h } → associative {a } { b } { c } { d } { f } { g } { h } } } where - identityL : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (MaybeHomId b + f) ≡≡ hom f ] + identityL : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (MaybeHomId b + f) ≡≡ hom f ] identityL {a} {b} {f} with hom f identityL {a} {b} {_} | nothing = nothing identityL {a} {b} {_} | just f = just ( IsCategory.identityL ( Category.isCategory A ) {a} {b} {f} ) - identityR : { a b : Obj A } { f : MaybeHom A a b } -> A [ hom (f + MaybeHomId a ) ≡≡ hom f ] + identityR : { a b : Obj A } { f : MaybeHom A a b } → A [ hom (f + MaybeHomId a ) ≡≡ hom f ] identityR {a} {b} {f} with hom f identityR {a} {b} {_} | nothing = nothing identityR {a} {b} {_} | just f = just ( IsCategory.identityR ( Category.isCategory A ) {a} {b} {f} ) @@ -120,7 +120,7 @@ associative {a} {b} {c} {d} {_} {_} {_} | just f | just g | just h = just ( IsCategory.associative ( Category.isCategory A ) {a} {b} {c} {d} {f} {g} {h} ) -≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) -> { a b : Obj A } - { f g : Hom A a b } -> - A [ f ≈ g ] -> (MaybeCat A) [ record { hom = just f } ≈ record { hom = just g } ] +≈-to-== : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → { a b : Obj A } + { f g : Hom A a b } → + A [ f ≈ g ] → (MaybeCat A) [ record { hom = just f } ≈ record { hom = just g } ] ≈-to-== A {a} {b} {f} {g} f≈g = just f≈g