[ new ] List map injection #1141
Conversation
There was a problem hiding this comment.
My main thoughts is that as these proofs are to do with the function hierarchy should perhaps live under a folder Data.List.Function just as binary relations live in Data.List.Relation.Binary?
I would tentatively recommend that they live in Data.List.Function.Map? We could then re-export the simple versions, e.g. map-injective in Data.List.Properties if we wanted to?
For example all the zipWith proofs under Data.Vec.Properties would then be moved to Data.Vec.Algebra.ZipWith...
| @@ -26,6 +26,7 @@ open import Data.Product as Prod hiding (map; zip) | |||
| open import Data.Sum.Base using (_⊎_; inj₁; inj₂) | |||
| open import Data.These.Base as These using (These; this; that; these) | |||
| open import Function | |||
| open import Function.Equality using (_⟨$⟩_) | |||
There was a problem hiding this comment.
You don't need this import?
| @@ -106,6 +107,15 @@ map-compose : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f | |||
| map-compose [] = refl | |||
| map-compose (x ∷ xs) = cong (_ ∷_) (map-compose xs) | |||
|
|
|||
| map-injective : ∀ (f : A ↣ B) → Injective _≡_ _≡_ (map (Injection.f f)) | |||
There was a problem hiding this comment.
f : A ↣ B is quite a heavy pre-condition. For the map-injective I'd have the type ∀ {f : A → B} → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (map f) .
| ... | fx≡fy , fxs≡fys = cong₂ _∷_ (injective fx≡fy) (map-injective f fxs≡fys) | ||
| where open Injection f hiding (f) | ||
|
|
||
| map-injection : ∀ (f : A ↣ B) → List A ↣ List B |
There was a problem hiding this comment.
As this is the propositional variant, I think we'd better name it map-↣ and save map-injection for the setoid variety.
|
Thanks for the review @MatthewDaggitt; that all sounds good to me. |
|
This was added as part of |
|
@ajrouvoet as @umazalakain says |
|
Having |
I'm afraid the PR was already merged in. |
|
Okay, let's close this anyway. Trying to keep the number of fun distractions low as I try to deliver a dissertation ;-) |
I think these were still missing