Junyoung/"Clare" Jang

Regarding `Surjective`, I do not see an alternative definition for that. Could you please provide such a definition? For `Injective`, I think the following definition would be good enough for...

Oh right, I miswrote `Injective`. Actually the definition I used should be the definition of `Functional` w.r.t. those equivalences: ```agda Functional R = ∀ x y z w → x...

Specifically, what I have in mind is defining partial algebraic structures, e.g. partial monoid and so on. These are useful tools for mechanizing substructural calculi such as the linear lambda...

@jamesmckinna Thanks for the suggestion. I proposed `_after-cong⟨_⟩_` as a separate step so that the order of equivalences stays the same. However, if this approach seems too verbose, what you...

@MatthewDaggitt Thank you for the valuable comment! That tactic seems indeed very useful. However, I want to argue that the reasoning step I suggest is still useful separately. The tactic...

That approach shares the issue in the second approach of the original post, i.e. one needs to duplicate the initial and final types. If they are fairly complex, extracting a...

Sure, that works. It is just more cumbersome in my opinion. I think the question is really how difficult to implement a combinator like this.

Hm, that's a fair point. However, I think that can be adjusted in the combinator, e.g. so that it explicitly mentioned `structure type3` before the combinator and skipping `type3` or...

How about the following syntax? ```agda begin type1 ≈⟨ equiv1 ⟩ type2 ≈⟨ equiv2 ⟩ structure type3 under⟨ cong structure ⟩≈⟨ equiv3 ⟩ type4 ≈⟨ equiv4 ⟩ type5 ≈⟨ equiv5...

I made a temporary fork as a workaround: https://www.npmjs.com/package/parjs-then It uses `andThen` for `then`. I renamed related combinators (`thenq` and `qthen`) as well for IMO, consistency. `butThen` is for `qthen`,...