Make Rels less strict, add a StrictRels for the previous version #365
Conversation
Because it's very strict and I'm defining a non-strict version more in keeping with the conventions of the library
|
Looking nice. What are you still intending to do before making it 'Ready for Review'? And would you like comments now anyways? |
|
I'd like comments now definitely, please! I still need to copy the top-level comment from (what is now) |
|
|
||
| open import Categories.Category.Dagger | ||
| open import Categories.Category.Instance.Rels | ||
|
|
||
| open import Data.Product |
There was a problem hiding this comment.
Please put explicit using in as many places as possible, strongly so on stdlib imports.
| ; sym = swap | ||
| ; trans = λ { (p₁ , p₂) (q₁ , q₂) → (q₁ ∘′ p₁) , p₂ ∘′ q₂} | ||
| } | ||
| ; ∘-resp-≈ = λ f⇔h g⇔i → |
There was a problem hiding this comment.
as you're already using pattern-matching lambdas, might as well continue to do so instead of using proj here?
| ; snd = λ { {inj₂ _} p q → Setoid.trans B q p } | ||
| } | ||
| } | ||
| ; ⟨_,_⟩ = λ L R → record |
There was a problem hiding this comment.
probably should use pattern-matching lambda here too
| module _ {o ℓ} where | ||
|
|
||
| Rels-Cartesian : Cartesian (Rels o ℓ) | ||
| Rels-Cartesian : Cartesian (Rels o (o ⊔ ℓ)) | ||
| Rels-Cartesian = record |
There was a problem hiding this comment.
So if anyone is going to use this record somewhere else, it is going to be a problem of sorts. Agda doesn't like huge explicit records. It much prefers records full of things that have local names, i.e. given using a where clause. That makes the unifier much happier.
There was a problem hiding this comment.
How huge is huge here? How much should I split the records up?
There was a problem hiding this comment.
It's not the size of the record, it's the size of the contents. 1-liners are fine, but embedded proofs with > 3 steps should definitely be named instead of inlined.
| } | ||
|
|
||
| StrictRels-Monoidal : Monoidal (StrictRels o ℓ) | ||
| StrictRels-Monoidal = monoidalHelper _ record |
There was a problem hiding this comment.
these monster records are probably best broken up in pieces too.
If you don't like where, I've also done private blocks above the definition where I put everything.
| StrictRels-Monoidal : Monoidal (StrictRels o ℓ) | ||
| StrictRels-Monoidal = monoidalHelper _ record | ||
| { ⊗ = record | ||
| { F₀ = λ { (A , B) → A ×.× B } |
There was a problem hiding this comment.
uncurry ×.× ? The reason to see it that way is that there might be room to re-use properties of ×.× directly, instead of expanding out everything. Yes, all the proofs are trivial, but they are also not 'conceptual'. [This one's more of a suggestion than a must fix]
|
If you give me permission to push to your fork, I can help push this to completion. |
No description provided.