[ 2511 ] Fixed module application for Categories.Cone[s]

copumpkin · Nov 4, 2016 · f8f7eb6 · f8f7eb6
1 parent 4c6cc6d
commit f8f7eb6
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 16 deletions.
diff --git a/Categories/Cone.agda b/Categories/Cone.agda
@@ -35,7 +35,7 @@ module ConeOver {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Categor
       { N-≣ = ≣-sym X≜Y.N-≣
       ; ψ-≡ = λ j → sym (X≜Y.ψ-≡ j)
       }
-    ; trans = λ X≜Y Y≜Z → 
+    ; trans = λ X≜Y Y≜Z →
       let module X≜Y = _≜_ X≜Y in
       let module Y≜Z = _≜_ Y≜Z in
       record
@@ -79,7 +79,7 @@ module ConeOver {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Categor
     ; sym = λ X≜′Y → let module X≜′Y = _≜′_ X≜′Y in record
       { ψ′-≡ = λ j → Equiv.sym (X≜′Y.ψ′-≡ j)
       }
-    ; trans = λ X≜′Y Y≜′Z → 
+    ; trans = λ X≜′Y Y≜′Z →
       let module X≜′Y = _≜′_ X≜′Y in
       let module Y≜′Z = _≜′_ Y≜′Z in
       record { ψ′-≡ = λ j → Equiv.trans (X≜′Y.ψ′-≡ j) (Y≜′Z.ψ′-≡ j) }
@@ -119,4 +119,4 @@ module ConeOver {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Categor
 
 open ConeOver public using (cone-setoid) renaming (_≜_ to _[_≜_]; Cone′ to Cone; _≜′_ to _[_≜′_]; ConeUnder′ to ConeUnder)
 
-module Cone {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} {F : Functor J C} (K : ConeOver.Cone F) = ConeOver.Cone F K
+module Cone {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} {F : Functor J C} (K : ConeOver.Cone F) = ConeOver.Cone K
diff --git a/Categories/Cones.agda b/Categories/Cones.agda
@@ -20,7 +20,7 @@ record ConeMorphism {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Cat
     .commute : ∀ {X} → c₁.ψ X ≡ c₂.ψ X ∘ f
 
 Cones : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) (ℓ ⊔ e ⊔ o′ ⊔ ℓ′) e
-Cones {C = C} F = record 
+Cones {C = C} F = record
   { Obj = Obj′
   ; _⇒_ = Hom′
   ; _≡_ = _≡′_
@@ -29,7 +29,7 @@ Cones {C = C} F = record
   ; assoc = assoc
   ; identityˡ = identityˡ
   ; identityʳ = identityʳ
-  ; equiv = record 
+  ; equiv = record
     { refl = Equiv.refl
     ; sym = Equiv.sym
     ; trans = Equiv.trans
@@ -54,13 +54,13 @@ Cones {C = C} F = record
   F ≡′ G = f F ≡ f G
 
   _∘′_ : ∀ {A B C} → Hom′ B C → Hom′ A B → Hom′ A C
-  _∘′_ {A} {B} {C} F G = record 
+  _∘′_ {A} {B} {C} F G = record
     { f = f F ∘ f G
     ; commute = commute′
     }
     where
     .commute′ : ∀ {X} → ψ A X ≡ ψ C X ∘ (f F ∘ f G)
-    commute′ {X} = 
+    commute′ {X} =
         begin
           ψ A X
         ↓⟨ ConeMorphism.commute G ⟩
@@ -109,23 +109,23 @@ module Float {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o
   morphism-determines-cone-morphism-≣ {A} {B} {m} {m′} pf = lemma₁ A B pf (ConeMorphism.commute m) (ConeMorphism.commute m′)
 
   float₂ : ∀ {A A′ B B′} → F [ A ≜ A′ ] → F [ B ≜ B′ ] → Cones F [ A , B ] → Cones F [ A′ , B′ ]
-  float₂ A≜A′ B≜B′ κ = record 
+  float₂ A≜A′ B≜B′ κ = record
     { f = H.float₂ (N-≣ A≜A′) (N-≣ B≜B′) f
     ; commute = λ {j} → ∼⇒≡ (trans (sym (ψ-≡ A≜A′ j)) (trans (≡⇒∼ commute) (∘-resp-∼ (ψ-≡ B≜B′ j) (float₂-resp-∼ (N-≣ A≜A′) (N-≣ B≜B′)))))
     }
     where
     open ConeMorphism κ
-    open ConeOver._≜_ F
+    open ConeOver._≜_
 
   floatˡ : ∀ {A B B′} → F [ B ≜ B′ ] → Cones F [ A , B ] → Cones F [ A , B′ ]
-  floatˡ {A = A} B≜B′ κ = record 
+  floatˡ {A = A} B≜B′ κ = record
     { f = H.floatˡ N-≣ f
     ; commute = λ {j} → C.Equiv.trans commute (∼⇒≡ (∘-resp-∼ (ψ-≡ j) (floatˡ-resp-∼ N-≣)))
     }
     where
     module A = Cone A
     open ConeMorphism κ
-    open ConeOver._≜_ F B≜B′
+    open ConeOver._≜_ B≜B′
 
   floatˡ-resp-refl : ∀ {A B} (κ : Cones F [ A , B ]) → floatˡ {A} {B} (ConeOver.≜-refl F) κ ≣ κ
   floatˡ-resp-refl f = ≣-refl
@@ -134,23 +134,23 @@ module Float {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o
   floatˡ-resp-trans {A} {B} {B′} {B″} B≜B′ B′≜B″ κ = morphism-determines-cone-morphism-≣ {A} {B″} {floatˡ {A} {B} {B″} (ConeOver.≜-trans F B≜B′ B′≜B″) κ} {floatˡ {A} {B′} {B″} B′≜B″ (floatˡ {A} {B} {B′} B≜B′ κ)} (H.floatˡ-resp-trans (N-≣ B≜B′) (N-≣ B′≜B″) f)
     where
     module A = Cone A
-    open ConeOver._≜_ F
+    open ConeOver._≜_
     open ConeMorphism κ
 
   floatʳ : ∀ {A A′ B} → F [ A ≜ A′ ] → Cones F [ A , B ] → Cones F [ A′ , B ]
-  floatʳ {B = B} A≜A′ κ = record 
+  floatʳ {B = B} A≜A′ κ = record
     { f = ≣-subst (λ X → C [ X , B.N ]) N-≣ f
     ; commute = λ {j} → ∼⇒≡ (trans (sym (ψ-≡ j)) (trans (≡⇒∼ commute) (∘-resp-∼ʳ (floatʳ-resp-∼ N-≣))))
     }
     where
     module B = Cone B
     open ConeMorphism κ
-    open ConeOver._≜_ F A≜A′
+    open ConeOver._≜_ A≜A′
 
   float₂-breakdown-lr : ∀ {A A′ B B′ : Cone F} (A≜A′ : F [ A ≜ A′ ]) (B≜B′ : F [ B ≜ B′ ]) (κ : Cones F [ A , B ]) → float₂ A≜A′ B≜B′ κ ≣ floatˡ B≜B′ (floatʳ A≜A′ κ)
   float₂-breakdown-lr {A′ = A′} {B′ = B′} A≜A′ B≜B′ κ = morphism-determines-cone-morphism-≣ {A = A′} {B′} {float₂ A≜A′ B≜B′ κ} {floatˡ B≜B′ (floatʳ A≜A′ κ)} (H.float₂-breakdown-lr (N-≣ A≜A′) (N-≣ B≜B′) (ConeMorphism.f κ))
-    where open ConeOver._≜_ F
+    where open ConeOver._≜_
 
   float₂-breakdown-rl : ∀ {A A′ B B′ : Cone F} (A≜A′ : F [ A ≜ A′ ]) (B≜B′ : F [ B ≜ B′ ]) (κ : Cones F [ A , B ]) → float₂ A≜A′ B≜B′ κ ≣ floatʳ A≜A′ (floatˡ B≜B′ κ)
   float₂-breakdown-rl {A′ = A′} {B′ = B′} A≜A′ B≜B′ κ = morphism-determines-cone-morphism-≣ {A = A′} {B′} {float₂ A≜A′ B≜B′ κ} {floatʳ A≜A′ (floatˡ B≜B′ κ)} (H.float₂-breakdown-rl (N-≣ A≜A′) (N-≣ B≜B′) (ConeMorphism.f κ))
-    where open ConeOver._≜_ F
+    where open ConeOver._≜_