------------------------------------------------------------------------
-- Atoms
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Atom where

open import Bag-equivalence
open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Decidable-UIP equality-with-J
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Injection equality-with-J using (Injective)
import Nat equality-with-J as Nat
open import Univalence-axiom equality-with-J

-- Atoms.

record Atoms : Set₁ where
  field
    -- The type of atoms.

    Name : Set

    -- The type must be countably infinite.

    countably-infinite : Name  

  -- Atoms have decidable equality.

  _≟_ : Decidable-equality Name
  _≟_ = Bijection.decidable-equality-respects
          (inverse countably-infinite) Nat._≟_

  -- Membership test.

  member : (x : Name) (xs : List Name)  Dec (x  xs)
  member x []       = no  ())
  member x (y  xs) with x  y
  ... | yes x≡y = yes (inj₁ x≡y)
  ... | no  x≢y with member x xs
  ...   | yes x∈xs = yes (inj₂ x∈xs)
  ...   | no  x∉xs = no [ x≢y , x∉xs ]

  -- Conversions.

  name :   Name
  name = _↔_.from countably-infinite

  code : Name  
  code = _↔_.to countably-infinite

  -- The name function is injective.

  name-injective : Injective name
  name-injective = _↔_.injective (inverse countably-infinite)

  -- Distinct natural numbers are mapped to distinct names.

  distinct-codes→distinct-names :  {m n}  m  n  name m  name n
  distinct-codes→distinct-names {m} {n} m≢n =
    name m  name n  ↝⟨ name-injective 
    m  n            ↝⟨ m≢n ⟩□
                    

  -- Name is a set.

  Name-set : Is-set Name
  Name-set = decidable⇒set _≟_

-- One implementation of atoms, using natural numbers.

ℕ-atoms : Atoms
Atoms.Name               ℕ-atoms = 
Atoms.countably-infinite ℕ-atoms = Bijection.id

-- Two sets of atoms, one for constants and one for variables.

record χ-atoms : Set₁ where
  field
    const-atoms var-atoms : Atoms

  module C = Atoms const-atoms renaming (Name to Const)
  module V = Atoms var-atoms   renaming (Name to Var)

  open C public using (Const)
  open V public using (Var)

-- One implementation of χ-atoms, using natural numbers.

χ-ℕ-atoms : χ-atoms
χ-atoms.const-atoms χ-ℕ-atoms = ℕ-atoms
χ-atoms.var-atoms   χ-ℕ-atoms = ℕ-atoms

-- The type of atoms is isomorphic to the unit type (assuming
-- univalence).

Atoms↔⊤ :
  Univalence (# 0) 
  Atoms  
Atoms↔⊤ univ =
  Atoms                          ↝⟨ eq 
  ( λ (Name : Set)  Name  )  ↝⟨ ∃-cong  _  Eq.↔↔≃′ ext ℕ-set) 
  ( λ (Name : Set)  Name  )  ↝⟨ singleton-with-≃-↔-⊤ ext univ ⟩□
                                
  where
  open Atoms

  eq : Atoms   λ (Name : Set)  Name  
  eq = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ a  Name a , countably-infinite a
        ; from = uncurry λ N c 
                   record { Name = N; countably-infinite = c }
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    }

-- The χ-atoms type is isomorphic to the unit type (assuming
-- univalence).

χ-atoms↔⊤ :
  Univalence (# 0) 
  χ-atoms  
χ-atoms↔⊤ univ =
  χ-atoms        ↝⟨ eq 
  Atoms × Atoms  ↝⟨ Atoms↔⊤ univ ×-cong Atoms↔⊤ univ 
   ×           ↝⟨ ×-right-identity ⟩□
                
  where
  open χ-atoms

  eq : χ-atoms  Atoms × Atoms
  eq = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ a  const-atoms a , var-atoms a
        ; from = uncurry λ c v 
                   record { const-atoms = c; var-atoms = v }
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    }

-- If a property holds for one choice of atoms, then it holds for any
-- other choice of atoms (assuming univalence).

invariant :
   {p} 
  Univalence (# 0) 
  (P : χ-atoms  Set p) 
   a₁ a₂  P a₁  P a₂
invariant univ P a₁ a₂ =
  subst P (_⇔_.to propositional⇔irrelevant
             (mono₁ 0 $ _⇔_.from contractible⇔↔⊤ $
                χ-atoms↔⊤ univ)
             a₁ a₂)

-- If a property holds for χ-ℕ-atoms, then it holds for any choice of
-- atoms (assuming univalence).

one-can-restrict-attention-to-χ-ℕ-atoms :
   {p} 
  Univalence (# 0) 
  (P : χ-atoms  Set p) 
  P χ-ℕ-atoms   a  P a
one-can-restrict-attention-to-χ-ℕ-atoms univ P p a =
  invariant univ P χ-ℕ-atoms a p