happy-modal-basics.rzk

#lang rzk-1

#def sharp-pure (A : U) (x : A)
  : _# A
  := mod _# x

#def sharp-map (A B : U) (f : A → B)
  : (x :_# A) → _# B
  := \ (x :_# A) → mod _# (f x)

#def b-extract (A :_b U) (x :_b A)
  : A
  := x

#def b-map (A B :_b U) (f :_b A → B)
  : (x :_b A) → _b B
  := \ (x :_b A) → mod _b (f x)

#def b-dup (A :_b U) (x :_b A)
  : _b (_b A)
  := mod _b (mod _b x)

#def op-map (A B :_op U) (f :_op A → B)
  : (x :_op A) → _op B
  := \ (x :_op A) → mod _op (f x)

#def double-op (A : U) (x : _op (_op A))
  : A
  :=
  let mod _op x_1 := x in
  let mod _op / _op x_2 := x_1 in
  x_2

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

#def flat-to-sharp (A :_b U) (x :_b A)
  : _# A
  := mod _# x

#def id-pure (A : U) (x : A)
  : _id A
  := mod _id x

#def id-map (A B : U) (f : A → B)
  : (x :_id A) → _id B
  := \ (x :_id A) → mod _id (f x)

#def id-join (A : U) (a : _id (_id A))
  : _id A
  :=
  let mod _id x_1 := a in
  let mod _id / _id x_2 := x_1 in
  mod _id x_2

#def op-op-is-id (A : U) (x : _op (_op A))
  : _id A
  :=
  let mod _op x_1 := x in
  let mod _op / _op x_2 := x_1 in
  mod _id x_2

-- comp(Flat, Op) = Flat: flat var stays accessible inside op-under-flat
#def flat-op-chain (A :_b U) (x :_b A)
  : _op (_b A)
  := mod _op (mod _b x)

-- comp(Sharp, Op) = Sharp: plain var stays accessible inside op-under-sharp
#def sharp-op-chain (A : U) (x : A)
  : _op (_# A)
  := mod _op (mod _# x)

-- Flat tope accessible at plain level with boundary
#def test-flat-tope-to-plain
  (A :_b U)
  (a :_b A)
  : (i :_b 2 | i === 0_2) -> A [ i === 0_2 |-> a ]
  := \ i -> a

-- recOR under flat: LEM covers 2
#def test-recOR-flat
  (A :_b U)
  (a b :_b A)
  : (i :_b 2) -> A
  := \(i :_b 2) -> recOR( i === 0_2 |-> a , i === 1_2 |-> b )

-- Flat accessible under sharp chain
#def test-sharp-from-flat-chain
  (A :_b U)
  (a :_b A)
  : (i :_b 2 | i === 0_2) -> _# A
  := \ i -> mod _# a

-- LEQ recOR under flat
#def test-flat-leq-recOR
  (A :_b U)
  (a :_b A)
  : (i :_b 2) -> A
  := \ (i :_b 2) -> recOR( i <= 0_2 |-> a, 0_2 <= i |-> a)

-- Disjunction restriction under flat
#def test-flat-disjunction-cover
  (A :_b U)
  (a b :_b A)
  : (i :_b 2 | (i === 0_2) \/ (i === 1_2)) -> A
  := \ (i :_b 2) -> recOR( i === 0_2 |-> a , i === 1_2 |-> b )

-- Conjunction split under flat
#def test-flat-conjunction-split
  (A :_b U)
  (a :_b A)
  : (i :_b 2 | i === 0_2) -> (j :_b 2 | j === 0_2) -> A
  := \ i j -> a

-- Product cube face under flat
#def test-flat-product-face
  (A :_b U)
  (a :_b A)
  : (ts :_b (2 * 2) | first ts === 0_2) -> A
  := \ ts -> a

-- Symmetry through saturation: (0 === i) => (i === 0)
#def test-flat-symmetry
  (A :_b U)
  (a :_b A)
  : (i :_b 2 | 0_2 === i) -> A [ i === 0_2 |-> a ]
  := \ i -> a

-- Transitivity under flat: (i === j) /\ (j === 0) => (i === 0)
#def test-flat-transitivity
  (A :_b U)
  (a :_b A)
  (i j :_b 2)
  : (i :_b 2 | (i === j) /\ (j === 0_2)) -> A [ i === 0_2 |-> a ]
  := \ _ -> a

-- Plain tope entails _# goal
#def test-solve-sharp-goal
  (A : U)
  (a : A)
  : (i : 2 | i === 0_2) -> _# Unit
  := \ i -> mod _# unit

-- Nested modal goal: _# (_b A)
#def test-solve-nested-modal-goal
  (A :_b U)
  (a :_b A)
  : _# (_b A)
  := mod _# (mod _b a)

-- Op var with extension boundary
#def test-op-var-boundary
  (A :_op U)
  (a :_op A)
  (i :_op 2)
  : (i :_op 2 |_op (i === 0_2)) -> (_op A) [ _op (i === 0_2) |-> (mod _op a) ]
  := \ _ -> (mod _op a)

-- _op var accessible under _op restriction
#def test-op-goal-with-op-var
  (A :_op U)
  (a :_op A)
  (i :_op 2)
  : (i :_op 2 | (_op (i === 0_2))) -> _op A
  := \ _ -> mod _op a

-- ============ Extension types under modalities ============

-- recOR with <= under mod _#: endpoint LEQs always solvable
#def test-sharp-tope-boundary
  (A : U) (a : A)
  : (t : 2) -> _# A
  := \ t -> mod _# (recOR( 0_2 <= t |-> a , t <= 1_2 |-> a ))

-- Sharp extension with boundary
#def test-sharp-extension
  (A : U)
  (a : A)
  : (i : 2) -> (_# A) [ i === 0_2 |-> mod _# a , i === 1_2 |-> mod _# a ]
  := \(i : 2) -> mod _# (recOR( 0_2 <= i |-> a , i <= 1_2 |-> a ))

-- Extension under flat with boundary
#def test-flat-extension-boundary
  (A :_b U)
  (a b :_b A)
  : (i :_b 2) -> A [ i === 0_2 |-> a , i === 1_2 |-> b ]
  := \(i :_b 2) -> recOR( i === 0_2 |-> a , i === 1_2 |-> b )

-- Constant path under flat
#def test-flat-const-path
  (A :_b U)
  (a :_b A)
  : (i :_b 2) -> A [ i === 0_2 |-> a , i === 1_2 |-> a ]
  := \(i :_b 2) -> a

-- Flat tope with sharp return type and boundary
#def test-flat-tope-sharp-boundary
  (A :_b U) (a :_b A)
  (i :_b 2)
  : (i :_b 2 | i === 0_2) -> _# A [ i === 0_2 |-> mod _# a ]
  := \ _ -> mod _# a

-- Mixed flat + plain variables in extension
#def test-mixed-flat-plain-vars
  (A :_b U)
  (a :_b A)
  (i :_b 2)
  (j : 2)
  : (i :_b 2 | (i === 0_2) /\ (j === 0_2)) -> A
  := \ _ -> a

-- Flat double-wrap with boundary
#def test-flat-double-wrap-boundary
  (A :_b U) (a :_b A) (i :_b 2)
  : (i :_b 2 | i === 0_2) -> _b (_b A) [ i === 0_2 |-> mod _b (mod _b a) ]
  := \ _ -> mod _b (mod _b a)

-- Flat to sharp chain with tope
#def test-flat-to-sharp-with-tope
  (A :_b U) (a :_b A) (i :_b 2)
  : (i :_b 2 | i === 0_2) -> _# (_# A)
  := \ _ -> mod _# (mod _# a)

-- ============ Manual conversions ============

-- Manual conversion: (x :_# A) → B  to  (_# A) → B
#def sharp-modal-to-explicit
  (A : U) (B : U) (f : (x :_# A) -> B)
  : (_# A) -> B
  := \ y -> let mod _# z := y in f z

-- Manual conversion: (_# A) → B  to  (x :_# A) → B
#def sharp-explicit-to-modal
  (A : U) (B : U) (f : (_# A) -> B)
  : (x :_# A) -> B
  := \ (x :_# A) -> f (mod _# x)

-- Manual conversion: (x :_op A) → B  to  (_op A) → B
#def op-modal-to-explicit
  (A :_op U) (B : U) (f : (x :_op A) -> B)
  : (_op A) -> B
  := \ y -> let mod _op z := y in f z

-- Manual conversion: (_op A) → B  to  (x :_op A) → B
#def op-explicit-to-modal
  (A :_op U) (B : U) (f : (_op A) -> B)
  : (x :_op A) -> B
  := \ (x :_op A) -> f (mod _op x)

-- Manual conversion: (x :_id A) → B  to  (_id A) → B
#def id-modal-to-explicit
  (A : U) (B : U) (f : (x :_id A) -> B)
  : (_id A) -> B
  := \ y -> let mod _id z := y in f z

-- Manual conversion: (_id A) → B  to  (x :_id A) → B
#def id-explicit-to-modal
  (A : U) (B : U) (f : (_id A) -> B)
  : (x :_id A) -> B
  := \ (x :_id A) -> f (mod _id x)

-- Manual conversion: (x :_b A) → B  to  (_b A) → B
#def flat-modal-to-explicit
  (A :_b U) (B : U) (f : (x :_b A) -> B)
  : (_b A) -> B
  := \ y -> let mod _b z := y in f z

-- Manual conversion: (_b A) → B  to  (x :_b A) → B
#def flat-explicit-to-modal
  (A :_b U) (B : U) (f : (_b A) -> B)
  : (x :_b A) -> B
  := \ (x :_b A) -> f (mod _b x)

-- ============ RA letmod commutativity ============

-- Sharp letmod commutes (RA)
#def sharp-letmod-commute
  (A : U) (B : U)
  (x : _# A) (y : _# B)
  : (let mod _# a := x in let mod _# b := y in mod _# (a))
  = (let mod _# b := y in let mod _# a := x in mod _# (a))
  := refl

-- Op letmod commutes (RA)
#def op-letmod-commute
  (A :_op U) (B :_op U)
  (x : _op A) (y : _op B)
  : (let mod _op a := x in let mod _op b := y in mod _op (a))
  = (let mod _op b := y in let mod _op a := x in mod _op (a))
  := refl

-- Id letmod commutes (RA)
#def id-letmod-commute
  (A : U) (B : U)
  (x : _id A) (y : _id B)
  : (let mod _id a := x in let mod _id b := y in mod _id (a))
  = (let mod _id b := y in let mod _id a := x in mod _id (a))
  := refl

-- ============ Modal eta: mod m (extract a) = a ============

-- Sharp eta
#def sharp-eta
  (A : U) (x : _# A)
  : (let mod _# a := x in mod _# a) = x
  := refl

-- Op eta
#def op-eta
  (A :_op U) (x : _op A)
  : (let mod _op a := x in mod _op a) = x
  := refl

-- Id eta
#def id-eta
  (A : U) (x : _id A)
  : (let mod _id a := x in mod _id a) = x
  := refl