Timeline for Are paths in HoTT perhaps just "cost-free" paths?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5, 2013 at 17:57 | history | edited | Noam Zeilberger | CC BY-SA 3.0 |
added some explanation
|
| Nov 5, 2013 at 4:35 | comment | added | Noam Zeilberger | @NoahS 𝔹 is the category of state types and state transformers. Traditionally in Hoare logic there is only state type, hence 𝔹 is a one-object category, i.e., a monoid (this restriction is not really necessary though). 𝔼 is the category of "predicates over states and proofs of Hoare triples". For example, if we identify predicates with subsets, then an arrow of 𝔼 from $P \subseteq S$ to $Q \subseteq S$ corresponds to a state transformer $c : S \to S$ such that $c(P) \subseteq Q$. Finally, $p : \mathbb{E} \to \mathbb{B}$ is just the forgetful functor. | |
| Nov 5, 2013 at 4:03 | comment | added | Noah Schweber | What are $\mathbb{E}$ and $\mathbb{B}$? | |
| Nov 4, 2013 at 22:21 | comment | added | Andrej Bauer | Your answer gives me the idea that we could view state transformers as paths in a space/type whose points/elements are states. Unfortunately, it cannot be that direct as paths are invertible but state transformers need not be. We need directed type theory. | |
| Nov 4, 2013 at 22:15 | history | edited | Noam Zeilberger | CC BY-SA 3.0 |
notation/wording
|
| Nov 4, 2013 at 22:09 | history | answered | Noam Zeilberger | CC BY-SA 3.0 |