gistfile1.txt

{-# OPTIONS --without-K #-}
open import HoTT

module b where

A : Set
A = ℕ

rev : (A → A → Set) → (A → A → Set)
rev R a a' = R a' a

data Opt : Set where
  none : Opt
  some : A → Opt

pairsa : Opt → List A → Opt → List (Opt × Opt)
pairsa u nil v = (u , v) :: nil
pairsa u (x :: tl) v = (u , some x) :: pairsa (some x) tl v

swpairsa : Opt → List A → Opt → List (Opt × Opt)
swpairsa u nil v = (u , v) :: nil
swpairsa u (x :: tl) v = (some x , v) :: swpairsa u tl (some x)

pairs : List A → List (Opt × Opt)
pairs ℓ = pairsa none ℓ none

swpairs : List A → List (Opt × Opt)
swpairs ℓ = swpairsa none ℓ none

swap : {X : Set} → X × X → X × X
swap (a , b) = (b , a)

-- pairsa (1 :: 2 :: 3 :: nil) (some 0) (some 999) =
-- (some 0 , some 1) ::
-- (some 1 , some 2) ::
-- (some 2 , some 3) :: (some 3 , some 999) :: nil

-- swpairsa (3 :: 2 :: 1 :: nil)  (some 0) (some 999) =
-- (some 3 , some 999) ::
-- (some 2 , some 3) :: (some 1 , some 2) :: (some 0 , some 1) :: nil

lemma : (ℓ : List A) (u v : Opt) (x : A) →
      pairsa u (snoc ℓ x) v == snoc (pairsa u ℓ (some x)) (some x , v)
lemma nil u v x = idp
lemma (y :: ℓ) u v x = ap (λ z → (u , some y) :: z) (lemma ℓ (some y) v x)

thm : (ℓ : List A) (u v : Opt) → pairsa u (reverse ℓ) v == reverse (swpairsa u ℓ v)
thm nil u v = idp
thm (x :: ℓ) u v = lemma (reverse ℓ) u v x ∙ ap (λ z → snoc z (some x , v)) (thm ℓ u (some x))

satisfiesRel : Opt → List A → Opt → (Opt × Opt → Set) → Set
satisfiesRel u ℓ v R = All R (pairsa u ℓ v)

bigThmRephrase : (ℓ : List A) (u v : Opt) (R : Opt × Opt → Set) →
  All R (pairsa u ℓ v) →
  All (λ x → R (snd x , fst x)) (pairsa v (reverse ℓ) u)
bigThmRephrase ℓ u v R φ = {!transport!}

bigThm : (ℓ : List A) (u v : Opt) (R : Opt × Opt → Set) →
  satisfiesRel u ℓ v R → satisfiesRel v (reverse ℓ) u (R ∘ swap)
bigThm ℓ u v R = bigThmRephrase ℓ u v R