UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
217 stars 69 forks source link

Current definition of hydrocarbon actually defines Lewis structures of hydrocarbons #230

Open ghost opened 2 years ago

ghost commented 2 years ago

Benzene is a molecule with 6 carbon atoms and 6 hydrogen atoms, where the carbon atoms are arranged in a manner such that the projection into 2-dimesnional space is a hexagon.

The current definition of hydrocarbon assumes that bonds between carbon atoms are either a single, double, or triple bond. However, due to quantum mechanics, the bonds between carbon atoms in a Benzene molecule are neither a single bond nor a double bond; instead the electrons that would otherwise have been involved in forming bonds instead become delocalised, and are no longer associated to a bond between two carbon atoms. This phenomena is called resonance in chemistry. https://en.wikipedia.org/wiki/Resonance_(chemistry)

What is defined in this library is instead the Lewis structure of a hydrocarbon. https://en.wikipedia.org/wiki/Lewis_structure In hydrocarbons with resonance there are multiple Lewis structures associated with a hydrocarbon. The actual structure of a hydrocarbon could be said to be an average of all the Lewis structures of a hydrocarbon.

EgbertRijke commented 2 years ago

I think you're right about that. Thanks so much for pointing it out!

Do you have an idea how to incorporate resonance in the type theoretic definition? I think what we want should be a definition that allows for resonance, and such that the type of self-identifications of a hydrocarbon such as benzene corresponds to its symmetries.

Either way, thank you so much for this observation!