# HG changeset patch # User Shinji KONO # Date 1488422191 -32400 # Node ID 3c2ce4474d92336e04d812ba1f592ae4a5ba9c40 # Parent 7ed0045e4adf63b01ff404e53c43e2ae8d1eae60 try incomplete pattern for discrete diff -r 7ed0045e4adf -r 3c2ce4474d92 discrete.agda --- a/discrete.agda Tue Feb 28 22:33:03 2017 +0900 +++ b/discrete.agda Thu Mar 02 11:36:31 2017 +0900 @@ -3,12 +3,13 @@ module discrete where -open import cat-utility -open import HomReasoning 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 @@ -33,83 +34,21 @@ record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁} ) : Set ( c₂) where field - hom : Maybe ( Arrow {c₁} {c₂} a b ) - constraint1 : {c₁ c₂ : Level } → TwoObject {c₁} → TwoObject {c₁} → Maybe ( ⊥ ) - constraint1 t0 t0 = nothing - constraint1 {c₁} {c₂} t1 t0 = just ( {!!} ) - constraint1 t0 t1 = nothing - constraint1 t1 t1 = nothing + hom : Arrow {c₁} {c₂} a b -comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Maybe ( Arrow {c₁} {c₂} b c ) → Maybe ( Arrow {c₁} {c₂} a b ) → Maybe ( Arrow {c₁} {c₂} 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 {_} {_} {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 {_} {_} {_} {_} {_} (just _ ) ( just _ ) = nothing +comp : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → Arrow {c₁} {c₂} b c → Arrow {c₁} {c₂} a b → Arrow {c₁} {c₂} a c +comp {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f +comp {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g +comp {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 +comp {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f +comp {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g +comp {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 open TwoHom _×_ : ∀ {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₂} a b )) (c₂) -_==_ = Eq _≡_ - -==refl : ∀{ c₁ c₂ a b } → ∀ {x : Maybe (Arrow {c₁} {c₂} a b )} → x == x -==refl {_} {_} {_} {_} {just x} = just refl -==refl {_} {_} {_} {_} {nothing} = nothing - -==sym : ∀{ c₁ c₂ a b } → ∀ {x y : Maybe (Arrow {c₁} {c₂} 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₂} 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₂} a b )} → - (f : Maybe (Arrow {c₁} {c₂} a b ) → Maybe (Arrow {c₁} {c₂} 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₂} a b ))) : - Set c₂ where - relTo : (x≈y : x == y ) → x IsRelatedTo y - - begin_ : { a b : TwoObject {c₁} } {x : Maybe (Arrow {c₁} {c₂} a b ) } {y : Maybe (Arrow {c₁} {c₂} a b )} → - x IsRelatedTo y → x == y - begin relTo x≈y = x≈y - - _==⟨_⟩_ : { a b : TwoObject {c₁} } (x : Maybe (Arrow {c₁} {c₂} a b )) {y z : Maybe (Arrow {c₁} {c₂} 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₂} a b )) {y : Maybe (Arrow {c₁} {c₂} a b )} - → x IsRelatedTo y → x IsRelatedTo y - _ ==⟨⟩ x≈y = x≈y - - _∎ : { a b : TwoObject {c₁} }(x : Maybe (Arrow {c₁} {c₂} 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 @@ -120,126 +59,73 @@ {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 ) + 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₂} {_} {_} {_} {_} {f} {g} {h} | nothing | _ | _ = nothing -assoc-× {c₁} {c₂} {_} {_} {_} {_} {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 -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₂} {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-× {_} {_} {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} {t1} {_} {_} {_} | (just _) | (just _) | (just _) = 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-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | (just _) = nothing -assoc-× {_} {_} {t0} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing -assoc-× {_} {_} {t1} {t0} {t0} {t0} {_} {_} {_} | (just id-t0) | (just id-t0) | (just _) = nothing -assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-f) | (just id-t0) | (just _) = nothing -assoc-× {_} {_} {t1} {t0} {t0} {t1} {_} {_} {_} | (just arrow-g) | (just id-t0) | (just _) = nothing -assoc-× {_} {_} {t1} {t1} {t0} {_} {_} {_} {_} | (just _) | (just _) | (just _) = nothing -assoc-× {_} {_} {t1} {t1} {t0} {t0} {_} {_} {_} | (just _) | (just _) | nothing = nothing +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 = record { hom = just id-t0 } -TwoId {_} {_} t1 = record { hom = just id-t1 } +TwoId {_} {_} t0 = record { hom = id-t0 } +TwoId {_} {_} t1 = record { hom = id-t1 } open import Relation.Binary +open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) + 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 ; + _≈_ = λ x y → hom x ≡ hom y ; Id = λ{a} → TwoId {c₁ } { c₂} a ; isCategory = record { - isEquivalence = record {refl = ==refl ; trans = ==trans ; sym = ==sym } ; + 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₂} {a} {b} {f} with hom f | constraint1 f a b - identityL {c₁} {c₂} {t1} {t0} {f} | _ | just C = ⊥-elim C - identityL {c₁} {c₂} {t1} {t0} {_} | just _ | nothing = {!!} - 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} {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 + identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → hom ((TwoId B) × f) ≡ hom f + identityL {c₁} {c₂} {a} {b} {f} with hom 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 + 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} {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 - identityR {c₁} {c₂} {t1} {t0} {_} | just _ = {!!} + 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)} → - hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g ) + 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 + let open ≡-Reasoning in begin hom ( h × f ) - ==⟨⟩ + ≡⟨ refl ⟩ 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) - ==⟨⟩ + ≡⟨ refl ⟩ 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 - -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 -> TwoObject {c₁}) → Functor A A -indexFunctor {c₁} {c₂} {ℓ} A none a b f g obj→ hom→ = record { +indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → + (obj→ : Obj A -> TwoObject {c₁}) (hom→ : {a b : Obj A} -> Hom A a b -> TwoHom {c₁} {c₂} (obj→ a) (obj→ b) ) → Functor A A +indexFunctor {c₁} {c₂} {ℓ} A a b f g obj→ hom→ = record { FObj = λ a → fobj a ; FMap = λ {a} {b} f → fmap {a} {b} f ; isFunctor = record { - identity = λ{x} → identity {x} + 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} } @@ -249,62 +135,23 @@ fobj x | t0 = a fobj x | t1 = b fmap : {x y : Obj A } → (Hom A x y ) → Hom A (fobj x) (fobj y) - fmap {x} {y} h with obj→ x | obj→ y | hom→ h - fmap h | t0 | t0 | _ = id1 A a - fmap h | t1 | t1 | _ = id1 A b - fmap h | t0 | t1 | t0 = f - fmap h | t0 | t1 | t1 = g - fmap h | _ | _ | _ = nil none - open ≈-Reasoning A - ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ] + fmap {x} {y} h with obj→ x | obj→ y | hom ( hom→ h ) + fmap h | t0 | t0 | id-t0 = id1 A a + fmap h | t1 | t1 | id-t1 = id1 A b + fmap h | t0 | t1 | arrow-f = f + fmap h | t0 | t1 | arrow-g = g + ≈-cong : {a : Obj A} {b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ fmap f ≈ fmap g ] ≈-cong = {!!} - identity : {x : Obj A} → A [ fmap ( id1 A x ) ≈ id1 A (fobj x) ] - identity {x} with obj→ x - identity | t0 = refl-hom - identity | t1 = refl-hom - distr1 : {a₁ : Obj A} {b₁ : Obj A} {c : Obj A} {f₁ : Hom A a₁ b₁} {g₁ : Hom A b₁ c} → - A [ fmap (A [ g₁ o f₁ ]) ≈ A [ fmap g₁ o fmap f₁ ] ] - distr1 {a1} {b1} {c1} {f1} {g1} with obj→ a1 | obj→ b1 | obj→ c1 | hom→ f1 | hom→ g1 - distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t0 | _ | _ = begin - id1 A a - ≈↑⟨ idL ⟩ - id1 A a o id1 A a - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t1 | _ | _ = begin - id1 A b - ≈↑⟨ idL ⟩ - id1 A b o id1 A b - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t0 | _ | _ = begin - nil none - ≈↑⟨ nil-idR none ⟩ - id1 A a o nil none - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t1 | t0 | _ | _ = begin - nil none - ≈↑⟨ nil-idL none ⟩ - nil none o id1 A b - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t0 | _ | _ = begin - id1 A a - ≈↑⟨ nil-id none ⟩ - nil none - ≈↑⟨ nil-idL none ⟩ - nil none o _ - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t1 | t0 | t1 | _ | _ = begin - id1 A b - ≈↑⟨ nil-id none ⟩ - nil none - ≈↑⟨ nil-idR none ⟩ - _ o nil none - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t0 | t1 | _ | _ = begin - {!!} - ≈⟨ {!!} ⟩ - {!!} o id1 A a - ∎ - distr1 {a1} {b1} {c1} {f1} {g1} | t0 | t1 | t1 | _ | _ = {!!} + identity : (x : Obj A) → A [ fmap ( id1 A x ) ≈ id1 A (fobj x) ] + identity x = {!!} + -- identity x with obj→ x + -- identity _ | t0 = ? + -- identity _ | t1 = ? + distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} → + A [ fmap (A [ g o f ]) ≈ A [ fmap g o fmap f ] ] + distr1 {a} {b} {c} {f} {g} = {!!} + -- distr1 {a} {b} {c} {f} {g} with (obj→ a) | (obj→ b ) | ( obj→ c ) | ( hom→ f ) | ( hom→ g ) + -- distr1 {a} {b} {c} {f} {g} | _ | _ | _ | _ | _ = ? @@ -355,31 +202,13 @@ eqlim = isLimit comp Γ c = {!!} e = {!!} - 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 = {!!} - 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 - ≈⟨ {!!} ⟩ - 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 [ {!!} o k' ] ≈ {!!} ] - uniq-nat d h k' ek'=h = begin - {!!} o k' - ≈⟨⟩ - e o k' - ≈⟨ ek'=h ⟩ - h - ≈⟨⟩ - {!!} - ∎ - uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → + 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 = {!!} + 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 = {!!} + 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 [ {!!} o k' ] ≈ {!!} ] + uniq-nat = {!!} + 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 - k h fh=gh - ≈⟨ {!!} ⟩ - k' - ∎ - - + → {!!} -- A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] + uniquness = {!!} diff -r 7ed0045e4adf -r 3c2ce4474d92 negnat.agda --- a/negnat.agda Tue Feb 28 22:33:03 2017 +0900 +++ b/negnat.agda Thu Mar 02 11:36:31 2017 +0900 @@ -49,13 +49,13 @@ Fin-elim P s z fzero = z Fin-elim P s z (fsuc x) = s (Fin-elim P s z x) -Nope0 : ℕ → Set -Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥ - Nope1 : ℕ -> Set Nope1 zero = ⊥ Nope1 (suc _) = ⊤ +Nope0 : ℕ → Set +Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥ + bad : Fin 0 → ⊥ bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _ @@ -88,7 +88,7 @@ isEven : EvenDecidable isEven zero = yes _ -isEven (suc zero) = no λ () +isEven (suc zero) = no (λ ()) isEven (suc (suc n)) = isEven n data Bool : Set where @@ -148,13 +148,6 @@ mod (suc zero) = suc zero mod (suc (suc N)) = mod N -lemma1 : { n : ℕ } -> mod (suc (suc n )) ≡ mod n -lemma1 = refl - -lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n -lemma2 = refl - - proof1 : (n : ℕ ) -> ( if ⌊ isEven n ⌋ then zero else (suc zero) ) ≡ ( mod n ) proof1 zero = refl proof1 (suc zero) = refl @@ -167,6 +160,12 @@ mod n ≡⟨ sym (lemma1 {n}) ⟩ mod (suc (suc n)) - ∎ + ∎ where + lemma1 : { n : ℕ } -> mod (suc (suc n )) ≡ mod n + lemma1 = refl + lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n + lemma2 = refl + +