Skip to content

Commit

Permalink
Fix typechecking
Browse files Browse the repository at this point in the history
  • Loading branch information
valis committed Dec 4, 2022
1 parent e2d4be3 commit 89dcffa
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/Analysis/Calculus/Derivative.ard
Original file line number Diff line number Diff line change
Expand Up @@ -12,18 +12,18 @@
\open isDiff

\class DRing \extends CRing
| inv-dense {B : \Set} (U : E -> \Prop) (f g : \Sigma (z : E) (\property U z) -> B) : (\Pi (p : \Sigma (z : E) (\property u : U z)) -> Monoid.Inv p.1 -> f p = g p) -> \Pi (p : \Sigma (z : E) (\property u : U z)) -> f p = g p
| inv-dense {B : \Set} (U : E -> \Prop) (f g : \Sigma (z : E) (U z) -> B) : (\Pi (p : \Sigma (z : E) (u : U z)) -> Monoid.Inv p.1 -> f p = g p) -> \Pi (p : \Sigma (z : E) (u : U z)) -> f p = g p
\where
\lemma cancel-lem {R : DRing} {B : LModule' R} (U : R -> \Prop) (f g : \Sigma (z : R) (\property U z) -> B) (p : \Sigma (z : R) (\property u : U z)) (s : \Pi (p : \Sigma (z : R) (\property u : U z)) -> p.1 *c f p = p.1 *c g p) : f p = g p
\lemma cancel-lem {R : DRing} {B : LModule' R} (U : R -> \Prop) (f g : \Sigma (z : R) (U z) -> B) (p : \Sigma (z : R) (u : U z)) (s : \Pi (p : \Sigma (z : R) (u : U z)) -> p.1 *c f p = p.1 *c g p) : f p = g p
=> R.inv-dense U f g (\lam p p-inv => B.cancel p-inv (s p)) p

\func isDiff {R : DRing} {A B : LModule' R} {U : A -> \Prop} (f : \Sigma (x : A) (U x) -> B) : \Set
=> \Pi (x : \Sigma (a : A) (U a)) (a : A) (t : \Sigma (r : R) (\property U (x.1 + r *c a))) -> \Sigma (y : B) (t.1 *c y = f (x.1 + t.1 *c a, t.2) - f x)
=> \Pi (x : \Sigma (a : A) (U a)) (a : A) (t : \Sigma (r : R) (U (x.1 + r *c a))) -> \Sigma (y : B) (t.1 *c y = f (x.1 + t.1 *c a, t.2) - f x)
\where {
\use \level levelProp (d d' : isDiff f) : d = d'
=> ext $ \lam x a t => ext $ cancel-lem _ _ _ t $ \lam t => (d x a t).2 *> inv (d' x a t).2

\lemma isDiff-eq {f : \Sigma (x : A) (U x) -> B} (d : isDiff f) {x x' : \Sigma (a : A) (U a)} (p : x.1 = x'.1) {a : A} {t : \Sigma (r : R) (\property U (x.1 + r *c a))} {t' : \Sigma (r : R) (\property U (x'.1 + r *c a))} (q : t.1 = t'.1) : (d x a t).1 = (d x' a t').1
\lemma isDiff-eq {f : \Sigma (x : A) (U x) -> B} (d : isDiff f) {x x' : \Sigma (a : A) (U a)} (p : x.1 = x'.1) {a : A} {t : \Sigma (r : R) (U (x.1 + r *c a))} {t' : \Sigma (r : R) (U (x'.1 + r *c a))} (q : t.1 = t'.1) : (d x a t).1 = (d x' a t').1
=> path (\lam i => (d (p i, pathInProp _ _ _ i) a (q i, pathInProp _ _ _ i)).1)
}

Expand Down

0 comments on commit 89dcffa

Please sign in to comment.