In "fully constructive" versions of the normal algebraic structures
the "points" (i.e. the elements) come from a SeparationSpace -- a type with a separation relation x # y.
Then the negation ⌜¬x # y⌝ -- which we write ⌜x ≡ y⌝ -- is an equivalence
relation on the elements.
We could then form a quotient type ⌜x,x':Point(self)//x ≡ x'⌝ and use the
normal defintion of algebraic structures with elements from the quotient type.
But, in general, we may not be able to define the needed operations on the
quotient.
Instead, we state the "equations"
(e.g.associativity, inverse, and identity, for groups) using
the equivalence realtion x ≡ x' instead of equality.
In addition, we add as axioms that the algebraic operations
are "strongly extensional"⋅
Definition: Leibniz-type
Leibniz-type{i:l}(T) ==
∃sep:T ⟶ T ⟶ ℙ. ((∀x,y:T. ((sep x y) ⇒ (∀z:T. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:T. (x = y ∈ T ⇐⇒ ¬(sep x y))))
Lemma: Leibniz-type_wf
∀[T:𝕌']. (Leibniz-type{i:l}(T) ∈ 𝕌')
Lemma: decidable-equality-implies-Leibniz-type
∀T:Type. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ Leibniz-type{i:l}(T))
Lemma: function-Leibniz-type
∀A:Type. ∀B:A ⟶ Type. ((∀a:A. Leibniz-type{i:l}(B[a])) ⇒ Leibniz-type{i:l}(a:A ⟶ B[a]))
Lemma: prod-Leibniz-type
∀A,B:Type. (Leibniz-type{i:l}(A) ⇒ Leibniz-type{i:l}(B) ⇒ Leibniz-type{i:l}(A × B))
Lemma: union-Leibniz-type
∀A,B:Type. (Leibniz-type{i:l}(A) ⇒ Leibniz-type{i:l}(B) ⇒ Leibniz-type{i:l}(A + B))
Lemma: product-Leibniz-type
∀A:Type. ∀B:A ⟶ Type. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀a:A. Leibniz-type{i:l}(B[a])) ⇒ Leibniz-type{i:l}(a:A × B[a]))
Lemma: set-Leibniz-type
∀A:Type. (Leibniz-type{i:l}(A) ⇒ (∀B:A ⟶ ℙ. Leibniz-type{i:l}({a:A| B[a]} )))
Definition: separation-space
SeparationSpace ==
"Point":Type
"#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))}
"#or":∀x,y,z:self."Point". ((self."#" x y) ⇒ ((self."#" x z) ∨ (self."#" y z)))
Lemma: separation-space_wf
SeparationSpace ∈ 𝕌'
Definition: ss-point
Point(ss) == ss."Point"
Lemma: ss-point_wf
∀[ss:SeparationSpace]. (Point(ss) ∈ Type)
Definition: ss-sep
x # y == ss."#" x y
Lemma: ss-sep_wf
∀[ss:SeparationSpace]. ∀[x,y:Point(ss)]. (x # y ∈ ℙ)
Lemma: ss-sep-irrefl
∀[ss:SeparationSpace]. ∀[x:Point(ss)]. (¬x # x)
Lemma: ss-sep-or
∀ss:SeparationSpace. ∀x,y,z:Point(ss). (x # y ⇒ (x # z ∨ y # z))
Lemma: ss-sep-symmetry
∀ss:SeparationSpace. ∀x,y:Point(ss). (x # y ⇒ y # x)
Definition: mk-ss
Point=P #=Sep cotrans=C == λx.x["Point" := P]["#" := Sep]["#or" := C]
Lemma: mk-ss_wf
∀[P:Type]. ∀[Sep:{s:P ⟶ P ⟶ ℙ| ∀x:P. (¬(s x x))} ]. ∀[C:∀x,y,z:P. ((Sep x y) ⇒ ((Sep x z) ∨ (Sep y z)))].
(Point=P #=Sep cotrans=C ∈ SeparationSpace)
Definition: ss-map
ss-map(X;Y;f) == ∀x,x':Point(X). (f x # f x' ⇒ x # x')
Lemma: ss-map_wf
∀[X,Y:SeparationSpace]. ∀[f:Point(X) ⟶ Point(Y)]. (ss-map(X;Y;f) ∈ ℙ)
Definition: ss-eq
x ≡ y == ¬x # y
Lemma: ss-eq_wf
∀[ss:SeparationSpace]. ∀[x,y:Point(ss)]. (x ≡ y ∈ ℙ)
Lemma: stable__ss-eq
∀[ss:SeparationSpace]. ∀[x,y:Point(ss)]. Stable{x ≡ y}
Lemma: sq_stable__ss-eq
∀[ss:SeparationSpace]. ∀[x,y:Point(ss)]. SqStable(x ≡ y)
Lemma: ss-eq_weakening
∀ss:SeparationSpace. ∀x,y:Point(ss). ((x = y ∈ Point(ss)) ⇒ x ≡ y)
Lemma: ss-eq_inversion
∀ss:SeparationSpace. ∀x,y:Point(ss). (x ≡ y ⇒ y ≡ x)
Lemma: ss-eq_transitivity
∀ss:SeparationSpace. ∀x,y,z:Point(ss). (x ≡ y ⇒ y ≡ z ⇒ x ≡ z)
Lemma: ss-eq_functionality
∀ss:SeparationSpace. ∀x1,x2,y1,y2:Point(ss). (uiff(x1 ≡ y1;x2 ≡ y2)) supposing (y1 ≡ y2 and x1 ≡ x2)
Lemma: ss-sep_functionality
∀ss:SeparationSpace. ∀x,y,x',y':Point(ss). (x ≡ x' ⇒ y ≡ y' ⇒ {x # y ⇐⇒ x' # y'})
Lemma: ss-eq_test
∀ss:SeparationSpace. ∀x,y,z,w:Point(ss). (y ≡ x ⇒ y ≡ z ⇒ w ≡ z ⇒ x ≡ w)
Lemma: ss-sep_test
∀ss:SeparationSpace. ∀x,y,z,w,a:Point(ss). (y ≡ x ⇒ y ≡ z ⇒ w ≡ z ⇒ w # a ⇒ x # a)
Definition: ss-function
ss-function(X;Y;f) == ∀x,x':Point(X). (x ≡ x' ⇒ f x ≡ f x')
Lemma: ss-function_wf
∀[X,Y:SeparationSpace]. ∀[f:Point(X) ⟶ Point(Y)]. (ss-function(X;Y;f) ∈ ℙ)
Lemma: stable__ss-function
∀[X,Y:SeparationSpace]. ∀[f:Point(X) ⟶ Point(Y)]. Stable{ss-function(X;Y;f)}
Definition: fun-sep
fun-sep(ss;A;f;g) == ∃a:A. f a # g a
Lemma: fun-sep_wf
∀[A:Type]. ∀[ss:SeparationSpace]. ∀[f,g:A ⟶ Point(ss)]. (fun-sep(ss;A;f;g) ∈ ℙ)
Lemma: fun-sep-symmetry
∀[A:Type]. ∀ss:SeparationSpace. ∀f,g:A ⟶ Point(ss). (fun-sep(ss;A;f;g) ⇒ fun-sep(ss;A;g;f))
Lemma: fun-sep-co-trans
∀[A:Type]. ∀ss:SeparationSpace. ∀f,g,h:A ⟶ Point(ss). (fun-sep(ss;A;f;g) ⇒ (fun-sep(ss;A;f;h) ∨ fun-sep(ss;A;g;h)))
Definition: fun-ss
A ⟶ ss ==
Point=A ⟶ Point(ss) #=λf,g. fun-sep(ss;A;f;g) cotrans=λf,g,h,fsep. let a,sep = fsep
in case ss."#or" (f a) (g a) (h a) sep
of inl(x) =>
inl <a, x>
| inr(y) =>
inr <a, y>
Lemma: fun-ss_wf
∀[ss:SeparationSpace]. ∀[A:Type]. (A ⟶ ss ∈ SeparationSpace)
Lemma: fun-ss-point
∀[ss,A:Top]. (Point(A ⟶ ss) ~ A ⟶ Point(ss))
Lemma: fun-ss-sep
∀[ss,A,f,g:Top]. (f # g ~ ∃a:A. f a # g a)
Lemma: fun-ss-eq
∀[ss:SeparationSpace]. ∀[A:Type]. ∀[f,g:A ⟶ Point(ss)]. uiff(f ≡ g;∀a:A. f a ≡ g a)
Definition: prod-ss
ss1 × ss2 ==
Point=Point(ss1) × Point(ss2) #=λp,q. (fst(p) # fst(q) ∨ snd(p) # snd(q)) cotrans=λx,y,z,d. case d
of inl(a) =>
case ss1."#or" (fst(x))
(fst(y))
(fst(z))
a
of inl(u) =>
inl inl u
| inr(u) =>
inr (inl u)
| inr(b) =>
case ss2."#or" (snd(x))
(snd(y))
(snd(z))
b
of inl(u) =>
inl (inr u )
| inr(u) =>
inr inr u
Lemma: prod-ss_wf
∀[ss1,ss2:SeparationSpace]. (ss1 × ss2 ∈ SeparationSpace)
Lemma: prod-ss-point
∀[ss1,ss2:Top]. (Point(ss1 × ss2) ~ Point(ss1) × Point(ss2))
Lemma: prod-ss-sep
∀[ss1,ss2,x,y:Top]. (x # y ~ fst(x) # fst(y) ∨ snd(x) # snd(y))
Lemma: prod-ss-eq
∀[ss1,ss2:SeparationSpace]. ∀[x,y:Point(ss1 × ss2)]. uiff(x ≡ y;fst(x) ≡ fst(y) ∧ snd(x) ≡ snd(y))
Definition: set-ss
{x:ss | P[x]} == Point={x:Point(ss)| P[x]} #=λx,y. x # y cotrans=ss."#or"
Lemma: set-ss_wf
∀[ss:SeparationSpace]. ∀[P:Point(ss) ⟶ ℙ]. ({x:ss | P[x]} ∈ SeparationSpace)
Lemma: set-ss-point
∀[ss,P:Top]. (Point({x:ss | P[x]}) ~ {x:Point(ss)| P[x]} )
Lemma: set-ss-sep
∀[ss,P,x,y:Top]. (x # y ~ x # y)
Lemma: set-ss-eq
∀[ss,P,x,y:Top]. (x ≡ y ~ x ≡ y)
Definition: union-sep
union-sep(ss1;ss2;p;q) ==
case p
of inl(a) =>
case q of inl(a') => a # a' | inr(b') => True
| inr(b) =>
case q of inl(a') => True | inr(b') => b # b'
Lemma: union-sep_wf
∀[ss1,ss2:SeparationSpace]. ∀[p,q:Point(ss1) + Point(ss2)]. (union-sep(ss1;ss2;p;q) ∈ ℙ)
Definition: union-ss
ss1 + ss2 ==
Point=Point(ss1) + Point(ss2) #=λp,q. union-sep(ss1;ss2;p;q) cotrans=λx,y,z,sep. case x
of inl(a) =>
case y
of inl(a') =>
case z
of inl(a'') =>
ss1."#or" a a' a'' sep
| inr(_) =>
inl Ax
| inr(b') =>
case z
of inl(_) =>
inr Ax
| inr(_) =>
inl Ax
| inr(b) =>
case y
of inl(a') =>
case z
of inl(_) =>
inl Ax
| inr(_) =>
inr Ax
| inr(b') =>
case z
of inl(_) =>
inl Ax
| inr(b'') =>
ss2."#or" b b' b'' sep
Lemma: union-ss_wf
∀[ss1,ss2:SeparationSpace]. (ss1 + ss2 ∈ SeparationSpace)
Definition: list-ss
list(ss) ==
Point=Point(ss) List #=λp,q. if ||p||=||q|| then ∃i:ℕ||p||. p[i] # q[i] else True
cotrans=λp,q,r,sep. if ||p||=||q||
then if ||q||=||r||
then let i,x = sep
in case ss."#or" p[i] q[i] r[i] x of inl(a) => inl <i, a> | inr(a) => inr <i, a>
else (inr Ax )
else if ||q||=||r|| then inl Ax else (inr Ax )
Lemma: list-ss_wf
∀[ss:SeparationSpace]. (list(ss) ∈ SeparationSpace)
Definition: real-ss
ℝ == Point=ℝ #=λx,y. x ≠ y cotrans=TERMOF{rneq-cotrans:o, 1:l}
Lemma: real-ss_wf
ℝ ∈ SeparationSpace
Lemma: real-ss-point
Point(ℝ) ~ ℝ
Lemma: real-ss-eq
∀[x,y:ℝ]. uiff(x ≡ y;x = y)
Definition: unit-ss
𝕀 == {x:ℝ | x ∈ [r0, r1]}
Lemma: unit-ss_wf
𝕀 ∈ SeparationSpace
Lemma: unit_ss_point_lemma
Point(𝕀) ~ {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}
Definition: interval-ss
interval-ss(I) == {x:ℝ | x ∈ I}
Lemma: interval-ss_wf
∀[I:Interval]. (interval-ss(I) ∈ SeparationSpace)
Definition: ss-fun
X ⟶ Y == {f:Point(X) ⟶ Y | ss-function(X;Y;f)}
Lemma: ss-fun_wf
∀[X,Y:SeparationSpace]. (X ⟶ Y ∈ SeparationSpace)
Lemma: ss-fun-point
∀[X,Y:Top]. (Point(X ⟶ Y) ~ {f:Point(X) ⟶ Point(Y)| ss-function(X;Y;f)} )
Lemma: ss-fun-sep
∀[X,Y,f,g:Top]. (f # g ~ ∃a:Point(X). f a # g a)
Definition: ss-ap
f(x) == f x
Lemma: ss-ap_wf
∀[X,Y:SeparationSpace]. ∀[f:Point(X ⟶ Y)]. ∀[x:Point(X)]. (f(x) ∈ Point(Y))
Lemma: ss-fun-eq
∀[X,Y:SeparationSpace]. ∀[f,g:Point(X ⟶ Y)]. uiff(f ≡ g;∀a:Point(X). f(a) ≡ g(a))
Lemma: ss-ap_functionality
∀[X,Y:SeparationSpace]. ∀[f,g:Point(X ⟶ Y)]. ∀[x,x':Point(X)]. (f(x) ≡ g(x')) supposing (x ≡ x' and f ≡ g)
Definition: ss-id
ss-id() == λx.x
Lemma: ss-id_wf
∀[X:SeparationSpace]. (ss-id() ∈ Point(X ⟶ X))
Lemma: ss_ap_id_lemma
∀x:Top. (ss-id()(x) ~ x)
Definition: ss-comp
ss-comp(f;g) == f o g
Lemma: ss-comp_wf
∀[X,Y,Z:SeparationSpace]. ∀[f:Point(Y ⟶ Z)]. ∀[g:Point(X ⟶ Y)]. (ss-comp(f;g) ∈ Point(X ⟶ Z))
Definition: ss-const
ss-const(c) == λx.c
Lemma: ss-const_wf
∀[X,Y:SeparationSpace]. ∀[c:Point(Y)]. (ss-const(c) ∈ Point(X ⟶ Y))
Definition: ss-cat
ss-cat{i:l}() == Cat(ob = SeparationSpace;arrow(X,Y) = {f:Point(X) ⟶ Point(Y)| ss-map(X;Y;f)} ;id(X) = λp.p;comp(X,Y,Z\000C,f,g) = g o f)
Lemma: ss-cat_wf
ss-cat{i:l}() ∈ SmallCategory'
Definition: full-ss-cat
full-ss-cat{i:l}() == Cat(ob = SeparationSpace;arrow(X,Y) = {f:Point(X) ⟶ Point(Y)| ss-function(X;Y;f)} ;id(X) = λp.p;\000Ccomp(X,Y,Z,f,g) = g o f)
Lemma: full-ss-cat_wf
full-ss-cat{i:l}() ∈ SmallCategory'
Definition: sg-id
1 == sg."id"
Definition: sg-inv
x^-1 == sg."inv" x
Definition: sg-op
(x y) == sg."op" x y
Definition: s-group-structure
s-GroupStructure ==
SeparationSpace
"id":Point(self)
"inv":Point(self) ⟶ Point(self)
"op":Point(self) ⟶ Point(self) ⟶ Point(self)
"opsep":∀x,x',y,y':Point(self). (self."op" x y # self."op" x' y' ⇒ (x # x' ∨ y # y'))
"invsep":∀x,y:Point(self). (self."inv" x # self."inv" y ⇒ x # y)
Lemma: s-group-structure_wf
s-GroupStructure ∈ 𝕌'
Lemma: s-group-structure_subtype1
s-GroupStructure ⊆r SeparationSpace
Lemma: sg-id_wf
∀[sg:s-GroupStructure]. (1 ∈ Point(sg))
Lemma: sg-inv_wf
∀[sg:s-GroupStructure]. ∀[x:Point(sg)]. (x^-1 ∈ Point(sg))
Lemma: sg-op_wf
∀[sg:s-GroupStructure]. ∀[x,y:Point(sg)]. ((x y) ∈ Point(sg))
Lemma: sg-inv-sep
∀sg:s-GroupStructure. ∀x1,x2:Point(sg). (x1^-1 # x2^-1 ⇒ x1 # x2)
Lemma: sg-op-sep
∀sg:s-GroupStructure. ∀x1,y1,x2,y2:Point(sg). ((x1 y1) # (x2 y2) ⇒ (x1 # x2 ∨ y1 # y2))
Lemma: sg-inv_functionality
∀[sg:s-GroupStructure]. ∀[x1,x2:Point(sg)]. x1^-1 ≡ x2^-1 supposing x1 ≡ x2
Lemma: sg-op_functionality
∀[sg:s-GroupStructure]. ∀[x1,y1,x2,y2:Point(sg)]. ((x1 y1) ≡ (x2 y2)) supposing (x1 ≡ x2 and y1 ≡ y2)
Definition: s-group-axioms
s-group-axioms(sg) ==
(∀[x,y,z:Point(sg)]. (x (y z)) ≡ ((x y) z)) ∧ (∀[x:Point(sg)]. (x 1) ≡ x) ∧ (∀[x:Point(sg)]. (x x^-1) ≡ 1)
Lemma: s-group-axioms_wf
∀[sg:s-GroupStructure]. (s-group-axioms(sg) ∈ ℙ)
Lemma: sq_stable__s-group-axioms
∀[sg:s-GroupStructure]. SqStable(s-group-axioms(sg))
Definition: s-group
This is a "fully constructive" version of the normal
algebraic concept of a group.
The difference is that the "points" (i.e. the elements) of the group
come from a SeparationSpace -- a type with a separation relation x # x'.
Then the negation ⌜¬x # x'⌝ -- which we write ⌜x ≡ x'⌝ -- is an equivalence
relation on the elements.
We could then form a quotient type ⌜x,x':Point(self)//x ≡ x'⌝ and use the
normal defintion of a group with elements from the quotient type.
But, in general, we may not be able to define the needed operations on the
quotient.
Instead, we state the "equations" (associativity, inverse, and identity) using
the equivalence realtion x ≡ x' instead of equality.
In addition, we add as axioms that the group operations
are "strongly extensional"⋅
s-Group == {sg:s-GroupStructure| s-group-axioms(sg)}
Lemma: s-group_wf
s-Group ∈ 𝕌'
Lemma: s-group_subtype1
s-Group ⊆r s-GroupStructure
Lemma: sg-assoc
∀[sg:s-Group]. ∀[x,y,z:Point(sg)]. (x (y z)) ≡ ((x y) z)
Lemma: sg-op-id
∀[sg:s-Group]. ∀[x:Point(sg)]. (x 1) ≡ x
Lemma: sg-op-inv
∀[sg:s-Group]. ∀[x:Point(sg)]. (x x^-1) ≡ 1
Lemma: sg-id-op
∀[sg:s-Group]. ∀[x:Point(sg)]. (1 x) ≡ x
Lemma: sg-inv-op
∀[sg:s-Group]. ∀[x:Point(sg)]. (x^-1 x) ≡ 1
Lemma: sg-inv-unique
∀[sg:s-Group]. ∀[x,y:Point(sg)]. x^-1 ≡ y supposing (x y) ≡ 1
Lemma: sg-inv-inv
∀[sg:s-Group]. ∀[x:Point(sg)]. x^-1^-1 ≡ x
Lemma: sg-inv-id
∀[sg:s-Group]. 1^-1 ≡ 1
Lemma: sg-inv-of-op
∀[sg:s-Group]. ∀[x,y:Point(sg)]. (x y)^-1 ≡ (y^-1 x^-1)
Definition: mk-s-group
mk-s-group(ss; e; i; o; sep; invsep) == ss["id" := e]["inv" := i]["op" := o]["opsep" := sep]["invsep" := invsep]
Lemma: mk-s-group_wf
∀[ss:SeparationSpace]. ∀[e:Point(ss)]. ∀[i:Point(ss) ⟶ Point(ss)]. ∀[o:{f:Point(ss) ⟶ Point(ss) ⟶ Point(ss)|
(∀x,y,z:Point(ss). f x (f y z) ≡ f (f x y) z)
∧ (∀x:Point(ss). f x e ≡ x)
∧ (∀x:Point(ss). f x (i x) ≡ e)} ].
∀[sep:∀x,x',y,y':Point(ss). (o x y # o x' y' ⇒ (x # x' ∨ y # y'))]. ∀[invsep:∀x,y:Point(ss). (i x # i y ⇒ x # y)].
(mk-s-group(ss; e; i; o; sep; invsep) ∈ s-Group)
Definition: sg-subgroup
sg-subgroup(sg;x.P[x]) == P[1] ∧ (∀x:Point(sg). (P[x] ⇒ P[x^-1])) ∧ (∀x,y:Point(sg). (P[x] ⇒ P[y] ⇒ P[(x y)]))
Lemma: sg-subgroup_wf
∀[sg:s-Group]. ∀[P:Point(sg) ⟶ ℙ]. (sg-subgroup(sg;x.P[x]) ∈ ℙ)
Definition: mk-s-subgroup
mk-s-subgroup(sg;x.P[x]) == mk-s-group({x:sg | P[x]}; 1; λx.x^-1; λx,y. (x y); sg."opsep"; sg."invsep")
Lemma: mk-s-subgroup_wf
∀[sg:s-Group]. ∀[P:Point(sg) ⟶ ℙ]. mk-s-subgroup(sg;x.P[x]) ∈ s-Group supposing sg-subgroup(sg;x.P[x])
Definition: permutation-ss
permutation-ss(ss) ==
{fg:Point(ss) ⟶ ss × Point(ss) ⟶ ss | let f,g = fg
in (∀x:Point(ss). f (g x) ≡ x)
∧ (∀x:Point(ss). g (f x) ≡ x)
∧ (∀x,y:Point(ss). (f x # f y ⇒ x # y))
∧ (∀x,y:Point(ss). (g x # g y ⇒ x # y))}
Lemma: permutation-ss_wf
∀[ss:SeparationSpace]. (permutation-ss(ss) ∈ SeparationSpace)
Lemma: permutation-ss-point
∀[rv:Top]
(Point(permutation-ss(rv)) ~ {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))|
let f,g = fg
in (∀x:Point(rv). f (g x) ≡ x)
∧ (∀x:Point(rv). g (f x) ≡ x)
∧ (∀x,y:Point(rv). (f x # f y ⇒ x # y))
∧ (∀x,y:Point(rv). (g x # g y ⇒ x # y))} )
Lemma: permutation-ss-sep
∀[rv,f,g,f',g':Top]. (<f, g> # <f', g'> ~ fun-sep(rv;Point(rv);f;f') ∨ fun-sep(rv;Point(rv);g;g'))
Lemma: permutation-ss-eq
∀[rv,f,g,f',g':Top]. (<f, g> ≡ <f', g'> ~ ¬(fun-sep(rv;Point(rv);f;f') ∨ fun-sep(rv;Point(rv);g;g')))
Lemma: permutation-ss-eq-iff
∀[rv:SeparationSpace]. ∀[f,g,f',g':Point(rv) ⟶ Point(rv)].
uiff(<f, g> ≡ <f', g'>;(∀x:Point(rv). f x ≡ f' x) ∧ (∀x:Point(rv). g x ≡ g' x))
Lemma: permutation-s-group-sep-or
∀rv:SeparationSpace. ∀sepw:x:Point(rv) ⟶ y:{y:Point(rv)| x # y} ⟶ x # y. ∀x,x',y,y':Point(permutation-ss(rv)).
(let f,g = x
in let f',g' = y
in <f o f', g' o g> # let f,g = x'
in let f',g' = y'
in <f o f', g' o g>
⇒ (x # x' ∨ y # y'))
Definition: permutation-s-group
Perm(rv) ==
mk-s-group(permutation-ss(rv);
<λx.x, λx.x>;
λfg.let f,g = fg
in <g, f>;
λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g>;
TERMOF{permutation-s-group-sep-or:o, 1:l, 1:l} rv sepw;
λx,y,d. case d of inl(asep) => inr asep | inr(asep) => inl asep)
Lemma: permutation-s-group_wf
∀[rv:SeparationSpace]. ∀[sepw:∀x:Point(rv). ∀y:{y:Point(rv)| x # y} . x # y]. (Perm(rv) ∈ s-Group)
Definition: generated-s-subgroup
generated-s-subgroup(sg;f.P[f]) == mk-s-subgroup(sg;g.∃L:Point(sg) List. ((∀f∈L.P[f]) ∧ g ≡ reduce(λx,y. (x y);1;L)))
Lemma: generated-s-subgroup_wf
∀[sg:s-Group]. ∀[P:Point(sg) ⟶ ℙ]. generated-s-subgroup(sg;f.P[f]) ∈ s-Group supposing ∀f:Point(sg). (P[f] ⇒ P[f^-1])
Definition: sg-action
sg-action(g;n) ==
{a:Point(g) ⟶ Point(n) ⟶ Point(n)|
(∀x:Point(n). ∀f,h:Point(g). a f (a h x) ≡ a (f h) x) ∧ (∀x:Point(n). a 1 x ≡ x)}
Lemma: sg-action_wf
∀[g:s-Group]. ∀[n:SeparationSpace]. (sg-action(g;n) ∈ Type)
Definition: ap-action
h(x) == a h x
Lemma: ap-action_wf
∀[g:s-Group]. ∀[n:SeparationSpace]. ∀[a:sg-action(g;n)]. ∀[h:Point(g)]. ∀[x:Point(n)]. (h(x) ∈ Point(n))
Lemma: ap-action-1
∀[g:s-Group]. ∀[n:SeparationSpace]. ∀[a:sg-action(g;n)]. ∀[x:Point(n)]. 1(x) ≡ x
Lemma: ap-action-op
∀[g:s-Group]. ∀[n:SeparationSpace]. ∀[a:sg-action(g;n)]. ∀[f,h:Point(g)]. ∀[x:Point(n)]. f(h(x)) ≡ (f h)(x)
Home
Index