(* https://math.stackexchange.com/questions/3802938/computational-type-theory-for-topos-logic *)
From mathcomp Require Export all_ssreflect ssralg.
Require Export isomorphism weil_algebras axioms basic_infinitesimal_spaces.

Definition fiber {E B} (f : E -> B) : B -> Type
    := fun b => {e : E | f e = b}.

Definition bundle {B} (f : B -> Type) : Type
    := {b : B & f b}.

Definition field {B} (f : B -> Type) : Type
    := forall b : B, f b.



Lemma bundle_fiber {E B} (f : E -> B) : bundle (fiber f) <--> E.
Proof.
    refine({|
        Forward '(existT b (exist e _)) := e;
        Backward e := existT _ (f e) (exist _ e erefl);
    |}).
    - move=> [b [e pf]].
        move: b pf.
        by apply: eq_indd.
    - done.
Defined.

Lemma fiber_bundle {B} {F : B -> Type} {b} 
    : fiber (projT1 (P := _) : bundle F -> B) b <--> F b.
Proof.
    refine({|
        Forward '(exist (existT x f) pf) := eq_rect _ F f _ pf;
        Backward f := exist _ (existT _ b f) erefl;
    |}).
    - move=> [[b' f] pf].
        move: b pf.
        by apply: eq_indd.
    - done.
Defined.



Definition tangent_bundle M := 'D_1 -> M.
Definition tangent M := fiber (fun f : tangent_bundle M => f zero).