Created by finegeometer on February 20, 2022

`VJZMBX6RE7BBINBTXKXER3W2C5WYGUBGFAPFU5MB2JUQMYBUSZHAC`

main

###### File deletion: atomic.v

`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.`

###### Replacement in theories/common.v at line 3 [2.12647]

###### Replacement in theories/basic_infinitesimal_spaces.v at line 2 [2.13912]

###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 80 [2.13912]###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 148 [2.13912]###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 394 [2.13912]###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 395 [2.13912]###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 415 [2.13912]###### Deletion in

*theories/basic_infinitesimal_spaces.v*at line 417 [2.13912]###### Replacement in theories/axioms.v at line 2 [2.27667]

###### Deletion in

*theories/axioms.v*at line 24 [2.27667]###### Deletion in

*theories/axioms.v*at line 25 [2.27667]###### Deletion in

*_CoqProject*at line 2 [2.29308]###### File addition: AtomicWarning.md

[3.1]`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)`

`````