diff --git a/Graph.agda b/Graph.agda
new file mode 100644
index 0000000..90a224a
--- /dev/null
+++ b/Graph.agda
@@ -0,0 +1,3 @@
+module Graph where
+
+open import Graph.Base public
diff --git a/Graph/Base.agda b/Graph/Base.agda
new file mode 100644
index 0000000..4091511
--- /dev/null
+++ b/Graph/Base.agda
@@ -0,0 +1,90 @@
+module Graph.Base where
+
+infixl 4 _≡_
+infixl 4 _≤_
+infixl 8 _+_
+infixl 9 _⇀_
+
+data Graph (A : Set) : Set where
+  ε : Graph A
+  Vertex : A → Graph A
+  _+_ : Graph A → Graph A → Graph A
+  _⇀_ : Graph A → Graph A → Graph A
+
+-- vertex axioms
+data _∈ᵥ_ { A : Set } : A → Graph A → Set where
+  x∈Vx : ∀ { x : A } → x ∈ᵥ Vertex x
+  +ₗ : ∀ { x : A } { G H : Graph A } → x ∈ᵥ G → x ∈ᵥ (G + H)
+  +ᵣ : ∀ { x : A } { G H : Graph A } → x ∈ᵥ H → x ∈ᵥ (G + H)
+  ⇀ₗ : ∀ { x : A } { G H : Graph A } → x ∈ᵥ G → x ∈ᵥ (G ⇀ H)
+  ⇀ᵣ : ∀ { x : A } { G H : Graph A } → x ∈ᵥ H → x ∈ᵥ (G ⇀ H)
+
+-- edge axioms
+data ⟦_,_⟧∈ₑ_ { A : Set } : A → A → Graph A → Set where
+  +ₗ : ∀ { x y : A } { G H : Graph A } → ⟦ x , y ⟧∈ₑ G → ⟦ x , y ⟧∈ₑ (G + H)
+  +ᵣ : ∀ { x y : A } { G H : Graph A } → ⟦ x , y ⟧∈ₑ H → ⟦ x , y ⟧∈ₑ (G + H)
+  ⇀ₗ : ∀ { x y : A } { G H : Graph A } → ⟦ x , y ⟧∈ₑ G → ⟦ x , y ⟧∈ₑ (G ⇀ H)
+  ⇀ᵣ : ∀ { x y : A } { G H : Graph A } → ⟦ x , y ⟧∈ₑ H → ⟦ x , y ⟧∈ₑ (G ⇀ H)
+  ⇀ₗᵣ : ∀ { x y : A } { G H : Graph A } → x ∈ᵥ G → y ∈ᵥ H → ⟦ x , y ⟧∈ₑ (G ⇀ H)
+
+-- equality axioms
+record _≡_ { A : Set } ( G H : Graph A ) : Set where
+  field
+    vₗ : ∀ { x : A } → x ∈ᵥ G → x ∈ᵥ H
+    vᵣ : ∀ { x : A } → x ∈ᵥ H → x ∈ᵥ G
+    eₗ : ∀ { x y : A } → ⟦ x , y ⟧∈ₑ G → ⟦ x , y ⟧∈ₑ H
+    eᵣ : ∀ { x y : A } → ⟦ x , y ⟧∈ₑ H → ⟦ x , y ⟧∈ₑ G
+
+record _≤_ { A : Set} ( G H : Graph A ) : Set where
+  field
+    def : G + H ≡ H
+
+refl : ∀ { A : Set } { G : Graph A } → G ≡ G
+refl = record
+         { vₗ = λ z → z ; vᵣ = λ z → z ; eₗ = λ z → z ; eᵣ = λ z → z }
+
+sym : ∀ { A : Set } { G H : Graph A } → G ≡ H → H ≡ G
+sym G≡H = record
+            { vₗ = _≡_.vᵣ G≡H
+            ; vᵣ = _≡_.vₗ G≡H
+            ; eₗ = _≡_.eᵣ G≡H
+            ; eᵣ = _≡_.eₗ G≡H
+            }
+
+trans : ∀ { A : Set } { G H I : Graph A } → G ≡ H → H ≡ I → G ≡ I
+trans G≡H H≡I = record
+                  { vₗ = λ z → _≡_.vₗ H≡I (_≡_.vₗ G≡H z)
+                  ; vᵣ = λ z → _≡_.vᵣ G≡H (_≡_.vᵣ H≡I z)
+                  ; eₗ = λ z → _≡_.eₗ H≡I (_≡_.eₗ G≡H z)
+                  ; eᵣ = λ z → _≡_.eᵣ G≡H (_≡_.eᵣ H≡I z)
+                  }
+
+≡-to-≤ : ∀ { A : Set } { G H : Graph A } → G ≡ H → G ≤ H
+≡-to-≤ G≡H = record
+               { def = record
+                         { vₗ = λ { (+ₗ x) → _≡_.vₗ G≡H x ; (+ᵣ x) → x }
+                         ; vᵣ = λ z → +ₗ (_≡_.vᵣ G≡H z)
+                         ; eₗ = λ { (+ₗ x) → _≡_.eₗ G≡H x ; (+ᵣ x) → x }
+                         ; eᵣ = λ z → +ₗ (_≡_.eᵣ G≡H z)
+                         }
+               }
+
+≤-refl : ∀ { A : Set } { G : Graph A } → G ≤ G
+≤-refl = record
+           { def = record
+                     { vₗ = λ { (+ₗ x) → x ; (+ᵣ x) → x }
+                     ; vᵣ = +ₗ
+                     ; eₗ = λ { (+ₗ x) → x ; (+ᵣ x) → x }
+                     ; eᵣ = +ₗ
+                     }
+           }
+
+≤-trans : ∀ { A : Set } { G H I : Graph A } → G ≤ H → H ≤ I → G ≤ I
+≤-trans G≤H H≤I = record
+                    { def = record
+                              { vₗ = λ { (+ₗ x) → _≡_.vₗ (_≤_.def H≤I) (+ₗ (_≡_.vₗ (_≤_.def G≤H) (+ₗ x))) ; (+ᵣ x) → x }
+                              ; vᵣ = +ᵣ
+                              ; eₗ = λ { (+ₗ x) → _≡_.eₗ (_≤_.def H≤I) (+ₗ (_≡_.eₗ (_≤_.def G≤H) (+ₗ x))) ; (+ᵣ x) → x }
+                              ; eᵣ = +ᵣ
+                              }
+                    }
diff --git a/Graph/Constructors.agda b/Graph/Constructors.agda
new file mode 100644
index 0000000..9c7e3a7
--- /dev/null
+++ b/Graph/Constructors.agda
@@ -0,0 +1,61 @@
+open import Graph.Base
+open import Graph.Properties
+open import Graph.Reasoning
+
+
+open import Data.List
+open import Function
+
+module Graph.Constructors where
+
+edge : {A : Set} → A → A → Graph A
+edge x y = (Vertex x) ⇀ (Vertex y)
+
+vertices : {A : Set} → List A → Graph A
+vertices = (foldr _+_ ε) ∘ (map Vertex)
+
+clique : {A : Set} → List A → Graph A
+clique = (foldr _⇀_ ε) ∘ (map Vertex)
+
+vertices[x]=Vx : { A : Set } → ∀ { x : A } → vertices [ x ] ≡ Vertex x
+vertices[x]=Vx {_} {x} = begin
+  vertices [ x ]  ≡⟨⟩
+  Vertex x + ε    ≡⟨ +-identityʳ ⟩
+  Vertex x        ∎
+  where open ≡-Reasoning
+
+edgexy=clique[x,y] : { A : Set } → ∀ { x y : A } → (edge x y) ≡ (clique (x ∷ (y ∷ [])))
+edgexy=clique[x,y] {_} {x} {y} = begin
+  edge x y                   ≡⟨⟩
+  Vertex x ⇀ Vertex y        ≡⟨ sym ⇀-identˡ ⟩
+  (Vertex x ⇀ Vertex y) ⇀ ε  ≡⟨ sym ⇀-assoc ⟩
+  Vertex x ⇀ (Vertex y ⇀ ε)  ≡⟨⟩
+  clique (x ∷ (y ∷ []))      ∎
+  where open ≡-Reasoning
+
+vertices≤clique : { A : Set } → ∀ ( xs : List A ) → (vertices xs) ≤ (clique xs)
+vertices≤clique [] = begin ε ∎
+  where open ≤-Reasoning
+vertices≤clique (x ∷ xs) = begin
+  vertices (x ∷ xs)      ≡⟨⟩
+  Vertex x + vertices xs ≤⟨ +⇀-order ⟩
+  Vertex x ⇀ vertices xs ≤⟨ ⇀-congʳ-≤ (vertices≤clique xs) ⟩
+  Vertex x ⇀ clique xs   ≡⟨⟩
+  clique (x ∷ xs)        ∎
+  where open ≤-Reasoning
+
+clique-++-connect : { A : Set } → ∀ ( xs ys : List A ) → clique (xs ++ ys) ≡ ((clique xs) ⇀ (clique ys))
+clique-++-connect [] ys = begin
+  clique ([] ++ ys)          ≡⟨⟩
+  clique ys                  ≡⟨ sym ⇀-identʳ ⟩
+  ε ⇀ clique ys              ≡⟨⟩
+  (clique []) ⇀ (clique ys)  ∎
+  where open ≡-Reasoning
+clique-++-connect (x ∷ xs) ys = begin
+  clique ((x ∷ xs) ++ ys)             ≡⟨⟩
+  clique (x ∷ (xs ++ ys))             ≡⟨⟩
+  Vertex x ⇀ clique (xs ++ ys)        ≡⟨ ⇀-congʳ (clique-++-connect xs ys) ⟩
+  Vertex x ⇀ (clique xs ⇀ clique ys)  ≡⟨ ⇀-assoc ⟩
+  (Vertex x ⇀ clique xs) ⇀ clique ys  ≡⟨⟩
+  clique (x ∷ xs) ⇀ clique ys         ∎
+  where open ≡-Reasoning
diff --git a/Graph/Properties.agda b/Graph/Properties.agda
new file mode 100644
index 0000000..760112b
--- /dev/null
+++ b/Graph/Properties.agda
@@ -0,0 +1,215 @@
+open import Graph.Base
+open import Graph.Reasoning
+
+module Graph.Properties where
+ 
++-sym : ∀ { A : Set } { G H : Graph A } → G + H ≡ H + G
++-sym = record
+  { vₗ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
+  ; vᵣ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
+  ; eₗ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
+  ; eᵣ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
+  }
+
++-assoc : ∀ { A : Set } { G H I : Graph A } → G + (H + I) ≡ (G + H) + I
++-assoc = record
+  { vₗ = λ { (+ₗ x) → +ₗ (+ₗ x) ; (+ᵣ (+ₗ x)) → +ₗ (+ᵣ x) ; (+ᵣ (+ᵣ x)) → +ᵣ x }
+  ; vᵣ = λ { (+ₗ (+ₗ x)) → +ₗ x ; (+ₗ (+ᵣ x)) → +ᵣ (+ₗ x) ; (+ᵣ x) → +ᵣ (+ᵣ x) }
+  ; eₗ = λ { (+ₗ x) → +ₗ (+ₗ x) ; (+ᵣ (+ₗ x)) → +ₗ (+ᵣ x) ; (+ᵣ (+ᵣ x)) → +ᵣ x }
+  ; eᵣ = λ { (+ₗ (+ₗ x)) → +ₗ x ; (+ₗ (+ᵣ x)) → +ᵣ (+ₗ x) ; (+ᵣ x) → +ᵣ (+ᵣ x) }
+  }
+  
++-identityʳ : ∀ { A : Set } { G : Graph A } → G + ε ≡ G
++-identityʳ = record
+  { vₗ = λ { (+ₗ x) → x }
+  ; vᵣ = λ x → +ₗ x
+  ; eₗ = λ { (+ₗ x) → x }
+  ; eᵣ = +ₗ 
+  }
+
++-identityˡ : ∀ { A : Set } { G : Graph A } → ε + G ≡ G
++-identityˡ = record
+  { vₗ = λ { (+ᵣ x) → x }
+  ; vᵣ = +ᵣ
+  ; eₗ = λ { (+ᵣ x) → x }
+  ; eᵣ = +ᵣ
+  }
+
++-congˡ : ∀ { A : Set } { G H I : Graph A } → G ≡ H → G + I ≡ H + I
++-congˡ G≈H = record
+               { vₗ = λ { (+ₗ x) → +ₗ (_≡_.vₗ G≈H x) ; (+ᵣ x) → +ᵣ x }
+               ; vᵣ = λ { (+ₗ x) → +ₗ (_≡_.vᵣ G≈H x) ; (+ᵣ x) → +ᵣ x }
+               ; eₗ = λ { (+ₗ x) → +ₗ (_≡_.eₗ G≈H x) ; (+ᵣ x) → +ᵣ x }
+               ; eᵣ = λ { (+ₗ x) → +ₗ (_≡_.eᵣ G≈H x) ; (+ᵣ x) → +ᵣ x }
+               }
+
++-congʳ : ∀ { A : Set } { G H I : Graph A } → H ≡ I → G + H ≡ G + I
++-congʳ {_} {G} {H} {I} H≡I = begin
+  G + H ≡⟨ +-sym ⟩
+  H + G ≡⟨ +-congˡ H≡I ⟩
+  I + G ≡⟨ +-sym ⟩
+  G + I ∎
+  where open ≡-Reasoning
+
+
+⇀-assoc : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H ⇀ I) ≡ (G ⇀ H) ⇀ I
+⇀-assoc = record
+  { vₗ = λ { (⇀ₗ x) → ⇀ₗ (⇀ₗ x) ; (⇀ᵣ (⇀ₗ x)) → ⇀ₗ (⇀ᵣ x) ; (⇀ᵣ (⇀ᵣ x)) → ⇀ᵣ x }
+  ; vᵣ = λ { (⇀ₗ (⇀ₗ x)) → ⇀ₗ x ; (⇀ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (⇀ᵣ x) → ⇀ᵣ (⇀ᵣ x) }
+  ; eₗ = λ { (⇀ₗ x) → ⇀ₗ (⇀ₗ x) ; (⇀ᵣ (⇀ₗ x)) → ⇀ₗ (⇀ᵣ x) ; (⇀ᵣ (⇀ᵣ x)) → ⇀ᵣ x ; (⇀ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (⇀ᵣ x) x₁ ; (⇀ₗᵣ x (⇀ₗ x₁)) → ⇀ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (⇀ᵣ x₁)) → ⇀ₗᵣ (⇀ₗ x) x₁ }
+  ; eᵣ = λ { (⇀ₗ (⇀ₗ x)) → ⇀ₗ x ; (⇀ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (⇀ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (⇀ₗ x₁) ; (⇀ᵣ x) → ⇀ᵣ (⇀ᵣ x) ; (⇀ₗᵣ (⇀ₗ x) x₁) → ⇀ₗᵣ x (⇀ᵣ x₁) ; (⇀ₗᵣ (⇀ᵣ x) x₁) → ⇀ᵣ (⇀ₗᵣ x x₁) }
+  }
+ 
+⇀-identˡ : ∀ { A : Set } { G : Graph A } → G ⇀ ε ≡ G
+⇀-identˡ = record
+  { vₗ = λ { (⇀ₗ x) → x }
+  ; vᵣ = ⇀ₗ
+  ; eₗ = λ { (⇀ₗ x) → x }
+  ; eᵣ = ⇀ₗ
+  }
+
+⇀-identʳ : ∀ { A : Set } { G : Graph A } → ε ⇀ G ≡ G
+⇀-identʳ = record
+  { vₗ = λ { (⇀ᵣ x) → x }
+  ; vᵣ = ⇀ᵣ
+  ; eₗ = λ { (⇀ᵣ x) → x }
+  ; eᵣ = ⇀ᵣ
+  }
+
+⇀-congˡ : ∀ { A : Set } { G H I : Graph A } → G ≡ H → G ⇀ I ≡ H ⇀ I
+⇀-congˡ G≈H = record
+               { vₗ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.vₗ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x }
+               ; vᵣ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.vᵣ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x }
+               ; eₗ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.eₗ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ (_≡_.vₗ G≈H x) x₁ }
+               ; eᵣ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.eᵣ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ (_≡_.vᵣ G≈H x) x₁ }
+               }
+
+⇀-congʳ : ∀ { A : Set } { G H I : Graph A } → H ≡ I → G ⇀ H ≡ G ⇀ I
+⇀-congʳ G≈H = record
+               { vₗ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.vₗ G≈H x) }
+               ; vᵣ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.vᵣ G≈H x) }
+               ; eₗ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.eₗ G≈H x) ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ x (_≡_.vₗ G≈H x₁) }
+               ; eᵣ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.eᵣ G≈H x) ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ x (_≡_.vᵣ G≈H x₁) }
+               }
+
+⇀-congʳ-≤ : ∀ { A : Set } { G H I : Graph A } → H ≤ I → G ⇀ H ≤ G ⇀ I
+⇀-congʳ-≤ H≤I = record
+                  { def = record
+                            { vₗ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (_≡_.vₗ (_≤_.def H≤I) (+ₗ x)) ; (+ᵣ x) → x }
+                            ; vᵣ = +ᵣ
+                            ; eₗ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (_≡_.eₗ (_≤_.def H≤I) (+ₗ x)) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (_≡_.vₗ (_≤_.def H≤I) (+ₗ x₁)) ; (+ᵣ x) → x }
+                            ; eᵣ = +ᵣ
+                            }
+                  }
+
+⇀-distrib-+ : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H + I) ≡ G ⇀ H + G ⇀ I
+⇀-distrib-+ = record
+                { vₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ (+ₗ x)) → +ₗ (⇀ᵣ x) ; (⇀ᵣ (+ᵣ x)) → +ᵣ (⇀ᵣ x) }
+                ; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (+ₗ x) ; (+ᵣ (⇀ₗ x)) → ⇀ₗ x ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ (+ᵣ x) }
+                ; eₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ (+ₗ x)) → +ₗ (⇀ᵣ x) ; (⇀ᵣ (+ᵣ x)) → +ᵣ (⇀ᵣ x) ; (⇀ₗᵣ x (+ₗ x₁)) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (+ᵣ x₁)) → +ᵣ (⇀ₗᵣ x x₁) }
+                ; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (+ₗ x) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (+ₗ x₁) ; (+ᵣ (⇀ₗ x)) → ⇀ₗ x ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ (+ᵣ x) ; (+ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (+ᵣ x₁) }
+                }
+
++-distrib-⇀ : ∀ { A : Set } { G H I : Graph A } → (G + H) ⇀ I ≡ G ⇀ I + H ⇀ I
++-distrib-⇀ = record
+                { vₗ = λ { (⇀ₗ (+ₗ x)) → +ₗ (⇀ₗ x) ; (⇀ₗ (+ᵣ x)) → +ᵣ (⇀ₗ x) ; (⇀ᵣ x) → +ₗ (⇀ᵣ x) }
+                ; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ (+ₗ x) ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ x ; (+ᵣ (⇀ₗ x)) → ⇀ₗ (+ᵣ x) ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ x }
+                ; eₗ = λ { (⇀ₗ (+ₗ x)) → +ₗ (⇀ₗ x) ; (⇀ₗ (+ᵣ x)) → +ᵣ (⇀ₗ x) ; (⇀ᵣ x) → +ₗ (⇀ᵣ x) ; (⇀ₗᵣ (+ₗ x) x₁) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ (+ᵣ x) x₁) → +ᵣ (⇀ₗᵣ x x₁) }
+                ; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ (+ₗ x) ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ x ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (+ₗ x) x₁ ; (+ᵣ (⇀ₗ x)) → ⇀ₗ (+ᵣ x) ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ x ; (+ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (+ᵣ x) x₁ }
+                }
+
+⇀-decomp : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H ⇀ I) ≡ G ⇀ H + (G ⇀ I + H ⇀ I)
+⇀-decomp = record
+             { vₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ x) → +ᵣ (+ᵣ x) }
+             ; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (+ᵣ (+ₗ (⇀ₗ x))) → ⇀ₗ x ; (+ᵣ (+ₗ (⇀ᵣ x))) → ⇀ᵣ (⇀ᵣ x) ; (+ᵣ (+ᵣ x)) → ⇀ᵣ x }
+             ; eₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ x) → +ᵣ (+ᵣ x) ; (⇀ₗᵣ x (⇀ₗ x₁)) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (⇀ᵣ x₁)) → +ᵣ (+ₗ (⇀ₗᵣ x x₁)) }
+             ; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (⇀ₗ x₁) ; (+ᵣ (+ₗ (⇀ₗ x))) → ⇀ₗ x ; (+ᵣ (+ₗ (⇀ᵣ x))) → ⇀ᵣ (⇀ᵣ x) ; (+ᵣ (+ₗ (⇀ₗᵣ x x₁))) → ⇀ₗᵣ x (⇀ᵣ x₁) ; (+ᵣ (+ᵣ x)) → ⇀ᵣ x }
+             }
+
++-idem : ∀ { A : Set } { G : Graph A } → G + G ≡ G
++-idem {_} {G} = begin
+  G + G                          ≡⟨ sym ⇀-identˡ ⟩
+  (G + G) ⇀ ε                    ≡⟨ +-distrib-⇀ ⟩
+  (G ⇀ ε) + (G ⇀ ε)              ≡⟨ sym +-identityʳ ⟩
+  ((G ⇀ ε) + (G ⇀ ε)) + ε        ≡⟨ sym (+-congʳ ⇀-identˡ) ⟩
+  ((G ⇀ ε) + (G ⇀ ε)) + (ε ⇀ ε)  ≡⟨ sym +-assoc ⟩
+  (G ⇀ ε) + ((G ⇀ ε) + (ε ⇀ ε))  ≡⟨ sym ⇀-decomp ⟩
+  G ⇀ (ε ⇀ ε)                    ≡⟨ ⇀-assoc ⟩
+  (G ⇀ ε) ⇀ ε                    ≡⟨ ⇀-identˡ ⟩
+  G ⇀ ε                          ≡⟨ ⇀-identˡ ⟩
+  G                              ∎
+  where open ≡-Reasoning
+  
++-absorp : ∀ { A : Set } { G H : Graph A } → G ⇀ H + G + H ≡ G ⇀ H
++-absorp {_} {G} {H} = begin
+  G ⇀ H + G + H             ≡⟨ +-congˡ (+-congʳ (sym ⇀-identˡ)) ⟩
+  G ⇀ H + G ⇀ ε + H         ≡⟨ +-congʳ (sym ⇀-identˡ) ⟩
+  G ⇀ H + G ⇀ ε + H ⇀ ε     ≡⟨ sym +-assoc ⟩
+  G ⇀ H + (G ⇀ ε + H ⇀ ε)   ≡⟨ sym ⇀-decomp ⟩
+  G ⇀ (H ⇀ ε)               ≡⟨ ⇀-congʳ ⇀-identˡ ⟩
+  G ⇀ H                     ∎
+  where open ≡-Reasoning
+  
+⇀-sat : ∀ { A : Set } { G : Graph A } → G ⇀ G ⇀ G ≡ G ⇀ G
+⇀-sat {_} {G} = begin
+  G ⇀ G ⇀ G                ≡⟨ sym ⇀-assoc ⟩
+  G ⇀ (G ⇀ G)              ≡⟨ ⇀-decomp ⟩
+  G ⇀ G + (G ⇀ G + G ⇀ G)  ≡⟨ +-congʳ +-idem ⟩
+  G ⇀ G + G ⇀ G            ≡⟨ +-idem ⟩
+  G ⇀ G                    ∎
+  where open ≡-Reasoning
+  
+≡→≤ : ∀ { A : Set } { G H : Graph A } → G ≡ H → G ≤ H
+≡→≤ {_} {G} {H} G≡H = begin
+  G  ≡⟨ G≡H ⟩
+  H  ∎
+  where open ≤-Reasoning
+
+≲-least : ∀ { A : Set } { G : Graph A } → ε ≤ G
+≲-least {_} {G} = record { def = begin
+  ε + G ≡⟨ +-identityˡ ⟩
+  G ∎}
+  where open ≡-Reasoning
+
++-order : ∀ { A : Set } { G H : Graph A } → G ≤ G + H
++-order {_} {G} {H} = record { def = begin
+  G + (G + H) ≡⟨ +-assoc ⟩
+  G + G + H ≡⟨ +-congˡ +-idem ⟩
+  G + H ∎}
+  where open ≡-Reasoning
+
++⇀-order : ∀ { A : Set } { G H : Graph A } → G + H ≤ G ⇀ H
++⇀-order {_} {G} {H} = record { def = begin
+  G + H + G ⇀ H ≡⟨ +-congˡ +-sym ⟩
+  H + G + G ⇀ H ≡⟨ +-sym ⟩
+  G ⇀ H + (H + G) ≡⟨ +-congʳ +-sym ⟩
+  G ⇀ H + (G + H) ≡⟨ +-assoc ⟩
+  G ⇀ H + G + H ≡⟨ +-absorp ⟩
+  G ⇀ H ∎}
+  where open ≡-Reasoning
+
++-mono : ∀ { A : Set } { G H I : Graph A } → G ≤ H → G + I ≤ H + I
++-mono {_} {G} {H} {I} G≤H = record { def = begin
+  G + I + (H + I) ≡⟨ +-congˡ +-sym ⟩
+  I + G + (H + I) ≡⟨ +-assoc ⟩
+  I + G + H + I ≡⟨ +-congˡ (sym +-assoc) ⟩
+  I + (G + H) + I ≡⟨ +-congˡ (+-congʳ (_≤_.def G≤H)) ⟩
+  I + H + I ≡⟨ +-congˡ +-sym ⟩
+  H + I + I ≡⟨ sym +-assoc ⟩
+  H + (I + I) ≡⟨ +-congʳ +-idem ⟩
+  H + I ∎}
+  where open ≡-Reasoning
+
+⇀-monoˡ : ∀ { A : Set } { G H I : Graph A } → G ≤ H → G ⇀ I ≤ H ⇀ I
+⇀-monoˡ {_} {G} {H} {I} G≤H = record { def = begin
+  G ⇀ I + H ⇀ I ≡⟨ sym +-distrib-⇀ ⟩
+  (G + H) ⇀ I ≡⟨ ⇀-congˡ (_≤_.def G≤H) ⟩
+  H ⇀ I ∎}
+  where open ≡-Reasoning
+
+⇀-monoʳ : ∀ { A : Set } { G H I : Graph A } → G ≤ H → I ⇀ G ≤ I ⇀ H
+⇀-monoʳ {_} {G} {H} {I} G≤H = record { def = begin
+  I ⇀ G + I ⇀ H ≡⟨ sym ⇀-distrib-+ ⟩
+  I ⇀ (G + H) ≡⟨ ⇀-congʳ (_≤_.def G≤H) ⟩
+  I ⇀ H ∎}
+  where open ≡-Reasoning
diff --git a/Graph/Reasoning.agda b/Graph/Reasoning.agda
new file mode 100644
index 0000000..94409af
--- /dev/null
+++ b/Graph/Reasoning.agda
@@ -0,0 +1,47 @@
+open import Graph.Base
+
+module Graph.Reasoning where
+
+
+  module ≡-Reasoning where
+
+    infix 1 begin_
+    infixr 2 _≡⟨⟩_ _≡⟨_⟩_
+    infix 3 _∎
+
+    begin_ : ∀ { A : Set } { G H : Graph A } → G ≡ H → G ≡ H
+    begin G≡H = G≡H
+
+    _≡⟨⟩_ : ∀ { A : Set } (G : Graph A) { H : Graph A } → G ≡ H → G ≡ H
+    G ≡⟨⟩ G≡H = G≡H
+
+    _≡⟨_⟩_ : ∀ { A : Set } (G : Graph A) { H I : Graph A } → G ≡ H → H ≡ I → G ≡ I
+    G ≡⟨ G≡H ⟩ H≡I = trans G≡H H≡I
+
+    _∎ : ∀ { A : Set } (G : Graph A) → G ≡ G
+    G ∎ = refl
+
+
+  module ≤-Reasoning where
+
+    infix 1 begin_
+    infixr 2 _≡⟨⟩_ _≡⟨_⟩_ _≤⟨⟩_ _≤⟨_⟩_
+    infix 3 _∎
+
+    begin_ : ∀ { A : Set } { G H : Graph A } → G ≤ H → G ≤ H
+    begin G≤H = G≤H
+
+    _≡⟨⟩_ : ∀ { A : Set } (G : Graph A) { H : Graph A } → G ≤ H → G ≤ H
+    G ≡⟨⟩ G≤H = G≤H
+  
+    _≡⟨_⟩_ : ∀ { A : Set } (G : Graph A) { H I : Graph A } → G ≡ H → H ≤ I → G ≤ I
+    G ≡⟨ G≡H ⟩ H≤I = ≤-trans (≡-to-≤ G≡H) H≤I
+
+    _≤⟨⟩_ : ∀ { A : Set } (G : Graph A) { H : Graph A } → G ≤ H → G ≤ H
+    G ≤⟨⟩ G≤H = G≤H
+
+    _≤⟨_⟩_ : ∀ { A : Set } (G : Graph A) { H I : Graph A } → G ≤ H → H ≤ I → G ≤ I
+    G ≤⟨ G≤H ⟩ H≤I = ≤-trans G≤H H≤I
+
+    _∎ : ∀ { A : Set } (G : Graph A) → G ≤ G
+    G ∎ = ≤-refl