happy-modal-let-into.rzk

#lang rzk-1

#def sharp-join-into
  (A : U)
  (a : _# (_# A))
  : _# A
  :=
  let mod _# x_1 := a into (\ _ -> _# A) in
  let _# mod _# x_2 := x_1 in
  mod _# x_2

#def double-op-into
  (A : U)
  (x : _op (_op A))
  : A
  :=
  let mod _op x_1 := x into (\ _ -> A) in
  let _op mod _op x_2 := x_1 in
  x_2

#def into-agrees-with-plain
  (A : U)
  (x : _# A)
  : (let mod _# a := x into (\ _ -> _# A) in mod _# a) = x
  := refl

-- The dependent elimination the motive exists for: the goal is C x, while the
-- body only proves C (mod ♭ a). Flat has no eta rule, so without the motive
-- there is nothing identifying x with mod ♭ a and the body does not check.
#def flat-dependent-into
  (A :_b U)
  (C : (_b A) -> U)
  (c : (a :_b A) -> C (mod _b a))
  (x : _b A)
  : C x
  := let mod _b a := x into C in c a

-- The same, with the motive written out as a lambda rather than named.
#def sharp-dependent-into
  (A : U)
  (C : (_# A) -> U)
  (c : (a :_# A) -> C (mod _# a))
  (x : _# A)
  : C x
  := let mod _# a := x into (\ z -> C z) in c a

-- The single-modality binding accepts a motive too. Its value is `mod _# a`
-- by construction, so the motive is applied to that.
#def sugar-into
  (A : U)
  (C : (_# A) -> U)
  (c : (a :_# A) -> C (mod _# a))
  (a :_# A)
  : C (mod _# a)
  := let _# x := a into C in c x

-- A motive on the full composition form, where the external lock is not `_id`.
#def comp-into
  (A : U)
  (a : _# (_# A))
  : _# A
  :=
  let mod _# x_1 := a in
  let _# mod _# x_2 := x_1 into (\ _ -> _# A) in
  mod _# x_2