Computational M-types #1233
Computational M-types #1233
Conversation
…ech's construction (see p. 22)
definitional inductives
this is by transfer of the already formalized proof by Felix Rech
…g for proper behaviour
- uses function composition more often - upstream lemmas were mostly in the library, one moved to MoreFoundations/PartA.v - extended header information about the UniMath schools that contributed to the present file
…ased this does not give a clean commit history, but at least, the overall diff for the PR under construction will be readable
UniMath/Induction/M/ComputationalM.v
Outdated
| cbn. apply funextsec. intros b. rewrite <- helper_A. | ||
| unfold carriers_eq. rewrite weqpath_transport. | ||
| cbn. rewrite eq_corecM0. apply idpath. | ||
| Qed. |
There was a problem hiding this comment.
Would it be better to use Defined. here?
|
The code looks very good. I would only like to have confirmation that the many |
|
@benediktahrens : I cannot confirm that |
|
@rmatthes : thanks a lot for your feedback. Why is the body of |
|
@benediktahrens : I thought that such equations are rarely used for rewriting since one would normally solve the goal at hand by |
a fruit of the UniMath School 2019: a streamlined version of the construction by Felix Rech of M-types (coinductive trees) that enjoy the equational rule of coiteration definitionally:
Lemma corec_computationis proved merely byidpath. As input we take any final coalgebra for the respective polynomial functor (hence, with the provable coiteration rule), the output is the refined final coalgebra with the law holding definitionally (of course, both coalgebras are equal - provably). The proof tries to use as much as possible already existing results in the library. Only one lemma of a general nature is added toMoreFoundations.PartA.The commit history contains also the development made by Scoccola and Rech at UniMath School 2017 and other stuff that is deleted later. For reviewing this PR, looking at the diff will be much easier than following the commit history.