In "fully constructive" versions of the normal algebraic structures 
the "points" (i.e. the elements) come from SeparationSpace -- type with separation relation y.
Then the negation ⌜¬y⌝ -- which we write ⌜x ≡ y⌝ -- is an equivalence
relation on the elements. 
We could then form 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

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 y)  (∀z:T. ((sep z) ∨ (sep z))))) ∧ (∀x,y:T.  (x y ∈ ⇐⇒ ¬(sep 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 ==
  "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (s x))} 
  "#or":∀x,y,z:self."Point".  ((self."#" y)  ((self."#" z) ∨ (self."#" 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
==  ss."#" y

Lemma: ss-sep_wf
[ss:SeparationSpace]. ∀[x,y:Point(ss)].  (x y ∈ ℙ)

Lemma: ss-sep-irrefl
[ss:SeparationSpace]. ∀[x:Point(ss)].  x)

Lemma: ss-sep-or
ss:SeparationSpace. ∀x,y,z:Point(ss).  (x  (x z ∨ z))

Lemma: ss-sep-symmetry
ss:SeparationSpace. ∀x,y:Point(ss).  (x  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))} ]. ∀[C:∀x,y,z:P.  ((Sep y)  ((Sep z) ∨ (Sep z)))].
  (Point=P #=Sep cotrans=C ∈ SeparationSpace)

Definition: ss-map
ss-map(X;Y;f) ==  ∀x,x':Point(X).  (f x'  x')

Lemma: ss-map_wf
[X,Y:SeparationSpace]. ∀[f:Point(X) ⟶ Point(Y)].  (ss-map(X;Y;f) ∈ ℙ)

Definition: ss-eq
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 ≡ x)

Lemma: ss-eq_transitivity
ss:SeparationSpace. ∀x,y,z:Point(ss).  (x ≡  y ≡  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 ⇐⇒ x' y'})

Lemma: ss-eq_test
ss:SeparationSpace. ∀x,y,z,w:Point(ss).  (y ≡  y ≡  w ≡  x ≡ w)

Lemma: ss-sep_test
ss:SeparationSpace. ∀x,y,z,w,a:Point(ss).  (y ≡  y ≡  w ≡   a)

Definition: ss-function
ss-function(X;Y;f) ==  ∀x,x':Point(X).  (x ≡ x'  x ≡ 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. 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 ~ ∃a:A. a)

Lemma: fun-ss-eq
[ss:SeparationSpace]. ∀[A:Type]. ∀[f,g:A ⟶ Point(ss)].  uiff(f ≡ g;∀a:A. a ≡ 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)) 
                                                                                           of inl(u) =>
                                                                                           inl inl u
                                                                                           inr(u) =>
                                                                                           inr (inl u) 
                                                                                          inr(b) =>
                                                                                          case ss2."#or" (snd(x)) 
                                                                                           of inl(u) =>
                                                                                           inl (inr )
                                                                                           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 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. 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)

Lemma: set-ss-eq
[ss,P,x,y:Top].  (x ≡ x ≡ y)

Definition: union-sep
union-sep(ss1;ss2;p;q) ==
  case p
   of inl(a) =>
   case of inl(a') => a' inr(b') => True
   inr(b) =>
   case of inl(a') => True inr(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'' 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'' 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] 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 ≠ 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 ⟶ ==  {f:Point(X) ⟶ 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 ~ ∃a:Point(X). a)

Definition: ss-ap
f(x) ==  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) ==  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) 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) f)

Lemma: full-ss-cat_wf
full-ss-cat{i:l}() ∈ SmallCategory'

Definition: sg-id
==  sg."id"

Definition: sg-inv
x^-1 ==  sg."inv" x

Definition: sg-op
(x y) ==  sg."op" y

Definition: s-group-structure
s-GroupStructure ==
  "inv":Point(self) ⟶ Point(self)
  "op":Point(self) ⟶ Point(self) ⟶ Point(self)
  "opsep":∀x,x',y,y':Point(self).  (self."op" self."op" x' y'  (x x' ∨ y'))
  "invsep":∀x,y:Point(self).  (self."inv" self."inv"  y)

Lemma: s-group-structure_wf
s-GroupStructure ∈ 𝕌'

Lemma: s-group-structure_subtype1
s-GroupStructure ⊆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 "fully constructive" version of the normal 
algebraic concept of group. 
The difference is that the "points" (i.e. the elements) of the group
come from SeparationSpace -- type with separation relation x'.
Then the negation ⌜¬x'⌝ -- which we write ⌜x ≡ x'⌝ -- is an equivalence
relation on the elements. 
We could then form quotient type ⌜x,x':Point(self)//x ≡ x'⌝ and use the 
normal defintion of group with elements from the quotient type.
But, in general, we may not be able to define the needed operations on the

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 ⊆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 ≡ 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 z) ≡ (f y) z)
                                                                         ∧ (∀x:Point(ss). e ≡ x)
                                                                         ∧ (∀x:Point(ss). (i x) ≡ e)} ].
[sep:∀x,x',y,y':Point(ss).  (o x' y'  (x x' ∨ y'))]. ∀[invsep:∀x,y:Point(ss).  (i  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). (g x) ≡ x)
                                             ∧ (∀x:Point(ss). (f x) ≡ x)
                                             ∧ (∀x,y:Point(ss).  (f  y))
                                             ∧ (∀x,y:Point(ss).  (g  y))}

Lemma: permutation-ss_wf
[ss:SeparationSpace]. (permutation-ss(ss) ∈ SeparationSpace)

Lemma: permutation-ss-point
  (Point(permutation-ss(rv)) {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| 
                                let f,g fg 
                                in (∀x:Point(rv). (g x) ≡ x)
                                   ∧ (∀x:Point(rv). (f x) ≡ x)
                                   ∧ (∀x,y:Point(rv).  (f  y))
                                   ∧ (∀x,y:Point(rv).  (g  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). x ≡ f' x) ∧ (∀x:Point(rv). x ≡ g' x))

Lemma: permutation-s-group-sep-or
rv:SeparationSpace. ∀sepw:x:Point(rv) ⟶ y:{y:Point(rv)| y}  ⟶ y. ∀x,x',y,y':Point(permutation-ss(rv)).
  (let f,g 
   in let f',g' 
      in <f', g' g> let f,g x' 
                            in let f',g' y' 
                               in <f', g' g>
   (x x' ∨ y'))

Definition: permutation-s-group
Perm(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', g' g>;
             TERMOF{permutation-s-group-sep-or:o, 1:l, 1:l} rv sepw;
             λx,y,d. case of inl(asep) => inr asep  inr(asep) => inl asep)

Lemma: permutation-s-group_wf
[rv:SeparationSpace]. ∀[sepw:∀x:Point(rv). ∀y:{y:Point(rv)| y} .  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 x) ≡ (f h) x) ∧ (∀x:Point(n). x ≡ x)} 

Lemma: sg-action_wf
[g:s-Group]. ∀[n:SeparationSpace].  (sg-action(g;n) ∈ Type)

Definition: ap-action
h(x) ==  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