Agda-2.3.2.2: 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
---------------------------------------------------------------------------}