File tree Expand file tree Collapse file tree 3 files changed +4
-4
lines changed Expand file tree Collapse file tree 3 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -265,7 +265,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
265
265
-- IsA A
266
266
-- / || \ / || \
267
267
-- IsB IsC IsD B C D
268
-
268
+
269
269
-- The procedure for re-exports in the bundles is as follows:
270
270
271
271
-- 1. `open IsA isA public using (IsC, M)` where `M` is everything
@@ -280,7 +280,7 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where
280
280
281
281
-- 5. `open B b public using (O)` where `O` is everything exported
282
282
-- by `B` but not exported by `IsA`.
283
-
283
+
284
284
-- 6. Construct `d : D` via the `isC` obtained in step 1.
285
285
286
286
-- 7. `open D d public using (P)` where `P` is everything exported
Original file line number Diff line number Diff line change @@ -56,7 +56,7 @@ record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where
56
56
-- Haskell-style alternative name for pure
57
57
return : A → F A
58
58
return = pure
59
-
59
+
60
60
-- backwards compatibility: unicode variants
61
61
_⊛_ : F (A → B) → F A → F B
62
62
_⊛_ = _<*>_
Original file line number Diff line number Diff line change @@ -380,7 +380,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
380
380
-- For further background on (split) surjections, one may consult any
381
381
-- general mathematical references which work without the principle
382
382
-- of choice. For example:
383
- --
383
+ --
384
384
-- https://ncatlab.org/nlab/show/split+epimorphism.
385
385
--
386
386
-- The connection to set-theoretic notions with the same names is
You can’t perform that action at this time.
0 commit comments