{-# OPTIONS --allow-unsolved-meta #-} {- plan for today: 1. game theory 2. simply-typed lambda calculus 3. your questions -} {- In Standard Agda and in ordinary Martin-Löf type theory, for any two types "A" and "B", we have a type "A ≡ B" of equality witnesses between "A" and "B". However, unlike in HoTT / CTT, this type is severely underspecified. In HoTT / CTT, this defect is remedied. Namely: Every equivalence A → B can be turned into an equality witness A ≡ B. ("univalence axiom") -} module transcript10a where data ℕ : Set where zero : ℕ succ : ℕ → ℕ data _⊎_ (X Y : Set) : Set where left : X → X ⊎ Y right : Y → X ⊎ Y module _ (String : Set) where data Bool : Set where false true : Bool record Person : Set where field surname : String age : ℕ address : String jenny : Person jenny = record { surname = {!!} ; age = succ (succ zero) ; address = {!!} } isOfLegalAge : Person → Bool isOfLegalAge (record { surname = surname ; age = age ; address = address }) = {!age ≥? 18!} isOfLegalAge' : (surname : String) (age : ℕ) (address : String) → Bool isOfLegalAge' surname age address = {!!} record Game : Set₁ where field Pos : Set -- type of possible positions Move : Pos → Pos → Set -- Move a b is the type of possible moves from position a to pos. b module Basics (G : Game) where open Game G -- now we have "Pos" and "Move" available; -- without opening, we would need to write "Game.Pos G" data Winning : Pos → Set data Loosing : Pos → Set data Winning where -- win : {a : Pos} → ...there is a move out of position a which results in a loosing position... → Winning a win : {a b : Pos} → Move a b → Loosing b → Winning a data Loosing where -- trivial : {a : Pos} → (...no moves are possible starting in position a...) → Loosing a -- trivial : {a : Pos} → ({b : Pos} → Move a b → ⊥) → Loosing a -- the "trivial" constructor is redundant -- loose : {a : Pos} → (...no matter which move we take, the next position) → Loosing a -- will be a winning position..................... loose : {a : Pos} → ({b : Pos} → Move a b → Winning b) → Loosing a module _ (enum : {!!}) where determined : (a : Pos) → Winning a ⊎ Loosing a determined = {!!} {- | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | -} module Take-3 where Pos : Set Pos = ℕ data Move : Pos → Pos → Set where take₁ : {n : Pos} → Move (succ n) n take₂ : {n : Pos} → Move (succ (succ n)) n take₃ : {n : Pos} → Move (succ (succ (succ n))) n G : Game G = record { Pos = Pos ; Move = Move } open Basics G 0-loosing : Loosing zero 0-loosing = loose (λ ()) 1-winning : Winning (succ zero) 1-winning = win take₁ 0-loosing -- TASK: Verify that G is finite in the sense required by "determined". module Chomp where -- 1. The game is finite. -- 2. No draw possible. -- 3. Hence the game is determined: For one of the two players, a winning strategy needs to exist. -- 4. Even though concrete winning strategies are unknown in most cases, we do know that -- there is a winning strategy for the first player. ("strategy stealing")