------------------------------------------------------------------------
-- Operational semantics using the partiality monad
--
-- Nils Anders Danielsson, with some help from Andreas Abel
------------------------------------------------------------------------

-- Outline:
--
-- Prelude
--
-- The partiality monad
-- Weak (bi)similarity
-- Weak bisimilarity can be defined using weak similarity
-- Some congruences
--
-- A simply typed lambda-calculus with a fixpoint operator
-- Environments and values
-- Operational semantics
--
-- Equality (and inequality)
-- Key lemmas
-- Term equality is compatible
-- Reflexivity
-- Contexts with zero or more holes (all of the same type)
-- Term equality is closed under contexts
-- The equality is symmetric
-- The inequality is transitive
-- Contextual equality (and inequality)

------------------------------------------------------------------------
-- * Prelude

-- Natural numbers.

data Nat : Set
{ zero : Nat
; suc  : Nat -> Nat
}

-- Predecessor (total).

fun pred : Nat -> Nat
{ pred zero    = zero
; pred (suc n) = n
}

-- A conditional.

fun ifZero : [A : Set] -> Nat -> A -> A -> A
{ ifZero A zero    t e = t
; ifZero A (suc n) t e = e
}

-- Propositional equality.

data Id [A : Set] (x : A) : A -> Set
{ reflId : Id A x x
}

-- Propositional equality is substitutive.

fun subst : [A : Set] -> (x, y : A) -> Id A x y ->
            [P : A -> Set] -> P x -> P y
{ subst .A .x .x (reflId A x) P p = p
}

-- The unit type.

data Unit : Set
{ unit : Unit
}

-- The always true relation.

fun Always : [A : Set] -> A -> A -> Set
{ Always A x y = Unit
}

-- The converse of a sized relation.

fun Flip : [A : Set] ->
           ++(-Size -> A -> A -> Set) -> (-Size -> A -> A -> Set)
{ Flip A rel i x y = rel i y x
}

------------------------------------------------------------------------
-- * The partiality monad

-- The partiality monad.

sized codata Lift (+ A : Set) : Size -> Set
{ now   : [i : Size] -> A        -> Lift A ($ i)
; later : [i : Size] -> Lift A i -> Lift A ($ i)
}

-- Non-termination.

cofun never : [i : Size] -> [A : Set] -> Lift A i
{ never ($ i) A = later A i (never i A)
}

-- The bind operation of the monad.

cofun bind : [A : Set] -> [B : Set] ->
             [i : Size] -> Lift A i -> (A -> Lift B i) -> Lift B i
{ bind A B ($ i) (now   .A .i a) f = f a
; bind A B ($ i) (later .A .i x) f = later B i (bind A B i x f)
}

------------------------------------------------------------------------
-- * Weak (bi)similarity

-- The two kinds of similarity.

data Kind : Set
{ sim   : Kind
; bisim : Kind
}

-- Some utility functions.

fun sucIfSim : Kind -> ^Size -> Size
{ sucIfSim sim   i = $ i
; sucIfSim bisim i = i
}

fun sucIfBisim : Kind -> ^Size -> Size
{ sucIfBisim sim   i = i
; sucIfBisim bisim i = $ i
}

-- The inductive part of weak (bi)similarity.

data Rel' (A : Set) (+ Rel : Lift A # -> Lift A # -> Set)
          (+ rel : A -> A -> Set) :
          Kind -> Lift A # -> Lift A # -> Set
{ nowCong'   : [k : Kind] -> (v1, v2 : A) -> rel v1 v2 ->
               Rel' A Rel rel k (now A # v1) (now A # v2)
; laterCong' : [x1, x2 : Lift A #] ->
               Rel x1 x2 ->
               Rel' A Rel rel bisim (later A # x1) (later A # x2)
; laterL'    : [k : Kind] -> [x1, x2 : Lift A #] ->
               Rel' A Rel rel k x1 x2 ->
               Rel' A Rel rel k (later A # x1) x2
; laterRB'   : [x1, x2 : Lift A #] ->
               Rel' A Rel rel bisim x1 x2 ->
               Rel' A Rel rel bisim x1 (later A # x2)
; laterRS'   : [x1, x2 : Lift A #] ->
               Rel x1 x2 ->
               Rel' A Rel rel sim x1 (later A # x2)
}

-- Weak (bi)similarity.

sized codata Rel (A : Set) (+ rel : -Size -> A -> A -> Set) :
                 Size -> Kind -> Lift A # -> Lift A # -> Set
{ tie : [i : Size] -> [k : Kind] -> [x1, x2 : Lift A #] ->
        Rel' A (Rel A rel i k) (rel ($ i)) k x1 x2 ->
        Rel A rel ($ i) k x1 x2
}

fun force : [A : Set] -> [rel : -Size -> A -> A -> Set] ->
            [i : Size] -> [k : Kind] -> [x1, x2 : Lift A #] ->
            Rel A rel ($ i) k x1 x2 ->
            Rel' A (Rel A rel i k) (rel ($ i)) k x1 x2
{ force A rel i k x1 x2 (tie .A .rel .i .k .x1 .x2 xRel) = xRel
}

-- Weak bisimilarity.

fun Eq : ^(A : Set) -> ++(eq : -Size -> A -> A -> Set) ->
         -Size -> Lift A # -> Lift A # -> Set
{ Eq A eq i = Rel A eq i bisim
}

-- Weak similarity. Note the order of the arguments: if x is greater
-- than or equal to y (GEq A eq # x y), then the termination of y
-- implies the termination of x.

fun GEq : ^(A : Set) -> ++(eq : -Size -> A -> A -> Set) ->
          -Size -> Lift A # -> Lift A # -> Set
{ GEq A geq i = Rel A geq i sim
}

-- The constructors of Rel' can be "lifted" to the level of Rel.

cofun nowCong : [A : Set] -> [rel : -Size -> A -> A -> Set] ->
                [i : Size] -> [k : Kind] -> (v1, v2 : A) ->
                rel i v1 v2 -> Rel A rel i k (now A # v1) (now A # v2)
{ nowCong A rel ($ i) k v1 v2 vRel =
    tie A rel i k (now A # v1) (now A # v2)
        (nowCong' A (Rel A rel i k) (rel ($ i)) k v1 v2 vRel)
}

cofun laterL : [A : Set] -> [rel : -Size -> A -> A -> Set] ->
               [i : Size] -> [k : Kind] -> [x1, x2 : Lift A #] ->
               Rel A rel i k x1 x2 -> Rel A rel i k (later A # x1) x2
{ laterL A rel ($ i) k x1 x2 (tie .A .rel .i .k .x1 .x2 xRel) =
    tie A rel i k (later A # x1) x2
        (laterL' A (Rel A rel i k) (rel ($ i)) k x1 x2 xRel)
}

cofun laterRB : [A : Set] -> [eq : -Size -> A -> A -> Set] ->
                [i : Size] -> [x1, x2 : Lift A #] ->
                Eq A eq i x1 x2 -> Eq A eq i x1 (later A # x2)
{ laterRB A eq ($ i) x1 x2 (tie .A .eq .i .bisim .x1 .x2 xEq) =
    tie A eq i bisim x1 (later A # x2)
        (laterRB' A (Eq A eq i) (eq ($ i)) x1 x2 xEq)
}

fun laterRS : [A : Set] -> [geq : -Size -> A -> A -> Set] ->
              [i : Size] -> [x1, x2 : Lift A #] ->
              GEq A geq i x1 x2 -> GEq A geq ($ i) x1 (later A # x2)
{ laterRS A geq i x1 x2 xGEq =
    tie A geq i sim x1 (later A # x2)
        (laterRS' A (GEq A geq i) (geq ($ i)) x1 x2 xGEq)
}

fun laterR : [A : Set] -> [rel : -Size -> A -> A -> Set] ->
             [i : Size] -> (k : Kind) -> [x1, x2 : Lift A #] ->
             Rel A rel i k x1 x2 ->
             Rel A rel (sucIfSim k i) k x1 (later A # x2)
{ laterR A eq i bisim x1 x2 xEq = laterRB A eq i x1 x2 xEq
; laterR A geq i sim x1 x2 xGEq = laterRS A geq i x1 x2 xGEq
}

fun laterCong : [A : Set] -> [rel : -Size -> A -> A -> Set] ->
                [i : Size] -> (k : Kind) -> [x1, x2 : Lift A #] ->
                Rel A rel i     k x1 x2 ->
                Rel A rel ($ i) k (later A # x1) (later A # x2)
{ laterCong A eq i bisim x1 x2 xEq =
    tie A eq i bisim (later A # x1) (later A # x2)
        (laterCong' A (Eq A eq i) (eq ($ i)) x1 x2 xEq)
; laterCong A geq i sim x1 x2 xGEq =
    laterL A geq ($ i) sim x1 (later A # x2)
      (laterR A geq i sim x1 x2 xGEq)
}

-- Map.

mutual {

  cofun mapRel' : [i : Size] -> [k : Kind] -> [A : Set] ->
                  [rel1, rel2 : -Size -> A -> A -> Set] ->
                  ([j : Size] -> |j| <= |$ i| ->
                   (v1, v2 : A) -> rel1 j v1 v2 -> rel2 j v1 v2) ->
                  (x1, x2 : Lift A #) ->
                  Rel' A (Rel A rel1 i k) (rel1 ($ i)) k x1 x2 ->
                  Rel A rel2 ($ i) k x1 x2
  { mapRel' i k A rel1 rel2 f (now .A .# v1) (now .A .# v2)
      (nowCong' .A .(Rel A rel1 i k) .(rel1 ($ i)) .k .v1 .v2 vRel) =
      nowCong A rel2 ($ i) k v1 v2 (f ($ i) v1 v2 vRel)
  ; mapRel' i .bisim A rel1 rel2 f (later .A .# x1) (later .A .# x2)
      (laterCong' .A .(Rel A rel1 i bisim) .(rel1 ($ i)) .x1 .x2 xRel) =
      laterCong A rel2 i bisim x1 x2
                (mapRel i bisim A rel1 rel2 f x1 x2 xRel)
  ; mapRel' i k .A rel1 rel2 f (later .A .# x1) x2
      (laterL' A .(Rel A rel1 i k) .(rel1 ($ i)) .k .x1 .x2 xRel) =
      laterL A rel2 ($ i) k x1 x2 (mapRel' i k A rel1 rel2 f x1 x2 xRel)
  ; mapRel' i .bisim .A rel1 rel2 f x1 (later .A .# x2)
      (laterRB' A .(Rel A rel1 i bisim) .(rel1 ($ i)) .x1 .x2 xRel) =
      laterR A rel2 ($ i) bisim x1 x2
             (mapRel' i bisim A rel1 rel2 f x1 x2 xRel)
  ; mapRel' i .sim .A rel1 rel2 f x1 (later .A .# x2)
      (laterRS' A .(Rel A rel1 i sim) .(rel1 ($ i)) .x1 .x2 xRel) =
      laterR A rel2 i sim x1 x2 (mapRel i sim A rel1 rel2 f x1 x2 xRel)
  }

  cofun mapRel : [i : Size] -> [k : Kind] -> [A : Set] ->
                 [rel1, rel2 : -Size -> A -> A -> Set] ->
                 ([j : Size] -> |j| <= |i| ->
                  (v1, v2 : A) -> rel1 j v1 v2 -> rel2 j v1 v2) ->
                 (x1, x2 : Lift A #) ->
                 Rel A rel1 i k x1 x2 -> Rel A rel2 i k x1 x2
  { mapRel ($ i) k A rel1 rel2 f x1 x2
             (tie .A .rel1 .i .k .x1 .x2 xRel) =
      mapRel' i k A rel1 rel2 f x1 x2 xRel
  }

}

-- Eq implies GEq.

mutual {

  cofun eqImpliesGEq' :
    [A : Set] -> [rel : -Size -> A -> A -> Set] ->
    [i : Size] -> (x1, x2 : Lift A #) ->
    Rel' A (Eq A rel i) (rel ($ i)) bisim x1 x2 ->
    GEq A rel ($ i) x1 x2
  { eqImpliesGEq' A rel i (now .A .# v1) (now .A .# v2)
      (nowCong' .A .(Eq A rel i) .(rel ($ i)) .bisim .v1 .v2 vRel) =
      nowCong A rel ($ i) sim v1 v2 vRel
  ; eqImpliesGEq' A rel i (later .A .# x1) (later .A .# x2)
      (laterCong' .A .(Eq A rel i) .(rel ($ i)) .x1 .x2 xEq) =
      laterCong A rel i sim x1 x2
        (eqImpliesGEq A rel i x1 x2 xEq)
  ; eqImpliesGEq' A rel i (later .A .# x1) x2
      (laterL' .A .(Eq A rel i) .(rel ($ i)) .bisim .x1 .x2 xEq) =
      laterL A rel ($ i) sim x1 x2
        (eqImpliesGEq' A rel i x1 x2 xEq)
  ; eqImpliesGEq' A rel i x1 (later .A .# x2)
      (laterRB' .A .(Eq A rel i) .(rel ($ i)) .x1 .x2 xEq) =
      laterR A rel ($ i) sim x1 x2
        (eqImpliesGEq' A rel i x1 x2 xEq)
  }

  cofun eqImpliesGEq :
    [A : Set] -> [rel : -Size -> A -> A -> Set] ->
    [i : Size] -> (x1, x2 : Lift A #) ->
    Eq A rel i x1 x2 -> GEq A rel i x1 x2
  { eqImpliesGEq A rel ($ i) x1 x2
      (tie .A .rel .i .bisim .x1 .x2 xEq) =
      eqImpliesGEq' A rel i x1 x2 xEq
  }

}

-- Later can be dropped (but the size may not be preserved).

fun dropLaterR' :
  [i : Size] -> [k : Kind] -> [A : Set] ->
  [rel : -Size -> A -> A -> Set] ->
  (x1, x2 : Lift A #) ->
  Rel' A (Rel A rel i k) (rel ($ i)) k x1 (later A # x2) ->
  Rel A rel i k x1 x2
{ dropLaterR' i .bisim A eq (later .A .# x1) x2
    (laterCong' .A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
    laterL A eq i bisim x1 x2 xEq
; dropLaterR' i .bisim A eq x1 x2
    (laterRB' .A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
    tie A eq i bisim x1 x2 xEq
; dropLaterR' i .sim A geq x1 x2
    (laterRS' .A .(GEq A geq i) .(geq i) .x1 .x2 xGeq) =
    xGeq
; dropLaterR' i k A rel (later .A .# x1) x2
    (laterL' .A .(Rel A rel i k) .(rel ($ i)) .k
             .x1 .(later A # x2) xRel) =
    laterL A rel i k x1 x2 (dropLaterR' i k A rel x1 x2 xRel)
}

fun dropLaterR :
  [i : Size] -> [k : Kind] -> [A : Set] ->
  [rel : -Size -> A -> A -> Set] ->
  (x1, x2 : Lift A #) ->
  Rel A rel ($ i) k x1 (later A # x2) -> Rel A rel i k x1 x2
{ dropLaterR i k A rel x1 x2
    (tie .A .rel .i .k .x1 .(later A # x2) xRel) =
    dropLaterR' i k A rel x1 x2 xRel
}

mutual {

  cofun dropLaterL' :
    [i : Size] -> (k : Kind) -> [A : Set] ->
    [rel : -Size -> A -> A -> Set] ->
    (x1, x2 : Lift A #) ->
    Rel' A (Rel A rel i k) (rel ($ i)) k (later A # x1) x2 ->
    Rel A rel (sucIfSim k i) k x1 x2
  { dropLaterL' i .bisim A eq x1 (later .A .# x2)
      (laterCong' .A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
      laterR A eq i bisim x1 x2 xEq
  ; dropLaterL' i .sim A geq x1 (later .A .# x2)
      (laterRS' .A .(GEq A geq i) .(geq ($ i))
                .(later A # x1) .x2 xGEq) =
      laterR A geq i sim x1 x2 (dropLaterLS i A geq x1 x2 xGEq)
  ; dropLaterL' i .bisim A eq x1 (later .A .# x2)
      (laterRB' .A .(Eq A eq i) .(eq ($ i))
                .(later A # x1) .x2 xEq) =
      laterR A eq i bisim x1 x2 (dropLaterL' i bisim A eq x1 x2 xEq)
  ; dropLaterL' i sim A geq x1 x2
      (laterL' .A .(GEq A geq i) .(geq ($ i)) .sim .x1 .x2 xGEq) =
      tie A geq i sim x1 x2 xGEq
  ; dropLaterL' i bisim A eq x1 x2
      (laterL' .A .(Eq A eq i) .(eq ($ i)) .bisim .x1 .x2 xEq) =
      tie A eq i bisim x1 x2 xEq
  }

  cofun dropLaterLS :
    [i : Size] -> [A : Set] ->
    [geq : -Size -> A -> A -> Set] ->
    (x1, x2 : Lift A #) ->
    GEq A geq i (later A # x1) x2 -> GEq A geq i x1 x2
  { dropLaterLS ($ i) A geq x1 x2
      (tie .A .geq .i .sim .(later A # x1) .x2 xGEq) =
      dropLaterL' i sim A geq x1 x2 xGEq
  }

}

fun dropLaterL :
  [i : Size] -> (k : Kind) -> [A : Set] ->
  [rel : -Size -> A -> A -> Set] ->
  (x1, x2 : Lift A #) ->
  Rel A rel (sucIfBisim k i) k (later A # x1) x2 ->
  Rel A rel i k x1 x2
{ dropLaterL i bisim A eq x1 x2
    (tie .A .eq .i .bisim .(later A # x1) .x2 xEq) =
    dropLaterL' i bisim A eq x1 x2 xEq
; dropLaterL i sim A geq x1 x2 xGEq =
    dropLaterLS i A geq x1 x2 xGEq
}

fun dropLater' :
  [i : Size] -> [k : Kind] -> [A : Set] ->
  [rel : -Size -> A -> A -> Set] ->
  (x1, x2 : Lift A #) ->
  Rel' A (Rel A rel i k) (rel ($ i)) k (later A # x1) (later A # x2) ->
  Rel A rel i k x1 x2
{ dropLater' i .bisim A eq x1 x2
    (laterCong' .A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
    xEq
; dropLater' i .sim A geq x1 x2
    (laterRS' .A .(GEq A geq i) .(geq i) .(later A # x1) .x2 xGEq) =
    dropLaterL i sim A geq x1 x2 xGEq
; dropLater' i .bisim A eq x1 x2
    (laterRB' .A .(Eq A eq i) .(eq i) .(later A # x1) .x2 xEq) =
    dropLaterL' i bisim A eq x1 x2 xEq
; dropLater' i k A rel x1 x2
    (laterL' .A .(Rel A rel i k) .(rel i) .k .x1 .(later A # x2) xRel) =
    dropLaterR' i k A rel x1 x2 xRel
}

fun dropLater :
  [i : Size] -> [k : Kind] -> [A : Set] ->
  [rel : -Size -> A -> A -> Set] ->
  (x1, x2 : Lift A #) ->
  Rel A rel ($ i) k (later A # x1) (later A # x2) ->
  Rel A rel i k x1 x2
{ dropLater i k A rel x1 x2
    (tie .A .rel .i .k .(later A # x1) .(later A # x2) xRel) =
    dropLater' i k A rel x1 x2 xRel
}

-- Weak (bi)similarity is reflexive if the underlying relation is.

cofun reflRel : [i : Size] -> (k : Kind) -> [A : Set] ->
                [rel : -Size -> A -> A -> Set] ->
                ((v : A) -> rel i v v) ->
                (x : Lift A #) -> Rel A rel i k x x
{ reflRel i k A rel relRefl (now .A .# v) =
    nowCong A rel i k v v (relRefl v)
; reflRel ($ i) k A rel relRefl (later .A .# x) =
    laterCong A rel i k x x (reflRel i k A rel relRefl x)
}

-- Weak bisimilarity is symmetric if the underlying relation is.

mutual {

  cofun symEq'' : [i : Size] -> [A : Set] ->
                  [eq : -Size -> A -> A -> Set] ->
                  (x1, x2 : Lift A #) ->
                  Rel' A (Eq A eq i) (eq ($ i)) bisim x1 x2 ->
                  Eq A (Flip A eq) ($ i) x2 x1
  { symEq'' i A eq (now .A .# v1) (now .A .# v2)
      (nowCong' .A .(Eq A eq i) .(eq ($ i)) .bisim .v1 .v2 vEq) =
      nowCong A (Flip A eq) ($ i) bisim v2 v1 vEq
  ; symEq'' i A eq (later .A .# x1) (later .A .# x2)
      (laterCong' .A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
      laterCong A (Flip A eq) i bisim x2 x1 (symEq' i A eq x1 x2 xEq)
  ; symEq'' i .A eq (later .A .# x1) x2
      (laterL' A .(Eq A eq i) .(eq ($ i)) .bisim .x1 .x2 xEq) =
      laterR A (Flip A eq) ($ i) bisim x2 x1 (symEq'' i A eq x1 x2 xEq)
  ; symEq'' i .A eq x1 (later .A .# x2)
      (laterRB' A .(Eq A eq i) .(eq ($ i)) .x1 .x2 xEq) =
      laterL A (Flip A eq) ($ i) bisim x2 x1 (symEq'' i A eq x1 x2 xEq)
  }

  cofun symEq' : [i : Size] -> [A : Set] ->
                 [eq : -Size -> A -> A -> Set] ->
                 (x1, x2 : Lift A #) ->
                 Eq A eq i x1 x2 -> Eq A (Flip A eq) i x2 x1
  { symEq' ($ i) A eq x1 x2 (tie .A .eq .i .bisim .x1 .x2 xEq) =
      symEq'' i A eq x1 x2 xEq
  }

}

cofun symEq : [i : Size] -> [A : Set] ->
              [eq : -Size -> A -> A -> Set] ->
              ([j : Size] -> |j| <= |i| ->
               (v1, v2 : A) -> eq j v1 v2 -> eq j v2 v1) ->
              (x1, x2 : Lift A #) ->
              Eq A eq i x1 x2 -> Eq A eq i x2 x1
{ symEq i A eq eqSym x1 x2 xEq =
    mapRel i bisim A (Flip A eq) eq (\ j v1 v2 -> eqSym j v2 v1) x2 x1
      (symEq' i A eq x1 x2 xEq)
}

-- Weak bisimilarity is transitive if the underlying relation is.
-- However, the size is not necessarily preserved (compare 'The
-- problem of "weak bisimulation up to"').

fun transEqNow : [i : Size] -> [A : Set] ->
                 [eq : -Size -> A -> A -> Set] ->
                 ((v1, v2, v3 : A) ->
                  eq # v1 v2 -> eq # v2 v3 -> eq ($ i) v1 v3) ->
                 (x1, x2 : Lift A #) -> (v3 : A) ->
                 Rel' A (Eq A eq #) (eq #) bisim x1 x2 ->
                 Rel' A (Eq A eq #) (eq #) bisim x2 (now A # v3) ->
                 Eq A eq ($ i) x1 (now A # v3)
{ transEqNow i A eq eqTrans (now .A .# v1) (now .A .# v2) v3
             (nowCong' .A .(Eq A eq #) .(eq #) .bisim .v1 .v2 eq12)
             (nowCong' .A .(Eq A eq #) .(eq #) .bisim .v2 .v3 eq23) =
    nowCong A eq ($ i) bisim v1 v3 (eqTrans v1 v2 v3 eq12 eq23)
; transEqNow i A eq eqTrans (later .A .# x1) x2 v3
             (laterL' .A .(Eq A eq #) .(eq #) .bisim .x1 .x2 eq12)
             eq23 =
    laterL A eq ($ i) bisim x1 (now A # v3)
           (transEqNow i A eq eqTrans x1 x2 v3 eq12 eq23)
; transEqNow i A eq eqTrans x1 (later .A .# x2) v3
    eq12
    (laterL' .A .(Eq A eq #) .(eq #) .bisim .x2 .(now A # v3) eq23) =
    transEqNow i A eq eqTrans x1 x2 v3
      (force A eq # bisim x1 x2 (dropLaterR' # bisim A eq x1 x2 eq12))
      eq23
}

mutual {

  cofun transEqLater : [i : Size] -> [A : Set] ->
                       [eq : -Size -> A -> A -> Set] ->
                       ((v1, v2, v3 : A) ->
                        eq # v1 v2 -> eq # v2 v3 -> eq ($ i) v1 v3) ->
                       (x1, x2, x3 : Lift A #) ->
                       Rel' A (Eq A eq #) (eq #) bisim x1 x2 ->
                       Rel' A (Eq A eq #) (eq #) bisim x2 (later A # x3) ->
                       Eq A eq ($ i) x1 (later A # x3)
  { transEqLater i A eq eqTrans (later .A .# x1) (later .A .# x2) x3
      (laterCong' .A .(Eq A eq #) .(eq #) .x1 .x2 eq12) eq23 =
      laterCong A eq i bisim x1 x3
        (transEq i A eq eqTrans x1 x2 x3
                 eq12 (dropLater' # bisim A eq x2 x3 eq23))
  ; transEqLater i A eq eqTrans (later .A .# x1) x2 x3
      (laterL' .A .(Eq A eq #) .(eq #) .bisim .x1 .x2 eq12) eq23 =
      laterCong A eq i bisim x1 x3
        (transEq i A eq eqTrans x1 x2 x3
                 (tie A eq # bisim x1 x2 eq12)
                 (dropLaterR' # bisim A eq x2 x3 eq23))
  ; transEqLater i A eq eqTrans x1 (later .A .# x2) x3
      (laterRB' .A .(Eq A eq #) .(eq #) .x1 .x2 eq12) eq23 =
      transEqLater i A eq eqTrans x1 x2 x3
        eq12
        (force A eq # bisim x2 (later A # x3)
           (dropLaterL' # bisim A eq x2 (later A # x3) eq23))
  ; transEqLater i A eq eqTrans x1 x2 x3
      eq12 (laterRB' .A .(Eq A eq #) .(eq #) .x2 .x3 eq23) =
      laterR A eq ($ i) bisim x1 x3
        (transEq' ($ i) A eq eqTrans x1 x2 x3 eq12 eq23)
  }

  cofun transEq' : [i : Size] -> [A : Set] ->
                   [eq : -Size -> A -> A -> Set] ->
                   ((v1, v2, v3 : A) ->
                    eq # v1 v2 -> eq # v2 v3 -> eq i v1 v3) ->
                   (x1, x2, x3 : Lift A #) ->
                   Rel' A (Eq A eq #) (eq #) bisim x1 x2 ->
                   Rel' A (Eq A eq #) (eq #) bisim x2 x3 ->
                   Eq A eq i x1 x3
  { transEq' ($ i) A eq eqTrans x1 x2 (now .A .# v3) eq12 eq23 =
      transEqNow i A eq eqTrans x1 x2 v3 eq12 eq23
  ; transEq' ($ i) A eq eqTrans x1 x2 (later .A .# x3) eq12 eq23 =
      transEqLater i A eq eqTrans x1 x2 x3 eq12 eq23
  }

  cofun transEq : [i : Size] -> [A : Set] ->
                  [eq : -Size -> A -> A -> Set] ->
                  ((v1, v2, v3 : A) ->
                   eq # v1 v2 -> eq # v2 v3 -> eq i v1 v3) ->
                  (x1, x2, x3 : Lift A #) ->
                  Eq A eq # x1 x2 -> Eq A eq # x2 x3 -> Eq A eq i x1 x3
  { transEq i A eq eqTrans x1 x2 x3 eq12 eq23 =
      transEq' i A eq eqTrans x1 x2 x3
               (force A eq # bisim x1 x2 eq12)
               (force A eq # bisim x2 x3 eq23)
  }

}

-- Weak similarity is transitive if the underlying relation is.
-- However, this is not proved here. What is proved here is that, if
-- the underlying relation is transitive in such a way that the second
-- size is preserved (for all sizes up to a given limit), then the
-- same applies to weak similarity (for the given limit).

mutual {

  cofun transGEqNow :
          [i : Size] -> [A : Set] ->
          [geq : -Size -> A -> A -> Set] ->
          ([j : Size] -> |j| <= |$ i| -> (v1, v2, v3 : A) ->
           geq # v1 v2 -> geq j v2 v3 -> geq j v1 v3) ->
          (v1 : A) -> (x2, x3 : Lift A #) ->
          Rel' A (GEq A geq #) (geq #)     sim (now A # v1) x2 ->
          Rel' A (GEq A geq i) (geq ($ i)) sim x2 x3 ->
          GEq A geq ($ i) (now A # v1) x3
  { transGEqNow i A geq geqTrans v1 (now .A .# v2) (now .A .# v3)
      (nowCong' .A .(GEq A geq #) .(geq #)     .sim .v1 .v2 geq12)
      (nowCong' .A .(GEq A geq i) .(geq ($ i)) .sim .v2 .v3 geq23) =
      nowCong A geq ($ i) sim v1 v3 (geqTrans ($ i) v1 v2 v3 geq12 geq23)
  ; transGEqNow i A geq geqTrans v1 x2 (later .A .# x3)
      geq12 (laterRS' .A .(GEq A geq i) .(geq ($ i)) .x2 .x3 geq23) =
      laterR A geq i sim (now A # v1) x3
        (transGEq i A geq geqTrans (now A # v1) x2 x3
           (tie A geq # sim (now A # v1) x2 geq12) geq23)
  ; transGEqNow i A geq geqTrans v1 (later .A .# x2) x3
      (laterRS' .A .(GEq A geq i) .(geq ($ i))
                .(now A # v1) .x2 geq12)
      (laterL' .A .(GEq A geq i) .(geq ($ i)) .sim .x2 .x3 geq23) =
      transGEqNow i A geq geqTrans v1 x2 x3
         (force A geq # sim (now A # v1) x2 geq12) geq23
  }

  cofun transGEqLater :
          [i : Size] -> [A : Set] ->
          [geq : -Size -> A -> A -> Set] ->
          ([j : Size] -> |j| <= |$ i| -> (v1, v2, v3 : A) ->
           geq # v1 v2 -> geq j v2 v3 -> geq j v1 v3) ->
          (x1, x2, x3 : Lift A #) ->
          Rel' A (GEq A geq #) (geq #)     sim (later A # x1) x2 ->
          Rel' A (GEq A geq i) (geq ($ i)) sim x2 x3 ->
          GEq A geq ($ i) (later A # x1) x3
  { transGEqLater i A geq geqTrans x1 x2 x3
      (laterL' .A .(GEq A geq #) .(geq #) .sim .x1 .x2 geq12) geq23 =
      laterL A geq ($ i) sim x1 x3
        (transGEq' i A geq geqTrans x1 x2 x3 geq12 geq23)
  ; transGEqLater i A geq geqTrans x1 (later .A .# x2) x3
      (laterRS' .A .(GEq A geq #) .(geq #) .(later A # x1) .x2 geq12)
      (laterL' .A .(GEq A geq i) .(geq ($ i)) .sim .x2 .x3 geq23) =
        transGEqLater i A geq geqTrans x1 x2 x3
          (force A geq # sim (later A # x1) x2 geq12) geq23
  ; transGEqLater i A geq geqTrans x1 x2 (later .A .# x3)
      geq12 (laterRS' .A .(GEq A geq i) .(geq ($ i)) .x2 .x3 geq23) =
      laterCong A geq i sim x1 x3
        (transGEq i A geq geqTrans x1 x2 x3
           (dropLaterL' # sim A geq x1 x2 geq12) geq23)
  }

  cofun transGEq' : [i : Size] -> [A : Set] ->
                    [geq : -Size -> A -> A -> Set] ->
                    ([j : Size] -> |j| <= |$ i| -> (v1, v2, v3 : A) ->
                     geq # v1 v2 -> geq j v2 v3 -> geq j v1 v3) ->
                    (x1, x2, x3 : Lift A #) ->
                    Rel' A (GEq A geq #) (geq #)     sim x1 x2 ->
                    Rel' A (GEq A geq i) (geq ($ i)) sim x2 x3 ->
                    GEq A geq ($ i) x1 x3
  { transGEq' i A geq geqTrans (now .A .# v1) x2 x3 geq12 geq23 =
      transGEqNow i A geq geqTrans v1 x2 x3 geq12 geq23
  ; transGEq' i A geq geqTrans (later .A .# x1) x2 x3 geq12 geq23 =
      transGEqLater i A geq geqTrans x1 x2 x3 geq12 geq23
  }

  cofun transGEq : [i : Size] -> [A : Set] ->
                   [geq : -Size -> A -> A -> Set] ->
                   ([j : Size] -> |j| <= |i| -> (v1, v2, v3 : A) ->
                    geq # v1 v2 -> geq j v2 v3 -> geq j v1 v3) ->
                   (x1, x2, x3 : Lift A #) ->
                   GEq A geq # x1 x2 -> GEq A geq i x2 x3 ->
                   GEq A geq i x1 x3
  { transGEq ($ i) A geq geqTrans x1 x2 x3 geq12 geq23 =
      transGEq' i A geq geqTrans x1 x2 x3
                (force A geq # sim x1 x2 geq12)
                (force A geq i sim x2 x3 geq23)
  }

}

------------------------------------------------------------------------
-- * Weak bisimilarity can be defined using weak similarity

-- An alternative definition of weak bisimilarity.

data EqUsingGEq (A : Set) (eq1, eq2 : -Size -> A -> A -> Set)
                -(i : Size) *(x1, x2 : Lift A #) : Set
{ geqAndGEq :
    GEq A eq1 i x1 x2 -> GEq A eq2 i x2 x1 ->
    EqUsingGEq A eq1 eq2 i x1 x2
}

-- The definition is complete with respect to the one above.

fun eqUsingGEqComplete :
  [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] -> [i : Size] ->
  ([j : Size] -> |j| <= |i| -> (v1, v2 : A) ->
   eq j v1 v2 -> eq1 j v1 v2) ->
  ([j : Size] -> |j| <= |i| -> (v1, v2 : A) ->
   eq j v1 v2 -> eq2 j v2 v1) ->
  (x1, x2 : Lift A #) ->
  Eq A eq i x1 x2 -> EqUsingGEq A eq1 eq2 i x1 x2
{ eqUsingGEqComplete A eq eq1 eq2 i hyp1 hyp2 x1 x2 xEq =
    geqAndGEq A eq1 eq2 i x1 x2
      (eqImpliesGEq A eq1 i x1 x2
         (mapRel i bisim A eq eq1 hyp1 x1 x2 xEq))
      (eqImpliesGEq A eq2 i x2 x1
         (mapRel i bisim A (Flip A eq) eq2
            (\ j v1 v2 -> hyp2 j v2 v1) x2 x1
            (symEq' i A eq x1 x2 xEq)))
}

-- The definition is sound with respect to the one above (but the size
-- may not be preserved).

fun eqUsingGEqSoundNow :
  [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] -> [i : Size] ->
  ((v1, v2 : A) -> eq1 # v1 v2 -> eq2 # v2 v1 -> eq ($ i) v1 v2) ->
  (x1 : Lift A #) -> (v2 : A) ->
  Rel' A (GEq A eq1 #) (eq1 #) sim x1 (now A # v2) ->
  Rel' A (GEq A eq2 #) (eq2 #) sim (now A # v2) x1 ->
  Eq A eq ($ i) x1 (now A # v2)
{ eqUsingGEqSoundNow A eq eq1 eq2 i hyp (now .A .# v1) v2
    (nowCong' .A .(GEq A eq1 i) .(eq1 ($ i)) .sim .v1 .v2 vEq12)
    (nowCong' .A .(GEq A eq2 #) .(eq2 #)     .sim .v2 .v1 vEq21) =
    nowCong A eq ($ i) bisim v1 v2 (hyp v1 v2 vEq12 vEq21)
; eqUsingGEqSoundNow A eq eq1 eq2 i hyp (later .A .# x1) v2
    (laterL' .A .(GEq A eq1 i) .(eq1 ($ i)) .sim .x1 .(now A # v2) xvEq)
    (laterRS' .A .(GEq A eq2 #) .(eq2 #) .(now A # v2) .x1 vxEq) =
    laterL A eq ($ i) bisim x1 (now A # v2)
      (eqUsingGEqSoundNow A eq eq1 eq2 i hyp x1 v2
         xvEq (force A eq2 # sim (now A # v2) x1 vxEq))
}

mutual {

  cofun eqUsingGEqSoundLater :
    [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] ->
    [i : Size] ->
    ((v1, v2 : A) -> eq1 # v1 v2 -> eq2 # v2 v1 -> eq ($ i) v1 v2) ->
    (x1, x2 : Lift A #) ->
    Rel' A (GEq A eq1 #) (eq1 #) sim x1 (later A # x2) ->
    Rel' A (GEq A eq2 #) (eq2 #) sim (later A # x2) x1 ->
    Eq A eq ($ i) x1 (later A # x2)
  { eqUsingGEqSoundLater A eq eq1 eq2 i hyp (later .A .# x1) x2
      (laterL' .A .(GEq A eq1 #) .(eq1 #) .sim
               .x1 .(later A # x2) xGEq1)
      xGEq2 =
      laterCong A eq i bisim x1 x2
        (eqUsingGEqSound' A eq eq1 eq2 i hyp x1 x2
           (dropLaterR' # sim A eq1 x1 x2 xGEq1)
           (dropLater'  # sim A eq2 x2 x1 xGEq2))
  ; eqUsingGEqSoundLater A eq eq1 eq2 i hyp x1 x2
      (laterRS' .A .(GEq A eq1 #) .(eq1 #) .x1 .x2 xGEq1)
      (laterL' .A .(GEq A eq2 #) .(eq2 #) .sim .x2 .x1 xGEq2) =
      laterR A eq ($ i) bisim x1 x2
        (eqUsingGEqSound'' A eq eq1 eq2 i hyp x1 x2
           (force A eq1 # sim x1 x2 xGEq1) xGEq2)
  ; eqUsingGEqSoundLater A eq eq1 eq2 i hyp (later .A .# x1) x2
      (laterRS' .A .(GEq A eq1 #) .(eq1 #) .(later A # x1) .x2 xGEq1)
      (laterRS' .A .(GEq A eq2 #) .(eq2 #) .(later A # x2) .x1 xGEq2) =
      laterCong A eq i bisim x1 x2
        (eqUsingGEqSound' A eq eq1 eq2 i hyp x1 x2
           (dropLaterL # sim A eq1 x1 x2 xGEq1)
           (dropLaterL # sim A eq2 x2 x1 xGEq2))
  }

  cofun eqUsingGEqSound'' :
    [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] ->
    [i : Size] ->
    ((v1, v2 : A) -> eq1 # v1 v2 -> eq2 # v2 v1 -> eq ($ i) v1 v2) ->
    (x1, x2 : Lift A #) ->
    Rel' A (GEq A eq1 #) (eq1 #) sim x1 x2 ->
    Rel' A (GEq A eq2 #) (eq2 #) sim x2 x1 ->
    Eq A eq ($ i) x1 x2
  { eqUsingGEqSound'' A eq eq1 eq2 i hyp x1 (now .A .# v2) xvGEq vxGEq =
      eqUsingGEqSoundNow A eq eq1 eq2 i hyp x1 v2 xvGEq vxGEq
  ; eqUsingGEqSound'' A eq eq1 eq2 i hyp x1 (later .A .# x2)
      xGEq1 xGEq2 =
      eqUsingGEqSoundLater A eq eq1 eq2 i hyp x1 x2 xGEq1 xGEq2
  }

  cofun eqUsingGEqSound' :
    [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] ->
    [i : Size] ->
    ((v1, v2 : A) -> eq1 # v1 v2 -> eq2 # v2 v1 -> eq i v1 v2) ->
    (x1, x2 : Lift A #) ->
    GEq A eq1 # x1 x2 -> GEq A eq2 # x2 x1 -> Eq A eq i x1 x2
  { eqUsingGEqSound' A eq eq1 eq2 ($ i) hyp x1 x2 xGEq1 xGEq2 =
      eqUsingGEqSound'' A eq eq1 eq2 i hyp x1 x2
        (force A eq1 # sim x1 x2 xGEq1)
        (force A eq2 # sim x2 x1 xGEq2)
  }

}

fun eqUsingGEqSound :
  [A : Set] -> [eq, eq1, eq2 : -Size -> A -> A -> Set] ->
  ((v1, v2 : A) -> eq1 # v1 v2 -> eq2 # v2 v1 -> eq # v1 v2) ->
  (x1, x2 : Lift A #) ->
  EqUsingGEq A eq1 eq2 # x1 x2 -> Eq A eq # x1 x2
{ eqUsingGEqSound A eq eq1 eq2 hyp x1 x2
    (geqAndGEq .A .eq1 .eq2 .# .x1 .x2 xGEq1 xGEq2) =
    eqUsingGEqSound' A eq eq1 eq2 # hyp x1 x2 xGEq1 xGEq2
}

------------------------------------------------------------------------
-- * Some congruences

-- Bind preserves weak (bi)similarity.

mutual {

  cofun bindCong' :
          [i : Size] -> [k : Kind] -> [A, B : Set] ->
          [relA : -Size -> A -> A -> Set] ->
          [relB : -Size -> B -> B -> Set] ->
          (x1, x2 : Lift A #) -> [f1, f2 : A -> Lift B #] ->
          Rel' A (Rel A relA i k) (relA ($ i)) k x1 x2 ->
          ([j : Size] -> |j| <= |$ i| -> (v1, v2 : A) ->
           relA j v1 v2 -> Rel B relB j k (f1 v1) (f2 v2)) ->
          Rel B relB ($ i) k (bind A B # x1 f1) (bind A B # x2 f2)
  { bindCong' i k A B relA relB (now .A .# v1) (now .A .# v2) f1 f2
      (nowCong' .A .(Rel A relA i k) .(relA ($ i)) .k .v1 .v2 vRel)
      fRel =
      fRel ($ i) v1 v2 vRel
  ; bindCong' i .bisim A B eqA eqB
      (later .A .# x1) (later .A .# x2) f1 f2
      (laterCong' .A .(Eq A eqA i) .(eqA ($ i)) .x1 .x2 xEq) fEq =
      laterCong B eqB i bisim (bind A B # x1 f1) (bind A B # x2 f2)
                (bindCong i bisim A B eqA eqB x1 x2 f1 f2 xEq fEq)
  ; bindCong' i k .A B relA relB (later .A .# x1) x2 f1 f2
      (laterL' A .(Rel A relA i k) .(relA ($ i)) .k .x1 .x2 xRel) fRel =
      laterL B relB ($ i) k (bind A B # x1 f1) (bind A B # x2 f2)
             (bindCong' i k A B relA relB x1 x2 f1 f2 xRel fRel)
  ; bindCong' i .bisim .A B eqA eqB x1 (later .A .# x2) f1 f2
      (laterRB' A .(Eq A eqA i) .(eqA ($ i)) .x1 .x2 xEq) fEq =
      laterR B eqB ($ i) bisim (bind A B # x1 f1) (bind A B # x2 f2)
             (bindCong' i bisim A B eqA eqB x1 x2 f1 f2 xEq fEq)
  ; bindCong' i .sim .A B geqA geqB x1 (later .A .# x2) f1 f2
      (laterRS' A .(GEq A geqA i) .(geqA ($ i)) .x1 .x2 xGEq) fGEq =
      laterR B geqB i sim (bind A B # x1 f1) (bind A B # x2 f2)
             (bindCong i sim A B geqA geqB x1 x2 f1 f2 xGEq fGEq)
  }

  cofun bindCong :
          [i : Size] -> [k : Kind] -> [A, B : Set] ->
          [relA : -Size -> A -> A -> Set] ->
          [relB : -Size -> B -> B -> Set] ->
          (x1, x2 : Lift A #) -> [f1, f2 : A -> Lift B #] ->
          Rel A relA i k x1 x2 ->
          ([j : Size] -> |j| <= |i| -> (v1, v2 : A) ->
           relA j v1 v2 -> Rel B relB j k (f1 v1) (f2 v2)) ->
          Rel B relB i k (bind A B # x1 f1) (bind A B # x2 f2)
  { bindCong ($ i) k A B relA relB x1 x2 f1 f2
             (tie .A .relA .i .k .x1 .x2 xRel) fRel =
      bindCong' i k A B relA relB x1 x2 f1 f2 xRel fRel
  }

}

-- A specialised variant of bindCong.

fun bindCongId : [i : Size] -> [k : Kind] -> [A, B : Set] ->
                 [relB : -Size -> B -> B -> Set] ->
                 (x1, x2 : Lift A #) -> [f1, f2 : A -> Lift B #] ->
                 Rel A (\ j -> Id A) i k x1 x2 ->
                 ((v : A) -> Rel B relB i k (f1 v) (f2 v)) ->
                 Rel B relB i k (bind A B # x1 f1) (bind A B # x2 f2)
{ bindCongId i k A B relB x1 x2 f1 f2 xRel fRel =
    bindCong i k A B (\ j -> Id A) relB x1 x2 f1 f2 xRel
             (\ j v1 v2 vRel ->
                  subst A v1 v2 vRel
                        (\ v -> Rel B relB j k (f1 v1) (f2 v))
                        (fRel v1))
}

-- ifZero preserves weak (bi)similarity.

fun ifZeroCong :
      [A : Set] -> [k : Kind] -> [rel : -Size -> A -> A -> Set] ->
      [i : Size] -> [x1, x2, y1, y2 : Lift A #] ->
      (n : Nat) -> Rel A rel i k x1 x2 -> Rel A rel i k y1 y2 ->
      Rel A rel i k (ifZero (Lift A #) n x1 y1)
                    (ifZero (Lift A #) n x2 y2)
{ ifZeroCong A rel i k x1 x2 y1 y2 zero    xRel yRel = xRel
; ifZeroCong A rel i k x1 x2 y1 y2 (suc n) xRel yRel = yRel
}

------------------------------------------------------------------------
-- * A simply typed lambda-calculus with a fixpoint operator

-- Types.

data Ty : Set
{ nat : Ty
; arr : Ty -> Ty -> Ty
}

-- Contexts.

data Ctxt : Set
{ empty : Ctxt
; snoc  : Ctxt -> Ty -> Ctxt
}

-- Well-typed terms.

data Tm : Ctxt -> Ty -> Set
{ vz  : [G : Ctxt] -> [   b : Ty] -> Tm (snoc G b) b
; wk  : [G : Ctxt] -> [a, b : Ty] -> Tm G b -> Tm (snoc G a) b
; lam : [G : Ctxt] -> [a, b : Ty] -> Tm (snoc G a) b -> Tm G (arr a b)
; app : [G : Ctxt] -> [a, b : Ty] -> Tm G (arr a b) -> Tm G a -> Tm G b
; fix : [G : Ctxt] -> [a, b : Ty] -> Tm G (arr (arr a b) (arr a b)) -> Tm G a -> Tm G b
; z   : [G : Ctxt]                -> Tm G nat
; s   : [G : Ctxt]                -> Tm G nat -> Tm G nat
; p   : [G : Ctxt]                -> Tm G nat -> Tm G nat
; ifZ : [G : Ctxt] -> [   b : Ty] -> Tm G nat -> Tm G b -> Tm G b -> Tm G b
}

------------------------------------------------------------------------
-- * Environments and values

-- Environments and values are defined as a single family, indexed by
-- a "flag".

data Flag : Set
{ env : Flag
; val : Flag
}

-- The environment-value family has another index as well, given by
-- the following type.

fun Index : Flag -> Set
{ Index env = Ctxt
; Index val = Ty
}

-- The environment-value family.

data EnvOrVal : (f : Flag) -> Index f -> Set
{ emptyE : EnvOrVal env empty
; snocE  : [G : Ctxt] -> [b : Ty] -> EnvOrVal env G -> EnvOrVal val b -> EnvOrVal env (snoc G b)
; natV   : Nat -> EnvOrVal val nat
; arrV   : [G : Ctxt] -> [a, b : Ty] -> Tm (snoc G a) b -> EnvOrVal env G -> EnvOrVal val (arr a b)
}

-- Environments.

fun Env : Ctxt -> Set
{ Env = EnvOrVal env
}

-- Values.

fun Value : Ty -> Set
{ Value = EnvOrVal val
}

-- A helper function.

fun unNatV : Value nat -> Nat
{ unNatV (natV n) = n
}

------------------------------------------------------------------------
-- * Operational semantics

-- A helper function, used to define the semantics of the fixpoint
-- operator.

fun fixV : [a, b : Ty] ->
           Value (arr (arr a b) (arr a b)) -> Value (arr a b)
{ fixV a b f =
    let [abab : Ty] = arr (arr a b) (arr a b) in
    let [G : Ctxt]  = snoc empty abab         in
    arrV G a b
         (fix (snoc G a) a b
              (wk G a abab (vz empty abab))
              (vz G a))
         (snocE empty abab emptyE f)
}

mutual {

  -- Operational semantics. Note that I have chosen to make p
  -- (predecessor) a total operation.

  cofun sem : [i : Size] -> [G : Ctxt] -> [b : Ty] ->
              Tm G b -> Env G -> Lift (Value b) i
  { sem i .(snoc G b) .b         (vz G b)           (snocE .G .b rho v) = now (Value b) i v
  ; sem i .(snoc G a) .b         (wk G a b t)       (snocE .G .a rho v) = sem i G b t rho
  ; sem i .G          .(arr a b) (lam G a b t)      rho                 = now (Value (arr a b)) i (arrV G a b t rho)
  ; sem i .G          .b         (app G a b t1 t2)  rho                 =
     bind (Value (arr a b)) (Value b) i (sem i G (arr a b) t1 rho) (\ f ->
     bind (Value a)         (Value b) i (sem i G a         t2 rho) (\ v ->
     appV i a b f v))
  ; sem i .G          .b         (fix G a b t1 t2)  rho                 =
     let [abab : Ty] = arr (arr a b) (arr a b) in
     bind (Value abab)      (Value b) i (sem i G abab t1 rho)                       (\ f ->
     bind (Value a)         (Value b) i (sem i G a    t2 rho)                       (\ v ->
     bind (Value (arr a b)) (Value b) i (appV i (arr a b) (arr a b) f (fixV a b f)) (\ g ->
     appV i a b g v)))
  ; sem i .G          .nat       (z G)              rho                 = now (Value nat) i (natV zero)
  ; sem i .G          .nat       (s G t)            rho                 =
     bind (Value nat) (Value nat) i (sem i G nat t rho) (\ n ->
     now (Value nat) i (natV (suc (unNatV n))))
  ; sem i .G          .nat       (p G t)            rho                 =
     bind (Value nat) (Value nat) i (sem i G nat t rho) (\ n ->
     now (Value nat) i (natV (pred (unNatV n))))
  ; sem i .G          .b         (ifZ G b t1 t2 t3) rho                 =
     bind (Value nat) (Value b) i (sem i G nat t1 rho) (\ n ->
     ifZero (Lift (Value b) i) (unNatV n) (sem i G b t2 rho)
                                          (sem i G b t3 rho))
  }

  -- Value application.

  cofun appV : [i : Size] -> [a, b : Ty] ->
               Value (arr a b) -> Value a -> Lift (Value b) i
  { appV ($ i) .a .b (arrV G a b t1 rho) v2 =
     later (Value b) i (sem i (snoc G a) b t1 (snocE G a rho v2))
  }

}

------------------------------------------------------------------------
-- * Equality (and inequality)

mutual {

  -- Equality of computations.

  fun EqL : (a : Ty) -> ^Kind -> -Size ->
            Lift (Value a) # -> Lift (Value a) # -> Set
  { EqL a k i x y = Rel (Value a) (EqV a k) i k x y
  }

  -- Equality of values. I wanted to use a parametric (LF) function
  -- space in the function space case (to avoid proofs which destruct
  -- their inputs), but the current version of MiniAgda doesn't allow
  -- this. Thorsten Altenkirch informed me that one can encode
  -- parametric function spaces using Kripke models (Hofmann, LICS
  -- 1999), and this seems to work better.
  --
  -- Note that the inequality seems to be very closely related to
  -- step-indexed logical relations; one difference is that <= is used
  -- instead of <. The inequality also seems to be closely related to
  -- Koutavas-Wand bisimilarity (see "Relating step-indexed logical
  -- relations and bisimulations" by Vytiniotis and Koutavas).

  fun EqV : (a : Ty) -> ^Kind -> -Size -> Value a -> Value a -> Set
  { EqV nat       k i n1                      n2                      =
      Id (Value nat) n1 n2
  ; EqV (arr a b) k i (arrV G1 .a .b t1 rho1) (arrV G2 .a .b t2 rho2) =
      [j : Size] ->
      |j| <= |i| ->
      (v1, v2 : Value a) ->
      EqV a k j v1 v2 ->
      EqL b k j (sem # (snoc G1 a) b t1 (snocE G1 a rho1 v1))
                (sem # (snoc G2 a) b t2 (snocE G2 a rho2 v2))
  }

}

-- Equality of environments.

data EqEnv (k : Kind) -(i : Size) : (G : Ctxt) -> Env G -> Env G -> Set
{ emptyEq : EqEnv k i empty emptyE emptyE
; snocEq  : [G : Ctxt] -> [b : Ty] ->
            (rho1, rho2 : Env G) -> (v1, v2 : Value b) ->
            EqEnv k i G rho1 rho2 -> EqV b k i v1 v2 ->
            EqEnv k i (snoc G b) (snocE G b rho1 v1) (snocE G b rho2 v2)
}

-- Equality of terms.

fun EqT : ^Kind -> -Size -> (G : Ctxt) -> (b : Ty) ->
          Tm G b -> Tm G b -> Set
{ EqT k i G b t1 t2 = [j : Size] -> |j| <= |i| ->
                      (rho1, rho2 : Env G) ->
                      EqEnv k j G rho1 rho2 ->
                      EqL b k j (sem # G b t1 rho1) (sem # G b t2 rho2)
}

------------------------------------------------------------------------
-- * Key lemmas

-- Application preserves equality.

fun appVCong : (k : Kind) -> [i : Size] -> [a, b : Ty] ->
               [f1, f2 : Value (arr a b)] -> (v1, v2 : Value a) ->
               EqV (arr a b) k i f1 f2 -> EqV a k i v1 v2 ->
               EqL b k ($ i) (appV # a b f1 v1) (appV # a b f2 v2)
{ appVCong k i a b
           (arrV G1 .a .b t1 rho1) (arrV G2 .a .b t2 rho2) v1 v2
           fEq vEq =
    laterCong (Value b) (EqV b k) i k
              (sem # (snoc G1 a) b t1 (snocE G1 a rho1 v1))
              (sem # (snoc G2 a) b t2 (snocE G2 a rho2 v2))
              (fEq i v1 v2 vEq)
}

-- fixV preserves equality.

cofun fixVCong : (k : Kind) -> [i : Size] -> [a, b : Ty] ->
                 (f1, f2 : Value (arr (arr a b) (arr a b))) ->
                 EqV (arr (arr a b) (arr a b)) k i f1 f2 ->
                 EqV (arr a b) k i (fixV a b f1) (fixV a b f2)
{ fixVCong k ($ i) a b f1 f2 fEq = \ j v1 v2 vEq ->
    bindCong j k (Value (arr a b)) (Value b) (EqV (arr a b) k) (EqV b k)
             (appV # (arr a b) (arr a b) f1 (fixV a b f1))
             (appV # (arr a b) (arr a b) f2 (fixV a b f2))
             (\ g1 -> appV # a b g1 v1)
             (\ g2 -> appV # a b g2 v2)
             (appVCong k i (arr a b) (arr a b)
                       f1 f2 (fixV a b f1) (fixV a b f2)
                       fEq (fixVCong k i a b f1 f2 fEq))
             (\ l g1 g2 gEq ->
                appVCong k l a b g1 g2 v1 v2 gEq vEq)
}

------------------------------------------------------------------------
-- * Term equality is compatible

data EqTCong (k : Kind) -(i : Size) :
             [G : Ctxt] -> [b : Ty] -> Tm G b -> Tm G b -> Set
{ congComplete : [G : Ctxt] -> [b : Ty] -> (t1, t2 : Tm G b) ->
                 EqT k i G b t1 t2 -> EqTCong k i G b t1 t2
; vzCong       : [G : Ctxt] -> [b : Ty] ->
                 EqTCong k i (snoc G b) b (vz G b) (vz G b)
; wkCong       : [G : Ctxt] -> [a, b : Ty] -> (t1, t2 : Tm G b) ->
                 EqTCong k i G b t1 t2 ->
                 EqTCong k i (snoc G a) b (wk G a b t1) (wk G a b t2)
; lamCong      : [G : Ctxt] -> [a, b : Ty] ->
                 (t1, t2 : Tm (snoc G a) b) ->
                 EqTCong k i (snoc G a) b t1 t2 ->
                 EqTCong k i G (arr a b) (lam G a b t1) (lam G a b t2)
; appCong      : [G : Ctxt] -> [a, b : Ty] ->
                 (t1, t2 : Tm G (arr a b)) -> (t3, t4 : Tm G a) ->
                 EqTCong k i G (arr a b) t1 t2 ->
                 EqTCong k i G a t3 t4 ->
                 EqTCong k i G b (app G a b t1 t3) (app G a b t2 t4)
; fixCong      : [G : Ctxt] -> [a, b : Ty] ->
                 (t1, t2 : Tm G (arr (arr a b) (arr a b))) ->
                 (t3, t4 : Tm G a) ->
                 EqTCong k i G (arr (arr a b) (arr a b)) t1 t2 ->
                 EqTCong k i G a t3 t4 ->
                 EqTCong k i G b (fix G a b t1 t3) (fix G a b t2 t4)
; zCong        : [G : Ctxt] -> EqTCong k i G nat (z G) (z G)
; sCong        : [G : Ctxt] -> (t1, t2 : Tm G nat) ->
                 EqTCong k i G nat t1 t2 ->
                 EqTCong k i G nat (s G t1) (s G t2)
; pCong        : [G : Ctxt] -> (t1, t2 : Tm G nat) ->
                 EqTCong k i G nat t1 t2 ->
                 EqTCong k i G nat (p G t1) (p G t2)
; ifZCong      : [G : Ctxt] -> [b : Ty] ->
                 (t1, t2 : Tm G nat) -> (t3, t4, t5, t6 : Tm G b) ->
                 EqTCong k i G nat t1 t2 ->
                 EqTCong k i G b t3 t4 -> EqTCong k i G b t5 t6 ->
                 EqTCong k i G b (ifZ G b t1 t3 t5) (ifZ G b t2 t4 t6)
}

fun congSound : (k : Kind) -> [i : Size] -> [G : Ctxt] -> [b : Ty] ->
                (t1, t2 : Tm G b) ->
                EqTCong k i G b t1 t2 -> EqT k i G b t1 t2
{ congSound k .i .(snoc G b) .b .(vz G b) .(vz G b) (vzCong .k i G b)
            .j (snocE .G .b rho1 v1) (snocE .G .b rho2 v2)
        (snocEq .k j .G .b .rho1 .rho2 .v1 .v2 rhoEq vEq) =
    nowCong (Value b) (EqV b k) j k v1 v2 vEq
; congSound k .i .(snoc G a) .b (wk .G .a .b t1) (wk .G .a .b t2)
            (wkCong .k i G a b .t1 .t2 tEq)
            j (snocE .G .a rho1 v1) (snocE .G .a rho2 v2)
            (snocEq .k .j .G .a .rho1 .rho2 .v1 .v2 rhoEq vEq) =
    congSound k i G b t1 t2 tEq j rho1 rho2 rhoEq
; congSound k .i .G .(arr a b) (lam .G .a .b t1) (lam .G .a .b t2)
            (lamCong .k i G a b .t1 .t2 tEq) j rho1 rho2 rhoEq =
    nowCong (Value (arr a b)) (EqV (arr a b) k) j k
            (arrV G a b t1 rho1)
            (arrV G a b t2 rho2)
            (\ l v1 v2 vEq ->
    congSound k l (snoc G a) b t1 t2 tEq l
          (snocE G a rho1 v1)
          (snocE G a rho2 v2)
          (snocEq k l G a rho1 rho2 v1 v2 rhoEq vEq))
; congSound k .i .G .b (app .G .a .b t1 t3) (app .G .a .b t2 t4)
            (appCong .k i G a b .t1 .t2 .t3 .t4 tEq1 tEq2)
            j rho1 rho2 rhoEq =
    bindCong j k (Value (arr a b)) (Value b) (EqV (arr a b) k) (EqV b k)
             (sem # G (arr a b) t1 rho1)
             (sem # G (arr a b) t2 rho2)
             (\ f -> bind (Value a) (Value b) # (sem # G a t3 rho1) (\ v -> appV # a b f v))
             (\ f -> bind (Value a) (Value b) # (sem # G a t4 rho2) (\ v -> appV # a b f v))
             (congSound k i G (arr a b) t1 t2 tEq1 j rho1 rho2 rhoEq)
             (\ l f1 f2 fEq ->
    bindCong l k (Value a) (Value b) (EqV a k) (EqV b k)
             (sem # G a t3 rho1)
             (sem # G a t4 rho2)
             (appV # a b f1)
             (appV # a b f2)
             (congSound k i G a t3 t4 tEq2 l rho1 rho2 rhoEq)
             (\ m v1 v2 vEq ->
    appVCong k m a b f1 f2 v1 v2 fEq vEq))
; congSound k .i .G .b (fix .G .a .b t1 t3) (fix .G .a .b t2 t4)
            (fixCong .k i G a b .t1 .t2 .t3 .t4 tEq1 tEq2)
            j rho1 rho2 rhoEq =
    let [abab : Ty] = arr (arr a b) (arr a b) in
    bindCong j k (Value abab) (Value b) (EqV abab k) (EqV b k)
             (sem # G abab t1 rho1)
             (sem # G abab t2 rho2)
             (\ f1 -> bind (Value a)         (Value b) # (sem # G a t3 rho1)                           (\ v ->
                      bind (Value (arr a b)) (Value b) # (appV # (arr a b) (arr a b) f1 (fixV a b f1)) (\ g ->
                      appV # a b g v)))
             (\ f2 -> bind (Value a)         (Value b) # (sem # G a t4 rho2)                           (\ v ->
                      bind (Value (arr a b)) (Value b) # (appV # (arr a b) (arr a b) f2 (fixV a b f2)) (\ g ->
                      appV # a b g v)))
             (congSound k i G abab t1 t2 tEq1 j rho1 rho2 rhoEq)
             (\ l f1 f2 fEq ->
    bindCong l k (Value a) (Value b) (EqV a k) (EqV b k)
             (sem # G a t3 rho1)
             (sem # G a t4 rho2)
             (\ v -> bind (Value (arr a b)) (Value b) # (appV # (arr a b) (arr a b) f1 (fixV a b f1)) (\ g ->
                     appV # a b g v))
             (\ v -> bind (Value (arr a b)) (Value b) # (appV # (arr a b) (arr a b) f2 (fixV a b f2)) (\ g ->
                     appV # a b g v))
             (congSound k i G a t3 t4 tEq2 l rho1 rho2 rhoEq)
             (fixVCong k l a b f1 f2 fEq))
; congSound k .i .G .nat (z .G) (z .G) (zCong .k i G) j rho1 rho2 rhoEq =
    nowCong (Value nat) (EqV nat k) j k
            (natV zero) (natV zero) (reflId (Value nat) (natV zero))
; congSound k .i .G .nat (s .G t1) (s .G t2)
            (sCong .k i G .t1 .t2 tEq) j rho1 rho2 rhoEq =
    bindCongId j k (Value nat) (Value nat) (EqV nat k)
               (sem # G nat t1 rho1)
               (sem # G nat t2 rho2)
               (\ n -> now (Value nat) # (natV (suc (unNatV n))))
               (\ n -> now (Value nat) # (natV (suc (unNatV n))))
               (congSound k i G nat t1 t2 tEq j rho1 rho2 rhoEq)
               (\ n ->
    nowCong (Value nat) (EqV nat k) j k
            (natV (suc (unNatV n))) (natV (suc (unNatV n)))
            (reflId (Value nat) (natV (suc (unNatV n)))))
; congSound k .i .G .nat (p .G t1) (p .G t2)
            (pCong .k i G .t1 .t2 tEq) j rho1 rho2 rhoEq =
    bindCongId j k (Value nat) (Value nat) (EqV nat k)
               (sem # G nat t1 rho1)
               (sem # G nat t2 rho2)
               (\ n -> now (Value nat) # (natV (pred (unNatV n))))
               (\ n -> now (Value nat) # (natV (pred (unNatV n))))
               (congSound k i G nat t1 t2 tEq j rho1 rho2 rhoEq)
               (\ n ->
    nowCong (Value nat) (EqV nat k) j k
            (natV (pred (unNatV n))) (natV (pred (unNatV n)))
            (reflId (Value nat) (natV (pred (unNatV n)))))
; congSound k .i .G .b (ifZ .G .b t1 t3 t5) (ifZ .G .b t2 t4 t6)
            (ifZCong .k i G b .t1 .t2 .t3 .t4 .t5 .t6 tEq1 tEq2 tEq3)
            j rho1 rho2 rhoEq =
    bindCongId j k (Value nat) (Value b) (EqV b k)
               (sem # G nat t1 rho1)
               (sem # G nat t2 rho2)
               (\ n -> ifZero (Lift (Value b) #) (unNatV n) (sem # G b t3 rho1) (sem # G b t5 rho1))
               (\ n -> ifZero (Lift (Value b) #) (unNatV n) (sem # G b t4 rho2) (sem # G b t6 rho2))
               (congSound k i G nat t1 t2 tEq1 j rho1 rho2 rhoEq)
               (\ n ->
    ifZeroCong (Value b) k (EqV b k) j
               (sem # G b t3 rho1) (sem # G b t4 rho2)
               (sem # G b t5 rho1) (sem # G b t6 rho2)
               (unNatV n)
               (congSound k i G b t3 t4 tEq2 j rho1 rho2 rhoEq)
               (congSound k i G b t5 t6 tEq3 j rho1 rho2 rhoEq))
}

------------------------------------------------------------------------
-- * Reflexivity

fun reflTCong : [k : Kind] -> [G : Ctxt] -> [b : Ty] ->
                (t : Tm G b) -> EqTCong k # G b t t
{ reflTCong k .(snoc G b) .b (vz G b) = vzCong k # G b
; reflTCong k .(snoc G a) .b (wk G a b t) =
    wkCong k # G a b t t (reflTCong k G b t)
; reflTCong k .G .(arr a b) (lam G a b t) =
    lamCong k # G a b t t (reflTCong k (snoc G a) b t)
; reflTCong k .G .b (app G a b t1 t2) =
    appCong k # G a b t1 t1 t2 t2
      (reflTCong k G (arr a b) t1) (reflTCong k G a t2)
; reflTCong k .G .b (fix G a b t1 t2) =
    fixCong k # G a b t1 t1 t2 t2
      (reflTCong k G (arr (arr a b) (arr a b)) t1) (reflTCong k G a t2)
; reflTCong k .G .nat (z G) = zCong k # G
; reflTCong k .G .nat (s G t) = sCong k # G t t (reflTCong k G nat t)
; reflTCong k .G .nat (p G t) = pCong k # G t t (reflTCong k G nat t)
; reflTCong k .G .b (ifZ G b t1 t2 t3) =
    ifZCong k # G b t1 t1 t2 t2 t3 t3
      (reflTCong k G nat t1) (reflTCong k G b t2) (reflTCong k G b t3)
}

fun reflT : (k : Kind) -> [i : Size] -> [G : Ctxt] -> [b : Ty] ->
            (t : Tm G b) -> EqT k i G b t t
{ reflT k i G b t = congSound k # G b t t (reflTCong k G b t)
}

mutual {

  fun reflV : [a : Ty] -> (k : Kind) -> (v : Value a) -> EqV a k # v v
  { reflV .nat       k (natV n)           = reflId (Value nat) (natV n)
  ; reflV .(arr a b) k (arrV G a b t rho) = \ j v1 v2 vEq ->
      reflT k j (snoc G a) b t j
            (snocE G a rho v1)
            (snocE G a rho v2)
            (snocEq k j G a rho rho v1 v2 (reflEnv k G rho) vEq)
  }

  fun reflEnv : (k : Kind) -> [G : Ctxt] ->
                (rho : Env G) -> EqEnv k # G rho rho
  { reflEnv k .empty      emptyE            = emptyEq k #
  ; reflEnv k .(snoc G a) (snocE G a rho v) =
      snocEq k # G a rho rho v v (reflEnv k G rho) (reflV a k v)
  }

}

fun reflL : [a : Ty] -> (k : Kind) ->
            (x : Lift (Value a) #) -> EqL a k # x x
{ reflL a k x = reflRel # k (Value a) (EqV a k) (reflV a k) x
}

------------------------------------------------------------------------
-- * Contexts with zero or more holes (all of the same type)

data Context (G1 : Ctxt) (c : Ty) : Ctxt -> Ty -> Set
{ hole : Context G1 c G1 c
; vzC  : [G2 : Ctxt] -> [b : Ty] -> Context G1 c (snoc G2 b) b
; wkC  : [G2 : Ctxt] -> [a, b : Ty] ->
         Context G1 c G2 b -> Context G1 c (snoc G2 a) b
; lamC : [G2 : Ctxt] -> [a, b : Ty] ->
         Context G1 c (snoc G2 a) b -> Context G1 c G2 (arr a b)
; appC : [G2 : Ctxt] -> [a, b : Ty] ->
         Context G1 c G2 (arr a b) -> Context G1 c G2 a ->
         Context G1 c G2 b
; fixC : [G2 : Ctxt] -> [a, b : Ty] ->
         Context G1 c G2 (arr (arr a b) (arr a b)) ->
         Context G1 c G2 a -> Context G1 c G2 b
; zC   : [G2 : Ctxt] -> Context G1 c G2 nat
; sC   : [G2 : Ctxt] -> Context G1 c G2 nat -> Context G1 c G2 nat
; pC   : [G2 : Ctxt] -> Context G1 c G2 nat -> Context G1 c G2 nat
; ifZC : [G2 : Ctxt] -> [b : Ty] ->
         Context G1 c G2 nat -> Context G1 c G2 b ->
         Context G1 c G2 b -> Context G1 c G2 b
}

-- Fills the holes.

fun fill : [G1, G2 : Ctxt] -> [a, b : Ty] ->
           Context G1 a G2 b -> Tm G1 a -> Tm G2 b
{ fill .G1 .G1          .c .c         (hole G1 c)               t = t
; fill .G1 .(snoc G2 b) .c .b         (vzC G1 c G2 b)           t = vz G2 b
; fill .G1 .(snoc G2 a) .c .b         (wkC G1 c G2 a b C)       t = wk G2 a b (fill G1 G2 c b C t)
; fill .G1 .G2          .c .(arr a b) (lamC G1 c G2 a b C)      t = lam G2 a b (fill G1 (snoc G2 a) c b C t)
; fill .G1 .G2          .c .b         (appC G1 c G2 a b C1 C2)  t = app G2 a b (fill G1 G2 c (arr a b) C1 t)
                                                                               (fill G1 G2 c a         C2 t)
; fill .G1 .G2          .c .b         (fixC G1 c G2 a b C1 C2)  t = fix G2 a b (fill G1 G2 c (arr (arr a b) (arr a b)) C1 t)
                                                                               (fill G1 G2 c a                         C2 t)
; fill .G1 .G2          .c .nat       (zC G1 c G2)              t = z G2
; fill .G1 .G2          .c .nat       (sC G1 c G2 C)            t = s G2 (fill G1 G2 c nat C t)
; fill .G1 .G2          .c .nat       (pC G1 c G2 C)            t = p G2 (fill G1 G2 c nat C t)
; fill .G1 .G2          .c .b         (ifZC G1 c G2 b C1 C2 C3) t = ifZ G2 b (fill G1 G2 c nat C1 t)
                                                                             (fill G1 G2 c b   C2 t)
                                                                             (fill G1 G2 c b   C3 t)
}

------------------------------------------------------------------------
-- * Term equality is closed under contexts

-- EqTCong is closed under contexts.

fun contextClosedCong :
  (k : Kind) -> [i : Size] -> [G1, G2 : Ctxt] -> [a, b : Ty] ->
  (C : Context G1 a G2 b) -> (t1, t2 : Tm G1 a) ->
  EqTCong k i G1 a t1 t2 ->
  EqTCong k i G2 b (fill G1 G2 a b C t1) (fill G1 G2 a b C t2)
{ contextClosedCong k i .G1 .G1 .c .c (hole G1 c) t1 t2 tEq = tEq
; contextClosedCong k i .G1 .(snoc G2 b) .c .b (vzC G1 c G2 b) t1 t2 tEq =
    vzCong k i G2 b
; contextClosedCong k i .G1 .(snoc G2 a) .c .b
                    (wkC G1 c G2 a b C) t1 t2 tEq =
    wkCong k i G2 a b (fill G1 G2 c b C t1) (fill G1 G2 c b C t2)
           (contextClosedCong k i G1 G2 c b C t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .(arr a b)
                    (lamC G1 c G2 a b C) t1 t2 tEq =
    lamCong k i G2 a b (fill G1 (snoc G2 a) c b C t1)
                       (fill G1 (snoc G2 a) c b C t2)
            (contextClosedCong k i G1 (snoc G2 a) c b C t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .b (appC G1 c G2 a b C1 C2) t1 t2 tEq =
    appCong k i G2 a b (fill G1 G2 c (arr a b) C1 t1)
                       (fill G1 G2 c (arr a b) C1 t2)
                       (fill G1 G2 c a C2 t1)
                       (fill G1 G2 c a C2 t2)
            (contextClosedCong k i G1 G2 c (arr a b) C1 t1 t2 tEq)
            (contextClosedCong k i G1 G2 c a C2 t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .b (fixC G1 c G2 a b C1 C2) t1 t2 tEq =
    let [abab : Ty] = arr (arr a b) (arr a b) in
    fixCong k i G2 a b (fill G1 G2 c abab C1 t1)
                       (fill G1 G2 c abab C1 t2)
                       (fill G1 G2 c a C2 t1)
                       (fill G1 G2 c a C2 t2)
            (contextClosedCong k i G1 G2 c abab C1 t1 t2 tEq)
            (contextClosedCong k i G1 G2 c a C2 t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .nat (zC G1 c G2) t1 t2 tEq =
    zCong k i G2
; contextClosedCong k i .G1 .G2 .c .nat (sC G1 c G2 C) t1 t2 tEq =
    sCong k i G2 (fill G1 G2 c nat C t1)
                 (fill G1 G2 c nat C t2)
          (contextClosedCong k i G1 G2 c nat C t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .nat (pC G1 c G2 C) t1 t2 tEq =
    pCong k i G2 (fill G1 G2 c nat C t1)
                 (fill G1 G2 c nat C t2)
          (contextClosedCong k i G1 G2 c nat C t1 t2 tEq)
; contextClosedCong k i .G1 .G2 .c .b (ifZC G1 c G2 b C1 C2 C3) t1 t2 tEq =
    ifZCong k i G2 b (fill G1 G2 c nat C1 t1)
                   (fill G1 G2 c nat C1 t2)
                   (fill G1 G2 c b C2 t1)
                   (fill G1 G2 c b C2 t2)
                   (fill G1 G2 c b C3 t1)
                   (fill G1 G2 c b C3 t2)
            (contextClosedCong k i G1 G2 c nat C1 t1 t2 tEq)
            (contextClosedCong k i G1 G2 c b C2 t1 t2 tEq)
            (contextClosedCong k i G1 G2 c b C3 t1 t2 tEq)
}

-- EqT is closed under contexts.

fun contextClosed :
  (k : Kind) -> [i : Size] -> [G1, G2 : Ctxt] -> [a, b : Ty] ->
  (C : Context G1 a G2 b) -> (t1, t2 : Tm G1 a) ->
  EqT k i G1 a t1 t2 ->
  EqT k i G2 b (fill G1 G2 a b C t1) (fill G1 G2 a b C t2)
{ contextClosed k i G1 G2 a b C t1 t2 tEq =
    congSound k i G2 b (fill G1 G2 a b C t1) (fill G1 G2 a b C t2)
      (contextClosedCong k i G1 G2 a b C t1 t2
         (congComplete k i G1 a t1 t2 tEq))
}

------------------------------------------------------------------------
-- * The equality is symmetric

mutual {

  fun symV : (b : Ty) -> [i : Size] ->
             (v1, v2 : Value b) ->
             EqV b bisim i v1 v2 -> EqV b bisim i v2 v1
  { symV nat i .n .n (reflId .(Value nat) n) = reflId (Value nat) n
  ; symV (arr a b) i (arrV G1 .a .b t1 rho1) (arrV G2 .a .b t2 rho2)
         fEq = \ j v2 v1 vEq ->
      symL b j (sem # (snoc G1 a) b t1 (snocE G1 a rho1 v1))
               (sem # (snoc G2 a) b t2 (snocE G2 a rho2 v2))
               (fEq j v1 v2 (symV a j v2 v1 vEq))
  }

  fun symL : (b : Ty) -> [i : Size] -> (x1, x2 : Lift (Value b) #) ->
             EqL b bisim i x1 x2 -> EqL b bisim i x2 x1
  { symL b i = symEq i (Value b) (EqV b bisim) (\ j v1 -> symV b j v1)
  }

}

fun symEnv : [i : Size] -> (G : Ctxt) -> (rho1, rho2 : Env G) ->
             EqEnv bisim i G rho1 rho2 -> EqEnv bisim i G rho2 rho1
{ symEnv .i .empty .emptyE .emptyE (emptyEq .bisim i) = emptyEq bisim i
; symEnv .i (snoc G b) (snocE .G .b rho1 v1) (snocE .G .b rho2 v2)
         (snocEq .bisim i .G .b .rho1 .rho2 .v1 .v2 rhoEq vEq) =
    snocEq bisim i G b rho2 rho1 v2 v1 (symEnv i G rho1 rho2 rhoEq)
                                       (symV b i v1 v2 vEq)
}

fun symT : [i : Size] -> (G : Ctxt) -> (b : Ty) ->
           (t1, t2 : Tm G b) ->
           EqT bisim i G b t1 t2 -> EqT bisim i G b t2 t1
{ symT i G b t1 t2 tEq j rho2 rho1 rhoEq =
    symL b j (sem # G b t1 rho1) (sem # G b t2 rho2)
             (tEq j rho1 rho2 (symEnv j G rho2 rho1 rhoEq))
}

------------------------------------------------------------------------
-- * The inequality is transitive

mutual {

  fun transVS :
        (b : Ty) -> [i : Size] -> (v1, v2, v3 : Value b) ->
        EqV b sim # v1 v2 -> EqV b sim i v2 v3 -> EqV b sim i v1 v3
  { transVS nat i .n .n .n
      (reflId .(Value nat) n) (reflId .(Value nat) .n) =
      reflId (Value nat) n
  ; transVS (arr a b) i (arrV G1 .a .b t1 rho1)
                        (arrV G2 .a .b t2 rho2)
                        (arrV G3 .a .b t3 rho3)
      fEq12 fEq23 = \ j v1 v3 vEq13 ->
      transLS b j (sem # (snoc G1 a) b t1 (snocE G1 a rho1 v1))
                  (sem # (snoc G2 a) b t2 (snocE G2 a rho2 v1))
                  (sem # (snoc G3 a) b t3 (snocE G3 a rho3 v3))
        (fEq12 # v1 v1 (reflV a sim v1))
        (fEq23 j v1 v3 vEq13)
  }

  fun transLS :
        (b : Ty) -> [i : Size] -> (x1, x2, x3 : Lift (Value b) #) ->
        EqL b sim # x1 x2 -> EqL b sim i x2 x3 -> EqL b sim i x1 x3
  { transLS b i =
      transGEq i (Value b) (EqV b sim) (\ j v1 -> transVS b j v1)
  }

}

fun transEnvS : [i : Size] -> (G : Ctxt) ->
                (rho1, rho2, rho3 : Env G) ->
                EqEnv sim # G rho1 rho2 -> EqEnv sim # G rho2 rho3 ->
                EqEnv sim i G rho1 rho3
{ transEnvS i .empty .emptyE .emptyE .emptyE
    (emptyEq .sim .#) (emptyEq .sim .#) =
    emptyEq sim i
; transEnvS i (snoc G b) (snocE .G .b rho1 v1)
                         (snocE .G .b rho2 v2)
                         (snocE .G .b rho3 v3)
           (snocEq .sim .# .G .b .rho1 .rho2 .v1 .v2 rhoEq12 vEq12)
           (snocEq .sim .# .G .b .rho2 .rho3 .v2 .v3 rhoEq23 vEq23) =
    snocEq sim i G b rho1 rho3 v1 v3
           (transEnvS i G rho1 rho2 rho3 rhoEq12 rhoEq23)
           (transVS b i v1 v2 v3 vEq12 vEq23)
}

fun transTS :
      [i : Size] -> (G : Ctxt) -> (b : Ty) -> (t1, t2, t3 : Tm G b) ->
      EqT sim # G b t1 t2 -> EqT sim i G b t2 t3 -> EqT sim i G b t1 t3
{ transTS i G b t1 t2 t3 tEq12 tEq23 j rho1 rho3 rhoEq13 =
    transLS b j (sem # G b t1 rho1)
                (sem # G b t2 rho1)
                (sem # G b t3 rho3)
      (tEq12 # rho1 rho1 (reflEnv sim G rho1))
      (tEq23 j rho1 rho3 rhoEq13)
}

------------------------------------------------------------------------
-- * Contextual equality (and inequality)

-- Contextual equality. Note that this definition is more
-- "constructive" than the standard one.

fun EqC : Kind -> -Size -> (G : Ctxt) -> (b : Ty) ->
          Tm G b -> Tm G b -> Set
{ EqC k i G b t1 t2 = (a : Ty) -> (C : Context G b empty a) ->
    Rel (Value a) (\ j -> Always (Value a)) i k
        (sem # empty a (fill G empty b a C t1) emptyE)
        (sem # empty a (fill G empty b a C t2) emptyE)
}

-- EqT is sound with respect to contextual equality.

fun eqTSound : (k : Kind) -> [i : Size] ->
               (G : Ctxt) -> (b : Ty) -> (t1, t2 : Tm G b) ->
               EqT k i G b t1 t2 -> EqC k i G b t1 t2
{ eqTSound k i G b t1 t2 tEq = \ a C ->
    mapRel i k (Value a) (EqV a k) (\ j -> Always (Value a))
           (\ j v1 v2 vEq -> unit)
           (sem # empty a (fill G empty b a C t1) emptyE)
           (sem # empty a (fill G empty b a C t2) emptyE)
           (contextClosed k i G empty b a C t1 t2 tEq
              i emptyE emptyE (emptyEq k i))
}

-- Local variables:
-- outline-regexp: "-- \\*+"
-- End: