File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
src/Data/List/Relation/Unary/Unique/Setoid Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -49,11 +49,11 @@ module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
4949
5050 map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
5151 ∀ {xs} → Unique S xs → Unique R (map f xs)
52- map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (λ x≈y → contraposition inj x≈y ) xs!)
52+ map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!)
5353
5454 map⁻ : ∀ {f} → Congruent _≈₁_ _≈₂_ f →
5555 ∀ {xs} → Unique R (map f xs) → Unique S xs
56- map⁻ cong fxs! = AllPairs.map (λ fx≉fy → contraposition cong fx≉fy ) (AllPairs.map⁻ fxs!)
56+ map⁻ cong fxs! = AllPairs.map (contraposition cong) (AllPairs.map⁻ fxs!)
5757
5858------------------------------------------------------------------------
5959-- ++
You can’t perform that action at this time.
0 commit comments