[Agda] Can intuitionistic type theory express derivations of physical equations more strictly?

[Mario Castelán Castro]

On 28/09/17 07:38, Hidekazu IWAKI wrote:
> I'd like to describe a physical system with the intuitionistic type
> theory(not computer simulation).  I wonder if it is possible to convince
> readers that all famous physical equations have evenly a strict derivation.
> So I want to confirm it with the type theory.
> 
> In order to refer, I'm looking about such a system, a plot or a
> interpretation of value with type in physics. Does anyone know such a
> information?

Hello.

First, I must note that my knowledge of constructive type theory is near
null. I am subscribed to this mailing list because I am interested in
learning Agda and its underlying logic but so far I have not allocated
the required time.

What specific famous physical equations do you have in mind?

I have been thinking about formalizing (in HOL4) a derivation of the
Lorentz transform from invariance or symmetry axioms, something like the
textbook derivation (in special relativity) of the Lorentz transform
based on the invariance of the speed of light and isotropy of space.
Having done this, the natural continuation is to follow with the laws of
relativistic mechanics and eventually electromagnetics. Unfortunately, I
need more background in analysis before undertaking the part about
electromagnetics.

(Side note: Poincaré and Lorentz formulated special relativity; Einstein
just took what these men had already discovered, added his own
metaphysical interpretation and published it as if it was his sole work;
in other words, plagiarism combined with philosophical bullshit)

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170928/d9818fd5/attachment-0001.sig>