[ add ] properties of Relation.Unary adjoints
#2866
Conversation
jamesmckinna
added
addition
status: blocked-by-issue
jamesmckinna
removed
the
status: blocked-by-issue
|
|
||
| ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y) | ||
| ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py) | ||
| ∃-≡ P {x} = mk↔ₛ′ (⟨ id ⟩⊢⁻ id) (⟨ id ⟩⊢⁺ id) |
There was a problem hiding this comment.
Nice. I wish the proofs could get a similar treatment!
There was a problem hiding this comment.
Well, ok... but downstream?
I think when I last looked at this, the proofs for the left adjoint behave nicely, while the corresponding ones for the right need (lots of) extensionality, to the point of being unilluminating/incomprehensible.
Also, they should be generalised to
'property of f implies related property of adjoint diagram'
(iso; injective; surjective... adjoint), but I got a headache working out the details...
The special case f = id is almost too special to be worth singling out, but... baby steps. It's one reason I went back on my original thought to rewrite the lemma statement to use the adjoint notation... it felt like overkill for too-small stakes.
There was a problem hiding this comment.
Oh, and the use of id to proxy for its definitionally-equal ⊆-refl (Yoneda lemma!) is a bit cheeky, but arguably it looks worse by using the (conceptually) type-correct version, cf. the functoriality proofs, which I wrote Yoneda-style, rather than flattening out the compositions to re duplicate the pattern-matching versions which precede them...
2 participants
Follows on from #2840 .
Tweaks some of the text introduced there.