Agda-2.3.2.2: examples/outdated-and-incorrect/iird/IID-Proof-Setup.agda

module IID-Proof-Setup where

open import LF
open import Identity
open import IID
open import IIDr
open import DefinitionalEquality

OPg : Set -> Set1
OPg I = OP I I

-- Encoding indexed inductive types as non-indexed types.
ε : {I : Set}(γ : OPg I) -> OPr I
ε (ι i)     j = σ (i == j) (\_ -> ι ★)
ε (σ A γ)   j = σ A (\a -> ε (γ a) j)
ε (δ H i γ) j = δ H i (ε γ j)

-- Adds a reflexivity proof.
g→rArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (a : Args γ U) ->
	      rArgs (ε γ) U (index γ U a)
g→rArgs (ι e)     U arg	= (refl , ★)
g→rArgs (σ A γ)   U arg = (π₀ arg , g→rArgs (γ (π₀ arg)) U (π₁ arg))
g→rArgs (δ H i γ) U arg = (π₀ arg , g→rArgs γ U (π₁ arg))

-- Strips the equality proof.
r→gArgs : {I : Set}(γ : OPg I)(U : I -> Set)
	      (i : I)(a : rArgs (ε γ) U i) ->
	      Args γ U
r→gArgs (ι i)     U j _	  = ★
r→gArgs (σ A γ)   U j arg = (π₀ arg , r→gArgs (γ (π₀ arg)) U j (π₁ arg))
r→gArgs (δ H i γ) U j arg = (π₀ arg , r→gArgs γ U j (π₁ arg))

-- Converting an rArgs to a gArgs and back is (provably, not definitionally)
-- the identity.
r←→gArgs-subst :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (C : (i : I) -> rArgs (ε γ) U i -> Set)
  (i : I)(a : rArgs (ε γ) U i) ->
  (C (index γ U (r→gArgs γ U i a))
     (g→rArgs γ U (r→gArgs γ U i a))
  ) -> C i a

r←→gArgs-subst {I} (ι i) U C j arg m =
  elim== i (\k q -> C k (q , ★)) m j (π₀ arg)

r←→gArgs-subst (σ A γ)   U C j arg m = 
  r←→gArgs-subst (γ (π₀ arg)) U (\i c -> C i (π₀ arg , c)) j (π₁ arg) m

r←→gArgs-subst (δ H i γ) U C j arg m =
  r←→gArgs-subst γ U (\i c -> C i (π₀ arg , c)) j (π₁ arg) m

-- r←→gArgs-subst eliminates the identity proof stored in the rArgs. If this proof is
-- by reflexivity r←→gArgs-subst is a definitional identity. This is the case
-- when a = g→rArgs a'
r←→gArgs-subst-identity :
  {I  : Set}(γ : OPg I)(U : I -> Set)
  (C  : (i : I) -> rArgs (ε γ) U i -> Set)
  (a' : Args γ U) ->
  let a = g→rArgs γ U a'
      i = index γ U a' in
  (h : C (index γ U (r→gArgs γ U i a))
	 (g→rArgs γ U (r→gArgs γ U i a))
  ) -> r←→gArgs-subst γ U C i a h ≡ h
r←→gArgs-subst-identity (ι i)	  U C _   h = refl-≡
r←→gArgs-subst-identity (σ A γ)	  U C arg h = r←→gArgs-subst-identity (γ (π₀ arg)) U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)
r←→gArgs-subst-identity (δ H i γ) U C arg h = r←→gArgs-subst-identity γ U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)

-- Going the other way around is definitionally the identity.
g←→rArgs-identity :
  {I : Set}(γ : OPg I)(U : I -> Set)
  (a : Args γ U) ->
  r→gArgs γ U (index γ U a) (g→rArgs γ U a) ≡ a
g←→rArgs-identity (ι i)	    U _	  = refl-≡
g←→rArgs-identity (σ A γ)   U arg = cong-≡ (\ ∙ -> (π₀ arg , ∙)) (g←→rArgs-identity (γ (π₀ arg)) U (π₁ arg))
g←→rArgs-identity (δ H i γ) U arg = cong-≡ (\ ∙ -> (π₀ arg , ∙)) (g←→rArgs-identity γ U (π₁ arg))

-- Corresponding conversion functions for assumptions to inductive occurrences.
-- Basically an identity function.
g→rIndArg : {I : Set}(γ : OPg I)(U : I -> Set)
        (i : I)(a : rArgs (ε γ) U i) ->
        IndArg γ U (r→gArgs γ U i a) -> IndArg (ε γ i) U a
g→rIndArg (ι j)	    U i _ ()
g→rIndArg (σ A γ)   U i arg v       = g→rIndArg (γ (π₀ arg)) U i (π₁ arg) v
g→rIndArg (δ A j γ) U i arg (inl a) = inl a
g→rIndArg (δ A j γ) U i arg (inr v) = inr (g→rIndArg γ U i (π₁ arg) v)

-- Basically we can substitute general inductive occurences for the encoded
-- restricted inductive occurrences.
g→rIndArg-subst :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a)) ->
    C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
      (Ind	(ε γ i) U a (g→rIndArg γ U i a v)) ->
    C (IndIndex γ U (r→gArgs γ U i a) v)
      (Ind	γ U (r→gArgs γ U i a) v)
g→rIndArg-subst (ι j)	  U C i _ ()	    h
g→rIndArg-subst (σ A γ)	  U C i arg v	    h = g→rIndArg-subst (γ (π₀ arg)) U C i (π₁ arg) v h
g→rIndArg-subst (δ A j γ) U C i arg (inl a) h = h
g→rIndArg-subst (δ A j γ) U C i arg (inr v) h = g→rIndArg-subst γ U C i (π₁ arg) v h

-- g→rIndArg-subst is purely book-keeping. On the object level it's definitional identity.
g→rIndArg-subst-identity :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i)
    (v : IndArg γ U (r→gArgs γ U i a))
    (h : C (IndIndex (ε γ i) U a (g→rIndArg γ U i a v))
	   (Ind	(ε γ i) U a (g→rIndArg γ U i a v))
    ) -> g→rIndArg-subst γ U C i a v h ≡ h
g→rIndArg-subst-identity (ι j)	   U C i _   ()	   h
g→rIndArg-subst-identity (σ A γ)   U C i arg v	   h =
  g→rIndArg-subst-identity (γ (π₀ arg)) U C i (π₁ arg) v h
g→rIndArg-subst-identity (δ A j γ) U C i arg (inl a) h = refl-≡
g→rIndArg-subst-identity (δ A j γ) U C i arg (inr v) h =
  g→rIndArg-subst-identity γ U C i (π₁ arg) v h

-- And finally conversion of induction hypotheses. This goes the other direction.
r→gIndHyp :
    {I : Set}(γ : OPg I)(U : I -> Set)
    (C : (i : I) -> U i -> Set)
    (i : I)(a : rArgs (ε γ) U i) ->
    IndHyp (ε γ i) U C a -> IndHyp γ U C (r→gArgs γ U i a)
r→gIndHyp γ U C i a h v = g→rIndArg-subst γ U C i a v (h (g→rIndArg γ U i a v))