From Coq Require Import PropExtensionality FunctionalExtensionality ProofIrrelevance ssreflect.
Require Export isomorphism.
Class Atomic (O : Type) := {
    Amazing : Type -> Type;
    amaze : forall {A B}, ((O -> A) -> B) <--> (A -> Amazing B);
}.
Notation "{ 'amazing' O , X }" := (Amazing (O := O) X)
    (at level 0, format "{ 'amazing' O , X }") : type_scope.
    
#[refine]
Global Instance iUnit : Atomic unit := {
    Amazing T := T;
    amaze _ _ := {|
        Forward f t := f (fun 'tt => t);
        Backward f t := f (t tt);
    |}
}.
Proof.
    - move=> f.
        apply: functional_extensionality => x.
        suff: x = fun 'tt => x tt by move=>->.
        apply: functional_extensionality.
        by move=>[].
    - done.
Qed.

Require Export isomorphism atomic weil_algebras axioms basic_infinitesimal_spaces.

Require Export isomorphism weil_algebras axioms basic_infinitesimal_spaces.

Require Import isomorphism axioms atomic.

Require Import isomorphism axioms.

    Axiom atomicD : forall {n}, Atomic 'D_n.

    Axiom atomicΔ : forall {n}, Atomic (Δ n).

    Definition atomicD {n} : Atomic 'D_n := {|
        Amazing X := { amazing Spec R (Weil (nilpotent_weil n)), X };
        amaze _ _ := iso_trans (iso_exp (iso_exp nilpotent_weil_iso)) amaze;
    |}.
    

Global Instance atomicD {n} : Atomic 'D_n := atomicD.

    Admitted.
    Definition atomicΔ {n} : Atomic (Δ n).

Global Instance atomicΔ {n} : Atomic (Δ n) := atomicΔ.
(* Can this be done?
#[refine]
Global Instance atomicD_union : Atomic 'D_∞ := {|
    Amazing X := _;
    amaze _ _ := _;
|}.
Admitted.
*)

Require Import weil_algebras atomic.

Require Import weil_algebras.

(* Axiom 3, from *Synthetic Differential Geometry*. *)
Axiom atomicAxiom : Atomic (Spec R (Weil W)).

Global Instance iSpec {W} : Atomic (Spec R (Weil W)) := atomicAxiom W.

theories/atomic.v

An element J of a topos is *atomic* if the functor `(–)^J` has a right adjoint, called `(–)_J`.
In other words, morphisms `B^J -> C` uniquely correspond to morphisms `B -> C_J`.
But this does *not* mean that the objects `C^(B^J)` and `(C_J)^B` are isomorphic.
They only have the same global elements.
In fact:
```text
X -> (C_J)^B
= X * B -> C_J
= (X * B)^J -> C
= X^J * B^J -> C
= X^J -> C^(B^J)
≠ X -> C^(B^J)
```
This issue does not happen for exponentials, because:
```text
X -> (B^J)^A
= X * A -> B^J
= (X * A) * J -> B
= X * (A * J) -> B
= X -> B^(A * J)
```