namespace http://mathhub.info/MitM/Foundation/Units ❚

import rules scala://rules.mitm.mmt.kwarc.info ❚

theory Dimensions : ur:?LF = 

  /T An SI Dimension. ❙
  dimension : type❙
  
  include ☞http://mathhub.info/MitM/Foundation?IntLiterals ❙
  
  /T A normalized representation used for equality reasoning etc. ❙
  NormedDimension : ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ dimension ❙

  /T We want the actual dimensions as a dimension. ❙
  /T We use the SI base dimensions for this. ❙
  Length : dimension ❘ // = NormedDimension 1 0 0 0 0 0 0❙
  Time : dimension❘ // = NormedDimension 0 1 0 0 0 0 0❙
  Mass : dimension❘ // = NormedDimension 0 0 1 0 0 0 0❙
  Amount : dimension❘ // = NormedDimension 0 0 0 1 0 0 0❙
  Temperature : dimension❘ // = NormedDimension 0 0 0 0 1 0 0❙
  Current : dimension❘ // = NormedDimension 0 0 0 0 0 1 0❙
  LuminousIntensity : dimension❘ // = NormedDimension 0 0 0 0 0 0 1 ❙
  DimNone : dimension❘ // = NormedDimension 0 0 0 0 0 0 0 ❙

  /T Now we want to make even more dimensions. ❙
  DimTimes: dimension ⟶ dimension ⟶ dimension ❘ # 1 *' 2 ❙
  DimDiv: dimension ⟶ dimension ⟶ dimension ❘ # 1 /' 2 ❙
  
  rule rules?DimEq ❙
❚

theory DimensionsExtended : ur:?LF =
  include ?Dimensions❙

  // Dimensionless stuff❙
  Information : dimension ❘= DimNone❙

  // Velocity, Accelleration ❙
  Velocity : dimension ❘= Length /' Time❙
  Acceleration : dimension ❘= Velocity /' Time❙

  // Area and Volume❙
  Area : dimension ❘= Length *' Length❙
  Volume : dimension ❘= Area *' Length❙
  
  // Densities ❙
  VolumeDensity : dimension ❘= DimNone /' Volume ❘  // # Density //?? ❙
  AreaDensity : dimension ❘= DimNone /' Area❙
  LineDensity : dimension ❘= DimNone /' Length❙

  // Force and Pressure❙                   
  Force : dimension ❘= Mass *' Acceleration❙
  Pressure : dimension ❘= Force /' Area❙

  // Electric Charge and Charge Densities❙
  ElectricCharge : dimension ❘= Current *' Time ❙
  ElectricChargeVolumeDensity : dimension ❘= ElectricCharge *' VolumeDensity ❘ # ElectricChargeDensity❙
  ElectricChargeAreaDensity : dimension ❘= ElectricCharge *' AreaDensity ❘ # ElectricChargeSurfaceDensity❙
  ElectricChargeLineDensity : dimension ❘= ElectricCharge *' LineDensity❙
  
  // Energy and Power❙
  Energy : dimension ❘= Force *' Length ❙
  Power : dimension ❘= Energy /' Time❙
  
  // Basic Electrostatic Units❙
  ElectricPotential : dimension ❘= Energy /' ElectricCharge ❘ # Voltage❙
  ElectricDisplacement : dimension ❘ = ElectricCharge /' Area ❙ 
  ElectricCurrentDensity : dimension ❘= Current *' AreaDensity ❘ # Polarization ❘ // # CurrentDensity ❙
  ElectricField : dimension ❘ = Voltage /' Length ❘ # ElectricFieldIntensity ❙
  
  // Other Electrical Units❙
  ElectricalResistance : dimension ❘ = Voltage /' Current ❙
  ElectricalResistivity : dimension ❘ = ElectricalResistance *' Area /' Length ❙
  ElectricalConductivity : dimension ❘ = DimNone /' ElectricalResistivity ❙ 
  ElectricFlux : dimension ❘ = Voltage *' Length ❙ 
  ElectricalCapacitance : dimension ❘ = ElectricCharge /' Voltage ❙
  ElectricalPermittivity : dimension ❘ = ElectricalCapacitance /' Length ❙
  ElectricalMobility : dimension ❘ = Velocity /' ElectricField ❙
  
  IonRecombination : dimension ❘ = Volume /' Time ❙

  // Magnetism // Hoping we don't need that for now
  
  // Heat-related , cf. Thermistor example❙
  Heat : dimension ❘ = Energy ❙ 
	// ThermalConductivity : dimension ❘ = Energy /' Length /' Temperature ❙ // TODO Name clash with quantities.mmt ❙
	ThermalHeatFlux : dimension ❘ = Energy /' Area ❙ 
  
❚