agda/examples/outdated-and-incorrect/OTT/ObsEq.agda

module ObsEq where

data Zero : Set where

record One : Set where

data Two : Set where
  tt : Two
  ff : Two

Π : (S : Set)(T : S -> Set) -> Set
Π S T = (x : S) -> T x

record Σ (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Σ S T
s , t = record {fst = s; snd = t}

open module Σ' {S : Set}{T : S -> Set} = Σ {S} {T}

data W (S : Set)(T : S -> Set) : Set where
  _<|_ : (s : S) -> (T s -> W S T) -> W S T


mutual

  data ∗ : Set where
    /0/ : ∗
    /1/ : ∗
    /2/ : ∗
    /Π/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /Σ/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /W/ : (S : ∗)(T : [ S ] -> ∗) -> ∗

  [_] : ∗ -> Set
  [ /0/ ]      = Zero
  [ /1/ ]      = One
  [ /2/ ]      = Two
  [ /Π/ S T ]  = Π [ S ] \s -> [ T s ]
  [ /Σ/ S T ]  = Σ [ S ] \s -> [ T s ]
  [ /W/ S T ]  = W [ S ] \s -> [ T s ]

infixr 40 _⟶_

_⟶_ : ∗ -> ∗ -> ∗
S ⟶ T = /Π/ S \_ -> T

{-
_Ψ_ : Zero -> (S : ∗) -> [ S ]
() Ψ S   -- magic as there's no such thing
-}

_Ψ : Zero -> {S : Set} -> S
() Ψ

Case : Two -> ∗ -> ∗ -> ∗
Case tt St Sf = St
Case ff St Sf = Sf

case : (P : Two -> ∗)(b : Two) -> [ P tt ] -> [ P ff ] -> [ P b ]
case P tt ptt pff = ptt
case P ff ptt pff = pff

rec : {S : Set}{T : S -> Set}(P : W S T -> ∗)(x : W S T) ->
      ((s : S)(f : T s -> W S T) ->
       ((t : T s) -> [ P (f t) ]) -> [ P (s <| f) ]) ->
      [ P x ]
rec P (s <| f) p = p s f \t -> rec P (f t) p


/Nat/ : ∗
/Nat/ = /W/ /2/ \b -> Case b /0/ /1/

zero : [ /Nat/ ]
zero = tt <| \z -> z Ψ

suc : [ /Nat/ ⟶ /Nat/ ]
suc n = ff <| \_ -> n

{-
elimNatSet : (P : [ /Nat/ ] -> Set) ->
          P zero ->
          ((k : [ /Nat/ ]) -> P k -> P (suc k)) ->
          (n : [ /Nat/ ]) -> P n
elimNatSet P pz ps (tt <| g) = {! !}
elimNatSet P pz ps (ff <| g) = {! !}
-}

infixr 60 _∧_

data † : Set where
  ⊥   : †
  TT  : †
  _∧_ : † -> † -> †
  ∏   : (S : ∗) -> ([ S ] -> †) -> †

|- : † -> ∗
|- ⊥       = /0/
|- TT      = /1/
|- (P ∧ Q) = /Σ/ (|- P) \_ -> |- Q
|- (∏ S P) = /Π/ S \s -> |- (P s)

Prf : † -> Set
Prf P = [ |- P ]

infixr 40 _⇒_

_⇒_ : † -> † -> †
P ⇒ Q = ∏ (|- P) \_ -> Q

infix 80 _⇔_

mutual

  _⇔_ : ∗ -> ∗ -> †
  /0/        ⇔  /0/        =  TT
  /1/        ⇔  /1/        =  TT
  /2/        ⇔  /2/        =  TT
  /Π/ S0 T0  ⇔  /Π/ S1 T1  =
    S1 ⇔ S0  ∧
    ∏ S1 \s1 -> ∏ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⇒ (T0 s0 ⇔ T1 s1)
  /Σ/ S0 T0  ⇔  /Σ/ S1 T1  =
    S0 ⇔ S1  ∧
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒ (T0 s0 ⇔ T1 s1)
  /W/ S0 T0  ⇔  /W/ S1 T1  =
    S0 ⇔ S1  ∧
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒ (T1 s1 ⇔ T0 s0)
  _          ⇔  _ = ⊥

  _>_≅_>_ : (S : ∗) -> [ S ] -> (T : ∗) -> [ T ] -> †
  /0/ > _  ≅ /0/ > _  = TT
  /1/ > _  ≅ /1/ > _  = TT
  /2/ > tt ≅ /2/ > tt = TT
  /2/ > ff ≅ /2/ > ff = TT

  /Π/ S0 T0 > f0 ≅ /Π/ S1 T1 > f1 =
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
      (T0 s0 > f0 s0 ≅ T1 s1 > f1 s1)

  /Σ/ S0 T0 > p0 ≅ /Σ/ S1 T1 > p1 =
    (S0          > fst p0 ≅ S1          > fst p1) ∧
    (T0 (fst p0) > snd p0 ≅ T1 (fst p1) > snd p1)

  /W/ S0 T0 > (s0 <| f0) ≅ /W/ S1 T1 > (s1 <| f1) =
    (S0 > s0 ≅ S1 > s1)  ∧
    ∏ (T0 s0) \t0 -> ∏ (T1 s1) \t1 ->
       (T0 s0 > t0 ≅ T1 s1 > t1) ⇒
       (/W/ S0 T0 > f0 t0 ≅ /W/ S1 T1 > f1 t1)

  _ > _ ≅ _ > _ = ⊥

mutual

  _>_<_!_ : (S : ∗) -> [ S ] -> (T : ∗) -> Prf (S ⇔ T) -> [ T ]

  /0/ > z < /0/ ! _  = z
  /1/ > u < /1/ ! _  = u
  /2/ > b < /2/ ! _  = b

  /Π/ S0 T0 > f0 < /Π/ S1 T1 ! Q =
    let S1S0 : Prf (S1 ⇔ S0)
        S1S0 = fst Q
        T0T1 : Prf (∏ S1 \s1 -> ∏ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⇒
                      (T0 s0 ⇔ T1 s1))
        T0T1 = snd Q
    in  \s1 ->
        let s0   : [ S0 ]
            s0   = S1 > s1 < S0 ! S1S0
            s1s0 : Prf (S1 > s1 ≅ S0 > s0)
            s1s0 = [| S1 > s1 < S0 ! S1S0 |]
        in  T0 s0 > f0 s0 < T1 s1 ! T0T1 s1 s0 s1s0

  /Σ/ S0 T0 > p0 < /Σ/ S1 T1 ! Q =
    let S0S1 : Prf (S0 ⇔ S1)
        S0S1 = fst Q
        T0T1 : Prf (∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
                      (T0 s0 ⇔ T1 s1))
        T0T1 = snd Q
        s0   : [ S0 ]
        s0   = fst p0
        s1   : [ S1 ]
        s1   = S0 > s0 < S1 ! S0S1
        s0s1 : Prf (S0 > s0 ≅ S1 > s1)
        s0s1 = [| S0 > s0 < S1 ! S0S1 |]
        t0   : [ T0 s0 ]
        t0   = snd p0
        t1   : [ T1 s1 ]
        t1   = T0 s0 > t0 < T1 s1 ! T0T1 s0 s1 s0s1
    in  s1 , t1

  /W/ S0 T0 > (s0 <| f0) < /W/ S1 T1 ! Q =
    let S0S1 : Prf (S0 ⇔ S1)
        S0S1 = fst Q
        T1T0 : Prf (∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
                      (T1 s1 ⇔ T0 s0))
        T1T0 = snd Q
        s1   : [ S1 ]
        s1   = S0 > s0 < S1 ! S0S1
        s0s1 : Prf (S0 > s0 ≅ S1 > s1)
        s0s1 = [| S0 > s0 < S1 ! S0S1 |]
    in  s1 <| \t1 ->
        let t0   : [ T0 s0 ]
            t0   = T1 s1 > t1 < T0 s0 ! T1T0 s0 s1 s0s1
        in  /W/ S0 T0 > f0 t0 < /W/ S1 T1 ! Q

  /0/     > _ < /1/     ! ()
  /0/     > _ < /2/     ! ()
  /0/     > _ < /Π/ _ _ ! ()
  /0/     > _ < /Σ/ _ _ ! ()
  /0/     > _ < /W/ _ _ ! ()
  /1/     > _ < /0/     ! ()
  /1/     > _ < /2/     ! ()
  /1/     > _ < /Π/ _ _ ! ()
  /1/     > _ < /Σ/ _ _ ! ()
  /1/     > _ < /W/ _ _ ! ()
  /2/     > _ < /0/     ! ()
  /2/     > _ < /1/     ! ()
  /2/     > _ < /Π/ _ _ ! ()
  /2/     > _ < /Σ/ _ _ ! ()
  /2/     > _ < /W/ _ _ ! ()
  /Π/ _ _ > _ < /0/     ! ()
  /Π/ _ _ > _ < /1/     ! ()
  /Π/ _ _ > _ < /2/     ! ()
  /Π/ _ _ > _ < /Σ/ _ _ ! ()
  /Π/ _ _ > _ < /W/ _ _ ! ()
  /Σ/ _ _ > _ < /0/     ! ()
  /Σ/ _ _ > _ < /1/     ! ()
  /Σ/ _ _ > _ < /2/     ! ()
  /Σ/ _ _ > _ < /Π/ _ _ ! ()
  /Σ/ _ _ > _ < /W/ _ _ ! ()
  /W/ _ _ > _ < /0/     ! ()
  /W/ _ _ > _ < /1/     ! ()
  /W/ _ _ > _ < /2/     ! ()
  /W/ _ _ > _ < /Π/ _ _ ! ()
  /W/ _ _ > _ < /Σ/ _ _ ! ()

  [|_>_<_!_|] : (S : ∗)(s : [ S ])(T : ∗)(q : Prf (S ⇔ T)) ->
    Prf (S > s ≅ T > (S > s < T ! q))
  [| S > s < T ! q |] = {! !}

Resp : (S : ∗)(P : [ S ] -> ∗)
       {s0 s1 : [ S ]} -> Prf ((S > s0 ≅ S > s1) ⇒ (P s0 ⇔ P s1))
Resp = {! !}

[|_>_|] : (S : ∗)(s : [ S ]) -> Prf (S > s ≅ S > s)
[| S > s |] = {! !}

Sym : (S0 S1 : ∗) -> Prf ((S0 ⇔ S1) ⇒ (S1 ⇔ S0))
Sym = {! !}

sym : (S0 : ∗)(s0 : [ S0 ])(S1 : ∗)(s1 : [ S1 ]) ->
      Prf ((S0 > s0 ≅ S1 > s1) ⇒ (S1 > s1 ≅ S0 > s0))
sym = {! !}

elimNat∗ : (P : [ /Nat/ ] -> ∗) ->
           [( P zero ⟶ (/Π/ /Nat/ \k -> P k ⟶ P (suc k)) ⟶
              /Π/ /Nat/ \n -> P n )]
{-
elimNat∗ P pz ps (tt <| g) = P zero > pz < P (tt <| g) !
  Resp /Nat/ P (_ , \z0 -> z0 Ψ)
elimNat∗ P pz ps (ff <| g) =
  let n = g _
  in  P (suc n) > ps n (elimNat∗ P pz ps n) < P (ff <| g) !
         Resp /Nat/ P
           (_ , \u0 u1 u0u1 -> [| (/1/ ⟶ /Nat/) > g |] _ u1 _)
-}
elimNat∗ P pz ps n = rec P n
  \b -> case (\ b -> /Π/ ((Case b /0/ /1/) ⟶ /Nat/) \g ->
                        (/Π/ (Case b /0/ /1/) \t -> P (g t)) ⟶
                        P (b <| g)) b
    (\g _ -> P zero > pz < P (tt <| g) ! Resp /Nat/ P (_ , \z0 -> z0 Ψ))
    (\g h ->
       let n = g _
       in  P (suc n) > ps n (h _) < P (ff <| g) !
             Resp /Nat/ P
               (_ , \u0 u1 u0u1 -> [| (/1/ ⟶ /Nat/) > g |] _ u1 _))

plus : [ /Nat/ ⟶ /Nat/ ⟶ /Nat/ ]
plus x y = elimNat∗ (\_ -> /Nat/) y (\_ -> suc) x

irr : (P0 P1 : †) -> Prf ((|- P0 ⇔ |- P1) ⇒
      ∏ (|- P0) \p0 -> ∏ (|- P1) \p1 -> |- P0 > p0 ≅ |- P1 > p1)

irr ⊥  ⊥  _ _ _ = _

irr TT TT _ _ _ = _

irr (P0 ∧ Q0) (P1 ∧ Q1) PQ01 pq0 pq1 =
  let p01 : Prf (|- P0 > fst pq0 ≅ |- P1 > fst pq1)
      p01 = irr P0 P1 (fst PQ01) (fst pq0) (fst pq1)
  in  p01 , irr Q0 Q1 (snd PQ01 (fst pq0) (fst pq1) p01) (snd pq0) (snd pq1)

irr (∏ S0 P0) (∏ S1 P1) SP01 f0 f1 = \s0 s1 s0s1 ->
  irr (P0 s0) (P1 s1) (snd SP01 s1 s0 (sym S0 s0 S1 s1 s0s1)) (f0 s0) (f1 s1)

irr        ⊥  TT       () _ _
irr        ⊥  (_ ∧ _)  () _ _
irr        ⊥  (∏ _ _)  () _ _
irr       TT  ⊥        () _ _
irr       TT  (_ ∧ _)  () _ _
irr       TT  (∏ _ _)  () _ _
irr  (_ ∧ _)  TT       () _ _
irr  (_ ∧ _)  ⊥        () _ _
irr  (_ ∧ _)  (∏ _ _)  () _ _
irr  (∏ _ _)  TT       () _ _
irr  (∏ _ _)  ⊥        () _ _
irr  (∏ _ _)  (_ ∧ _)  () _ _

{---------------------------------------------------------------------------

              The News from Nottingham (with subtitles)

                            Conor McBride

                           joint work with
         Thorsten Altenkirch, Wouter Swierstra, Peter Hancock,
            Nicolas Oury, James Chapman and Peter Morris

---------------------------------------------------------------------------}