module Game-Morphs where
open import Data.Empty
open import Data.Unit
open import Data.Maybe
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming (_+_ to _+'_)
open import Game-Core
dist01 : ∀ {M} → (I ⊘ M) ≈ I
dist01 {gam f} = bsm (sim ⊥-elim λ())
(sim ⊥-elim λ())
dist02 : ∀ {P} → (P ⊸ I) ≈ I
dist02 {gam f} = bsm (sim ⊥-elim λ())
(sim ⊥-elim λ())
mutual
unit⊸ : ∀ {M} → (I ⊸ M) ≈ M
unit⊸ {gam f} = bsm (sim id (λ m → wk₁ $ unit⊗ {f m}))
(sim id (λ m → wk₂ $ unit⊗ {f m}))
unit⊗ : ∀ {M} → (M ⊗ I) ≈ M
unit⊗ {gam f}
= bsm (sim ([ id , ⊥-elim ])
([ (λ m → wk₁ $ unit⊸ {f m}) , (λ()) ] ))
(sim inj₁ (λ m → wk₂ $ unit⊸ {f m}))
unit⊘ : ∀ {M} → M ⊘ I ≈ M
unit⊘ {gam f} = bsm (sim id (λ i → wk₁ $ unit⊸))
(sim id (λ i → wk₂ $ unit⊸))
sym⊗ : ∀ {M N} → (M ⊗ N) ≈ (N ⊗ M)
sym⊗ {gam f} {gam g}
= bsm (sim [ inj₂ , inj₁ ]
[ (λ _ → id≲) , (λ _ → id≲) ])
(sim [ inj₂ , inj₁ ]
[ (λ _ → id≲) , (λ _ → id≲) ])
dist10 : ∀ {M} → (I ⊗ M) ≈ M
dist10 = sym⊗ ≈∘≈ unit⊗
dec1 : ∀ {M N} → M ⊗ N ≈ (M ⊘ N) ×' (N ⊘ M)
dec1 {gam f} {gam g}
= bsm (sim id (λ _ → id≲))
(sim id (λ _ → id≲))
dist1 : ∀ {M N O} → (M ×' N) ⊘ O ≈ (M ⊘ O) ×' (N ⊘ O)
dist1 {gam f} {gam g} {gam h}
= bsm (sim id [ (λ _ → id≲) , (λ _ → id≲) ])
(sim id [ (λ _ → id≲) , (λ _ → id≲) ])
dist1ω : ∀ {M N} → (ω× M) ⊘ N ≈ ω× (M ⊘ N)
dist1ω {gam f} {gam g} = bsm (sim id (λ _ → id≲)) (sim id (λ _ → id≲))
dist2 : ∀ {M N O} → O ⊸ (M ×' N) ≈ (O ⊸ M) ×' (O ⊸ N)
dist2 {gam f} {gam g} {gam h}
= bsm (sim id [ (λ _ → id≲) , (λ _ → id≲) ])
(sim id [ (λ _ → id≲) , (λ _ → id≲) ])
dist2ω : ∀ {M N} → M ⊸ (ω× N) ≈ ω× (M ⊸ N)
dist2ω {gam f} {gam g} = bsm (sim id (λ _ → id≲)) (sim id (λ _ → id≲))
sym× : ∀ {M N} → M ×' N ≈ N ×' M
sym× {gam f} {gam g}
= bsm (sim [ inj₂ , inj₁ ] [ (λ _ → id≲) , (λ _ → id≲) ])
(sim [ inj₂ , inj₁ ] [ (λ _ → id≲) , (λ _ → id≲) ])
lfe : ∀ {M N} → (M ⊸ N) ⊸o ≈ (N ⊸o) ⊘ M
lfe {gam f} {gam g}
= bsm (sim id (λ _ → id≲))
(sim id (λ _ → id≲))
curryo : ∀ {M N} → M ⊸ (N ⊸o) ≈ (N ⊗ M) ⊸o
curryo {gam f} {gam g}
= bsm (sim id (λ _ → id≲))
(sim id (λ _ → id≲))
↑≈⊸o : ∀ {M} → M ⊸o ≈ M ⊸ o
↑≈⊸o = bsm (sim (λ _ → tt) (λ _ → wk₂ $ sym⊗ ≈∘≈ unit⊗))
(sim (λ _ → tt) (λ _ → wk₁ $ sym⊗ ≈∘≈ unit⊗))
mutual
_⊸≲_ : ∀ {M N} O → N ≲ M → (O ⊸ N) ≲ (O ⊸ M)
_⊸≲_ {gam f} {gam g} (gam h) (sim f' g')
= sim f' (λ m → g' m ≲⊗ (gam h))
_≲⊗_ : ∀ {M N} → M ≲ N → ∀ O → (M ⊗ O) ≲ (N ⊗ O)
_≲⊗_ {gam f} {gam g} (sim f' g') (gam h)
= sim [ inj₁ ∘ f' , inj₂ ]
[ (λ m → gam h ⊸≲ (g' m)) ,
(λ o' → (sim f' g') ≲⊸ (h o')) ]
_≲⊸_ : ∀ {M N} → N ≲ M → ∀ O → (M ⊸ O) ≲ (N ⊸ O)
_≲⊸_ {gam f} {gam g} s (gam h) =
sim id (λ o' → h o' ⊗≲ s)
_⊗≲_ : ∀ {M N} O → M ≲ N → (O ⊗ M) ≲ (O ⊗ N)
_⊗≲_ {M} {N} O s = (wk₁ $ sym⊗) ≲∘≲ (s ≲⊗ O) ≲∘≲ (wk₁ $ sym⊗)
_≲⊘_ : ∀ {M N} → M ≲ N → ∀ O → (M ⊘ O) ≲ (N ⊘ O)
_≲⊘_ {gam f} {gam g} (sim f' g') (gam h)
= sim f' (λ m → gam h ⊸≲ (g' m))
_⊘≲_ : ∀ {M N} O → M ≲ N → (O ⊘ M) ≲ (O ⊘ N)
(gam o) ⊘≲ s = sim id (λ m → s ≲⊸ (o m))
_⊗≈_ : ∀ {M N} O → M ≈ N → (O ⊗ M) ≈ (O ⊗ N)
O ⊗≈ s = bsm (O ⊗≲ wk₂ s) (O ⊗≲ wk₁ s)
_≈⊘_ : ∀ {M N} → M ≈ N → ∀ O → (M ⊘ O) ≈ (N ⊘ O)
s ≈⊘ O = bsm (wk₂ s ≲⊘ O) (wk₁ s ≲⊘ O)
_⊘≈_ : ∀ {M N} O → M ≈ N → O ⊘ M ≈ O ⊘ N
O ⊘≈ s = bsm (O ⊘≲ (wk₂ s)) (O ⊘≲ (wk₁ s))
_⊸≈_ : ∀ {M N} O → M ≈ N → (O ⊸ M) ≈ (O ⊸ N)
O ⊸≈ s = bsm (O ⊸≲ (wk₂ s)) (O ⊸≲ (wk₁ s))
_≈⊸_ : ∀ {M N} → M ≈ N → ∀ O → (M ⊸ O) ≈ (N ⊸ O)
s ≈⊸ O = bsm (wk₁ s ≲⊸ O) (wk₂ s ≲⊸ O)
lfe' : ∀ {M N} → (M ⊸ N) ⊸ o ≈ (N ⊸ o) ⊘ M
lfe' {M} {N} = (↑≈⊸o ^-1) ≈∘≈ lfe ≈∘≈ (↑≈⊸o ≈⊘ M)
mutual
pasc⊸ : ∀ {M N O} → M ⊸ (N ⊸ O) ≈ (M ⊗ N) ⊸ O
pasc⊸ {gam m} {gam n} {gam o}
= bsm (sim id (λ i → (o i ⊗≲ (wk₂ $ sym⊗)) ≲∘≲
(wk₁ $ asc⊗ {o i} {gam n} {gam m})))
(sim id (λ i → (wk₂ $ asc⊗ {o i} {gam n} {gam m}) ≲∘≲
(o i ⊗≲ (wk₁ $ sym⊗))))
asc⊗ : ∀ {M N O} → (M ⊗ N) ⊗ O ≈ M ⊗ (N ⊗ O)
asc⊗ {gam m} {gam n} {gam o}
= bsm (sim [ [ inj₁ , inj₂ ∘ inj₁ ] , inj₂ ∘ inj₂ ]
[ [ (λ i → (wk₂ (sym⊗) ≲⊸ (m i)) ≲∘≲
(wk₁ $ pasc⊸ {gam o} {gam n} {m i}))
, (λ i → wk₂ $ psym⊸ {gam m} {gam o} {n i}) ]
, (λ i → wk₂ $ pasc⊸ {gam m} {gam n} {o i}) ])
(sim [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ] ]
[ (λ i → _≲∘≲_ (wk₂ $ pasc⊸ {gam o} {gam n} {m i})
(wk₁ (sym⊗) ≲⊸ (m i)))
, [ (λ i → wk₂ $ psym⊸ {gam o} {gam m} {n i})
, (λ i → wk₁ $ pasc⊸ {gam m} {gam n} {o i}) ] ])
psym⊸ : ∀ {M N O} → M ⊸ (N ⊸ O) ≈ N ⊸ (M ⊸ O)
psym⊸ = pasc⊸ ≈∘≈ (sym⊗ ≈⊸ _) ≈∘≈ (pasc⊸ ^-1)
pasc⊘ : ∀ {M N O} → (M ⊘ N) ⊘ O ≈ M ⊘ (N ⊗ O)
pasc⊘ {gam m} {gam n} {gam o}
= bsm (sim id (λ i → (wk₂ (sym⊗) ≲⊸ (m i)) ≲∘≲ (wk₁ $ pasc⊸)))
(sim id (λ i → (wk₂ $ pasc⊸) ≲∘≲ (wk₂ (sym⊗) ≲⊸ (m i))))
psym⊘ : ∀ {M N O} → (M ⊘ N) ⊘ O ≈ (M ⊘ O) ⊘ N
psym⊘ = pasc⊘ ≈∘≈ (_ ⊘≈ sym⊗) ≈∘≈ (pasc⊘ ^-1)
mutual
≲⊗af : ∀ {M N} → M ⊗ N ≲ M
≲⊗af {gam g} {gam _} = sim inj₁ (λ m → ≲⊸af {g m})
≲⊸af : ∀ {M N} → M ≲ N ⊸ M
≲⊸af {gam g} = sim id (λ m → ≲⊗af {g m})
≲⊘af : ∀ {M N} → M ⊘ N ≲ M
≲⊘af {gam _} = sim id (λ m → ≲⊸af)
≲wk : ∀ {M N} → M ⊗ N ≲ M ⊘ N
≲wk {gam _} {gam _} = sim inj₁ (λ x → id≲)
≲I : ∀ {M} → M ≲ I
≲I = sim ⊥-elim (λ())
abs : ∀ {M} → o ⊘ M ≈ o
abs {M} = (unit⊸ ^-1) ≈⊘ M ≈∘≈ (lfe' {M} {I} ^-1) ≈∘≈ dist02 {M} ≈⊸ o ≈∘≈ unit⊸
≲π₁ : ∀ {M N} → M ×' N ≲ M
≲π₁ {gam _} {gam _} = sim inj₁ (λ _ → id≲)
≲π₂ : ∀ {M N} → M ×' N ≲ N
≲π₂ {gam _} {gam _} = sim inj₂ (λ _ → id≲)
≲π : ∀ {M} → ℕ → ω× M ≲ M
≲π {gam _} n = sim (λ m → n , m) (λ _ → id≲)
⊸≲⊸̂ : ∀ {M N} → M ⊸̂ N ≲ M ⊸ N
⊸≲⊸̂ {gam m} {gam n} = sim id (λ n' → ≲wk {gam m} {n n'} ≲∘≲ (wk₂ sym⊗))