Detailed Descriptions: Variance Queue UML

For the embedding of fibrations into the logic of PVS I follow very closely Ulrich Hensels PhD thesis (which is no longer online). The only difference is that, for definitions, I prefer to use the abstract categorical characterizations, whereas Uli uses their concrete PVS incarnations. This way it is possible to see abstract fibrational notion becoming alive. Of course at the expense of using rewrite lemmas to transfer the abstract notation into concreate proof obligations.

- preservation of truth and equality
- Monotonicity (that is functoriality) of most definitions
- several commutation results
- fibredness and cofibredness results

- Prove for polynomial functors that <Tpi_1, Tpi_2> restricts to an isomorphism (see file pol_aczel.pvs). Do then two inductions with aczel_property and image_property and use the isomorphism in the induction step of the exponent. (Theory AczelExtendedFun)
- Do only one mutual induction and do a more complicated induction step for the exponent (Theory AczelExtendedAAFun).

- it does not have a final coalgebra
- bisimulations are not closed under intersection and composition
- its relation lifting is not fibred
- the union of bisimulations is a bisimulation
- the graph and the kernel of a G-coalgebra morphism are bisimulations

- the union of two bisimulations is not always a bisimulation
- there are models with several maximal but no greatest bisimulations
- there is no final coalgebra if contains at least 2 elements

```
``````
M-x load-file typecheck.el
```

Home Science Overview All Publications Talks PhD CCSL Robin

last modified on 20 Sep 2011 by Hendrik