From mathcomp Require Import ssralg ssreflect ssrfun.
Require Import weil_algebras.

From Coq Require Export FunctionalExtensionality ProofIrrelevance Description.

Open Scope R.
Export GRing.Theory.

(* The ring of numbers. *)
Parameter R : comUnitRingType.

Section WeilAxioms.

Variable (W : WeilData R).

Definition Spec (R : ringType) (A : algType R) := {lrmorphism A -> R^o}.

(* Axiom 1W, from *Synthetic Differential Geometry*. *)
Definition KL_inv : Weil W -> (Spec R (Weil W) -> R) := fun a f => f a.
Axiom KL : (Spec R (Weil W) -> R) -> Weil W.
Axiom KL_linv : cancel KL_inv KL.
Axiom KL_rinv : cancel KL KL_inv.

End WeilAxioms.