misc fixes (#446)

Fixes #443

Author: ncfavier

src/1Lab/Path.lagda.md

@@ -1593,8 +1593,8 @@ _∙'_ {x = x} p q = transport (λ i → x ≡ q i) p
 Since we know that `transport`{.Agda} reduces when applied to type
 formers, the definition above is *not* neutral, even when $p$ and $q$
 are variables. But what does it reduce *to*? A natural attempt would be
-to say that, at a point $i : \bI$, the path $\transport{(\lam{i}. x \is
-q(i))}{p}$ is $t = \transport{(\lam{i}. A)}{p(i)}$ --- i.e., transport
+to say that, at a point $i : \bI$, the path $\transport{(\lam{i} x \is
+q(i))}{p}$ is $t = \transport{(\lam{i} A)}{p(i)}$ --- i.e., transport
 of paths is, pointwise, transport along the base. But this can't be the
 case, since $t$ has endpoints
 

support/shake/app/Shake/Markdown.hs

@@ -452,6 +452,7 @@ renderMarkdown authors references modname baseUrl digest markdown@(Pandoc (Meta
 don'tFold :: Set.Set Text
 don'tFold = Set.fromList
   [ "`⟨" -- used in CC.Lambda
+  , "‶⟨" -- used in Cat.Diagram.Product.Solver
   ]
 
 -- | Removes the RHS of equation reasoning steps?? IDK, ask Amelia.