fix whitespace, document category solver better

Author: maxsnew

Cubical/Categories/NaturalTransformation/Properties.agda

@@ -163,9 +163,9 @@ module _ {B : Category ℓB ℓB'}{C : Category ℓC ℓC'}{D : Category ℓD 
   open Functor
   _∘ˡi_ : ∀ (K : Functor B C) → {G H : Functor C D} (β : NatIso G H)
        → NatIso (G ∘F K) (H ∘F K)
-  _∘ˡi_ K β .trans = β .trans ∘ˡ K 
+  _∘ˡi_ K β .trans = β .trans ∘ˡ K
   _∘ˡi_ K β .nIso b  = β .nIso (K ⟅ b ⟆)
-  
+
   CAT⋆Assoc : {E : Category ℓE ℓE'}
             (F : Functor B C)(G : Functor C D)(H : Functor D E)
             → NatIso (H ∘F (G ∘F F)) ((H ∘F G) ∘F F)

Cubical/Tactics/CategorySolver/Solver.agda

@@ -24,19 +24,21 @@ module Eval (𝓒 : Category ℓ ℓ') where
   𝓘 : Functor FreeCat 𝓟
   𝓘 = PseudoYoneda {C = FreeCat}
 
-  -- Semantics in 𝓟o 𝓒, interpreting fun symbols using Yoneda
+  -- Semantics in 𝓟 (𝓒 .ob), interpreting fun symbols using Yoneda
   module YoSem = Semantics 𝓟 (𝓘 ∘Interp η)
   ⟦_⟧yo = YoSem.sem .F-hom
-  
-  -- | Evaluate by taking the semantics in 𝓟 𝓒 and
-  -- | use the Yoneda lemma to extract a morphism in 𝓒.
+
+  -- | Evaluate by taking the semantics in 𝓟 (𝓒 .ob)
   eval : ∀ {A B} → FreeCat [ A , B ] → _
   eval {A}{B} e = ⟦ e ⟧yo
 
+  -- Evaluation agrees with the Yoneda embedding, and so is fully faithful
   Yo-YoSem-agree : 𝓘 ≡ YoSem.sem
   Yo-YoSem-agree = YoSem.sem-uniq refl
 
-  -- | Eval agrees with the tautological semantics
+  -- If two expressions in the free category are equal when evaluated
+  -- in 𝓟 (𝓒 .ob), then they are equal, and so are equal when
+  -- evaluated in 𝓒.
   solve : ∀ {A B} → (e₁ e₂ : FreeCat [ A , B ])
         → eval e₁ ≡ eval e₂
         → ⟦ e₁ ⟧c ≡ ⟦ e₂ ⟧c