```-- File: axiomatizing

-- In this file we postulate only the axiom of choice and the existence of
-- quotient and subset types, and show how to prove the existence of quotient
-- and subset algebras from these axioms.
-- This file is divided into three parts.
-- 1. The axiom of choice and the axioms stating the existence of quotient
--    and subset types. This corresponds to definition 6.8.1.3 on page 194.
--    We also show that the existence of QuotSubset types follows from the
--    last two axioms.
-- 2. We prove the existence of quotient and subset algebras for all
--    simply-typed interfaces (including higher-order ones). This corresponds
--    to Conjectures 6.8.2.1, 6.8.2.2 and 6.8.2.6
-- 3. We prove the existence of quotient and subset algebras for first-order
--    interfaces. This does not follow directly from part 2, since the
--    theorems that state the existence are formulated quite differently.
--    This corresponds to Theorem 6.8.1.4.

Path "../lol"
Path "../lolExtra"

----------------------
----------------------
--                  --
--  1. A X I O M S  --
--                  --
----------------------
----------------------

Var axiom_choice :  @A,B:*s.@P:A->B->*p.
(@x:A.Ex y:B. P x y) ->
Ex f:A->B. @x:A. P x (f x)

Def IsQuotType := \R:*s. \(~~):R->R->*p. \Q:*s.
Ex surj:R->Q.
(@r,r':R. r ~~ r' <=> surj r = surj r') /\
IsSurjection surj :
@R:*s. (R->R->*p) -> *s -> *p

Var exis_QuotType : @R:*s. @(~~):R->R->*p. IsER (~~) ->
ExK Q:*s.
IsQuotType R (~~) Q

Def IsSubsetType := \R:*s. \Inv:R->*p. \S:*s.
Ex inj:S->R.
IsInjection inj /\
(Inv <==> Image inj) :
@R:*s. (R->*p) -> *s -> *p

Var exis_SubsetType : @R:*s. @Inv:R->*p.
ExK S:*s.
IsSubsetType R Inv S

Def IsQuotSubsetType := \R:*s. \(~~):R->R->*p. \Inv:R->*p. \Q:*s.
ExR rel:R->Q->*p.
(Inv <==> Dom rel) /\
(@q:Q. Ex r:R. rel r q) /\
(@r,r':R. @q,q':Q. rel r q -> rel r' q' ->
r~~r' <=> q=q') :
@R:*s. (R->R->*p) -> (R->*p) -> *s -> *p

Prove exis_QuotSubsetType : @R:*s. @(~~):R->R->*p. @Inv:R->*p.
IsERon (~~) Inv ->
ExK Q:*s.
IsQuotSubsetType R (~~) Inv Q

----------------------------------------------------
----------------------------------------------------
--                                                --
--  2. H I G H E R - O R D E R   A L G E B R A S  --
--                                                --
----------------------------------------------------
----------------------------------------------------

-- auxialary result
Prove has_elem : @I:*s->*s. SimplyT I ->
@R : *s. @S : *s.
(Ex r:R. True) ->
(Ex s:S. True) ->
(Ex r:I R. True) ->
(Ex s:I S. True)

-- induction-step for Sim_LeftC for the case I = I1 -> I2
prove Sim_lemma :
@I1,I2 : *s->*s. SimplyT I1 -> SimplyT I2 ->
@Y,Z : *s. (Ex r:Y. True) -> (Ex s:Z. True) ->
@(~) : Y->Z->*p.
IsZclosed (Sim I2 Y Z (~)) ->
LeftC (Sim I1 Y Z (~)) <===> Sim I1 Y Y (LeftC (~)) ->
LeftC (Sim I2 Y Z (~)) <===> Sim I2 Y Y (LeftC (~)) ->
LeftC (Sim (\X:*s. I1 X -> I2 X) Y Z (~)) <===>
Sim (\X:*s. I1 X -> I2 X) Y Y (LeftC (~))

Prove Sim_LeftC :
@I:*s->*s. SimplyT I ->
@Y : *s.
@Z : *s.
(Ex r:Y.True) ->
(Ex s:Z.True) ->
@(~) : Y->Z->*p.
IsZclosed (~) ->
(Sim I Y Y (LeftC (~)) <===> LeftC (Sim I Y Z (~)))

-- simple corollary of Sim_LeftC
prove Sim_LeftC_weak : @I:*s->*s. SimplyT I ->
@Y : *s.
@Z : *s.
(Ex r:Y.True) ->
(Ex s:Z.True) ->
@(~) : Y->Z->*p.
IsZclosed (~) ->
@opsY : I Y. Bisim I Y (LeftC (~)) opsY ->
Ex opsZ : I Z. Sim I Y Z (~) opsY opsZ

-- Now we are ready to consider quotient/subset algebras.

Def IsQuotAlg := \I:*s->*s.
\R:*s. \opsR : I R. \(~~):R->R->*p. \Q:*s. \opsQ : I Q.
Ex surj:R->Q.
(@r,r':R. r ~~ r' <=> surj r = surj r') /\
IsSurjection surj /\
Sim I R Q (\r:R.\q:Q. q = surj r) opsR opsQ  :
@I:*s->*s.@R:*s. I R -> (R->R->*p) -> @Q:*s. I Q -> *p
LatexVar 1 IsQuotAlg

Def IsSubsetAlg := \I:*s->*s.\R:*s. \opsR : I R. \Inv:R->*p. \S:*s.\opsS : I S.
Ex inj:S->R.
IsInjection inj /\
(Inv <==> Image inj) /\
Sim I R S (\r:R.\s:S. r = inj s) opsR opsS  :
@I:*s->*s. @R:*s. I R -> (R->*p) -> @S:*s. I S -> *p
LatexVar 1 IsSubsetAlg

Def IsQuotSubsetAlg := \I:*s->*s.
\R:*s. \opsR : I R. \(~~) : R->R->*p. \Inv:R->*p.
\Q:*s. \opsQ : I Q.
ExR rel:R->Q->*p.
(Inv <==> Dom rel) /\
(@q:Q. Ex r:R. rel r q) /\
(@r,r':R. @q,q':Q. rel r q -> rel r' q' ->
r~~r' <=> q=q') /\
Sim I R Q rel opsR opsQ :
@I:*s->*s.@R:*s. I R -> (R->R->*p) -> (R->*p) -> @Q:*s. I Q -> *p
LatexVar 1 IsQuotSubsetAlg

Prove exis_QuotSubsetAlgHO : @I:*s->*s. SimplyT I ->
@R:*s. @opsR:I R. @(~~):R->R->*p. @Inv:R->*p.
IsERon (~~) Inv ->
(Ex r:R. Inv r) ->
Bisim I R (Restr (~~) Inv) opsR ->
ExK Q:*s. Ex opsQ: I Q.
IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ

Prove exis_QuotAlgHO : @I:*s->*s. SimplyT I ->
@R:*s. @opsR:I R. @(~~):R->R->*p.
Bisim I R (~~) opsR -> IsER (~~) ->
ExK Q:*s. Ex opsQ: I Q.
IsQuotAlg I R opsR (~~) Q opsQ

Prove exis_SubsetAlgHO : @I:*s->*s. SimplyT I ->
@R:*s. @opsR:I R. @Inv:R->*p. (Ex r:R. Inv r) ->
Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR ->
ExK S:*s. Ex opsS: I S.
IsSubsetAlg I R opsR Inv S opsS

--------------------------------------------------
--------------------------------------------------
--                                              --
--  3. F I R S T - O R D E R   A L G E B R A S  --
--                                              --
--------------------------------------------------
--------------------------------------------------

-- We first consider quotients, then subsets, and then quotients of subsets.

---------------
-- QUOTIENTS --
---------------

Prove exis_QuotAlg :@I:*s->*s. FirstO I ->
@R:*s. @opsR:I R. @(~~):R->R->*p.
Bisim I R (~~) opsR -> IsER (~~) ->
ExK Q:*s. Ex opsQ: I Q.
IsQuotAlg I R opsR (~~) Q opsQ

-------------
-- SUBSETS --
-------------

-- Now first-order subset algebras. We do this in two steps.
-- First we prove exis_SubsetAlg_Bisim, i.e.
--                  @I:*s->*s. FirstO I ->
--                  @R:*s. @Inv:R->*p.  @opsR:I R.
--                  Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR ->
--                  ExK S:*s. Ex opsS: I S.
--                  IsSubsetAlg I R opsR Inv S opsS
-- This requires three auxiliary results.
-- Then it is easy to prove exis_SubsetAlg.

-- Auxiliary result 1: Sim_LeftC for Basic interfaces, but with possibly
-- empty types.
prove Sim_Basic_LeftC_strong : @I:*s->*s. Basic I ->
@Y : *s.
@Z : *s.
@(~) : Y->Z->*p.
IsZclosed (~) ->
Sim I Y Y (LeftC (~)) <===> LeftC (Sim I Y Z (~))

-- Auxiliary result 2
prove Sim_FirstO_LeftC_weak_lemma : @I:*s->*s. Basic I ->
@Y : *s.
@Z : *s.
@(~) : Y->Z->*p.
(@z:Z. Ex y:Y. y~z) ->
(@opsZ:I Z. Ex opsY:I Y. Sim I Y Z (~) opsY opsZ )

-- Auxiliary result 3
prove Sim_FirstO_LeftC_weak : @I:*s->*s. FirstO I ->
@Y : *s.
@Z : *s.
@(~) : Y->Z->*p.
IsZclosed (~) -> (@z:Z. Ex y:Y. y~z) ->
@opsY,opsY':I Y. Sim I Y Y (LeftC (~)) opsY opsY' ->
LeftC (Sim I Y Z (~)) opsY opsY'

-- The next result is equal to exis_SubsetAlg, except that it has
--    Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR
--    IsInvar I R Inv opsR
Prove exis_SubsetAlg_Bisim : @I:*s->*s. FirstO I ->
@R:*s. @Inv:R->*p.  @opsR:I R.
Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR ->
ExK S:*s. Ex opsS: I S.
IsSubsetAlg I R opsR Inv S opsS

Prove exis_SubsetAlg :
@I:*s->*s. FirstO I ->
@R:*s. @opsR:I R. @Inv:R->*p.
IsInvar I R Inv opsR ->
ExK S:*s. Ex opsS: I S.
IsSubsetAlg I R opsR Inv S opsS

--------------------------
-- QUOTIENTS OF SUBSETS --
--------------------------

-- By combining exis_QuotAlg and exis_SubsetAlg
prove exis_QuotSubsetAlg : @I:*s->*s. FirstO I ->
@R:*s. @opsR:I R. @(~~):R->R->*p. @Inv:R->*p.
IsERon (~~) Inv ->
Bisim I R (~~) opsR ->
IsInvar I R Inv opsR ->
ExK Q:*s. Ex opsQ: I Q.
IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ

```