From f41f5226b93437341609879e72e499aedd4f0902 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Sat, 15 Feb 2020 13:41:51 +0000 Subject: [PATCH] Some graphs stuff (#98) --- Categories/Examples.agda | 25 +++++++++++++---------- Everything/Safe.agda | 6 ++++++ Graphs/Colouring.agda | 21 ++++++++++++++++++++ Graphs/CompleteGraph.agda | 28 ++++++++++++++++++++++++++ Graphs/CycleGraph.agda | 28 ++++++++++++++++++++++++++ Graphs/Definition.agda | 34 ++++++++++++++++++++++++++++++++ Graphs/PathGraph.agda | 26 ++++++++++++++++++++++++ Graphs/RamseyTriangle.agda | 23 +++++++++++++++++++++ Graphs/UnionGraph.agda | 29 +++++++++++++++++++++++++++ Groups/Abelian/DirectSum.agda | 4 ++-- Groups/DirectSum/Definition.agda | 4 ++-- Lists/Lists.agda | 8 ++++++++ LogicalFormulae.agda | 3 +++ Modules/DirectSum.agda | 12 +++++------ Numbers/Naturals/Definition.agda | 5 +++++ Rings/DirectSum.agda | 16 +++++++-------- Setoids/DirectSum.agda | 23 ++++++++++----------- Setoids/Product.agda | 19 ++++++++++++++++++ 18 files changed, 275 insertions(+), 39 deletions(-) create mode 100644 Graphs/Colouring.agda create mode 100644 Graphs/CompleteGraph.agda create mode 100644 Graphs/CycleGraph.agda create mode 100644 Graphs/Definition.agda create mode 100644 Graphs/PathGraph.agda create mode 100644 Graphs/RamseyTriangle.agda create mode 100644 Graphs/UnionGraph.agda create mode 100644 Setoids/Product.agda diff --git a/Categories/Examples.agda b/Categories/Examples.agda index cb5b036..b461c9e 100644 --- a/Categories/Examples.agda +++ b/Categories/Examples.agda @@ -8,6 +8,11 @@ open import Vectors open import Semirings.Definition open import Categories.Definition open import Groups.Definition +open import Setoids.Setoids +open import Groups.Homomorphisms.Definition +open import Groups.Homomorphisms.Examples +open import Groups.Homomorphisms.Lemmas +open import Functions module Categories.Examples where @@ -20,13 +25,13 @@ Category.rightId (SET {a}) = λ f → refl Category.leftId (SET {a}) = λ f → refl Category.compositionAssociative (SET {a}) = λ f g h → refl -GROUP : {a b : _} → Category {lsuc a ⊔ b} {a ⊔ b} -Category.objects (GROUP {a}) = Group {!!} {!!} -Category.arrows (GROUP {a}) = {!!} -Category.id (GROUP {a}) = {!!} -Category._∘_ (GROUP {a}) = {!!} -Category.rightId (GROUP {a}) = {!!} -Category.leftId (GROUP {a}) = {!!} +GROUP : {a b : _} → Category {lsuc a ⊔ lsuc b} {a ⊔ b} +Category.objects (GROUP {a} {b}) = Sg (Set a) (λ A → Sg (A → A → A) (λ _+_ → Sg (Setoid {a} {b} A) (λ S → Group S _+_))) +Category.arrows (GROUP {a}) (A , (_+A_ , (S , G))) (B , (_+B_ , (T , H))) = Sg (A → B) (GroupHom G H) +Category.id (GROUP {a}) (A , (_+A_ , (S , G))) = (λ i → i) , identityHom G +Category._∘_ (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} {C , (_+C_ , (U , I))} (f , fHom) (g , gHom) = (f ∘ g) , groupHomsCompose gHom fHom +Category.rightId (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} (f , fHom) = {!!} +Category.leftId (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} (f , fHom) = {!!} Category.compositionAssociative (GROUP {a}) = {!!} DISCRETE : {a : _} (X : Set a) → Category {a} {a} @@ -34,6 +39,6 @@ Category.objects (DISCRETE X) = X Category.arrows (DISCRETE X) = λ a b → a ≡ b Category.id (DISCRETE X) = λ x → refl Category._∘_ (DISCRETE X) = λ y=z x=y → transitivity x=y y=z -Category.rightId (DISCRETE X) = {!!} -Category.leftId (DISCRETE X) = {!!} -Category.compositionAssociative (DISCRETE X) = {!!} +Category.rightId (DISCRETE X) refl = refl +Category.leftId (DISCRETE X) refl = refl +Category.compositionAssociative (DISCRETE X) refl refl refl = refl diff --git a/Everything/Safe.agda b/Everything/Safe.agda index cbc4db7..3de1cae 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -133,4 +133,10 @@ open import Modules.Examples open import Modules.Lemmas open import Modules.DirectSum +open import Graphs.PathGraph +open import Graphs.CycleGraph +open import Graphs.UnionGraph +open import Graphs.CompleteGraph +open import Graphs.Colouring + module Everything.Safe where diff --git a/Graphs/Colouring.agda b/Graphs/Colouring.agda new file mode 100644 index 0000000..810a94f --- /dev/null +++ b/Graphs/Colouring.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.FinSet.Definition +open import Numbers.Naturals.Semiring + +module Graphs.Colouring where + +Colouring : (n : ℕ) {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) → Set (a ⊔ c) +Colouring n {V' = V'} G = {x y : V'} → (Graph._<->_ G x y) → FinSet n + +inheritColouring : {n : ℕ} {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} → (k : Colouring n G) → {e : _} {pred : V' → Set e} {sub : subset V pred} {d : _} {_<->'_ : Rel {_} {d} (Sg V' pred)} (H : Subgraph G sub _<->'_) → Colouring n (subgraphIsGraph H) +inheritColouring k H {v1 , _} {v2 , _} x-y = k (Subgraph.inherits H x-y) + +Monochromatic : {a b c : Level} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} {n : ℕ} → (k : Colouring n G) → {d e : _} {pred : V' → Set d} {sub : subset V pred} {_<->'_ : Rel {_} {e} (Sg V' pred)} (H : Subgraph G sub _<->'_) → Set (a ⊔ d ⊔ e) +Monochromatic {V' = V'} {n = n} k {pred = pred} {sub = sub} {_<->'_} H = Sg (FinSet n) (λ c → {x : Sg V' pred} {y : Sg V' pred} (edge : x <->' y) → (inheritColouring k H) edge ≡ c) diff --git a/Graphs/CompleteGraph.agda b/Graphs/CompleteGraph.agda new file mode 100644 index 0000000..9083749 --- /dev/null +++ b/Graphs/CompleteGraph.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.FinSet.Definition +open import Numbers.Naturals.Semiring +open import Sets.EquivalenceRelations + +module Graphs.CompleteGraph where + +CompleteGraph : {a b : _} {V' : Set a} (V : Setoid {a} {b} V') → Graph b V +Graph._<->_ (CompleteGraph V) x y = ((Setoid._∼_ V x y) → False) +Graph.noSelfRelation (CompleteGraph V) x x!=x = x!=x (Equivalence.reflexive (Setoid.eq V)) +Graph.symmetric (CompleteGraph V) x!=y y=x = x!=y ((Equivalence.symmetric (Setoid.eq V)) y=x) +Graph.wellDefined (CompleteGraph V) {x} {y} {r} {s} x=y r=s x!=r y=s = x!=r (transitive x=y (transitive y=s (symmetric r=s))) + where + open Setoid V + open Equivalence eq + +Kn : (n : ℕ) → Graph _ (reflSetoid (FinSet n)) +Kn n = CompleteGraph (reflSetoid (FinSet n)) + +triangle : Graph _ (reflSetoid (FinSet 3)) +triangle = Kn 3 diff --git a/Graphs/CycleGraph.agda b/Graphs/CycleGraph.agda new file mode 100644 index 0000000..39d99f1 --- /dev/null +++ b/Graphs/CycleGraph.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.FinSet.Definition +open import Sets.FinSet.Lemmas +open import Numbers.Naturals.Semiring +open import Numbers.Naturals.Order +open import Sets.EquivalenceRelations +open import Graphs.PathGraph + +module Graphs.CycleGraph where + +CycleGraph : (n : ℕ) → .(2 _ (CycleGraph n _) x y = ((toNat x ≡ succ (toNat y)) || (toNat y ≡ succ (toNat x))) || (((toNat x ≡ 0) && (toNat y ≡ n)) || ((toNat y ≡ 0) && (toNat x ≡ n))) +Graph.noSelfRelation (CycleGraph n _) y (inl (inl x)) = nNotSucc x +Graph.noSelfRelation (CycleGraph n _) y (inl (inr x)) = nNotSucc x +Graph.noSelfRelation (CycleGraph (succ n) _) y (inr (inl (fst ,, snd))) = naughtE (transitivity (equalityCommutative fst) snd) +Graph.noSelfRelation (CycleGraph (succ n) _) y (inr (inr (fst ,, snd))) = naughtE (transitivity (equalityCommutative fst) snd) +Graph.symmetric (CycleGraph n _) (inl (inl x)) = inl (inr x) +Graph.symmetric (CycleGraph n _) (inl (inr x)) = inl (inl x) +Graph.symmetric (CycleGraph n _) (inr (inl x)) = inr (inr x) +Graph.symmetric (CycleGraph n _) (inr (inr x)) = inr (inl x) +Graph.wellDefined (CycleGraph n _) refl refl i = i diff --git a/Graphs/Definition.agda b/Graphs/Definition.agda new file mode 100644 index 0000000..935663e --- /dev/null +++ b/Graphs/Definition.agda @@ -0,0 +1,34 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset + +module Graphs.Definition where + +record Graph {a b : _} (c : _) {V' : Set a} (V : Setoid {a} {b} V') : Set (a ⊔ b ⊔ lsuc c) where + field + _<->_ : Rel {a} {c} V' + noSelfRelation : (x : V') → x <-> x → False + symmetric : {x y : V'} → x <-> y → y <-> x + wellDefined : {x y r s : V'} → Setoid._∼_ V x y → Setoid._∼_ V r s → x <-> r → y <-> s + +record GraphIso {a b c d e m : _} {V1' : Set a} {V2' : Set b} {V1 : Setoid {a} {c} V1'} {V2 : Setoid {b} {d} V2'} (G : Graph e V1) (H : Graph m V2) (f : V1' → V2') : Set (a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ m) where + field + bij : SetoidBijection V1 V2 f + respects : (x y : V1') → Graph._<->_ G x y → Graph._<->_ H (f x) (f y) + respects' : (x y : V1') → Graph._<->_ H (f x) (f y) → Graph._<->_ G x y + +record Subgraph {a b c d e : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) {pred : V' → Set d} (sub : subset V pred) (_<->'_ : Rel {_} {e} (Sg V' pred)) : Set (a ⊔ b ⊔ c ⊔ d ⊔ e) where + field + inherits : {x y : Sg V' pred} → (x <->' y) → (Graph._<->_ G (underlying x) (underlying y)) + symmetric : {x y : Sg V' pred} → (x <->' y) → (y <->' x) + wellDefined : {x y r s : Sg V' pred} → Setoid._∼_ (subsetSetoid V sub) x y → Setoid._∼_ (subsetSetoid V sub) r s → x <->' r → y <->' s + +subgraphIsGraph : {a b c d e : _} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} {pred : V' → Set d} {sub : subset V pred} {rel : Rel {_} {e} (Sg V' pred)} (H : Subgraph G sub rel) → Graph e (subsetSetoid V sub) +Graph._<->_ (subgraphIsGraph {rel = rel} H) = rel +Graph.noSelfRelation (subgraphIsGraph {G = G} H) (v , isSub) v=v = Graph.noSelfRelation G v (Subgraph.inherits H v=v) +Graph.symmetric (subgraphIsGraph H) v1=v2 = Subgraph.symmetric H v1=v2 +Graph.wellDefined (subgraphIsGraph H) = Subgraph.wellDefined H diff --git a/Graphs/PathGraph.agda b/Graphs/PathGraph.agda new file mode 100644 index 0000000..0613129 --- /dev/null +++ b/Graphs/PathGraph.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.FinSet.Definition +open import Sets.FinSet.Lemmas +open import Numbers.Naturals.Semiring +open import Sets.EquivalenceRelations + +module Graphs.PathGraph where + +nNotSucc : {n : ℕ} → (n ≡ succ n) → False +nNotSucc {zero} () +nNotSucc {succ n} pr = nNotSucc (succInjective pr) + +PathGraph : (n : ℕ) → Graph _ (reflSetoid (FinSet (succ n))) +Graph._<->_ (PathGraph n) x y = (toNat x ≡ succ (toNat y)) || (toNat y ≡ succ (toNat x)) +Graph.noSelfRelation (PathGraph n) x (inl bad) = nNotSucc bad +Graph.noSelfRelation (PathGraph n) x (inr bad) = nNotSucc bad +Graph.symmetric (PathGraph n) (inl x) = inr x +Graph.symmetric (PathGraph n) (inr x) = inl x +Graph.wellDefined (PathGraph n) refl refl i = i diff --git a/Graphs/RamseyTriangle.agda b/Graphs/RamseyTriangle.agda new file mode 100644 index 0000000..8610d63 --- /dev/null +++ b/Graphs/RamseyTriangle.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --warning=error --safe --without-K #-} + +open import LogicalFormulae +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) +open import Functions +open import Setoids.Setoids +open import Setoids.Subset +open import Graphs.Definition +open import Sets.FinSet.Definition +open import Numbers.Naturals.Semiring +open import Numbers.Naturals.Order +open import Sets.EquivalenceRelations +open import Graphs.CompleteGraph +open import Graphs.Colouring + +module Graphs.RamseyTriangle where + +hasMonochromaticTriangle : {a : _} {n : ℕ} (G : Graph a (reflSetoid (FinSet n))) → Set (lsuc lzero) +hasMonochromaticTriangle {n = n} G = Sg (FinSet n → Set) λ pred → (subset (reflSetoid (FinSet n)) pred) && {!!} + +ramseyForTriangle : (k : ℕ) → Sg ℕ (λ N → (n : ℕ) → (N _ (unionGraph {c = c} {f = f} G H) (inl v) (inl v2) = embedLevel {c} {f} (Graph._<->_ G v v2) +Graph._<->_ (unionGraph G H) (inl v) (inr w) = False' +Graph._<->_ (unionGraph G H) (inr w) (inl v) = False' +Graph._<->_ (unionGraph {c = c} {f = f} G H) (inr w) (inr w2) = embedLevel {f} {c} (Graph._<->_ H w w2) +Graph.noSelfRelation (unionGraph G H) (inl v) (v=v ,, _) = Graph.noSelfRelation G v v=v +Graph.noSelfRelation (unionGraph G H) (inr w) (w=w ,, _) = Graph.noSelfRelation H w w=w +Graph.symmetric (unionGraph G H) {inl x} {inl y} (x=y ,, _) = Graph.symmetric G x=y ,, record {} +Graph.symmetric (unionGraph G H) {inr x} {inr y} (x=y ,, _) = Graph.symmetric H x=y ,, record {} +Graph.wellDefined (unionGraph G H) {inl x} {inl y} {inl z} {inl w} (x=y ,, _) (y=z ,, _) (z=w ,, _) = Graph.wellDefined G x=y y=z z=w ,, record {} +Graph.wellDefined (unionGraph G H) {inr x} {inr y} {inr z} {inr w} (x=y ,, _) (y=z ,, _) (z=w ,, _) = Graph.wellDefined H x=y y=z z=w ,, record {} diff --git a/Groups/Abelian/DirectSum.agda b/Groups/Abelian/DirectSum.agda index 4b8a72a..79fb13e 100644 --- a/Groups/Abelian/DirectSum.agda +++ b/Groups/Abelian/DirectSum.agda @@ -7,7 +7,7 @@ open import Groups.Abelian.Definition module Groups.Abelian.DirectSum {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+1_ : A → A → A} {_+2_ : B → B → B} {G1' : Group S _+1_} {G2' : Group T _+2_} (G1 : AbelianGroup G1') (G2 : AbelianGroup G2') where open import Groups.DirectSum.Definition G1' G2' -open import Setoids.DirectSum S T +open import Setoids.Product S T directSumAbGroup : AbelianGroup directSumGroup -AbelianGroup.commutative directSumAbGroup = directSumLift (AbelianGroup.commutative G1) (AbelianGroup.commutative G2) +AbelianGroup.commutative directSumAbGroup = productLift (AbelianGroup.commutative G1) (AbelianGroup.commutative G2) diff --git a/Groups/DirectSum/Definition.agda b/Groups/DirectSum/Definition.agda index fb86445..8cea052 100644 --- a/Groups/DirectSum/Definition.agda +++ b/Groups/DirectSum/Definition.agda @@ -6,9 +6,9 @@ open import Groups.Definition module Groups.DirectSum.Definition {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) where -open import Setoids.DirectSum S T +open import Setoids.Product S T -directSumGroup : Group directSumSetoid (λ x1 y1 → (((_&&_.fst x1) ·A (_&&_.fst y1)) ,, ((_&&_.snd x1) ·B (_&&_.snd y1)))) +directSumGroup : Group productSetoid (λ x1 y1 → (((_&&_.fst x1) ·A (_&&_.fst y1)) ,, ((_&&_.snd x1) ·B (_&&_.snd y1)))) Group.+WellDefined directSumGroup (s ,, t) (u ,, v) = Group.+WellDefined G s u ,, Group.+WellDefined H t v Group.0G directSumGroup = (Group.0G G ,, Group.0G H) Group.inverse directSumGroup (g1 ,, H1) = (Group.inverse G g1) ,, (Group.inverse H H1) diff --git a/Lists/Lists.agda b/Lists/Lists.agda index be53e18..eb0e9fd 100644 --- a/Lists/Lists.agda +++ b/Lists/Lists.agda @@ -38,3 +38,11 @@ listZip : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) listZip f f1 f2 [] l2 = map f2 l2 listZip f f1 f2 (x :: l1) [] = map f1 (x :: l1) listZip f f1 f2 (x :: l1) (y :: l2) = (f x y) :: listZip f f1 f2 l1 l2 + +contains : {a : _} {A : Set a} (l : List A) (needle : A) → Set a +contains [] needle = False' +contains (x :: l) needle = (x ≡ needle) || contains l needle + +containsMap : {a b : _} {A : Set a} {B : Set b} (f : A → B) (l : List A) (needle : A) → (contains l needle) → contains (map f l) (f needle) +containsMap f (x :: l) needle (inl cont) = inl (applyEquality f cont) +containsMap f (x :: l) needle (inr cont) = inr (containsMap f l needle cont) diff --git a/LogicalFormulae.agda b/LogicalFormulae.agda index 6bd4821..c6ae14a 100644 --- a/LogicalFormulae.agda +++ b/LogicalFormulae.agda @@ -116,3 +116,6 @@ decidableOr : {a b : _} → (A : Set a) → (B : Set b) → (A || (A → False)) decidableOr {a} {b} A B decidable (inl x) = inl x decidableOr {a} {b} A B (inl y) (inr x) = inl y decidableOr {a} {b} A B (inr y) (inr x) = inr (record { fst = y ; snd = x}) + +embedLevel : {a b : _} → Set a → Set (a ⊔ b) +embedLevel {a} {b} A = A && (True' {b}) diff --git a/Modules/DirectSum.agda b/Modules/DirectSum.agda index f061fef..bc3d54d 100644 --- a/Modules/DirectSum.agda +++ b/Modules/DirectSum.agda @@ -11,11 +11,11 @@ open import Modules.Definition module Modules.DirectSum {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*R_ : A → A → A} (R : Ring S _+R_ _*R_) {m n o p : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·1_ : A → M → M} {N : Set o} {U : Setoid {o} {p} N} {_+'_ : N → N → N} {H' : Group U _+'_} {H : AbelianGroup H'} {_·2_ : A → N → N} (M1 : Module R G _·1_) (M2 : Module R H _·2_) where open import Groups.Abelian.DirectSum G H -open import Setoids.DirectSum T U +open import Setoids.Product T U directSumModule : Module R directSumAbGroup λ r mn → ((r ·1 (_&&_.fst mn)) ,, (r ·2 (_&&_.snd mn))) -Module.dotWellDefined directSumModule r=s t=u = directSumLift (Module.dotWellDefined M1 r=s (_&&_.fst t=u)) (Module.dotWellDefined M2 r=s (_&&_.snd t=u)) -Module.dotDistributesLeft directSumModule = directSumLift (Module.dotDistributesLeft M1) (Module.dotDistributesLeft M2) -Module.dotDistributesRight directSumModule = directSumLift (Module.dotDistributesRight M1) (Module.dotDistributesRight M2) -Module.dotAssociative directSumModule = directSumLift (Module.dotAssociative M1) (Module.dotAssociative M2) -Module.dotIdentity directSumModule = directSumLift (Module.dotIdentity M1) (Module.dotIdentity M2) +Module.dotWellDefined directSumModule r=s t=u = productLift (Module.dotWellDefined M1 r=s (_&&_.fst t=u)) (Module.dotWellDefined M2 r=s (_&&_.snd t=u)) +Module.dotDistributesLeft directSumModule = productLift (Module.dotDistributesLeft M1) (Module.dotDistributesLeft M2) +Module.dotDistributesRight directSumModule = productLift (Module.dotDistributesRight M1) (Module.dotDistributesRight M2) +Module.dotAssociative directSumModule = productLift (Module.dotAssociative M1) (Module.dotAssociative M2) +Module.dotIdentity directSumModule = productLift (Module.dotIdentity M1) (Module.dotIdentity M2) diff --git a/Numbers/Naturals/Definition.agda b/Numbers/Naturals/Definition.agda index f56f317..b2cd49a 100644 --- a/Numbers/Naturals/Definition.agda +++ b/Numbers/Naturals/Definition.agda @@ -29,3 +29,8 @@ aIsNotSuccA (succ a) pr = aIsNotSuccA a (succInjective pr) ℕDecideEquality (succ a) (succ b) with ℕDecideEquality a b ℕDecideEquality (succ a) (succ b) | inl x = inl (applyEquality succ x) ℕDecideEquality (succ a) (succ b) | inr x = inr λ pr → x (succInjective pr) + +ℕDecideEquality' : (a b : ℕ) → Bool +ℕDecideEquality' a b with ℕDecideEquality a b +ℕDecideEquality' a b | inl x = BoolTrue +ℕDecideEquality' a b | inr x = BoolFalse diff --git a/Rings/DirectSum.agda b/Rings/DirectSum.agda index 767059d..edcc639 100644 --- a/Rings/DirectSum.agda +++ b/Rings/DirectSum.agda @@ -8,7 +8,7 @@ open import Rings.Definition module Rings.DirectSum {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ : A → A → A} {_*1_ : A → A → A} {C : Set c} {T : Setoid {c} {d} C} {_+2_ : C → C → C} {_*2_ : C → C → C} (R1 : Ring S _+1_ _*1_) (R2 : Ring T _+2_ _*2_) where -open import Setoids.DirectSum S T +open import Setoids.Product S T pairPlus : A && C → A && C → A && C pairPlus (a ,, b) (c ,, d) = (a +1 c) ,, (b +2 d) @@ -16,12 +16,12 @@ pairPlus (a ,, b) (c ,, d) = (a +1 c) ,, (b +2 d) pairTimes : A && C → A && C → A && C pairTimes (a ,, b) (c ,, d) = (a *1 c) ,, (b *2 d) -directSumRing : Ring directSumSetoid pairPlus pairTimes +directSumRing : Ring productSetoid pairPlus pairTimes Ring.additiveGroup directSumRing = directSumGroup (Ring.additiveGroup R1) (Ring.additiveGroup R2) -Ring.*WellDefined directSumRing r=t s=u = directSumLift (Ring.*WellDefined R1 (_&&_.fst r=t) (_&&_.fst s=u)) (Ring.*WellDefined R2 (_&&_.snd r=t) (_&&_.snd s=u)) +Ring.*WellDefined directSumRing r=t s=u = productLift (Ring.*WellDefined R1 (_&&_.fst r=t) (_&&_.fst s=u)) (Ring.*WellDefined R2 (_&&_.snd r=t) (_&&_.snd s=u)) Ring.1R directSumRing = Ring.1R R1 ,, Ring.1R R2 -Ring.groupIsAbelian directSumRing = directSumLift (Ring.groupIsAbelian R1) (Ring.groupIsAbelian R2) -Ring.*Associative directSumRing = directSumLift (Ring.*Associative R1) (Ring.*Associative R2) -Ring.*Commutative directSumRing = directSumLift (Ring.*Commutative R1) (Ring.*Commutative R2) -Ring.*DistributesOver+ directSumRing = directSumLift (Ring.*DistributesOver+ R1) (Ring.*DistributesOver+ R2) -Ring.identIsIdent directSumRing = directSumLift (Ring.identIsIdent R1) (Ring.identIsIdent R2) +Ring.groupIsAbelian directSumRing = productLift (Ring.groupIsAbelian R1) (Ring.groupIsAbelian R2) +Ring.*Associative directSumRing = productLift (Ring.*Associative R1) (Ring.*Associative R2) +Ring.*Commutative directSumRing = productLift (Ring.*Commutative R1) (Ring.*Commutative R2) +Ring.*DistributesOver+ directSumRing = productLift (Ring.*DistributesOver+ R1) (Ring.*DistributesOver+ R2) +Ring.identIsIdent directSumRing = productLift (Ring.identIsIdent R1) (Ring.identIsIdent R2) diff --git a/Setoids/DirectSum.agda b/Setoids/DirectSum.agda index 9037ab1..2920760 100644 --- a/Setoids/DirectSum.agda +++ b/Setoids/DirectSum.agda @@ -1,19 +1,20 @@ {-# OPTIONS --safe --warning=error --without-K #-} +open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) open import LogicalFormulae open import Sets.EquivalenceRelations open import Setoids.Setoids module Setoids.DirectSum {m n o p : _} {A : Set m} {B : Set n} (R : Setoid {m} {o} A) (S : Setoid {n} {p} B) where -open Setoid - -directSumSetoid : Setoid (A && B) -_∼_ (directSumSetoid) (a ,, b) (c ,, d) = (Setoid._∼_ R a c) && (Setoid._∼_ S b d) -Equivalence.reflexive (eq (directSumSetoid)) {(a ,, b)} = Equivalence.reflexive (Setoid.eq R) ,, Equivalence.reflexive (Setoid.eq S) -Equivalence.symmetric (eq (directSumSetoid)) {(a ,, b)} {(c ,, d)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq R) fst ,, Equivalence.symmetric (Setoid.eq S) snd -Equivalence.transitive (eq (directSumSetoid)) {a ,, b} {c ,, d} {e ,, f} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq R) fst1 fst2 ,, Equivalence.transitive (Setoid.eq S) snd1 snd2 - -directSumLift : {r s : A} {t u : B} → (Setoid._∼_ R r s) → (Setoid._∼_ S t u) → Setoid._∼_ directSumSetoid (r ,, t) (s ,, u) -_&&_.fst (directSumLift r=s t=u) = r=s -_&&_.snd (directSumLift r=s t=u) = t=u +directSumSetoid : Setoid {m ⊔ n} (A || B) +Setoid._∼_ directSumSetoid (inl x) (inl y) = embedLevel {o} {p} (Setoid._∼_ R x y) +Setoid._∼_ directSumSetoid (inl x) (inr y) = False' +Setoid._∼_ directSumSetoid (inr x) (inl y) = False' +Setoid._∼_ directSumSetoid (inr x) (inr y) = embedLevel {p} {o} (Setoid._∼_ S x y) +Equivalence.reflexive (Setoid.eq directSumSetoid) {inl x} = Equivalence.reflexive (Setoid.eq R) {x} ,, record {} +Equivalence.reflexive (Setoid.eq directSumSetoid) {inr x} = Equivalence.reflexive (Setoid.eq S) {x} ,, record {} +Equivalence.symmetric (Setoid.eq directSumSetoid) {inl x} {inl y} (x=y ,, _) = (Equivalence.symmetric (Setoid.eq R) x=y) ,, record {} +Equivalence.symmetric (Setoid.eq directSumSetoid) {inr x} {inr y} (x=y ,, _) = (Equivalence.symmetric (Setoid.eq S) x=y) ,, record {} +Equivalence.transitive (Setoid.eq directSumSetoid) {inl x} {inl y} {inl z} (x=y ,, _) (y=z ,, _) = Equivalence.transitive (Setoid.eq R) x=y y=z ,, record {} +Equivalence.transitive (Setoid.eq directSumSetoid) {inr x} {inr y} {inr z} (x=y ,, _) (y=z ,, _) = Equivalence.transitive (Setoid.eq S) x=y y=z ,, record {} diff --git a/Setoids/Product.agda b/Setoids/Product.agda new file mode 100644 index 0000000..09a9e50 --- /dev/null +++ b/Setoids/Product.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --safe --warning=error --without-K #-} + +open import LogicalFormulae +open import Sets.EquivalenceRelations +open import Setoids.Setoids + +module Setoids.Product {m n o p : _} {A : Set m} {B : Set n} (R : Setoid {m} {o} A) (S : Setoid {n} {p} B) where + +open Setoid + +productSetoid : Setoid (A && B) +_∼_ (productSetoid) (a ,, b) (c ,, d) = (Setoid._∼_ R a c) && (Setoid._∼_ S b d) +Equivalence.reflexive (eq (productSetoid)) {(a ,, b)} = Equivalence.reflexive (Setoid.eq R) ,, Equivalence.reflexive (Setoid.eq S) +Equivalence.symmetric (eq (productSetoid)) {(a ,, b)} {(c ,, d)} (fst ,, snd) = Equivalence.symmetric (Setoid.eq R) fst ,, Equivalence.symmetric (Setoid.eq S) snd +Equivalence.transitive (eq (productSetoid)) {a ,, b} {c ,, d} {e ,, f} (fst1 ,, snd1) (fst2 ,, snd2) = Equivalence.transitive (Setoid.eq R) fst1 fst2 ,, Equivalence.transitive (Setoid.eq S) snd1 snd2 + +productLift : {r s : A} {t u : B} → (Setoid._∼_ R r s) → (Setoid._∼_ S t u) → Setoid._∼_ productSetoid (r ,, t) (s ,, u) +_&&_.fst (productLift r=s t=u) = r=s +_&&_.snd (productLift r=s t=u) = t=u