πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Connectives.More
import Padova2025.Recreational.Choice.Boxes.Base as Base
import Padova2025.Recreational.Choice.Boxes.Stage1 as Stage1
import Padova2025.Recreational.Choice.Boxes.Stage2 as Stage2

module Padova2025.Recreational.Choice.Boxes.Stage3
  (ℝ : Set) (n : β„•) (R : Normalizer β„• ℝ)
  (open Base ℝ n)
  (p : Player)
  (open Stage1 ℝ n p)
  (their-box-contents : I β†’ ℝ)
  (open Stage2 ℝ n R p their-box-contents)
  (our-box-contents : J β†’ ℝ)
  where

Stage 3

open Normalizer R

dummy : ℝ
dummy = our-box-contents (zero , Ξ» ())

-- The boxes of our lane, with `dummy` inserted as placeholder for the unique unopened box
mostly-our-lane : Config
mostly-our-lane = insert (succ M) our-box-contents dummy

our-guess : ℝ
our-guess = rep mostly-our-lane (succ M)