Skip to content

Commit

Permalink
Use partially applied syntax extensively
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Mar 28, 2020
1 parent 7eaa38b commit 13c8c28
Show file tree
Hide file tree
Showing 45 changed files with 134 additions and 135 deletions.
8 changes: 4 additions & 4 deletions src/Algebra/Domain.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,10 +17,10 @@
#0-zro (transport #0 x*y=0 (apartZeroProduct x y x#0 y#0))))))

\lemma nonZero-left (x y : E) (x/=0 : Not (x = zro)) (x*y=0 : x * y = zro) : y = zro =>
separatedEq (\lam y/=0 => nonZeroProduct x y x/=0 y/=0 x*y=0)
separatedEq (nonZeroProduct x y x/=0 __ x*y=0)

\lemma nonZero-right (x y : E) (y/=0 : Not (y = zro)) (x*y=0 : x * y = zro) : x = zro =>
separatedEq (\lam x/=0 => nonZeroProduct x y x/=0 y/=0 x*y=0)
separatedEq (nonZeroProduct x y __ y/=0 x*y=0)

\lemma nonZero-cancel-left (x y z : E) (x/=0 : Not (x = zro)) (x*y=x*z : x * y = x * z) : y = z =>
AddGroup.fromZero y z (nonZero-left x (y - z) x/=0 (ldistr x y (negative z) *> pmap (x * y +) (Ring.negative_*-right x z) *> AddGroup.toZero (x * y) (x * z) x*y=x*z))
Expand All @@ -35,8 +35,8 @@
| ide-left x => SigmaPropExt #0 _ _ (ide-left x.1)
| ide-right x => SigmaPropExt #0 _ _ (ide-right x.1)
| *-assoc x y z => SigmaPropExt #0 _ _ (*-assoc x.1 y.1 z.1)
| cancel-left x y z x*y=x*z => SigmaPropExt #0 y z (nonZero-cancel-left x.1 y.1 z.1 (\lam x=0 => #0-zro (transport #0 x=0 x.2)) (pmap (\lam t => t.1) x*y=x*z))
| cancel-right x y z x*z=y*z => SigmaPropExt #0 x y (nonZero-cancel-right x.1 y.1 z.1 (\lam z=0 => #0-zro (transport #0 z=0 z.2)) (pmap (\lam t => t.1) x*z=y*z))
| cancel-left x y z x*y=x*z => SigmaPropExt #0 y z (nonZero-cancel-left x.1 y.1 z.1 (\lam x=0 => #0-zro (transport #0 x=0 x.2)) (pmap (__.1) x*y=x*z))
| cancel-right x y z x*z=y*z => SigmaPropExt #0 x y (nonZero-cancel-right x.1 y.1 z.1 (\lam z=0 => #0-zro (transport #0 z=0 z.2)) (pmap (__.1) x*z=y*z))
} \where {
\class Dec \extends Domain, Ring.Dec
\where
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Domain/Bezout.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,9 +17,9 @@
| inv-right =>
g * (p.1 * g|x.inv + p.2 * g|y.inv) ==< ldistr g (p.1 * g|x.inv) (p.2 * g|y.inv) >==
g * (p.1 * g|x.inv) + g * (p.2 * g|y.inv) ==< inv (pmap2 (+) (*-assoc g p.1 g|x.inv) (*-assoc g p.2 g|y.inv)) >==
(g * p.1) * g|x.inv + (g * p.2) * g|y.inv ==< pmap2 (\lam t s => t * g|x.inv + s * g|y.inv) (*-comm g p.1) (*-comm g p.2) >==
(g * p.1) * g|x.inv + (g * p.2) * g|y.inv ==< pmap2 (__ * g|x.inv + __ * g|y.inv) (*-comm g p.1) (*-comm g p.2) >==
(p.1 * g) * g|x.inv + (p.2 * g) * g|y.inv ==< pmap2 (+) (*-assoc p.1 g g|x.inv) (*-assoc p.2 g g|y.inv) >==
p.1 * (g * g|x.inv) + p.2 * (g * g|y.inv) ==< pmap2 (\lam t s => p.1 * t + p.2 * s) g|x.inv-right g|y.inv-right >==
p.1 * (g * g|x.inv) + p.2 * (g * g|y.inv) ==< pmap2 (p.1 * __ + p.2 * __) g|x.inv-right g|y.inv-right >==
p.1 * x + p.2 * y `qed
}
})
6 changes: 3 additions & 3 deletions src/Algebra/Domain/GCD.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@
| inv-right => SigmaPropExt #0 _ y g.gcd|val2.inv-right
}
| gcd-univ h (h|x : LDiv h x) (h|y : LDiv h y) =>
\let h|g : LDiv h.1 g.gcd => g.gcd-univ h.1 (\new LDiv h.1 x.1 h|x.inv.1 (pmap (\lam t => t.1) h|x.inv-right))
(\new LDiv h.1 y.1 h|y.inv.1 (pmap (\lam t => t.1) h|y.inv-right))
\let h|g : LDiv h.1 g.gcd => g.gcd-univ h.1 (\new LDiv h.1 x.1 h|x.inv.1 (pmap (__.1) h|x.inv-right))
(\new LDiv h.1 y.1 h|y.inv.1 (pmap (__.1) h|y.inv-right))
\in \new LDiv {
| inv => (h|g.inv, #0-*-right h.1 h|g.inv (transport #0 (inv h|g.inv-right) g#0))
| inv-right => SigmaPropExt #0 _ (g.gcd, g#0) h|g.inv-right
Expand All @@ -46,7 +46,7 @@
| inv => g|x.inv K.* x#0.inv
| inv-right =>
g * (g|x.inv * x#0.inv) ==< inv (*-assoc g g|x.inv x#0.inv) >==
(g * g|x.inv) * x#0.inv ==< pmap (\lam t => t * x#0.inv) g|x.inv-right >==
(g * g|x.inv) * x#0.inv ==< pmap (__ * x#0.inv) g|x.inv-right >==
x * x#0.inv ==< x#0.inv-right >==
ide `qed
}
Expand Down
12 changes: 6 additions & 6 deletions src/Algebra/Group.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,11 +49,11 @@
})
\where {
\lemma inverse-equality (G H : Group) (p : G = {Monoid} H) : Path (\lam i => p @ i -> p @ i) G.inverse H.inverse
=> \let | q => pmap (\lam X => Monoid.E {X}) p
| f x => coe (\lam i => p @ i) x right
| g y => coe (\lam i => inv q @ i) y right
=> \let | q => pmap (Monoid.E {__}) p
| f x => coe (p @ __) x right
| g y => coe (inv q @) y right
| h' {H' : Monoid} (q : G = {Monoid} H') => transport (\lam (H' : Monoid) => MonoidHom G H') q (MonoidCategory.id G)
| h => transport (\lam f' => MonoidHom G H f') (Jl (\lam (H' : Monoid) q => func {h' q} = (\lam x => coe (\lam i => q @ i) x right)) idp p) (h' p)
| h => transport (MonoidHom G H __) (Jl (\lam (H' : Monoid) q => func {h' q} = (\lam x => coe (q @ __) x right)) idp p) (h' p)
| h-inv (y : H) => MonoidHom.presInvElem h
(\new Inv { | val => g y | inv => G.inverse (g y) | inv-left => G.inverse-left (g y) | inv-right => G.inverse-right (g y) })
(\new Inv { | inv => H.inverse (f (g y)) | inv-left => H.inverse-left (f (g y)) | inv-right => H.inverse-right (f (g y)) })
Expand Down Expand Up @@ -86,7 +86,7 @@
(x + y) - (x + y) ==< negative-right (x + y) >==
zro ==< inv (negative-right x) >==
x - x ==< pmap (x +) (inv (zro-left (negative x))) >==
x + (zro - x) ==< pmap (\lam t => x + (t - x)) (inv (negative-right y)) >==
x + (zro - x) ==< pmap (x + (__ - x)) (inv (negative-right y)) >==
x + ((y - y) - x) ==< pmap (x +) (+-assoc y (negative y) (negative x)) >==
x + (y + (negative y - x)) ==< inv (+-assoc x y (negative y - x)) >==
(x + y) + (negative y - x) `qed
Expand All @@ -111,7 +111,7 @@
\use \coerce fromGroup (G : Group) => \new AddGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.inverse-right
\use \coerce toGroup (G : AddGroup) => \new Group G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.negative-right

\func equals (A B : AddGroup) (p : A = {\Set} B) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : A) -> f (x + y) = f x + f y) : A = B
\func equals (A B : AddGroup) (p : A = {\Set} B) (q : \let f x => coe (p @) x right \in \Pi (x y : A) -> f (x + y) = f x + f y) : A = B
=> pmap {Group} {AddGroup} AddGroup.fromGroup (Group.equals A B (Monoid.equals {AddGroup.toGroup A} {AddGroup.toGroup B} p q))

-- | An additive group with a tight apartness relation.
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Group/Category.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
(inv (f.func-+ (zro {f.Dom}) (zro {f.Dom})) *> pmap f.func (zro-right {f.Dom} (zro {f.Dom})) *> inv (zro-right {f.Cod} (f.func (zro {f.Dom}))))

\func equals {A B : AddGroup} {f g : AbGroupHom A B} (p : \Pi (x : A) -> f.func x = g.func x) : f = g
=> path (\lam i => \new AbGroupHom A B (\lam x => p x @ i) (pathInProp (\lam j => \Pi (x y : A) -> p (x + y) @ j = (p x @ j) + (p y @ j)) f.func-+ g.func-+ @ i))
=> path (\lam i => \new AbGroupHom A B (p __ @ i) (pathInProp (\lam j => \Pi (x y : A) -> p (x + y) @ j = (p x @ j) + (p y @ j)) f.func-+ g.func-+ @ i))
}

\instance AddGroupCategory : Cat AddGroup
Expand All @@ -46,7 +46,7 @@
| o-assoc _ _ _ => idp
| univalence {A B : AddGroup} (f : AbGroupHom A B) (g : AbGroupHom B A) p q =>
\let A=B => AddGroup.equals A B (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-+
\in (A=B, AbGroupHom.equals (\lam x => Jl {AddGroup} (\lam C A=C => func {transport (\lam C => AbGroupHom A C) A=C (id A)} x = coe (\lam j => A=C @ j) x right) idp A=B))
\in (A=B, AbGroupHom.equals (\lam x => Jl {AddGroup} (\lam C A=C => func {transport (AbGroupHom A __) A=C (id A)} x = coe (A=C @ __) x right) idp A=B))
\where
\func id (G : AddGroup) : AbGroupHom G G \cowith
| func x => x
Expand Down
30 changes: 15 additions & 15 deletions src/Algebra/Monoid.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@
| ide-right (x : E) : x * ide = x
| *-assoc (x y z : E) : (x * y) * z = x * (y * z)
} \where {
\func equals {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = N
=> \let mp i => prop-equality p q @ i
\func equals {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = N
=> \let mp => prop-equality p q @ __
\in path (\lam i => \new Monoid (p @ i) (ide-equality p q @ i) (*-equality p q @ i) (ide-left {mp i}) (ide-right {mp i}) (*-assoc {mp i}))
\where {
\lemma ide-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
\lemma ide-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
: Path (\lam j => p @ j) M.ide N.ide
=> \let | f x => coe (\lam i => p @ i) x right
| g y => coe (\lam i => inv p @ i) y right
Expand All @@ -25,20 +25,20 @@
ide `qed
\in pathOver {\lam j => p @ j} r

\lemma *-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
\lemma *-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
: Path (\lam j => p @ j -> p @ j -> p @ j) (M.*) (N.*)
=> \let | f x => coe (\lam i => p @ i) x right
| g y => coe (\lam i => inv p @ i) y right
=> \let | f x => coe (p @) x right
| g y => coe (inv p @) y right
| fg y : f (g y) = y => transport_id_inv (\lam Z => Z) p y
| q' (x y : N) =>
coe (\lam i => p @ i -> p @ i -> p @ i) (*) right x y ==< pmap (\lam h => h y) (transport_pi (\lam Z => Z) (\lam Z => Z -> Z) p (*) x) >==
coe (\lam i => p @ i -> p @ i -> p @ i) (*) right x y ==< pmap (__ y) (transport_pi (\lam Z => Z) (\lam Z => Z -> Z) p (*) x) >==
coe (\lam i => p @ i -> p @ i) (* (g x)) right y ==< transport_pi (\lam Z => Z) (\lam Z => Z) p (* (g x)) y >==
f (g x * g y) ==< q (g x) (g y) >==
f (g x) * f (g y) ==< pmap2 (*) (fg x) (fg y) >==
x * y `qed
\in pathOver {\lam j => p @ j -> p @ j -> p @ j} (path (\lam j x y => q' x y @ j))

\lemma prop-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (\lam i => p @ i) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
\lemma prop-equality {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y)
: Path (\lam j => Monoid (p @ j) (ide-equality p q @ j) (*-equality p q @ j)) M N
=> pathInProp (\lam i => Monoid (p @ i) (ide-equality p q @ i) (*-equality p q @ i)) M N
}
Expand Down Expand Up @@ -94,7 +94,7 @@
\lemma cancelProp {M : Monoid} (x : M) (q : \Pi (a b : M) -> x * a = x * b -> a = b) (y : M) : isProp (LDiv x y) =>
\lam (d1 d2 : LDiv x y) =>
\let p => q d1.inv d2.inv (d1.inv-right *> Paths.inv d2.inv-right)
\in path (\lam i => \new LDiv x y (p @ i) (pathInProp (\lam j => x * (p @ j) = y) d1.inv-right d2.inv-right @ i))
\in path (\lam i => \new LDiv x y (p @ i) (pathInProp (x * (p @ __) = y) d1.inv-right d2.inv-right @ i))

\use \level levelProp {M : CancelMonoid} (x y : M) : isProp (LDiv x y) => cancelProp x (M.cancel-left x) y
}
Expand Down Expand Up @@ -125,7 +125,7 @@
\lemma levelProp {M : CancelMonoid} (x y : M) : isProp (RDiv x y) =>
\lam (d1 d2 : RDiv x y) =>
\let p => M.cancel-right d1.inv d2.inv x (d1.inv-left *> Paths.inv d2.inv-left)
\in path (\lam i => \new RDiv x y (p @ i) (pathInProp (\lam j => (p @ j) * x = y) d1.inv-left d2.inv-left @ i))
\in path (\lam i => \new RDiv x y (p @ i) (pathInProp ((p @ __) * x = y) d1.inv-left d2.inv-left @ i))
}

-- | The type of left inverses of an element
Expand Down Expand Up @@ -170,8 +170,8 @@
j'.inv * ide ==< ide-right j'.inv >==
j'.inv `qed
\in path (\lam i => \new Inv x (p @ i)
(pathInProp (\lam j => (p @ j) * x = ide) j.inv-left j'.inv-left @ i)
(pathInProp (\lam j => x * (p @ j) = ide) j.inv-right j'.inv-right @ i))
(pathInProp ((p @ __) * x = ide) j.inv-left j'.inv-left @ i)
(pathInProp (x * (p @ __) = ide) j.inv-right j'.inv-right @ i))

\lemma product {M : Monoid} (i j : Inv {M}) : Inv (i.val * j.val) => func i j
\where {
Expand All @@ -183,7 +183,7 @@
\lemma lem {M : Monoid} (i j : Inv {M}) : (j.inv * i.inv) * (i.val * j.val) = ide =>
(j.inv * i.inv) * (i.val * j.val) ==< *-assoc j.inv i.inv (i.val * j.val) >==
j.inv * (i.inv * (i.val * j.val)) ==< pmap (j.inv *) (Paths.inv (*-assoc i.inv i.val j.val)) >==
j.inv * ((i.inv * i.val) * j.val) ==< pmap (\lam t => j.inv * (t * j.val)) i.inv-left >==
j.inv * ((i.inv * i.val) * j.val) ==< pmap (j.inv * (__ * j.val)) i.inv-left >==
j.inv * (ide * j.val) ==< pmap (j.inv *) (ide-left j.val) >==
j.inv * j.val ==< j.inv-left >==
ide `qed
Expand All @@ -198,7 +198,7 @@
(i.inv * x) * (y * (j.inv * x)) ==< *-assoc i.inv x (y * (j.inv * x)) >==
i.inv * (x * (y * (j.inv * x))) ==< pmap (i.inv *) (Paths.inv (*-assoc x y (j.inv * x))) >==
i.inv * ((x * y) * (j.inv * x)) ==< pmap (i.inv *) (Paths.inv (*-assoc (x * y) j.inv x)) >==
i.inv * (((x * y) * j.inv) * x) ==< pmap (\lam t => i.inv * (t * x)) j.inv-right >==
i.inv * (((x * y) * j.inv) * x) ==< pmap (i.inv * (__ * x)) j.inv-right >==
i.inv * (ide * x) ==< pmap (i.inv *) (ide-left x) >==
i.inv * x ==< i.inv-left >==
ide `qed
Expand Down Expand Up @@ -227,7 +227,7 @@
lmake (i.inv * x) (*-assoc i.inv x y *> i.inv-left)

\lemma cfactor-left {M : CMonoid} (x y : M) (i : Inv (x * y)) : Inv x =>
cfactor-right y x (transport (\lam t => Inv t) (*-comm x y) i)
cfactor-right y x (transport (Inv __) (*-comm x y) i)
}
}

Expand Down
6 changes: 3 additions & 3 deletions src/Algebra/Monoid/Category.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@
}
\where {
\func equals {M N : Monoid} {f g : MonoidHom M N} (p : \Pi (x : M) -> f.func x = g.func x) : f = g
=> path (\lam i => \new MonoidHom M N (\lam x => p x @ i)
(pathInProp (\lam j => p ide @ j = ide) f.func-ide g.func-ide @ i)
=> path (\lam i => \new MonoidHom M N (p __ @ i)
(pathInProp (p ide @ __ = ide) f.func-ide g.func-ide @ i)
(pathInProp (\lam j => \Pi (x y : M) -> p (x * y) @ j = (p x @ j) * (p y @ j)) f.func-* g.func-* @ i))

\open Monoid(Inv)
Expand Down Expand Up @@ -44,7 +44,7 @@
| o-assoc _ _ _ => idp
| univalence {M N : Monoid} (f : MonoidHom M N) (g : MonoidHom N M) p q =>
\let M=N => Monoid.equals (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-*
\in (M=N, MonoidHom.equals (\lam x => Jl {Monoid} (\lam K M=K => func {transport (\lam K => MonoidHom M K) M=K (id M)} x = coe (\lam j => M=K @ j) x right) idp M=N))
\in (M=N, MonoidHom.equals (\lam x => Jl {Monoid} (\lam K M=K => func {transport (MonoidHom M __) M=K (id M)} x = coe (M=K @ __) x right) idp M=N))
\where
\func id (M : Monoid) : MonoidHom M M \cowith
| func x => x
Expand Down
6 changes: 3 additions & 3 deletions src/Algebra/Monoid/Prime.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
| isIrr (x y : M) : e = x * y -> Inv x || Inv y

\func decide (x y : M) (e=x*y : e = x * y) : Inv x `Or` Inv y =>
||.rec (Or.levelProp (\lam (i : Inv x) (j : Inv y) => notInv (transport (\lam x => Inv x) (inv e=x*y) (Inv.product i j)))) inl inr (isIrr x y e=x*y)
||.rec (Or.levelProp (\lam (i : Inv x) (j : Inv y) => notInv (transport (Inv __) (inv e=x*y) (Inv.product i j)))) inl inr (isIrr x y e=x*y)
}

\lemma Prime-isIrr {M : CancelCMonoid} (p : Prime {M}) : Irr p.e p.notInv \cowith
Expand Down Expand Up @@ -79,9 +79,9 @@
))
| byRight (xi : Inv x) => byLeft (\new LDiv p.e a (xi.inv * g|a.inv) (
p.e * (xi.inv * g|a.inv) ==< inv (*-assoc _ _ _) >==
(p.e * xi.inv) * g|a.inv ==< pmap (\lam t => (t * xi.inv) * g|a.inv) (inv g|p.inv-right) >==
(p.e * xi.inv) * g|a.inv ==< pmap ((__ * xi.inv) * g|a.inv) (inv g|p.inv-right) >==
((g * x) * xi.inv) * g|a.inv ==< pmap (`* g|a.inv) (*-assoc _ _ _) >==
(g * (x * xi.inv)) * g|a.inv ==< pmap (\lam t => (g * t) * g|a.inv) xi.inv-right >==
(g * (x * xi.inv)) * g|a.inv ==< pmap ((g * __) * g|a.inv) xi.inv-right >==
(g * ide) * g|a.inv ==< pmap (`* g|a.inv) (ide-right g) >==
g * g|a.inv ==< g|a.inv-right >==
a `qed
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Ordered.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
(y + z) - (x + z) ==< pmap ((y + z) +) (negative_+ x z) >==
(y + z) + (negative z - x) ==< +-assoc _ _ _ >==
y + (z + (negative z - x)) ==< inv (pmap (y +) (+-assoc _ _ _)) >==
y + ((z - z) - x) ==< pmap (\lam t => y + (t - x)) (negative-right z) >==
y + ((z - z) - x) ==< pmap (y + (__ - x)) (negative-right z) >==
y + (zro - x) ==< pmap (y +) (zro-left _) >==
y - x `qed)) x<y

Expand All @@ -56,7 +56,7 @@
\lemma diff_+ {A : AddGroup} {x y z : A} : (z - y) + (y - x) = z - x =>
(z - y) + (y - x) ==< +-assoc _ _ _ >==
z + (negative y + (y - x)) ==< inv (pmap (z +) (+-assoc _ _ _)) >==
z + ((negative y + y) - x) ==< pmap (\lam t => z + (t - x)) (negative-left y) >==
z + ((negative y + y) - x) ==< pmap (z + (__ - x)) (negative-left y) >==
z + (zro - x) ==< pmap (z +) (zro-left _) >==
z - x `qed
}
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Pointed.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
\class Pointed \extends BaseSet
| ide : E
\where {
\func equls {X Y : Pointed} (p : X = {\Set} Y) (q : coe (\lam i => p @ i) ide right = ide) : X = Y
=> path (\lam i => \new Pointed (p @ i) (pathOver {\lam j => p @ j} q @ i))
\func equls {X Y : Pointed} (p : X = {\Set} Y) (q : coe (p @) ide right = ide) : X = Y
=> path (\lam i => \new Pointed (p @ i) (pathOver {p @} q @ i))
}

\class AddPointed \extends BaseSet
Expand Down
4 changes: 2 additions & 2 deletions src/Algebra/Pointed/Category.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
| func-ide : func ide = ide
} \where
\func equals {X Y : Pointed} {f g : PointedHom X Y} (p : \Pi (x : X) -> f.func x = g.func x) : f = g
=> path (\lam i => \new PointedHom X Y (\lam x => p x @ i) (pathInProp (\lam j => p ide @ j = ide) f.func-ide g.func-ide @ i))
=> path (\lam i => \new PointedHom X Y (p __ @ i) (pathInProp (p ide @ __ = ide) f.func-ide g.func-ide @ i))

\instance PointedSetCat : Cat Pointed
| Hom X Y => PointedHom X Y
Expand All @@ -23,7 +23,7 @@
| o-assoc _ _ _ => idp
| univalence {X Y : Pointed} (f : PointedHom X Y) (g : PointedHom Y X) p q =>
\let X=Y => Pointed.equls (path (iso f.func g.func (\lam x => path (\lam i => func {p @ i} x)) (\lam y => path (\lam i => func {q @ i} y)))) f.func-ide
\in (X=Y, PointedHom.equals (\lam x => Jl {Pointed} (\lam Z X=Z => func {transport (\lam Z => PointedHom X Z) X=Z (id X)} x = coe (\lam j => X=Z @ j) x right) idp X=Y))
\in (X=Y, PointedHom.equals (\lam x => Jl {Pointed} (\lam Z X=Z => func {transport (PointedHom X __) X=Z (id X)} x = coe (\lam j => X=Z @ j) x right) idp X=Y))
\where
\func id (X : Pointed) : PointedHom X X \cowith
| func x => x
Expand Down
Loading

0 comments on commit 13c8c28

Please sign in to comment.