Use TDNR

src/Cat/Functor.agda

@@ -22,25 +22,24 @@ record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category
       → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
 
 module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
+  open Functor
+  open Category
   private
-    open module F = Functor F
-    open module G = Functor G
-    open module A = Category A
-    open module B = Category B
-    open module C = Category C
+    F* = F .func*
+    F→ = F .func→
+    G* = G .func*
+    G→ = G .func→
+    _A⊕_ = A ._⊕_
+    _B⊕_ = B ._⊕_
+    _C⊕_ = C ._⊕_
+    module _ {a0 a1 a2 : A .Object} {α0 : A .Arrow a0 a1} {α1 : A .Arrow a1 a2} where
 
-    F* = F.func*
-    F→ = F.func→
-    G* = G.func*
-    G→ = G.func→
-    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
-
-      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
+      dist : (F→ ∘ G→) (α1 A⊕ α0) ≡ (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0
       dist = begin
-        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
-        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
-        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
-        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
+        (F→ ∘ G→) (α1 A⊕ α0)         ≡⟨ refl ⟩
+        F→ (G→ (α1 A⊕ α0))           ≡⟨ cong F→ (G .distrib)⟩
+        F→ ((G→ α1) B⊕ (G→ α0))      ≡⟨ F .distrib ⟩
+        (F→ ∘ G→) α1 C⊕ (F→ ∘ G→) α0 ∎
 
   functor-comp : Functor A C
   functor-comp =
@@ -48,10 +47,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
       { func* = F* ∘ G*
       ; func→ = F→ ∘ G→
       ; ident = begin
-        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
-        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
-        F→ (B.𝟙)        ≡⟨ F.ident ⟩
-        C.𝟙             ∎
+        (F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩
+        F→ (G→ (A .𝟙))   ≡⟨ cong F→ (G .ident)⟩
+        F→ (B .𝟙)        ≡⟨ F .ident ⟩
+        C .𝟙             ∎
       ; distrib = dist
       }