%sig Base = {
  o     : type.
  ded   : o -> type. 
}.

%sig Truth = {
  %struct base     : Base   %open o.
  true  : o.
}.

%sig Falsity = {
  %struct base     : Base   %open o.
  false : o.
}.

%sig NEG = {
  %struct base     : Base   %open o.
  not   : o -> o.
}.

%sig IMP = {
  %struct base     : Base   %open o.
  imp   : o -> o -> o.        %infix none 15 imp.
}.

%sig CONJ = {
  %struct base     : Base   %open o.
  and   : o -> o -> o.        %infix none 10 and.
}.

%sig DISJ = {
  %struct base     : Base   %open o.
  or   : o -> o -> o.         %infix none 10 or.
}.

%sig PL = {
  %struct base     : Base.
  %struct truth    : Truth   = {%struct base := base.}.
  %struct falsity  : Falsity = {%struct base := base.}.
  %struct neg      : NEG     = {%struct base := base.}.
  %struct impl     : IMP     = {%struct base := base.}.
  %struct conj     : CONJ    = {%struct base := base.}.
  %struct disj     : DISJ    = {%struct base := base.}.
}. 

%sig BasePF = {
 %struct base      : Base.
}.

%sig TruthPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct truth    : Truth    = {%struct base := basepf.base.}  %open true.
  trueI  : ded true.
}.

%sig FalsityPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct falsity  : Falsity  = {%struct base := basepf.base.}  %open false.
  falseE : ded false -> {A} ded A.
}.

%sig NEGPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct neg      : NEG      = {%struct base := basepf.base.}  %open not.
  notI   : (ded A -> {B} ded B) -> ded (not A).
  notE   : ded A -> ded (not A) -> {B} ded B.
}.

%sig IMPPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct impl     : IMP      = {%struct base := basepf.base.}  %open imp.
  impI   : (ded A -> ded B) -> ded (A imp B).
  impE   : ded (A imp B) -> ded A -> ded B.
}.

%sig CONJPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct conj     : CONJ      = {%struct base := basepf.base.}  %open and.
  andI   : ded A -> ded B -> ded (A and B).
  andEl  : ded (A and B) -> ded A.
  andEr  : ded (A and B) -> ded B.
}.

%sig DISJPF = {
  %struct basepf   : BasePF %open base.ded.
  %struct disj     : DISJ      = {%struct base := basepf.base.}  %open or.
  orIl    : ded A -> ded (A or B).
  orIr    : ded B -> ded (A or B).
  orE     : ded (A or B) -> (ded A -> ded C) -> (ded B -> ded C) -> ded C.
}.

%sig IPLPF = {
  %struct basepf    : BasePF.
  %struct truthpf   : TruthPF = {%struct basepf := basepf.}.
  %struct falsitypf : FalsityPF = {%struct basepf := basepf.}.
  %struct negpf     : NEGPF = {%struct basepf := basepf.}.
  %struct imppf     : IMPPF = {%struct basepf := basepf.}.
  %struct conjpf    : CONJPF = {%struct basepf := basepf.}.
  %struct disjpf    : DISJPF = {%struct basepf := basepf.}.
}.

%sig TND = {  
  %struct basepf : BasePF %open base.ded.
  %struct neg  : NEG = {%struct base := basepf.base.} %open not.
  %struct disj : DISJ = {%struct base := basepf.base.} %open or. 
  tnd    : ded (A or (not A)).
}.

%sig CPLPF = {
  %struct iplpf : IPLPF.
  %struct tnd : TND = {%struct basepf := iplpf.basepf. %struct neg := iplpf.negpf.neg. %struct disj := iplpf.disjpf.disj.}.
}.

%sig BaseMOD = {
  %include MLTT %open tm tp - == ==' + subsType @.
  o'    : tp.
  ded'  : tm o' -> tp.
  %struct base : Base = {o := tm o'. ded := [a] tm (ded' a).} %open o ded.
  1 : o.
  0 : o.
  desig0 : - (ded' 0).
  desig1 : ded 1.
  boole  : {A} (A ==' 1 + A ==' 0).
  ded-1  : ded A -> A == 1
         = [p] (MLTT..D.case (boole A)
                     ([q : A == 1] q)
                     ([q : A == 0] (MLTT..!! (desig0 @ (MLTT..I.eq (subsType q ded') p))))
                 ).
  1-ded : A == 1 -> ded A
           = [p] (MLTT..I.eq (MLTT..TT.sym (subsType p ded')) desig1).
  cons  : - (0 ==' 1)
        = MLTT..lam [p : 0 == 1] (desig0 @ (MLTT..I.eq (MLTT..TT.sym (subsType p ded')) desig1)).
  contra : A == 0 -> A == 1 -> MLTT..void
         = [p][q] (cons @ (MLTT..I.trans (MLTT..I.sym p) q)).
  indirect : (A == 0 -> MLTT..void) -> A == 1
           = [f] MLTT..case (boole A)
               ([p : A == 1] p)
               ([p : A == 0] MLTT..!! (f p)).
}.

%sig TruthMOD = {
  %include MLTT %open ==.
  %struct basemod : BaseMOD %open 1.
  %struct truth : Truth = {%struct base := basemod.base.} %open true. 
  true1 : true == 1.
}.

%sig FalsityMOD = {
  %include MLTT %open ==.
  %struct basemod : BaseMOD %open 0.
  %struct falsity : Falsity = {%struct base := basemod.base.} %open false. 
  false0 : false == 0.
}.

%sig NEGMOD = {
  %include MLTT %open ==.
  %struct basemod : BaseMOD %open 1 0.
  %struct neg : NEG = {%struct base := basemod.base.} %open not. 
  not1 : A == 0 -> (not A) == 1.
  not0 : A == 1 -> (not A) == 0.
}.

%sig IMPMOD = {
  %include MLTT %open == ==' + *.
  %struct basemod : BaseMOD %open 1 0.
  %struct impl : IMP = {%struct base := basemod.base.} %open imp. 
  imp1 : A ==' 0 + B ==' 1 -> (A imp B) == 1.
  imp0 : A ==' 1 * B ==' 0 -> (A imp B) == 0.
}.


%sig CONJMOD = {
  %include MLTT %open == ==' + *.
  %struct basemod : BaseMOD %open 1 0.
  %struct conj : CONJ = {%struct base := basemod.base.} %open and.
  and1 : A ==' 1 * B ==' 1 -> (A and B) == 1. 
  and0 : A ==' 0 + B ==' 0 -> (A and B) == 0.
}.

%sig DISJMOD = {
  %include MLTT %open == ==' + *.
  %struct basemod : BaseMOD %open 1 0 ded.
  %struct disj : DISJ = {%struct base := basemod.base.} %open or.
  or1 : A ==' 1 + B ==' 1 -> (A or B) == 1. 
  or0 : A ==' 0 * B ==' 0 -> (A or B) == 0.
}.

%sig PLMOD = {
  %include MLTT.
  %struct basemod    : BaseMOD.
  %struct truthmod   : TruthMOD = {%struct basemod := basemod.}.
  %struct falsitymod : FalsityMOD = {%struct basemod := basemod.}.
  %struct negmod     : NEGMOD = {%struct basemod := basemod.}.
  %struct impmod     : IMPMOD = {%struct basemod := basemod.}.
  %struct conjmod    : CONJMOD = {%struct basemod := basemod.}.
  %struct disjmod    : DISJMOD = {%struct basemod := basemod.}.
}.

%view SoundBase : BasePF -> BaseMOD = {
  %struct base := base.
}.

%view SoundTruth : TruthPF -> TruthMOD = {
  %struct basepf := SoundBase TruthMOD..basemod.
  %struct truth := truth.
  trueI := basemod.1-ded true1.
}.

%view SoundFalsity : FalsityPF -> FalsityMOD = {
  %struct basepf := SoundBase FalsityMOD..basemod.
  %struct falsity := falsity.
  falseE := [p : basemod.base.ded false][A] (MLTT..!! (basemod.contra false0 (basemod.ded-1 p))).
}.

%view SoundIMP : IMPPF -> IMPMOD  = {
  %struct basepf := SoundBase IMPMOD..basemod.
  %struct impl := impl.
  impI := [A][B][p: basemod.base.ded A -> basemod.base.ded B] (
             basemod.1-ded (imp1 
               (MLTT..case (basemod.boole A)
                  ([q : A == 1] MLTT..inj2 (basemod.ded-1 (p (basemod.1-ded q))))
                  ([q : A == 0] MLTT..inj1 q)
               )
             )
          ).
  impE := [A][B][p : basemod.base.ded (A imp B)][q : basemod.base.ded A] (
             basemod.1-ded (
                MLTT..D.case (basemod.boole B)
                   ([r : B == 1] r)
                   ([r : B == 0] MLTT..!! (basemod.contra (imp0 (MLTT..pair (basemod.ded-1 q) r)) (basemod.ded-1 p)))
             )
          ).
}.

%view SoundNEG : NEGPF -> NEGMOD  = {
  %struct basepf := SoundBase NEGMOD..basemod.
  %struct neg := neg.
  notI := [A][p : basemod.base.ded A -> {B} basemod.base.ded B] (
             MLTT..D.case (basemod.boole A)
                ([q : A == 1] p (basemod.1-ded q) (not A))
                ([q : A == 0] basemod.1-ded (not1 q))
          ).
  notE := [A] ([p : basemod.base.ded A] [q : basemod.base.ded (not A)] [B] MLTT..!! (basemod.contra (not0 (basemod.ded-1 p)) (basemod.ded-1 q))).
}.


%view SoundCONJ : CONJPF -> CONJMOD = {
  %struct basepf := SoundBase CONJMOD..basemod.
  %struct conj := conj.
  andI := [A][B][p : basemod.base.ded A] [q : basemod.base.ded B] (
            basemod.1-ded (and1 (basemod.ded-1 p MLTT.., basemod.ded-1 q))).
  andEl := [A][B][p : basemod.base.ded (A and B)] (
              basemod.1-ded (basemod.indirect [q : A == 0]
                (basemod.contra (and0 (MLTT..inj1 q)) (basemod.ded-1 p))
              )
           ).
   andEr := [A][B][p : basemod.base.ded (A and B)] (
              basemod.1-ded (basemod.indirect [q : B == 0]
                (basemod.contra (and0 (MLTT..inj2 q)) (basemod.ded-1 p))
              )
           ).
}.

%view SoundDISJ : DISJPF -> DISJMOD = {
  %struct basepf := SoundBase DISJMOD..basemod.
  %struct disj := disj.
  orIl := [A][B][p : ded A] (basemod.1-ded (or1 (MLTT..inj1 (basemod.ded-1 p)))).
  orIr := [B][A][p : ded B] (basemod.1-ded (or1 (MLTT..inj2 (basemod.ded-1 p)))).
  orE  := [A][B][C][p : ded (A or B)] [q : ded A -> ded C][r : ded B -> ded C] (
            MLTT..case (basemod.boole A) 
              ([s : A == 1] q (basemod.1-ded s))
              ([s : A == 0] MLTT..case (basemod.boole B)
                                ([t : B == 1] r (basemod.1-ded t))
                                ([t : B == 0] MLTT..!! (basemod.contra 
                                                          (or0 (s MLTT.., t)) 
                                                          (basemod.ded-1 p)
                                                       )
                                )
              )
          ).   
}.


%view SoundTND : TND -> PLMOD = {  
 %struct basepf := SoundBase PLMOD..basemod.
 %struct neg    := negmod.neg.
 %struct disj   := disjmod.disj.
 
  tnd := [A] basemod.1-ded (MLTT..case (basemod.boole A)
                    ([p : A MLTT..== basemod.1] disjmod.or1 (MLTT..inj1 p))
                    ([p : A MLTT..== basemod.0] disjmod.or1 (MLTT..inj2 (negmod.not1 p)))
         ).
}.

%view SoundCPL : CPLPF -> PLMOD = {
  %struct iplpf.basepf := SoundBase PLMOD..basemod.
  %struct iplpf.truthpf := SoundTruth PLMOD..truthmod.
  %struct iplpf.falsitypf := SoundFalsity PLMOD..falsitymod.
  %struct iplpf.negpf := SoundNEG PLMOD..negmod.
  %struct iplpf.imppf := SoundIMP PLMOD..impmod.
  %struct iplpf.conjpf := SoundCONJ PLMOD..conjmod.
  %struct iplpf.disjpf := SoundDISJ PLMOD..disjmod.
  %struct tnd := SoundTND.
}.