text:
{-# OPTIONS --type-in-type #-}
module Reactive where

open import Prelude

infixr 9 _∘ᵗ_ _∘ᵀ_ _∘ᵇ_ _∙_
infixl 9 _∘ʷ_
infix 4 _,ᵀ_ _,ᵗ_
infix 2 _×ᵀ_

-- Coinductive trees will represent protocols of interactions
record Tree : Set where
  coinductive
  field
    Branch : Set
    child : Branch → Tree

open Tree

constᵀ : Set → Tree
constᵀ A .Branch = A
constᵀ A .child _ = constᵀ A

_×ᵀ_ : Tree → Tree → Tree
(p ×ᵀ q) .Branch = p .Branch × q .Branch
(p ×ᵀ q) .child (ph , qh) = p .child ph ×ᵀ q .child qh

alter : Tree → Tree → Tree
alter p q .Branch = p .Branch
alter p q .child hp = alter q (p .child hp)

alter' = λ A B → alter (constᵀ A) (constᵀ B)

-- signals
Sig = λ A B → alter' (Maybe A) (Maybe B)

NoSig  = Sig ⊥ ⊥
OutSig = λ A → Sig A ⊥
InSig  = λ A → Sig ⊥ A
BiSig  = λ A → Sig A A

{-
p:  P₁    P₂ -> P₃    P₄  ...
    |     ^     |     ^
    v     |     v     |
q:  Q₁ -> Q₂    Q₃ -> Q₄  ...
-}
merge : Tree → Tree → Tree
merge p q .Branch = p .Branch
merge p q .child hp .Branch = q .Branch
merge p q .child hp .child hq = merge (q .child hq) (p .child hp)

union2 : Tree → Tree → Tree
union2 p q .Branch = p .Branch ⊎ q .Branch
union2 p q .child (inj₁ ph) with p .child ph
... | r = λ where .Branch → q .Branch
                  .child rh → union2 r (q .child rh)
union2 p q .child (inj₂ qh) with q .child qh
... | r = λ where .Branch → p .Branch
                  .child rh → union2 (p .child rh) r

-- TODO: express with simpler combinators?
union2mb : Tree → Tree → Tree
union2mb p q .Branch = Maybe (p .Branch ⊎ q .Branch)
union2mb p q .child (just (inj₁ ph)) with p .child ph
... | r = λ where .Branch → q .Branch
                  .child rh → union2mb r (q .child rh)
union2mb p q .child (just (inj₂ qh)) with q .child qh
... | r = λ where .Branch → p .Branch
                  .child rh → union2mb (p .child rh) r
union2mb p q .child nothing .Branch = ⊤
union2mb p q .child nothing .child _ = union2mb p q

-----------------------------

data I/O : Set where I O : I/O   -- input and output phases

variable p q r s : Tree
variable i/o : I/O

opposite : I/O → I/O
opposite I = O
opposite O = I

ΠΣ : I/O → (A : Set) → (A → Set) → Set
ΠΣ I A P = (a : A) → P a
ΠΣ O A P = Σ A P

⟨_⟩ : I/O → (A → A → B) → A → A → B
⟨ I ⟩ = id
⟨ O ⟩ = flip

-- an interactive agent which communcates according to the protocol p
-- an agent can be called either in input or in output phase
record Agent (i/o : I/O) (p : Tree) : Set where
  coinductive
  field
    step : ΠΣ i/o (p .Branch) λ a → Agent (opposite i/o) (p .child a)

open Agent

_,ᵀ_ : Agent i/o p → Agent i/o q → Agent i/o (p ×ᵀ q)
_,ᵀ_ {i/o = I} a b .step (k , l) = a .step k ,ᵀ b .step l
_,ᵀ_ {i/o = O} a b .step with a .step | b .step
... | i , j | k , l = (i , k) , (j ,ᵀ l)

_∘ᵗ_ : Agent I (alter p q) → Agent I (alter q r) → Agent I (alter p r)
(b ∘ᵗ a) .step ph .step with b .step ph .step
... | qh , bt with a .step qh .step
... | rh , at = rh , bt ∘ᵗ at

-- stream processors
SP = λ A B → Agent I (alter' A B)

-- same as  Agent I (Sig A B)
SPM = λ A B → SP (Maybe A) (Maybe B)

arr : (A → B) → SP A B
arr f .step x .step = f x , arr f

accum : (A → B → B) → B → SP A B
accum f b .step a .step with f a b
... | b' = b' , accum f b'

maybefy : SP A B → SPM A B
maybefy f .step nothing .step = nothing , (maybefy f)
maybefy f .step (just a) .step with f .step a .step
... | x , y = just x , maybefy y

-- synchronous interaction transformers
IT = λ p q → Agent I (merge p q)

mapAgent : ⟨ i/o ⟩ IT q p → Agent i/o p → Agent i/o q
mapAgent {i/o = I} l i .step hq with l .step hq .step
... | a , l2 = mapAgent l2 (i .step a)
mapAgent {i/o = O} l i .step with i .step
... | a , b with l .step a .step
... | c , l2 = c , (mapAgent l2 b)

_∘ᵀ_ : IT p q → IT q r → IT p r
(b ∘ᵀ a) .step ph .step with b .step ph .step
... | qh , bt with a .step qh .step
... | rh , at = rh , at ∘ᵀ bt

_,ᵗ_ : IT p q → IT r s → IT (p ×ᵀ r) (q ×ᵀ s)
_,ᵗ_ a b .step (k , l) .step with a .step k .step | b .step l .step
... | c , d | e , f = (c , e) , (d ,ᵗ f)

idIT : IT p p
idIT .step a .step = a , idIT

swapIT : IT (p ×ᵀ q) (q ×ᵀ p)
swapIT .step (a , b) .step = (b , a) , swapIT

assocIT : ⟨ i/o ⟩ IT ((p ×ᵀ q) ×ᵀ r) (p ×ᵀ (q ×ᵀ r))
assocIT {i/o = I} .step ((a , b) , c) . step = (a , (b , c)) , assocIT {i/o = O}
assocIT {i/o = O} .step (a , (b , c)) . step = ((a , b) , c) , assocIT {i/o = I}

fstSig : IT (p ×ᵀ Sig A B) p
fstSig .step (x , y) .step = x , λ where .step x .step → (x , nothing) , fstSig

joinSig : A → B → ⟨ i/o ⟩ IT (⟨ i/o ⟩ Sig A C ×ᵀ ⟨ i/o ⟩ Sig B D) (⟨ i/o ⟩ Sig (A × B) (C × D))
joinSig {i/o = I} a b .step (nothing , nothing) .step = nothing      , joinSig {i/o = O} a b
joinSig {i/o = I} a b .step (nothing , just y ) .step = just (a , y) , joinSig {i/o = O} a y
joinSig {i/o = I} a b .step (just x  , nothing) .step = just (x , b) , joinSig {i/o = O} x b
joinSig {i/o = I} a b .step (just x  , just y ) .step = just (x , y) , joinSig {i/o = O} x y
joinSig {i/o = O} a b .step nothing        .step = (nothing , nothing) , joinSig {i/o = I} a b
joinSig {i/o = O} a b .step (just (x , y)) .step = (just x  , just y ) , joinSig {i/o = I} a b

noInput : IT (Sig A B) (OutSig A)
noInput .step x .step = x , λ where .step y .step → nothing , noInput

noOutput : IT (Sig A B) (InSig B)
noOutput .step x .step = nothing , λ where .step y .step → y , noOutput

mkIT : Agent i/o p → ⟨ i/o ⟩ IT p NoSig
mkIT {i/o = I} a .step x .step = nothing , mkIT {i/o = O} (a .step x)
mkIT {i/o = O} a .step _ .step with a .step
... | b , c = b , mkIT {i/o = I} c

constIT = λ S T A B → IT (alter' S T) (alter' A B)

constITM = λ S T A B → IT (Sig S T) (Sig A B)

lensIT : Lens S T A B → constIT S T A B
lensIT k .step s .step with k s
... | a , bt = a , λ where .step b .step → bt b , lensIT k

prismIT : Prism S T A B → constITM S T A B
prismIT f = lensIT (prismToLens f)

mkIT' : SP S A → SP B T → constIT S T A B
mkIT' f g .step s .step with f .step s .step
... | a , cont = a , (mkIT' g cont)

isoIT : (S → A) → (B → T) → constIT S T A B
isoIT f g = lensIT λ x → (f x) , g

-- bidirectional connection
Bi = λ p q → Agent I (union2 p q)

_∘ᵇ_ : Bi p q → Bi q r → Bi p r
(a ∘ᵇ b) .step (inj₁ x) .step with a .step (inj₁ x) .step
... | c , d with b .step (inj₁ c) .step
... | e , f = e , d ∘ᵇ f
(a ∘ᵇ b) .step (inj₂ x) .step with b .step (inj₂ x) .step
... | c , d with a .step (inj₂ c) .step
... | e , f = e , f ∘ᵇ d

isoBi : Iso A A B B → Bi (constᵀ A) (constᵀ B)
isoBi i .step (inj₁ x) .step = (i .proj₁ x) , isoBi i
isoBi i .step (inj₂ x) .step = (i .proj₂ x) , isoBi i

mmb : Bi p q → Agent I (union2mb p q)
mmb x .step nothing .step = _ , mmb x
mmb x .step (just (inj₁ y)) .step with x .step (inj₁ y) .step
... | a , b = a , mmb b
mmb x .step (just (inj₂ y)) .step with x .step (inj₂ y) .step
... | a , b = a , mmb b

entangleBi : IT (Sig A A ×ᵀ Sig B B) (union2mb (constᵀ A) (constᵀ B))
entangleBi .step (nothing , nothing) .step = nothing , λ where .step _ .step → (nothing , nothing) , entangleBi
entangleBi .step (just x , nothing) .step = just (inj₁ x) , λ where .step z .step → (nothing , just z) , entangleBi
entangleBi .step (nothing , just x) .step = just (inj₂ x) , λ where .step z .step → (just z , nothing) , entangleBi
entangleBi .step (just x , just y) .step = nothing , λ where .step _ .step → (nothing , nothing) , entangleBi

entangle : IT (Sig A C ×ᵀ Sig C B) (Sig A B)
entangle .step (a , c) .step = a , λ where .step b .step → (c , b) , entangle

enta : SP A B → IT (Sig A C ×ᵀ Sig C B) NoSig
enta x = entangle ∘ᵀ mkIT (maybefy x)

entaBi : Bi (constᵀ A) (constᵀ B) → IT (Sig A A ×ᵀ Sig B B) NoSig
entaBi x = entangleBi ∘ᵀ mkIT (mmb x)

---------------------------------------------------------------------

data Direction : Set where horizontal vertical : Direction
data Abled     : Set where enabled disabled : Abled
data Validity  : Set where valid invalid : Validity

variable fin      : Fin _
variable vec      : Vec _ _
variable checked  : Bool
variable size     : ℕ
variable name str : String
variable en       : Abled
variable dir      : Direction
variable val      : Validity

oppositeᵉ : Abled → Abled
oppositeᵉ enabled = disabled
oppositeᵉ disabled = enabled

oppositeᵛ : Validity → Validity
oppositeᵛ valid = invalid
oppositeᵛ invalid = valid

isEnabled : I/O → Abled → Set
isEnabled I enabled  = ⊤
isEnabled I disabled = ⊥
isEnabled O _ = ⊤

-- abstract widget
data Widget : Set where
  Button    : Abled → String → Widget
  CheckBox  : Abled → Bool → Widget
  ComboBox  : Abled → Vec String n → Fin n → Widget
  Entry     : Abled → (size : ℕ)(name contents : String) → Validity → Widget
  Label     : String → Widget
  Empty     : Widget
  Container : Direction → Widget → Widget → Widget

variable w w₁ w₂ : Widget

isInput : Widget → Maybe (Abled × Widget)
isInput (Button e x)       = just (e , Button (oppositeᵉ e) x)
isInput (CheckBox e x)     = just (e , CheckBox (oppositeᵉ e) x)
isInput (ComboBox e ss i)  = just (e , ComboBox (oppositeᵉ e) ss i)
isInput (Entry e n s s' v) = just (e , Entry (oppositeᵉ e) n s s' v)
isInput _ = nothing

isJust : Maybe A → Set
isJust = maybe ⊥ (λ _ → ⊤)

-- possible edits of a widget (I: by the user; O: by the program)
data WidgetEdit : I/O → Widget → Set
-- ⟪_⟫ performs the edit
⟪_⟫ : {d : I/O} {a : Widget} (p : WidgetEdit d a) → Widget

data WidgetEdit  where
  toggle         : {_ : isEnabled i/o en} → WidgetEdit i/o (CheckBox en checked)
  click          : WidgetEdit I (Button enabled str)
  setLabel       : String → WidgetEdit O (Label str)
  setEntry       : {_ : isEnabled i/o en} → String → WidgetEdit i/o (Entry en size name str val)
  select         : {vec : Vec String n}{_ : isEnabled i/o en} → Fin n → WidgetEdit i/o (ComboBox en vec fin)
  toggleEnable   : {_ : isJust (isInput w)} → WidgetEdit O w
  toggleValidity : WidgetEdit O (Entry en size name str val)
  replaceBy      : Widget → WidgetEdit O w
  modLeft        : WidgetEdit i/o w₁ → WidgetEdit i/o (Container dir w₁ w₂)
  modRight       : WidgetEdit i/o w₂ → WidgetEdit i/o (Container dir w₁ w₂)
  addToLeft addToRight    : Direction → Widget → WidgetEdit O w
  removeLeft removeRight  : WidgetEdit O (Container dir w₁ w₂)
  _∙_            : (p : WidgetEdit O w) → WidgetEdit O ⟪ p ⟫ → WidgetEdit O w

⟪ replaceBy x ⟫ = x
⟪ modLeft  {dir = dir} {w₂ = w₂} p ⟫ = Container dir ⟪ p ⟫ w₂
⟪ modRight {dir = dir} {w₁ = w₁} p ⟫ = Container dir w₁ ⟪ p ⟫
⟪ toggle {en = en} {checked} ⟫   = CheckBox en (not checked)
⟪ select {en = en} {vec = vec} fin ⟫ = ComboBox en vec fin
⟪ setEntry {_} {en} {size} {name} {_} {val} {_} str ⟫ = Entry en size name str val
⟪ toggleValidity {en} {size} {name} {str} {val} ⟫     = Entry en size name str (oppositeᵛ val)
⟪ click {s} ⟫  = Button enabled s
⟪ setLabel l ⟫ = Label l
⟪ toggleEnable {w} {e} ⟫ with isInput w | e
... | just (_ , w') | tt = w'     -- note: the JS backend cannot erase 'e', maybe because of the pattern maching on tt here
... | nothing | ()
⟪ addToLeft  {r} dir w ⟫ = Container dir w r
⟪ addToRight {l} dir w ⟫ = Container dir l w
⟪ removeLeft  {w₂ = w₂} ⟫ = w₂
⟪ removeRight {w₁ = w₁} ⟫ = w₁
⟪ p ∙ q ⟫ = ⟪ q ⟫

---------------------------------------

pw : I/O → Widget → Tree
pw i/o w .Branch = Maybe (WidgetEdit i/o w)
pw i/o w .child e = pw (opposite i/o) (maybe w ⟪_⟫ e)

-- GUI component (reactive widget)
WComp' = λ i/o w p → ⟨ i/o ⟩ IT (pw i/o w) p

WComp = λ i/o w A B → WComp' i/o w (⟨ i/o ⟩ Sig A B)

WC = λ p → Σ Widget λ w → WComp' I w p

processMain : WC (Sig A B) → Agent O (pw O Empty)
processMain (w , x) .step = just (replaceBy w) , mapAgent {i/o = I} (x ∘ᵀ noInput ∘ᵀ noOutput) (arr id)

-- enforcing  no input ⇒ no output
ease : WComp i/o w A B → WComp i/o w A B
ease {i/o = I} b .step nothing .step = nothing , λ where .step x .step → nothing , ease {i/o = I} b
ease {i/o = I} b .step (just z) .step with b .step (just z) .step
... | x , y = x , ease {i/o = O} y
ease {i/o = O} b .step x .step with b .step x .step
... | c , d = c , ease {i/o = I} d

ease' : WC (Sig A B) → WC (Sig A B)
ease' (_ , x) = _ , ease {i/o = I} x

_∘ʷ_ : WC p → IT p q → WC q
(_ , x) ∘ʷ y = (_ , x ∘ᵀ y)

----------------------------------------------------------

button : ∀ i/o → WComp i/o (Button enabled str) ⊤ ⊥
button I .step nothing      .step = nothing , button O
button I .step (just click) .step = just _  , button O
button O .step _ .step = nothing , button I

button' : String → WC (OutSig ⊤)
button' s = _ , button {s} I

checkbox : ∀ i/o → WComp i/o (CheckBox enabled checked) Bool Bool
checkbox I .step nothing  .step = nothing , checkbox O
checkbox {b} I .step (just toggle) .step = just (not b) , checkbox O
checkbox O .step nothing .step = nothing , checkbox I
checkbox {b} O .step (just b') .step with b == b'
... | true  = nothing     , checkbox I
... | false = just toggle , checkbox I

checkbox' : Bool → WC (BiSig Bool)
checkbox' b = _ , checkbox {b} I

comboBox : ∀ {vec : Vec String n} i/o → WComp i/o (ComboBox enabled vec fin) (Fin n) (Fin n)
comboBox I .step nothing  .step = nothing , comboBox O
comboBox I .step (just (select i)) .step = just i , comboBox O
comboBox O .step nothing .step = nothing , comboBox I
comboBox O .step (just i) .step = just (select i) , comboBox I

comboBox' : (vec : Vec String n)(fin : Fin n) → WC (Sig (Fin n) (Fin n))
comboBox' vec fin = _ , comboBox {fin = fin}{vec = vec} I

label : ∀ i/o → WComp i/o (Label str) ⊥ String
label I .step nothing  .step = nothing , label O
label I .step (just ())
label O .step nothing .step = nothing , label I
label O .step (just m) .step = just (setLabel m) , label I

label' : String → WC (InSig String)
label' n = _ , label {n} I

label'' = λ n → label' n -- ∘ʷ discard

-- todo: refactoring (use less cases)
entry : Bool → ∀ i/o → WComp' i/o (Entry en size name str val) (⟨ i/o ⟩ Sig String (Maybe String) ×ᵀ ⟨ i/o ⟩ Sig ⊥ ⊤)
entry _ I .step nothing .step = (nothing , nothing) , entry false O
entry _ I .step (just (setEntry s)) .step = (just s , nothing) , entry true O
entry {val = v} v' O .step (ii , td) .step with td | ii | v | v'
... | nothing | nothing        | invalid | true = just toggleValidity , entry false I
... | nothing | just nothing   | valid   | _    = just toggleValidity , entry false I
... | nothing | just (just ss) | valid   | _    = just (setEntry ss) , entry false I
... | nothing | just (just ss) | invalid | _    = just (setEntry ss ∙ toggleValidity) , entry false I
... | nothing | _              | _       | _    = nothing , entry false I
... | just _  | nothing        | invalid | true = just (toggleEnable ∙ toggleValidity) , entry false I
... | just _  | just nothing   | valid   | _    = just (toggleEnable ∙ toggleValidity) , entry false I
... | just _  | just (just ss) | valid   | _    = just (toggleEnable ∙ setEntry ss) , entry false I
... | just _  | just (just ss) | invalid | _    = just (toggleEnable ∙ setEntry ss ∙ toggleValidity) , entry false I
... | just _  | _              | _       | _    = just toggleEnable , entry false I

entryF : ℕ → Abled → String → WC (Sig String (Maybe String) ×ᵀ InSig ⊤)
entryF size en name = _ , entry {en} {size} {name} {""} {valid} false I

container' : ∀ i/o → WComp' i/o (Container dir w₁ w₂) (pw i/o w₁ ×ᵀ pw i/o w₂)
container' I .step nothing .step = (nothing , nothing) , container' O
container' I .step (just (modLeft e))  .step = (just e , nothing) , container' O
container' I .step (just (modRight e)) .step = (nothing , just e) , container' O
container' O .step (nothing , nothing) .step = nothing , container' I
container' O .step (just x , nothing) .step = just (modLeft x) , container' I
container' O .step (nothing , just y) .step = just (modRight y) , container' I
container' O .step (just x , just y) .step = just (modLeft x ∙ modRight y) , container' I

container : (dir : Direction) → WComp' I w₁ r → WComp' I w₂ s → WComp' I (Container dir w₁ w₂) (r ×ᵀ s)
container _ p q = container' I ∘ᵀ (p ,ᵗ q)

fc : Direction → WC p → WC (Sig C D) → WC p
fc dir (_ , b) (_ , d) = _ , container' {dir} I ∘ᵀ ({-ease {I}-} b ,ᵗ ease {i/o = I} d) ∘ᵀ fstSig

infixr 3 _<->_
infixr 4 _<|>_

_<|>_ : WC p → WC (Sig C D) → WC p
_<|>_ = fc horizontal
_<->_ : WC p → WC (Sig C D) → WC p
_<->_ = fc vertical

infix 5 _⟦_⟧_
_⟦_⟧_ : WC p → IT (p ×ᵀ q) r → WC q → WC r
(_ , b) ⟦ t ⟧ (_ , d) = _ , container' {horizontal} I ∘ᵀ (b ,ᵗ d) ∘ᵀ t

entry'' : Abled → ℕ → String → WC (Sig String (Maybe String) ×ᵀ InSig ⊤)
entry'' en len name = entryF len en name ⟦ fstSig ⟧ label' name

entry' = λ len name → entry'' enabled len name ∘ʷ fstSig

addLabel : String → WC p → WC p
addLabel s x = x ⟦ fstSig ⟧ label'' s

---------------------------------------------------------------------------------------------------------------

counter = λ n → label' (showNat n) ⟦ swapIT ∘ᵀ enta (arr (const 1) ∘ᵗ accum _+_ n ∘ᵗ arr showNat) ⟧ button' "Count"

counter' = λ f b n → checkbox' b ∘ʷ noInput ⟦ enta (arr f ∘ᵗ accum _+_ n ∘ᵗ arr showNat) ⟧ label' (showNat n)

floatEntry = λ s → entry' 4 s ∘ʷ prismIT floatPrism
dateEntry = λ en s → entry'' en 4 s ∘ʷ (prismIT floatPrism ,ᵗ idIT)

showDates : (Float × Float) → String
showDates (a , b) = primStringAppend (primShowFloat a) (primStringAppend " -- " (primShowFloat b))

main = processMain (
       label' "count clicks:"
  <|>  counter 0

  <->  label' "count checks:"
  <|>  counter' (if_then 1 else 0) false 0

  <->  label' "count checks and unchecks:"
  <|>  counter' (const 1)          false 0

  <->  label' "count unchecks:"
  <|>  counter' (if_then 0 else 1) false 0

  <->  label' "copy input to label:"
  <|>  entry' 10 "" ∘ʷ noInput ⟦ enta (arr id) ⟧ label' ""

  <->  label' "converter:"
  <|>  floatEntry "Celsius" ⟦ entaBi (isoBi (mulIso 1.8) ∘ᵇ isoBi (plusIso 32.0)) ⟧ floatEntry "Fahrenheit"

  <->  label' "flight booker (unfinished):"
  <|>  ((comboBox' ("one-way" ∷ "return" ∷ []) zero
            ⟦ (mkIT' (arr ( maybe nothing (const (just _))  -- mapMaybe (const _) cannot be used because Agda bug #3380
                          )) (arr id) ,ᵗ (assocIT {i/o = O} ∘ᵀ swapIT))
            ∘ᵀ assocIT {i/o = O}
            ∘ᵀ (swapIT ∘ᵀ entangle ,ᵗ joinSig {i/o = I} 0.0 0.0) ∘ᵀ (swapIT ∘ᵀ fstSig)
            ⟧
       (dateEntry enabled "start date" ∘ʷ fstSig ⟦ idIT ⟧ dateEntry disabled "return date")) ∘ʷ noInput)
            ⟦  {-(isoIT (showDates) (const nothing)  ,ᵗ idIT) ∘ᵀ entangle-} enta (arr showDates)
            ⟧
       (label' "")
 )


text:
import SOAS.Families.Core

-- Various properties of context map operations
module SOAS.ContextMaps.Properties {T : Set}
  (open SOAS.Families.Core {T}) (𝒳 : Familyₛ) where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.ContextMaps.CategoryOfRenamings {T}
open import SOAS.ContextMaps.Combinators

open import Categories.Functor.Bifunctor
open import Categories.Object.Initial
open import Categories.Object.Coproduct
open import Categories.Category.Cocartesian
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (niHelper) renaming (refl to NI-refl)

private
  variable
    Γ Δ Θ Ξ : Ctx
    α : T

-- Copairing and injection
copair∘i₁ : {σ : Γ ~[ 𝒳 ]↝ Θ}{ς : Δ ~[ 𝒳 ]↝ Θ} (v : ℐ α Γ)
          → copair 𝒳 σ ς (∔.i₁ v) ≡ σ v
copair∘i₁ new = refl
copair∘i₁ {σ = σ} (old v) = copair∘i₁ {σ = σ ∘ old} v

copair∘i₂ : {σ : Γ ~[ 𝒳 ]↝ Θ}{ς : Δ ~[ 𝒳 ]↝ Θ} (v : ℐ α Δ)
          → copair 𝒳 σ ς (∔.i₂  {Γ} v) ≡ ς v
copair∘i₂ {Γ = ∅} v = refl
copair∘i₂ {Γ = α ∙ Γ} {σ = σ} v = copair∘i₂ {σ = σ ∘ old} v

-- Push function into copairing
f∘copair : (𝒳 {𝒴} : Familyₛ) (f : Θ ~[ 𝒳 ➔ 𝒴 ]↝ Ξ)(σ : Γ ~[ 𝒳 ]↝ Θ)(ς : Δ ~[ 𝒳 ]↝ Θ)
          (v : ℐ α (Γ ∔ Δ))
         → f (copair 𝒳 σ ς v) ≡ copair 𝒴 (f ∘ σ) (f ∘ ς) v
f∘copair {Γ = ∅} 𝒳 f σ ς v = refl
f∘copair {Γ = α ∙ Γ} 𝒳 f σ ς new = refl
f∘copair {Γ = α ∙ Γ} 𝒳 f σ ς (old v) = f∘copair 𝒳 f (σ ∘ old) ς v

ext: agda


text:
open import Data.Sum
open import Data.Fin
open import Data.Product
open import Data.Maybe
open import Signature

Σ-N∞ : Sig
Σ-N∞ = record { ∥_∥ = Fin 2 ; ar = Σ-N∞-ar }
  where
    Σ-N∞-ar : Fin 2 → Set
    Σ-N∞-ar zero    = Fin 0
    Σ-N∞-ar (suc zero) = Fin 1
    Σ-N∞-ar (suc (suc ()))

D-N∞ : Set
D-N∞ = Fin 1

open import MixedTest Σ-N∞ D-N∞ as LP-N∞ renaming (Term to N∞μ; CoTerm to N∞)

stop' : N∞μ
stop' = cons (# 0 , λ())

step' : N∞ → N∞μ
step' x = (cons (# 1 , (λ _ → inj₂ x)))

-- Immediate stop -> 0
stop : N∞
destr stop zero = just (inj₁ stop')
destr stop (suc ())

-- Do a step -> successor
succ : N∞ → N∞
destr (succ x) zero    = just (inj₁ (step' x))
destr (succ x) (suc ())

-- Not actually in N∞
foo : N∞
destr foo x = nothing

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Base.Extensionality where

open import Level                                 using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_)

-- Postualting extensionality is consistent with agdas underlying theory.
postulate
  ext : ∀ {ℓ ℓ′ : Level} {A : Set ℓ} {B : A → Set ℓ′} {f g : (x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Magma.Construct.Unit where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Magma

open import Cubical.Data.Unit

_◯_ : Op₂ ⊤
_ ◯ _ = tt

⊤-isMagma : IsMagma ⊤ _◯_
⊤-isMagma = record { is-set = isSet⊤ }

⊤-Magma : Magma ℓ-zero
⊤-Magma = record { isMagma = ⊤-isMagma }


text:
------------------------------------------------------------------------
-- A monad-like structure
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Delay-monad.Sized.Monad where

open import Prelude
open import Prelude.Size

open import Delay-monad.Sized
open import Delay-monad.Sized.Bisimilarity

------------------------------------------------------------------------
-- Monadic combinators

-- Return.

return : ∀ {i a} {A : Size → Type a} → A i → Delay A i
return = now

-- Map. Note the function argument's type.

map : ∀ {i a b} {A : Size → Type a} {B : Size → Type b} →
      ({j : Size< (ssuc i)} → A j → B j) → Delay A i → Delay B i
map f (now   x) = now (f x)
map f (later x) = later λ { .force → map f (force x) }

-- Join.

join : ∀ {i a} {A : Size → Type a} →
       Delay (Delay A) i → Delay A i
join (now   x) = x
join (later x) = later λ { .force → join (force x) }

-- Bind. Note the function argument's type.

infixl 5 _>>=_

_>>=_ : ∀ {i a b} {A : Size → Type a} {B : Size → Type b} →
        Delay A i → ({j : Size< (ssuc i)} → A j → Delay B j) →
        Delay B i
x >>= f = join (map f x)

------------------------------------------------------------------------
-- Monad laws

left-identity :
  ∀ {a b} {A : Size → Type a} {B : Size → Type b}
  x (f : ∀ {i} → A i → Delay B i) →
  return x >>= f ∼ f x
left-identity x f = reflexive (f x)

right-identity : ∀ {a i} {A : Size → Type a} (x : Delay A ∞) →
                 [ i ] x >>= return ∼ x
right-identity (now   x) = now
right-identity (later x) = later λ { .force →
                             right-identity (force x) }

associativity :
  ∀ {a b c i}
    {A : Size → Type a} {B : Size → Type b} {C : Size → Type c} →
  (x : Delay A ∞) (f : ∀ {i} → A i → Delay B i)
  (g : ∀ {i} → B i → Delay C i) →
  [ i ] x >>= (λ x → f x >>= g) ∼ x >>= f >>= g
associativity (now   x) f g = reflexive (f x >>= g)
associativity (later x) f g = later λ { .force →
                                associativity (force x) f g }

------------------------------------------------------------------------
-- The functions map, join and _>>=_ preserve strong and weak
-- bisimilarity and expansion

map-cong : ∀ {k i a b} {A : Size → Type a} {B : Size → Type b}
           (f : ∀ {i} → A i → B i) {x y : Delay A ∞} →
           [ i ] x ⟨ k ⟩ y → [ i ] map f x ⟨ k ⟩ map f y
map-cong f now        = now
map-cong f (later  p) = later λ { .force → map-cong f (force p) }
map-cong f (laterˡ p) = laterˡ (map-cong f p)
map-cong f (laterʳ p) = laterʳ (map-cong f p)

join-cong : ∀ {k i a} {A : Size → Type a} {x y : Delay (Delay A) ∞} →
              [ i ] x ⟨ k ⟩ y → [ i ] join x ⟨ k ⟩ join y
join-cong now        = reflexive _
join-cong (later  p) = later λ { .force → join-cong (force p) }
join-cong (laterˡ p) = laterˡ (join-cong p)
join-cong (laterʳ p) = laterʳ (join-cong p)

infixl 5 _>>=-cong_

_>>=-cong_ :
  ∀ {k i a b} {A : Size → Type a} {B : Size → Type b}
    {x y : Delay A ∞} {f g : ∀ {i} → A i → Delay B i} →
  [ i ] x ⟨ k ⟩ y → (∀ z → [ i ] f z ⟨ k ⟩ g z) →
  [ i ] x >>= f ⟨ k ⟩ y >>= g
now      >>=-cong q = q _
later  p >>=-cong q = later λ { .force → force p >>=-cong q }
laterˡ p >>=-cong q = laterˡ (p >>=-cong q)
laterʳ p >>=-cong q = laterʳ (p >>=-cong q)

------------------------------------------------------------------------
-- A lemma

-- The function map can be expressed using _>>=′_ and now.

map∼>>=-now :
  ∀ {i a b} {A : Size → Type a} {B : Size → Type b}
    {f : ∀ {i} → A i → B i} (x : Delay A ∞) →
  [ i ] map f x ∼ x >>= now ∘ f
map∼>>=-now (now x)   = now
map∼>>=-now (later x) = later λ { .force → map∼>>=-now (x .force) }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Category.Monoidal.Instance.Setoids where

open import Level
open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function.Equality
open import Relation.Binary using (Setoid)

open import Categories.Category
open import Categories.Category.Instance.Setoids
open import Categories.Category.Cartesian
open import Categories.Category.Instance.SingletonSet

module _ {o ℓ} where

  Setoids-Cartesian : Cartesian (Setoids o ℓ)
  Setoids-Cartesian = record
    { terminal = SingletonSetoid-⊤
    ; products = record
      { product = λ {A B} →
        let module A = Setoid A
            module B = Setoid B
         in record
          { A×B      = ×-setoid A B -- the stdlib doesn't provide projections!
          ; π₁       = record
            { _⟨$⟩_ = proj₁
            ; cong  = proj₁
            }
          ; π₂       = record
            { _⟨$⟩_ = proj₂
            ; cong  = proj₂
            }
          ; ⟨_,_⟩    = λ f g → record
            { _⟨$⟩_ = λ x → f ⟨$⟩ x , g ⟨$⟩ x
            ; cong  = λ eq → cong f eq , cong g eq
            }
          ; project₁ = λ {_ h i} eq → cong h eq
          ; project₂ = λ {_ h i} eq → cong i eq
          ; unique   = λ {W h i j} eq₁ eq₂ eq → A.sym (eq₁ (Setoid.sym W eq)) , B.sym (eq₂ (Setoid.sym W eq))
          }
      }
    }

  module Setoids-Cartesian = Cartesian Setoids-Cartesian
  open Setoids-Cartesian renaming (monoidal to Setoids-Monoidal) public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --without-K #-}
module Data.Inductive.Higher.Interval where

open import Relation.Equality
open import Relation.Path.Operation

-- The interval, which we denote I, is perhaps an even simpler higher inductive type than the
-- circle generated by:
module Interval where
  private
    data #I : Set where
      #0 : #I
      #1 : #I

  I : Set
  I = #I

  -- A point 0ᵢ
  0ᵢ : I
  0ᵢ = #0

  -- A point 1₁
  1ᵢ : I
  1ᵢ = #1

  postulate -- A path segment
    path-seg : 0ᵢ ≡ 1ᵢ

  -- "The recursion principle for the interval says that given a type B along with
  interval-rec : ∀ {b} {B : Set b} →
                       (b₀ b₁ : B) → -- points b₀, b₁ and
                       (p : b₀ ≡ b₁) → -- a path b₀ ≡ b₁
                       (i : I) → B -- there is a function f : I → B such that
  interval-rec b₀ b₁ p #0 = b₀ -- f(0ᵢ) ≡ b₀
  interval-rec b₀ b₁ p #1 = b₁ -- f(1ᵢ) ≡ b₁"

  -- The induction principle says that given P : I → U along with
  interval-ind : ∀ {b} (P : I → Set b)
                       (b₀ : P 0ᵢ) → -- a point b₀ : P(0ᵢ)
                       (b₁ : P 1ᵢ) → -- a point b₁ : P(1ᵢ) and
                       (p : transport {_}{_}{I}{P} path-seg b₀ ≡ b₁) →
                       ∀ i → P i -- there is a function f : Π(x:I) P(x) such that
  interval-ind P b₀ b₁ p #0 = b₀ -- f(0ᵢ) ≡ b₀
  interval-ind P b₀ b₁ p #1 = b₁ -- f(1ᵢ) ≡ b₁"
open Interval public

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Haskell.Prim.Either where

open import Haskell.Prim
open import Haskell.Prim.Bool

--------------------------------------------------
-- Either

data Either (a b : Set) : Set where
  Left  : a → Either a b
  Right : b → Either a b

either : (a → c) → (b → c) → Either a b → c
either f g (Left  x) = f x
either f g (Right y) = g y

testBool : (b : Bool) → Either (IsFalse b) (IsTrue b)
testBool false = Left  itsFalse
testBool true  = Right itsTrue


text:
module Rat where

open import Data.Empty
open import Data.Unit
import Data.Sign as S
open import Data.String
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Nat.Coprimality renaming (sym to symCoprime)
open import Data.Nat.GCD
open import Data.Nat.Show renaming (show to ℕshow)
open import Data.Nat.Divisibility
open import Data.Integer hiding (_-_ ; -_)
  renaming (_+_ to _ℤ+_ ; _*_ to _ℤ*_ ; _≟_ to _ℤ≟_ ; show to ℤshow)
open import Data.Integer.Properties
open import Data.Rational
open import Data.Product
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

infix  8 -_ 1/_
infixl 7 _*_ _/_
infixl 6 _-_ _+_

------------------------------------------------------------------------------
-- Two lemmas to help with operations on rationals

NonZero : ℕ → Set
NonZero 0       = ⊥
NonZero (suc _) = ⊤

-- normalize takes two natural numbers, say 6 and 21 and their gcd 3, and
-- returns them normalized as 2 and 7 and a proof that they are coprime

normalize : ∀ {m n g} → {n≢0 : NonZero n} → {g≢0 : NonZero g} →
            GCD m n g → Σ[ p ∈ ℕ ] Σ[ q ∈ ℕ ] False (q ℕ.≟ 0) × Coprime p q
normalize {m} {n} {0} {_} {()} _
normalize {m} {n} {ℕ.suc g} {_} {_} G with Bézout.identity G
normalize {m} {.0} {ℕ.suc g} {()} {_}
  (GCD.is (divides p m≡pg' , divides 0 refl) _) | _
normalize {m} {n} {ℕ.suc g} {_} {_}
  (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _) | Bézout.+- x y eq =
    (p , ℕ.suc q , tt , Bézout-coprime {p} {ℕ.suc q} {g} (Bézout.+- x y
               (begin
                 ℕ.suc g ℕ.+ y ℕ.* (ℕ.suc q ℕ.* ℕ.suc g)
               ≡⟨ cong (λ h → ℕ.suc g ℕ.+ y ℕ.* h) (sym n≡qg') ⟩
                 ℕ.suc g ℕ.+ y ℕ.* n
               ≡⟨ eq ⟩
                 x ℕ.* m
               ≡⟨ cong (λ h → x ℕ.* h) m≡pg' ⟩
                 x ℕ.* (p ℕ.* ℕ.suc g) ∎)))
normalize {m} {n} {ℕ.suc g} {_} {_}
  (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _) | Bézout.-+ x y eq =
    (p , ℕ.suc q , tt , Bézout-coprime {p} {ℕ.suc q} {g} (Bézout.-+ x y
               (begin
                 ℕ.suc g ℕ.+ x ℕ.* (p ℕ.* ℕ.suc g)
               ≡⟨ cong (λ h → ℕ.suc g ℕ.+ x ℕ.* h) (sym m≡pg') ⟩
                 ℕ.suc g ℕ.+ x ℕ.* m
               ≡⟨ eq ⟩
                 y ℕ.* n
               ≡⟨ cong (λ h → y ℕ.* h) n≡qg' ⟩
                 y ℕ.* (ℕ.suc q ℕ.* ℕ.suc g) ∎)))

-- a version of gcd that returns a proof that the result is non-zero given
-- that one of the inputs is non-zero

gcd≢0 : (m n : ℕ) → {m≢0 : NonZero m} → ∃ λ d → GCD m n d × NonZero d
gcd≢0 m  n {m≢0} with gcd m n
gcd≢0 m  n {m≢0} | (0 , GCD.is (0|m , _) _) with 0∣⇒≡0 0|m
gcd≢0 .0 n {()}  | (0 , GCD.is (0|m , _) _) | refl
gcd≢0 m  n {_}   | (ℕ.suc d , G) = (ℕ.suc d , G , tt)

------------------------------------------------------------------------------
-- Operations on rationals: unary -, reciprocal, multiplication, addition

-- unary negation
--
-- Andreas Abel says: Agda's type-checker is incomplete when it has to handle
-- types with leading hidden quantification, such as the ones of Coprime m n
-- and c.  A work around is to use hidden abstraction explicitly.  In your
-- case, giving λ {i} -> c works.  Not pretty, but unavoidable until we
-- improve on the current heuristics. I recorded this as a bug
-- http://code.google.com/p/agda/issues/detail?id=1079

-_ : ℚ → ℚ
-_ p with ℚ.numerator p | ℚ.denominator-1 p | toWitness (ℚ.isCoprime p)
... | -[1+ n ]  | d | c = (+ ℕ.suc n ÷ ℕ.suc d) {fromWitness (λ {i} → c)}
... | + 0       | d | _ = p
... | + ℕ.suc n | d | c = (-[1+ n ]  ÷ ℕ.suc d) {fromWitness (λ {i} → c)}

-- reciprocal: requires a proof that the numerator is not zero

1/_ : (p : ℚ) → {n≢0 : NonZero ∣ ℚ.numerator p ∣} → ℚ
1/_ p {n≢0} with ℚ.numerator p | ℚ.denominator-1 p | toWitness (ℚ.isCoprime p)
1/_ p {()} | + 0 | d | c
... | + (ℕ.suc n) | d | c =
  ((S.+ ◃ ℕ.suc d) ÷ ℕ.suc n)
  {fromWitness (λ {i} →
    subst (λ h → Coprime h (ℕ.suc n))
          (sym (abs-◃ S.+ (ℕ.suc d)))
          (symCoprime c))}
... | -[1+ n ] | d | c =
  ((S.- ◃ ℕ.suc d) ÷ ℕ.suc n)
  {fromWitness (λ {i} →
    subst (λ h → Coprime h (ℕ.suc n))
          (sym (abs-◃ S.- (ℕ.suc d)))
          (symCoprime c))}

-- multiplication

private

  helper* : (n₁ : ℤ) → (d₁ : ℕ) → (n₂ : ℤ) → (d₂ : ℕ) →
            {n≢0 : NonZero ∣ n₁ ℤ* n₂ ∣} →
            {d≢0 : NonZero (d₁ ℕ.* d₂)} →
            ℚ
  helper* n₁ d₁ n₂ d₂ {n≢0} {d≢0} =
    let n = n₁ ℤ* n₂
        d = d₁ ℕ.* d₂
        (g , G , g≢0) = gcd≢0 ∣ n ∣ d {n≢0}
        (nn , nd , nd≢0 , nc) = normalize {∣ n ∣} {d} {g} {d≢0} {g≢0} G
    in ((sign n ◃ nn) ÷ nd)
       {fromWitness (λ {i} →
          subst (λ h → Coprime h nd) (sym (abs-◃ (sign n) nn)) nc)}
       {nd≢0}

_*_ : ℚ → ℚ → ℚ
p₁ * p₂ with ℚ.numerator p₁ | ℚ.numerator p₂
... | + 0  | _    = + 0 ÷ 1
... | _    | + 0  = + 0 ÷ 1
... | + ℕ.suc n₁ | + ℕ.suc n₂ =
  helper* (+ ℕ.suc n₁) (ℕ.suc (ℚ.denominator-1 p₁))
          (+ ℕ.suc n₂) (ℕ.suc (ℚ.denominator-1 p₂))
... | + ℕ.suc n₁ | -[1+ n₂ ] =
  helper* (+ ℕ.suc n₁) (ℕ.suc (ℚ.denominator-1 p₁))
          -[1+ n₂ ] (ℕ.suc (ℚ.denominator-1 p₂))
... | -[1+ n₁ ] | + ℕ.suc n₂ =
  helper* -[1+ n₁ ] (ℕ.suc (ℚ.denominator-1 p₁))
          (+ ℕ.suc n₂) (ℕ.suc (ℚ.denominator-1 p₂))
... | -[1+ n₁ ] | -[1+ n₂ ] =
  helper* -[1+ n₁ ] (ℕ.suc (ℚ.denominator-1 p₁))
          -[1+ n₂ ] (ℕ.suc (ℚ.denominator-1 p₂))

-- addition

private

  helper+ : (n : ℤ) → (d : ℕ) → {d≢0 : NonZero d} → ℚ
  helper+ (+ 0) d {d≢0} = + 0 ÷ 1
  helper+ (+ ℕ.suc n) d {d≢0} =
    let (g , G , g≢0) = gcd≢0 ∣ + ℕ.suc n ∣ d {tt}
        (nn , nd , nd≢0 , nc) = normalize {∣ + ℕ.suc n ∣} {d} {g} {d≢0} {g≢0} G
    in ((S.+ ◃ nn) ÷ nd)
       {fromWitness (λ {i} →
          subst (λ h → Coprime h nd) (sym (abs-◃ S.+ nn)) nc)}
       {nd≢0}
  helper+ -[1+ n ] d {d≢0} =
    let (g , G , g≢0) = gcd≢0 ∣ -[1+ n ] ∣ d {tt}
        (nn , nd , nd≢0 , nc) = normalize {∣ -[1+ n ] ∣} {d} {g} {d≢0} {g≢0} G
    in ((S.- ◃ nn) ÷ nd)
       {fromWitness (λ {i} →
          subst (λ h → Coprime h nd) (sym (abs-◃ S.- nn)) nc)}
       {nd≢0}

_+_ : ℚ → ℚ → ℚ
p₁ + p₂ =
  let n₁ = ℚ.numerator p₁
      d₁ = ℕ.suc (ℚ.denominator-1 p₁)
      n₂ = ℚ.numerator p₂
      d₂ = ℕ.suc (ℚ.denominator-1 p₂)
      n = (n₁ ℤ* + d₂) ℤ+ (n₂ ℤ* + d₁)
      d = d₁ ℕ.* d₂
  in helper+ n d

-- subtraction and division

_-_ : ℚ → ℚ → ℚ
p₁ - p₂ = p₁ + (- p₂)

_/_ : (p₁ p₂ : ℚ) → {n≢0 : NonZero ∣ ℚ.numerator p₂ ∣} → ℚ
_/_ p₁ p₂ {n≢0} = p₁ * (1/_ p₂ {n≢0})

-- conventional printed representation

show : ℚ → String
show p = ℤshow (ℚ.numerator p) ++ "/" ++ ℕshow (ℕ.suc (ℚ.denominator-1 p))

------------------------------------------------------------------------------
-- A few constants and some small tests

0ℚ 1ℚ : ℚ
0ℚ = + 0 ÷ 1
1ℚ = + 1 ÷ 1

private

  p₀ p₁ p₂ p₃ : ℚ
  p₀ = + 1 ÷ 2
  p₁ = + 1 ÷ 3
  p₂ = -[1+ 2 ] ÷ 4
  p₃ = + 3 ÷ 4

  test₀ = show p₂
  test₁ = show (- p₂)
  test₂ = show (1/ p₂)
  test₃ = show (p₀ + p₀)
  test₄ = show (p₁ * p₂)

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.DescendingList where

open import Cubical.Data.DescendingList.Base public
open import Cubical.Data.DescendingList.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --cubical --safe #-}

module Algebra.Construct.Free.Semilattice.Relation.Unary where

open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Def public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Dec public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Properties public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.All.Map public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Membership public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Def public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Dec public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Properties public
open import Algebra.Construct.Free.Semilattice.Relation.Unary.Any.Map public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Nat
open import Prelude
open import core
open import contexts

open import progress
open import lemmas-complete

module complete-progress where
  -- as in progress, we define a datatype for the possible outcomes of
  -- progress for readability.
  data okc : (d : iexp) (Δ : hctx) → Set where
    V : ∀{d Δ} → d val → okc d Δ
    S : ∀{d Δ} → Σ[ d' ∈ iexp ] (d ↦ d') → okc d Δ

  complete-progress : {Δ : hctx} {d : iexp} {τ : typ} →
                       Δ , ∅ ⊢ d :: τ →
                       d dcomplete →
                       okc d Δ
  complete-progress wt comp with progress wt
  complete-progress wt comp | S x = S x
  complete-progress wt comp | I x = abort (lem-ind-comp comp x)
  complete-progress wt comp | BV x = V (lem-comp-boxed-val wt comp x)

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import lemmas-consistency
open import lemmas-ground

open import progress-checks

open import canonical-boxed-forms
open import canonical-value-forms
open import canonical-indeterminate-forms

open import ground-decidable
open import htype-decidable

module progress where
  -- this is a little bit of syntactic sugar to avoid many layer nested Inl
  -- and Inrs that you would get from the more literal transcription of the
  -- consequent of progress
  data ok : (d : ihexp) (Δ : hctx) → Set where
    S  : ∀{d Δ} → Σ[ d' ∈ ihexp ] (d ↦ d') → ok d Δ
    I  : ∀{d Δ} → d indet → ok d Δ
    BV : ∀{d Δ} → d boxedval → ok d Δ

  progress : {Δ : hctx} {d : ihexp} {τ : htyp} →
             Δ , ∅ ⊢ d :: τ →
             ok d Δ
    -- constants
  progress TANum = BV (BVVal VNum)

    -- addition
  progress (TAPlus wt1 wt2) with progress wt1 | progress wt2
    -- if the left steps, the whole thing steps
  ... | S (_ , Step x y z) | _  = S (_ , Step (FHPlus1 x) y (FHPlus1 z))
  ... | I _ | S (_ , Step x y z) = S (_ , Step (FHPlus2 x) y (FHPlus2 z))
  ... | BV _ | S (_ , Step x y z) = S (_ , Step (FHPlus2 x) y (FHPlus2 z))
  ... | I x | I x₁ = I (IPlus1 x (FIndet x₁))
  ... | I x | BV x₁ = I (IPlus1 x (FBoxedVal x₁))
  ... | BV (BVVal VNum) | I x = I (IPlus2 (FBoxedVal (BVVal VNum)) x)
  ... | BV (BVVal VNum) | BV (BVVal VNum) = S (_ , Step FHOuter (ITPlus refl) FHOuter)

    -- variables
  progress (TAVar x₁) = abort (somenotnone (! x₁))

    -- lambdas
  progress (TALam _ wt) = BV (BVVal VLam)

    -- applications
  progress (TAAp wt1 wt2)
    with progress wt1 | progress wt2
    -- if the left steps, the whole thing steps
  ... | S (_ , Step x y z) | _ = S (_ , Step (FHAp1 x) y (FHAp1 z))
    -- if the left is indeterminate, step the right
  ... | I i | S (_ , Step x y z) = S (_ , Step (FHAp2 x) y (FHAp2  z))
    -- if they're both indeterminate, step when the cast steps and indet otherwise
  ... | I x | I y
    with canonical-indeterminate-forms-arr wt1 x
  ... | CIFACast (_ , _ , _ , _ , _ , refl , _ , _ ) = S (_ , Step FHOuter ITApCast FHOuter)
  ... | CIFAEHole (_ , _ , _ , refl , _)             = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFANEHole (_ , _ , _ , _ , _ , refl , _)    = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFAAp (_ , _ , _ , _ , _ , refl , _)        = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFACastHole (_ , refl , refl , refl , _ )   = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFAFailedCast (_ , _ , refl , _ )           = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFACase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFAFst (_ , _ , refl , _ , _ , _ , _) = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  ... | CIFASnd (_ , _ , refl , _ , _ , _ , _) = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))

    -- similar if the left is indeterminate but the right is a boxed val
  progress (TAAp wt1 wt2) | I x | BV y
    with canonical-indeterminate-forms-arr wt1 x
  ... | CIFACast (_ , _ , _ , _ , _ , refl , _ , _ ) = S (_ , Step FHOuter ITApCast FHOuter)
  ... | CIFAEHole (_ , _ , _ , refl , _)             = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFANEHole (_ , _ , _ , _ , _ , refl , _)    = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFAAp (_ , _ , _ , _ , _ , refl , _)        = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFACastHole (_ , refl , refl , refl , _ )   = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFAFailedCast (_ , _ , refl , _ )           = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFACase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFAFst (_ , _ , refl , _ , _ , _ , _) = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  ... | CIFASnd (_ , _ , refl , _ , _ , _ , _) = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))

    -- if the left is a boxed value, inspect the right
  progress (TAAp wt1 wt2) | BV v | S (_ , Step x y z) = S (_ , Step (FHAp2  x) y (FHAp2  z))
  progress (TAAp wt1 wt2) | BV v | I i
    with canonical-boxed-forms-arr wt1 v
  ... | CBFALam (_ , _ , refl , _)             = S (_ , Step FHOuter ITLam FHOuter)
  ... | CBFACastArr (_ , _ , _ , refl , _ , _) = S (_ , Step FHOuter ITApCast FHOuter)
  progress (TAAp wt1 wt2) | BV v | BV v₂
    with canonical-boxed-forms-arr wt1 v
  ... | CBFALam (_ , _ , refl , _)             = S (_ , Step FHOuter ITLam FHOuter)
  ... | CBFACastArr (_ , _ , _ , refl , _ , _) = S (_ , Step FHOuter ITApCast FHOuter)

    -- sum types
  progress (TAInl wt)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHInl x) y (FHInl z))
  ... | I x = I (IInl x)
  ... | BV x = BV (BVInl x)
  progress (TAInr wt)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHInr x) y (FHInr z))
  ... | I x = I (IInr x)
  ... | BV x = BV (BVInr x)
  progress (TACase wt _ wt₁ _ wt₂)
    with progress wt
  ... | S (_ , Step x y z)  = S (_ , Step (FHCase x) y (FHCase z))
  progress (TACase () _ wt₁ _ wt₂) | BV (BVVal VNum)
  progress (TACase () _ wt₁ _ wt₂) | BV (BVVal VLam)
  progress (TACase () _ wt₁ _ wt₂) | BV (BVVal (VPair x x₁))
  progress (TACase wt _ wt₁ _ wt₂) | BV (BVVal (VInl x)) = S (_ , Step FHOuter ITCaseInl FHOuter)
  ... | BV (BVVal (VInr x)) = S (_ , Step FHOuter ITCaseInr FHOuter)
  ... | BV (BVInl x)        = S (_ , Step FHOuter ITCaseInl FHOuter)
  ... | BV (BVInr x)        = S (_ , Step FHOuter ITCaseInr FHOuter)
  ... | BV (BVSumCast x x₁) = S (_ , Step FHOuter ITCaseCast FHOuter)
  ... | I (IAp x x₁ x₂) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (IAp x x₁ x₂))
  ... | I (IInl x) = S (_ , Step FHOuter ITCaseInl FHOuter)
  ... | I (IInr x) = S (_ , Step FHOuter ITCaseInr FHOuter)
  ... | I (ICase x x₁ x₂ x₃) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (ICase x x₁ x₂ x₃))
  ... | I (IFst x x₁ x₂) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (IFst x x₁ x₂))
  ... | I (ISnd x x₁ x₂) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (ISnd x x₁ x₂))
  ... | I IEHole = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) IEHole)
  ... | I (INEHole x) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (INEHole x))
  ... | I (ICastSum x x₁) = S (_ , Step FHOuter ITCaseCast FHOuter)
  ... | I (ICastHoleGround x x₁ x₂) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (ICastHoleGround x x₁ x₂))
  ... | I (IFailedCast x x₁ x₂ x₃) = I (ICase (λ _ _ ()) (λ _ _ ()) (λ _ _ _ _ _ ()) (IFailedCast x x₁ x₂ x₃))

    --product types
  progress (TAPair wt₁ wt₂)
    with progress wt₁ | progress wt₂
  ... | S (_ , Step x y z) | _  = S (_ , Step (FHPair1 x) y (FHPair1 z))
  ... | I _ | S (_ , Step x y z) = S (_ , Step (FHPair2 x) y (FHPair2 z))
  ... | BV _ | S (_ , Step x y z) = S (_ , Step (FHPair2 x) y (FHPair2 z))
  ... | I x | I x₁ = I (IPair1 x (FIndet x₁))
  ... | I x | BV x₁ = I (IPair1 x (FBoxedVal x₁))
  ... | BV x | I x₁ = I (IPair2 (FBoxedVal x) x₁)
  ... | BV x | BV x₁ = BV (BVPair x x₁)
  progress (TAFst wt)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHFst x) y (FHFst z))
  ... | I (IAp x x₁ x₂) = I (IFst (λ _ _ ()) (λ _ _ _ _ _()) (IAp x x₁ x₂))
  ... | I (ICase x x₁ x₂ x₃) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (ICase x x₁ x₂ x₃))
  ... | I (IPair1 x x₁) = S (_ , Step FHOuter ITFstPair FHOuter)
  ... | I (IPair2 x x₁) = S (_ , Step FHOuter ITFstPair FHOuter)
  ... | I (IFst x x₁ x₂) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (IFst x x₁ x₂))
  ... | I (ISnd x x₁ x₂) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (ISnd x x₁ x₂))
  ... | I IEHole = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) IEHole)
  ... | I (INEHole x) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (INEHole x))
  ... | I (ICastProd x x₁) = S (_ , Step FHOuter ITFstCast FHOuter)
  ... | I (ICastHoleGround x x₁ x₂) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (ICastHoleGround x x₁ x₂))
  ... | I (IFailedCast x x₁ x₂ x₃) = I (IFst (λ _ _ ()) (λ _ _ _ _ _ ()) (IFailedCast x x₁ x₂ x₃))
  ... | BV (BVVal (VPair x x₁)) = S (_ , Step FHOuter ITFstPair FHOuter)
  ... | BV (BVPair x x₁) = S (_ , Step FHOuter ITFstPair FHOuter)
  ... | BV (BVProdCast x x₁) = S (_ , Step FHOuter ITFstCast FHOuter)
  progress (TASnd wt)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHSnd x) y (FHSnd z))
  ... | I (IAp x x₁ x₂) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (IAp x x₁ x₂))
  ... | I (ICase x x₁ x₂ x₃) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (ICase x x₁ x₂ x₃))
  ... | I (IPair1 x x₁) = S (_ , Step FHOuter ITSndPair FHOuter)
  ... | I (IPair2 x x₁) = S (_ , Step FHOuter ITSndPair FHOuter)
  ... | I (IFst x x₁ x₂) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (IFst x x₁ x₂))
  ... | I (ISnd x x₁ x₂) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (ISnd x x₁ x₂))
  ... | I IEHole = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) IEHole)
  ... | I (INEHole x) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (INEHole x))
  ... | I (ICastProd x x₁) = S (_ , Step FHOuter ITSndCast FHOuter)
  ... | I (ICastHoleGround x x₁ x₂) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (ICastHoleGround x x₁ x₂))
  ... | I (IFailedCast x x₁ x₂ x₃) = I (ISnd (λ _ _ ()) (λ _ _ _ _ _ ()) (IFailedCast x x₁ x₂ x₃))
  ... | BV (BVVal (VPair x x₁)) = S (_ , Step FHOuter ITSndPair FHOuter)
  ... | BV (BVPair x x₁) = S (_ , Step FHOuter ITSndPair FHOuter)
  ... | BV (BVProdCast x x₁) = S (_ , Step FHOuter ITSndCast FHOuter)

    -- empty holes are indeterminate
  progress (TAEHole _ _ ) = I IEHole

    -- nonempty holes step if the innards step, indet otherwise
  progress (TANEHole xin wt x₁)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHNEHole x) y (FHNEHole z))
  ... | I  x = I (INEHole (FIndet x))
  ... | BV x = I (INEHole (FBoxedVal x))

    -- casts
  progress (TACast wt con)
    with progress wt
    -- step if the innards step
  ... | S (_ , Step x y z) = S (_ , Step (FHCast x) y (FHCast z))
    -- if indet, inspect how the types in the cast are realted by consistency:
    -- if they're the same, step by ID
  progress (TACast wt TCRefl)  | I x = S (_ , Step FHOuter ITCastID FHOuter)
    -- if first type is hole
  progress (TACast {τ1 = τ1} wt TCHole1) | I x
    with τ1
  ... | num = I (ICastGroundHole GNum x)
  ... | ⦇-⦈ = S (_ , Step FHOuter ITCastID FHOuter)
  ... | τ11 ==> τ12
    with ground-decidable (τ11 ==> τ12)
  ... | Inl GArrHole = I (ICastGroundHole GArrHole x)
  ... | Inr y =  S (_ , Step FHOuter (ITGround (MGArr (π1 (ground-not-holes y)))) FHOuter)
  progress (TACast {τ1 = τ1} wt TCHole1) | I x | τ11 ⊕ τ12
    with ground-decidable (τ11 ⊕ τ12)
  ... | Inl GSumHole = I (ICastGroundHole GSumHole x)
  ... | Inr y =  S (_ , Step FHOuter (ITGround (MGSum (π1 (π2 (ground-not-holes y))))) FHOuter)
  progress (TACast {τ1 = τ1} wt TCHole1) | I x | τ11 ⊠ τ12
    with ground-decidable (τ11 ⊠ τ12)
  ... | Inl GProdHole = I (ICastGroundHole GProdHole x)
  ... | Inr y = S (_ , Step FHOuter (ITGround (MGProd (π2 (π2 (ground-not-holes y))))) FHOuter)
    -- if second type is hole
  progress (TACast wt (TCHole2 {num})) | I x
    with canonical-indeterminate-forms-hole wt x
  ... | CIFHEHole (_ , _ , _ , refl , f)           = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHNEHole (_ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHAp (_ , _ , _ , refl , _ )             = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHCase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHFst (_ , _ , refl , _ , _ , _ , _)  = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHSnd (_ , _ , refl , _ , _ , _ , _)  = I (ICastHoleGround (λ _ _ ()) x GNum)
  ... | CIFHCast (_ , τ , refl , _ , grn , _)
    with htype-dec τ num
  ... | Inl refl = S (_ , Step FHOuter (ITCastSucceed grn ) FHOuter)
  ... | Inr y    = S (_ , Step FHOuter (ITCastFail grn GNum y) FHOuter)

  progress (TACast wt (TCHole2 {⦇-⦈}))| I x = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt (TCHole2 {τ11 ==> τ12})) | I x
    with ground-decidable (τ11 ==> τ12)
  ... | Inr y = S (_ , Step FHOuter (ITExpand (MGArr (π1 (ground-not-holes y)))) FHOuter)
  ... | Inl GArrHole
    with canonical-indeterminate-forms-hole wt x
  ... | CIFHEHole (_ , _ , _ , refl , _)            = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHNEHole (_ , _ , _ , _ , _ , refl , _)   = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHAp (_ , _ , _ , refl , _ )              = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHCase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHFst (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHSnd (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GArrHole)
  ... | CIFHCast (_ , ._ , refl , _ , GNum , _)     = S (_ , Step FHOuter (ITCastFail GNum GArrHole (λ ())) FHOuter)
  ... | CIFHCast (_ , ._ , refl , _ , GArrHole , _) = S (_ , Step FHOuter (ITCastSucceed GArrHole) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GSumHole , _)  = S (_ , Step FHOuter (ITCastFail GSumHole GArrHole (λ ())) FHOuter)
  ... | CIFHCast (_ , ._ , refl , _ , GProdHole , _) = S (_ , Step FHOuter (ITCastFail GProdHole GArrHole (λ ())) FHOuter)

  progress (TACast wt (TCHole2 {τ11 ⊕ τ12})) | I x
    with ground-decidable (τ11 ⊕ τ12)
  ... | Inr y = S (_ , Step FHOuter (ITExpand (MGSum (π1 (π2 (ground-not-holes y))))) FHOuter)
  ... | Inl GSumHole
    with canonical-indeterminate-forms-hole wt x
  ... | CIFHEHole (_ , _ , _ , refl , _)           = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHNEHole (_ , _ , _ , _ , _ , refl , _)  = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHAp (_ , _ , _ , refl , _ )             = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHCase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHFst (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHSnd (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GSumHole)
  ... | CIFHCast (_ , _ , refl , _ , GNum , _)     = S (_ , Step FHOuter (ITCastFail GNum GSumHole (λ ())) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GArrHole , _) = S (_ , Step FHOuter (ITCastFail GArrHole GSumHole (λ ())) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GSumHole , _) = S (_ , Step FHOuter (ITCastSucceed GSumHole) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GProdHole , _) = S (_ , Step FHOuter (ITCastFail GProdHole GSumHole λ ()) FHOuter)
  progress (TACast wt (TCHole2 {τ11 ⊠ τ12})) | I x
    with ground-decidable (τ11 ⊠ τ12)
  ... | Inr y = S (_ , Step FHOuter (ITExpand (MGProd (π2 (π2 (ground-not-holes y))))) FHOuter)
  ... | Inl GProdHole
    with canonical-indeterminate-forms-hole wt x
  ... | CIFHEHole (_ , _ , _ , refl , _)           = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHNEHole (_ , _ , _ , _ , _ , refl , _)  = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHAp (_ , _ , _ , refl , _ )             = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHCase (_ , _ , _ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHFst (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHSnd (_ , _ , refl , _ , _ , _ , _) = I (ICastHoleGround (λ _ _ ()) x GProdHole)
  ... | CIFHCast (_ , _ , refl , _ , GNum , _)     = S (_ , Step FHOuter (ITCastFail GNum GProdHole (λ ())) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GArrHole , _) = S (_ , Step FHOuter (ITCastFail GArrHole GProdHole (λ ())) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GSumHole , _) = S (_ , Step FHOuter (ITCastFail GSumHole GProdHole λ ()) FHOuter)
  ... | CIFHCast (_ , _ , refl , _ , GProdHole , _) = S (_ , Step FHOuter (ITCastSucceed GProdHole) FHOuter)

    -- if both are arrows
  progress (TACast wt (TCArr {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | I x
    with htype-dec (τ1 ==> τ2)  (τ1' ==> τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y    = I (ICastArr y x)

    -- if both are sums
  progress (TACast wt (TCSum {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | I x
    with htype-dec (τ1 ⊕ τ2) (τ1' ⊕ τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y    = I (ICastSum y x)
  progress (TACast wt (TCProd {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | I x
    with htype-dec (τ1 ⊠ τ2) (τ1' ⊠ τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y    = I (ICastProd y x)
    -- boxed value cases, inspect how the casts are related by consistency
    -- step by ID if the casts are the same
  progress (TACast wt TCRefl) | BV x = S (_ , Step FHOuter ITCastID FHOuter)
    -- if left is hole
  progress (TACast wt (TCHole1 {τ = τ})) | BV x
    with τ | ground-decidable τ
  ... | τ | Inl g = BV (BVHoleCast g x)
  ... | num | Inr y = abort (y GNum)
  ... | ⦇-⦈ | Inr y = S (_ , Step FHOuter ITCastID FHOuter)
  ... | τ1 ==> τ2 | Inr y
    with (htype-dec (τ1 ==> τ2) (⦇-⦈ ==> ⦇-⦈))
  ... | Inl refl = BV (BVHoleCast GArrHole x)
  ... | Inr y    = S (_ , Step FHOuter (ITGround (MGArr y)) FHOuter)
  progress (TACast wt (TCHole1 {τ = τ})) | BV x  | τ1 ⊕ τ2 | Inr y
    with (htype-dec (τ1 ⊕ τ2) (⦇-⦈ ⊕ ⦇-⦈))
  ... | Inl refl = BV (BVHoleCast GSumHole x)
  ... | Inr y    = S (_ , Step FHOuter (ITGround (MGSum y)) FHOuter)
  progress (TACast wt (TCHole1 {τ = τ})) | BV x  | τ1 ⊠ τ2 | Inr y
    with (htype-dec (τ1 ⊠ τ2) (⦇-⦈ ⊠ ⦇-⦈))
  ... | Inl refl = BV (BVHoleCast GProdHole x)
  ... | Inr y = S (_ , Step FHOuter (ITGround (MGProd y)) FHOuter)
    -- if right is hole
  progress {τ = τ} (TACast wt TCHole2) | BV x
    with canonical-boxed-forms-hole wt x
  ... | d' , τ' , refl , gnd , wt'
    with htype-dec τ τ'
  ... | Inl refl = S (_  , Step FHOuter (ITCastSucceed gnd) FHOuter)
  ... | Inr x₁
    with ground-decidable τ
  ... | Inl y = S (_ , Step FHOuter (ITCastFail gnd y (flip x₁)) FHOuter)
  ... | Inr y
    with not-ground y
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr (Inl (τ1 , τ2 , refl)) = S (_ , Step FHOuter (ITExpand (MGArr (π1 (ground-not-holes y)))) FHOuter)
  ... | Inr (Inr (Inl (τ1 , τ2 , refl))) =  S (_ , Step FHOuter (ITExpand (MGSum (π1 (π2 (ground-not-holes y))))) FHOuter)
  ... | Inr (Inr (Inr (τ1 , τ2 , refl))) = S (_ , Step FHOuter (ITExpand (MGProd (π2 (π2 (ground-not-holes y))))) FHOuter)
    -- if both arrows
  progress (TACast wt (TCArr {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | BV x
    with htype-dec (τ1 ==> τ2) (τ1' ==> τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y = BV (BVArrCast y x)
    -- if both sums
  progress (TACast wt (TCSum {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | BV x
    with htype-dec (τ1 ⊕ τ2) (τ1' ⊕ τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y = BV (BVSumCast y x)
  progress (TACast wt (TCProd {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | BV x
    with htype-dec (τ1 ⊠ τ2) (τ1' ⊠ τ2')
  ... | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  ... | Inr y = BV (BVProdCast y x)
   -- failed casts
  progress (TAFailedCast wt y z w)
    with progress wt
  ... | S (d' , Step x a q) = S (_ , Step (FHFailedCast x) a (FHFailedCast q))
  ... | I x = I (IFailedCast (FIndet x) y z w)
  ... | BV x = I (IFailedCast (FBoxedVal x) y z w)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --type-in-type #-}

open import Data.Empty
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_∘_; id)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst; cong; sym)

record _◁_ {ℓ} (A B : Set ℓ) : Set ℓ where
  constructor _,_,_
  field
    ϕ : A → B
    ψ : B → A
    retract : ψ ∘ ϕ ≡ id
open _◁_

record _◁′_ {ℓ} (A B : Set ℓ) : Set ℓ where
  constructor _,_,_
  field
    ϕ : A → B
    ψ : B → A
    retract : A ◁ B → ψ ∘ ϕ ≡ id
open _◁′_

postulate
  EM : ∀ {ℓ} (A : Set ℓ) → A ⊎ (¬ A)

℘ : ∀ {ℓ} → Set ℓ → Set _
℘ X = X → Set

t : ∀ {ℓ} (A B : Set ℓ) → ℘ A ◁′ ℘ B
t A B with EM (℘ A ◁ ℘ B)
... | inj₁  ℘A◁℘B =
      let ϕ , ψ , retract = ℘A◁℘B
      in ϕ , ψ , λ _ → retract
... | inj₂ ¬℘A◁℘B =
      (λ _ _ → ⊥) , (λ _ _ → ⊥) , λ ℘A◁℘B → ⊥-elim (¬℘A◁℘B ℘A◁℘B)

-- type-in-type allows U to be put into Set...
U : Set
U = ∀ X → ℘ X

-- ...so that u: U can be applied to U itself
projᵤ : U → ℘ U
projᵤ u = u U

injᵤ : ℘ U → U
injᵤ f X =
  let _ , ψ , _ = t X U
      ϕ , _ , _ = t U U
  in ψ (ϕ f)

projᵤ∘injᵤ : projᵤ ∘ injᵤ ≡ id
projᵤ∘injᵤ = retract (t U U) (id , id , refl)

_∈_ : U → U → Set
u ∈ v = projᵤ u v

Russell : ℘ U
Russell u = ¬ u ∈ u

r : U
r = injᵤ Russell

-- up to here EM + impredicativity is enough,
-- as long as _≡_ itself is in the impredicative universe,
-- but to go further, large elimination (via subst) is required
r∈r≡r∉r : r ∈ r ≡ (¬ r ∈ r)
r∈r≡r∉r = cong (λ f → f Russell r) projᵤ∘injᵤ

r∉r : ¬ r ∈ r
r∉r r∈r =
  let r∈r→r∉r = subst id r∈r≡r∉r
  in r∈r→r∉r r∈r r∈r

false : ⊥
false =
  let r∉r→r∈r = subst id (sym r∈r≡r∉r)
  in r∉r (r∉r→r∈r r∉r)


text:
module Preliminaries where

  -- universe levels
  postulate
    Level : Set
    lZ : Level
    lS : Level -> Level
    lmax : Level -> Level -> Level

  {-# BUILTIN LEVEL     Level #-}
  {-# BUILTIN LEVELZERO lZ  #-}
  {-# BUILTIN LEVELSUC  lS   #-}
  {-# BUILTIN LEVELMAX lmax #-}

  -- ----------------------------------------------------------------------
  -- functions

  _o_ : {A B C : Set} → (B → C) → (A → B) → A → C
  g o f = \ x → g (f x)
  infixr 10 _o_

  -- ----------------------------------------------------------------------
  -- identity type

  data _==_ {l : Level} {A : Set l} (M : A) : A → Set l where
    Refl : M == M

  {-# BUILTIN EQUALITY _==_ #-}
  {-# BUILTIN REFL Refl #-}

  transport : {l1 : Level} {l2 : Level} {A : Set l1} (B : A → Set l2)
              {a1 a2 : A} → a1 == a2 → (B a1 → B a2)
  transport B Refl = λ x → x

  ! : {l : Level} {A : Set l} {M N : A} → M == N → N == M
  ! Refl = Refl

  _∘_  : {l : Level} {A : Set l} {M N P : A}
      → N == P → M == N → M == P
  β ∘ Refl = β

  ap :  {l1 l2 : Level} {A : Set l1} {B : Set l2} {M N : A}
       (f : A → B) → M == N → (f M) == (f N)
  ap f Refl = Refl

  ap2 : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3} {M N : A} {M' N' : B} (f : A -> B -> C) -> M == N -> M' == N' -> (f M M') == (f N N')
  ap2 f Refl Refl = Refl

  postulate
    -- function extensionality
    λ=  : {l1 l2 : Level} {A : Set l1} {B : A -> Set l2} {f g : (x : A) -> B x} -> ((x : A) -> (f x) == (g x)) -> f == g
    -- function extensionality for implicit functions
    λ=i  : {l1 l2 : Level} {A : Set l1} {B : A -> Set l2} {f g : {x : A} -> B x} -> ((x : A) -> (f {x}) == (g {x})) -> _==_ {_}{ {x : A} → B x } f g

  private primitive primTrustMe : {l : Level} {A : Set l} {x y : A} -> x == y

  infixr 9 _==_

  infix  2 _∎
  infixr 2 _=〈_〉_

  _=〈_〉_ : {l : Level} {A : Set l} (x : A) {y z : A} → x == y → y == z → x == z
  _ =〈 p1 〉 p2 = (p2 ∘ p1)

  _∎ : {l : Level} {A : Set l} (x : A) → x == x
  _∎ _ = Refl

  -- ----------------------------------------------------------------------
  -- product types

  record Unit : Set where
    constructor <>

  record Σ {l1 l2 : Level} {A : Set l1} (B : A -> Set l2) : Set (lmax l1 l2) where
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ public

  infixr 0 _,_

  _×_ : {l1 l2 : Level} → Set l1 -> Set l2 -> Set (lmax l1 l2)
  A × B = Σ (\ (_ : A) -> B)

  infixr 10 _×_

  -- ----------------------------------------------------------------------
  -- booleans

  data Bool : Set where
     True : Bool
     False : Bool
  {-# COMPILED_DATA Bool Bool True False #-}
  {-# BUILTIN BOOL  Bool  #-}
  {-# BUILTIN TRUE  True  #-}
  {-# BUILTIN FALSE False #-}

  -- ----------------------------------------------------------------------
  -- order

  data Order : Set where
    Less : Order
    Equal : Order
    Greater : Order

  -- ----------------------------------------------------------------------
  -- sums

  data Void : Set where

  abort : {A : Set} → Void → A
  abort ()

  data Either (A B : Set) : Set where
    Inl : A → Either A B
    Inr : B → Either A B

  DecEq : Set → Set
  DecEq A = (x y : A) → Either (x == y) (x == y → Void)

  -- ----------------------------------------------------------------------
  -- natural numbers

  module Nat where
    data Nat : Set where
      Z : Nat
      S : Nat -> Nat

    -- let's you use numerals for Nat
    {-# BUILTIN NATURAL Nat #-}
    {-# BUILTIN SUC S #-}
    {-# BUILTIN ZERO Z #-}

    _+_ : Nat → Nat → Nat
    Z + n = n
    (S m) + n = S (m + n)

    max : Nat → Nat → Nat
    max Z n = n
    max m Z = m
    max (S m) (S n) = S (max m n)

    equal : Nat → Nat → Bool
    equal Z Z = True
    equal Z (S _) = False
    equal (S _) Z = False
    equal (S m) (S n) = equal m n

    compare : Nat → Nat → Order
    compare Z Z = Equal
    compare Z (S m) = Less
    compare (S n) Z = Greater
    compare (S n) (S m) = compare n m

  open Nat public using (Nat ; Z ; S)

  -- ----------------------------------------------------------------------
  -- monad

  module Monad where

    record Monad : Set1 where
      field
        T : Set → Set
        return : ∀ {A} → A → T A
        _>>=_  : ∀ {A B} → T A → (A → T B) -> T B

  -- ----------------------------------------------------------------------
  -- options

  module Maybe where

    data Maybe {l : Level} (A : Set l) : Set l where
      Some : A → Maybe A
      None : Maybe A

    Monad : Monad.Monad
    Monad = record { T = Maybe; return = Some; _>>=_ = (λ {None _ → None; (Some v) f → f v}) }

  open Maybe public using (Maybe;Some;None)

  -- ----------------------------------------------------------------------
  -- lists

  module List where
    data List {l : Level} (A : Set l) : Set l where
      []  : List A
      _::_ : A -> List A -> List A

    {-# COMPILED_DATA List [] [] (:) #-}
    {-# BUILTIN LIST List #-}
    {-# BUILTIN NIL [] #-}
    {-# BUILTIN CONS _::_ #-}

    infixr 99 _::_

    _++_ : {A : Set} → List A → List A → List A
    [] ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)

    infixr 10 _++_

    map : {l1 l2 : Level} {A : Set l1} {B : Set l2} → (A → B) → List A → List B
    map f [] = []
    map f (x :: xs) = f x :: map f xs

    map-id : {l : Level} {A : Set l} (l : List A) → map (\ (x : A) → x) l == l
    map-id [] = Refl
    map-id (x :: l) with map (\ x -> x) l | map-id l
    ... | ._ | Refl = Refl

    module Uninformative where
      -- simply typed version
      peelOff : {A : Set} (eq : A → A → Bool) → List A → List A → Maybe (List A)
      peelOff eq [] ys = Some ys
      peelOff eq (_ :: _) [] = None
      peelOff eq (x :: xs) (y :: ys) with eq x y
      ... | False = None
      ... | True = peelOff eq xs ys

    peelOff : {A : Set} (eq : DecEq A) → (xs ys : List A) → Maybe (Σ \ zs → (xs ++ zs) == ys )
    peelOff eq [] ys = Some (ys , Refl)
    peelOff eq (_ :: _) [] = None
    peelOff eq (x :: xs) (y :: ys) with eq x y
    ... | Inr xyneq = None
    peelOff eq (x :: xs) (.x :: ys) | Inl Refl with peelOff eq xs ys
    peelOff eq (x :: xs) (.x :: .(xs ++ zs)) | Inl Refl | Some (zs , Refl) = Some (zs , Refl)
    ... | None = None

    [_] : {A : Set} → A → List A
    [ c ] = c :: []

    ++-assoc : ∀ {A} (l1 l2 l3 : List A) → (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
    ++-assoc [] l2 l3 = Refl
    ++-assoc (x :: xs) l2 l3 = ap (_::_ x) (++-assoc xs l2 l3)

  open List public using (List ; [] ; _::_)

  -- ----------------------------------------------------------------------
  -- characters

  module Char where

    postulate {- Agda Primitive -}
      Char : Set

    {-# BUILTIN CHAR Char #-}
    {-# COMPILED_TYPE Char Char #-}

    private
     primitive
      primCharToNat    : Char → Nat
      primCharEquality : Char → Char → Bool

    toNat : Char → Nat
    toNat = primCharToNat

    equalb : Char -> Char -> Bool
    equalb = primCharEquality

    -- need to go outside the real language a little to give the primitives good types,
    -- but from the outside this should be safe
    equal : DecEq Char
    equal x y with equalb x y
    ... | True = Inl primTrustMe
    ... | False = Inr canthappen where
      postulate canthappen : _

  open Char public using (Char)

  -- ----------------------------------------------------------------------
  -- vectors

  module Vector where

    data Vec (A : Set) : Nat → Set where
      []   : Vec A 0
      _::_ : ∀ {n} → A → Vec A n → Vec A (S n)

    infixr 99 _::_

    Vec-elim : {A : Set} (P : {n : Nat} → Vec A n → Set)
               → (P [])
               → ({n : Nat} (x : A) (xs : Vec A n) → P xs → P (x :: xs))
               → {n : Nat} (v : Vec A n) → P v
    Vec-elim P n c [] = n
    Vec-elim P n c (y :: ys) = c y ys (Vec-elim P n c ys)

    fromList : {A : Set} → List A → Σ \n → Vec A n
    fromList [] = _ , []
    fromList (x :: xs) = _ , x :: snd (fromList xs)

    toList : {A : Set} {n : Nat} → Vec A n → List A
    toList [] = []
    toList (x :: xs) = x :: (toList xs)

    toList' : {A : Set} → (Σ \ n → Vec A n) → List A
    toList' (._ , []) = []
    toList' (._ , (x :: xs)) = x :: (toList' (_ , xs))

    to-from : {A : Set} (l : List A) → toList' (fromList l) == l
    to-from [] = Refl
    to-from (x :: l) with toList' (fromList l) | to-from l
    to-from (x :: l) | .l | Refl = Refl

    from-to : {A : Set} (l : Σ \n → Vec A n) → fromList (toList' l) == l
    from-to (._ , []) = Refl
    from-to (._ , x :: l) with fromList (toList' (_ , l)) | from-to (_ , l)
    from-to (.(S n) , _::_ {n} x l) | .(n , l) | Refl = Refl

  -- ----------------------------------------------------------------------
  -- strings

  module String where

    postulate {- Agda Primitive -}
      String : Set
    {-# BUILTIN STRING  String #-}
    {-# COMPILED_TYPE String String #-}

    private
      primitive
         primStringToList   : String -> List Char
         primStringFromList : List Char -> String
         primStringAppend   : String -> String -> String
         primStringEquality : String -> String -> Bool

    equal : String -> String -> Bool
    equal = primStringEquality

    toList = primStringToList
    fromList = primStringFromList

    append = primStringAppend

    toVec : String -> Σ \ m → Vector.Vec Char m
    toVec = Vector.fromList o toList

  -- ----------------------------------------------------------------------
  -- fancy order

  module FancyOrder where

    data FancyOrder {A : Set} {_≤_ : A → A → Set} (a1 a2 : A) : Set where
        Less    : a1 ≤ a2 -> (a1 == a2 -> Void) → FancyOrder a1 a2
        Equal   : a1 == a2 -> FancyOrder a1 a2
        Greater : a2 ≤ a1 → (a1 == a2 -> Void) -> FancyOrder a1 a2

    record DecidableOrder : Set1 where
      field
        A       : Set
        _≤_     : A → A → Set
        ≤-refl  : ∀ {a} → a ≤ a
        ≤-trans : ∀ {a1 a2 a3} → a1 ≤ a2 -> a2 ≤ a3 -> a1 ≤ a3
        ≤-saturated : ∀ {a1 a2} -> a1 ≤ a2 -> a2 ≤ a1 -> a1 == a2
        compare : (a1 a2 : A) → FancyOrder {A}{_≤_} a1 a2

      ≤-refl' : ∀ {a1 a2} → a1 == a2 -> a1 ≤ a2
      ≤-refl' Refl = ≤-refl

      min : A → A → A
      min a1 a2 with compare a1 a2
      ... | Less _ _ = a1
      ... | Equal _ = a1
      ... | Greater _ _ = a2

      min-≤-1 : {a1 a2 : A} → min a1 a2 ≤ a1
      min-≤-1 {a1}{a2} with compare a1 a2
      ... | Less lt _ = ≤-refl
      ... | Equal eq = ≤-refl
      ... | Greater gt _ = gt

      min-≤-2 : {a1 a2 : A} → min a1 a2 ≤ a2
      min-≤-2 {a1}{a2} with compare a1 a2
      ... | Less lt _ = lt
      min-≤-2 | Equal Refl = ≤-refl
      ... | Greater gt _ = ≤-refl

      min-sym : {a1 a2 : A} → min a1 a2 == min a2 a1
      min-sym {a1}{a2} with compare a1 a2 | compare a2 a1
      min-sym | Less lt12 _ | Less lt21 _ = ≤-saturated lt12 lt21
      min-sym | Less lt12 _ | Equal Refl = Refl
      min-sym | Less lt12 _ | Greater gt21 _ = Refl
      min-sym | Equal eq12 | Less lt21 _ = eq12
      min-sym | Equal eq12 | Equal eq21 = eq12
      min-sym | Equal eq12 | Greater gt21 _ = Refl
      min-sym | Greater gt12 _ | Less lt21 _ = Refl
      min-sym | Greater gt12 _ | Equal eq21 = Refl
      min-sym | Greater gt12 _ | Greater gt21 _ = ≤-saturated gt12 gt21

      min-≤ : {a1 a2 : A} → a1 ≤ a2 -> (min a1 a2) == a1
      min-≤ {a1} {a2} lt1 with compare a1 a2
      ... | Less lt _ = Refl
      ... | Equal eq = Refl
      ... | Greater gt _ = ≤-saturated gt lt1

      max : A → A → A
      max a1 a2 with compare a1 a2
      ... | Less _ _ = a2
      ... | Equal _ = a2
      ... | Greater _ _ = a1

      max-≥-1 : {a1 a2 : A} → a1 ≤ max a1 a2
      max-≥-1 {a1}{a2} with compare a1 a2
      ... | Less lt _ = lt
      max-≥-1 | Equal Refl = ≤-refl
      ... | Greater gt _ = ≤-refl

      max-≥-2 : {a1 a2 : A} → a2 ≤ max a1 a2
      max-≥-2 {a1}{a2} with compare a1 a2
      ... | Less lt _ = ≤-refl
      ... | Equal eq = ≤-refl
      ... | Greater gt _ = gt

      min-monotone : {a1 a1' a2 a2' : A} → a1 ≤ a1' -> a2 ≤ a2' -> min a1 a2 ≤ min a1' a2'
      min-monotone {a1}{a1'}{a2}{a2'} lt1 lt2 with compare a1 a2 | compare a1' a2'
      min-monotone lt1 lt2 | Less x x₁ | Less x₂ x₃ = lt1
      min-monotone lt1 lt2 | Less x x₁ | Equal x₂ = lt1
      min-monotone lt1 lt2 | Less x x₁ | Greater x₂ x₃ = ≤-trans x lt2
      min-monotone lt1 lt2 | Equal x | Less x₁ x₂ = lt1
      min-monotone lt1 lt2 | Equal x | Equal x₁ = lt1
      min-monotone lt1 lt2 | Equal Refl | Greater x₁ x₂ = lt2
      min-monotone lt1 lt2 | Greater x x₁ | Less x₂ x₃ = ≤-trans x lt1
      min-monotone lt1 lt2 | Greater x x₁ | Equal x₂ = ≤-trans x lt1
      min-monotone lt1 lt2 | Greater x x₁ | Greater x₂ x₃ = lt2

      max-sym : {a1 a2 : A} → max a1 a2 == max a2 a1
      max-sym {a1}{a2} with compare a1 a2 | compare a2 a1
      max-sym | Less lt12 _ | Less lt21 _ = ≤-saturated lt21 lt12
      max-sym | Less lt12 _ | Equal eq21 = eq21
      max-sym | Less lt12 _ | Greater gt21 _ = Refl
      max-sym | Equal eq12 | Less lt21 _ = ! eq12
      max-sym | Equal eq12 | Equal eq21 = eq21
      max-sym | Equal eq12 | Greater gt21 _ = Refl
      max-sym | Greater gt12 _ | Less lt21 _ = Refl
      max-sym | Greater gt12 _ | Equal eq21 = Refl
      max-sym | Greater gt12 _ | Greater gt21 _ = ≤-saturated gt21 gt12

      max-≤ : {a1 a2 : A} → a1 ≤ a2 -> (max a1 a2) == a2
      max-≤ {a1} {a2} lt1 with compare a1 a2
      ... | Less lt _ = Refl
      ... | Equal eq = Refl
      ... | Greater gt _ = ≤-saturated lt1 gt

      max-monotone : {a1 a1' a2 a2' : A} → a1 ≤ a1' -> a2 ≤ a2' -> max a1 a2 ≤ max a1' a2'
      max-monotone {a1}{a1'}{a2}{a2'} lt1 lt2 with compare a1 a2 | compare a1' a2'
      max-monotone lt1 lt2 | Less x x₁ | Less x₂ x₃ = lt2
      max-monotone lt1 lt2 | Less x x₁ | Equal x₂ = lt2
      max-monotone lt1 lt2 | Less x x₁ | Greater x₂ x₃ = ≤-trans lt2 x₂
      max-monotone lt1 lt2 | Equal x | Less x₁ x₂ = lt2
      max-monotone lt1 lt2 | Equal x | Equal x₁ = lt2
      max-monotone lt1 lt2 | Equal Refl | Greater x₁ x₂ = lt1
      max-monotone lt1 lt2 | Greater x x₁ | Less x₂ x₃ = ≤-trans lt1 x₂
      max-monotone lt1 lt2 | Greater x x₁ | Equal Refl = lt1
      max-monotone lt1 lt2 | Greater x x₁ | Greater x₂ x₃ = lt1

max_stars_repo_name: ayberkt/system-t-normalization

max_issues_repo_name: ayberkt/system-t-normalization

max_forks_repo_name: ayberkt/system-t-normalization


text:
{-# OPTIONS --without-K #-}

-- From nlab: FinSet is the category of finite sets and all functions
-- between them: the full subcategory of Set on finite sets. It is
-- easy (and thus common) to make FinSet skeletal; there is one object
-- for each natural number n (including n=0), and a morphism from m to
-- n is an m-tuple (f0,…,fm−1) of numbers satisfying 0≤fi<n. This
-- amounts to identifying n with the set {0,…,n−1}. (Sometimes {1,…,n}
-- is used instead.) This is exactly what we do below.

module SkFinSetCategory where

------------------------------------------------------------------------------
-- Categorical structure

import Level
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin; inject+; raise; zero; suc)
open import Function using (_∘_; id)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong₂)
open import Relation.Binary.PropositionalEquality.Core using (isEquivalence)

open import Categories.Category using (Category; module Category)
open import Categories.Functor using (Functor; module Functor)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalTransformation
  using (module NaturalTransformation)
  renaming (id to idn)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Monoidal.Braided using (Braided; module Braided)

open import FinVec
open F

-- Objects are natural numbers which are proxies for finite sets of
-- the given size; morphisms between m and n are finite functions, Vec
-- (Fin n) m, mapping each element of Fin m to an element in Fin
-- n. Two morphisms are considered the same if they are ≡ to each other.

finVecC : Category Level.zero Level.zero Level.zero
finVecC = record {
  Obj       = ℕ ;
  _⇒_       = FinVec ;
  _≡_       = _≡_ ;
  id        = 1C ;
  _∘_       = _∘̂_ ;
  assoc     = λ { {f = f} {g = g} {h = h} → sym (∘̂-assoc h g f) } ;
  identityˡ = λ { {f = f} → ∘̂-lid f } ;
  identityʳ = λ { {f = f} → ∘̂-rid f } ;
  equiv     = isEquivalence ;
  ∘-resp-≡  = cong₂ _∘̂_
  }

⊕-bifunctor : Bifunctor finVecC finVecC finVecC
⊕-bifunctor = record {
  F₀           = λ { (m , n) → m + n } ;
  F₁           = λ { (f , g) →  f ⊎c g } ;
  identity     = λ { { (m , n) } → 1C⊎1C≡1C {m} {n} } ;
  homomorphism = λ { {(x₁ , x₂)} {(y₁ , y₂)} {(z₁ , z₂)} {(x₁y₁ , x₂y₂)} {(y₁z₁ , y₂z₂)} →
                   sym (⊎c-distrib {p₁ = y₁z₁} {p₂ = y₂z₂} {p₃ = x₁y₁} {p₄ = x₂y₂}) } ;
  F-resp-≡     = λ { {(x₁ , x₂)} {(y₁ , y₂)} {(p₁ , p₂)} {(p₃ , p₄)} (p₁≡p₃ , p₂≡p₄) →
                   cong₂ _⊎c_ p₁≡p₃ p₂≡p₄ }
  }

⊗-bifunctor : Bifunctor finVecC finVecC finVecC
⊗-bifunctor = record {
  F₀           = λ { (m , n) → m * n } ;
  F₁           = λ { (f , g) →  f ×c g } ;
  identity     = λ { { (m , n) } → 1C×1C≡1C {m} {n} } ;
  homomorphism = λ { {(x₁ , x₂)} {(y₁ , y₂)} {(z₁ , z₂)} {(x₁y₁ , x₂y₂)} {(y₁z₁ , y₂z₂)} →
                   sym (×c-distrib {p₁ = y₁z₁} {p₂ = y₂z₂} {p₃ = x₁y₁} {p₄ = x₂y₂}) } ;
  F-resp-≡     = λ { {(x₁ , x₂)} {(y₁ , y₂)} {(p₁ , p₂)} {(p₃ , p₄)} (p₁≡p₃ , p₂≡p₄) →
                   cong₂ _×c_ p₁≡p₃ p₂≡p₄ }
  }

{--
CommutativeSquare f g h i = h ∘ f ≡ i ∘ g

Functor (C D):
  F₀           : C.Obj → D.Obj
  F₁           : ∀ {A B} → C [ A , B ] → D [ F₀ A , F₀ B ]
  identity     : ∀ {A} → D [ F₁ (C.id {A}) ≡ D.id ]
  homomorphism : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]}
                  → D [ F₁ (C [ g ∘ f ]) ≡ D [ F₁ g ∘ F₁ f ] ]
  F-resp-≡     : ∀ {A B} {F G : C [ A , B ]} → C [ F ≡ G ] → D [ F₁ F ≡ F₁ G ]

NaturalTransformation (F G : Functor C D):
  η       : ∀ X → D [ F₀ X , G₀ X ]
  commute : ∀ {X Y} (f : C [ X , Y ]) → D.CommutativeSquare (F₁ f) (η X) (η Y) (G₁ f)

NaturalIsomorphism (F G : Functor C D):
  F⇒G  : NaturalTransformation F G
  F⇐G  : NaturalTransformation G F
  iso  : ∀ X → Iso (⇒.η X) (⇐.η X)

Monoidal (C : Category):
  identityˡ : NaturalIsomorphism id⊗x x
  identityʳ : NaturalIsomorphism x⊗id x
  assoc     : NaturalIsomorphism [x⊗y]⊗z x⊗[y⊗z]
  triangle  : TriangleLeftSide ≡ⁿ (TriangleRightSide ∘₁ TriangleTopSide)
  pentagon  : (PentagonNESide ∘₁ PentagonNWSide) ≡ⁿ
              (PentagonSESide ∘₁ (PentagonSSide ∘₁ PentagonSWSide))
--}

private module CFV = Category finVecC
private module MFunctors = MonoidalHelperFunctors finVecC ⊕-bifunctor 0
private module Fid⊗x = Functor MFunctors.id⊗x
private module Fx = Functor MFunctors.x

finVecAdditiveM : Monoidal finVecC -- power = Fin 1 (so apply everything to zero)
finVecAdditiveM = record {
  ⊗  = ⊕-bifunctor ;
  id = 0 ;
  identityˡ = record {
    F⇒G = record { -- F, G : (0C ⊎ x) ⇒ x
      η       = λ X → 1C ;
      commute = λ f → trans (∘̂-lid (1C ⊎c f zero)) (trans 1C₀⊎x≡x (sym (∘̂-rid (f zero)))) -- ntp ηY ∘̂ (0C ⊎ f) ≡ f ∘̂ ηX
    } ;
    F⇐G = record {
      η       = λ _ → 1C ;
      commute = λ f → trans (∘̂-lid (f zero)) (trans (sym 1C₀⊎x≡x) (sym (∘̂-rid (1C ⊎c f zero))))
    } ;
    iso = λ X → record { isoˡ = ∘̂-rid 1C ; isoʳ = ∘̂-lid 1C }
  } ;
  identityʳ = record {
    F⇒G = record {
      η       = λ X → uniti+ ;
      commute = λ f → idʳ⊕ {x = f zero}
    } ;
    F⇐G = record {
      η       = λ X → unite+ ;
      commute = λ f → {!!}
    } ;
    iso = λ X → record { isoˡ = unite+∘̂uniti+~id ; isoʳ = uniti+∘̂unite+~id }
  } ;
  assoc = record
    { F⇒G = record { η = λ X → assocl+ {m = X zero}
                   ; commute = λ f → {!!} }
    ; F⇐G = record { η = λ X → assocr+ {m = X zero}
                    ; commute = {!!} }
    ; iso = λ X → record { isoˡ = assocr+∘̂assocl+~id {m = X zero}
                         ; isoʳ = assocl+∘̂assocr+~id {m = X zero}
                         }
    } ;
  triangle = {!!} ;
  pentagon = {!!}
  }
--  where
--  private module FVC = Category finVecC
--  private module MFunctors = MonoidalHelperFunctors finVecC ⊕-bifunctor 0
--  private module FF = Functor MFunctors.id⊗x
--  private module GF = Functor MFunctors.x

{--
-- Commutative semiring structure

import Level
open import Algebra
open import Algebra.Structures
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality using (subst; sym; trans; cong₂)

open F

_cauchy≃_ : (m n : ℕ) → Set
m cauchy≃ n = FinVec m n

id-iso : {m : ℕ} → FinVec m m
id-iso = 1C

private
  postulate sym-iso : {m n : ℕ} → FinVec m n → FinVec n m

trans-iso : {m n o : ℕ} → FinVec m n → FinVec n o → FinVec m o
trans-iso c₁ c₂ = c₂ ∘̂ c₁

cauchy≃IsEquiv : IsEquivalence {Level.zero} {Level.zero} {ℕ} _cauchy≃_
cauchy≃IsEquiv = record {
  refl = id-iso ;
  sym = sym-iso ;
  trans = trans-iso
  }

cauchyPlusIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _+_
cauchyPlusIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl+ {m} {n} {o} ;
  ∙-cong = _⊎c_
  }

cauchyTimesIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} _cauchy≃_ _*_
cauchyTimesIsSG = record {
  isEquivalence = cauchy≃IsEquiv ;
  assoc = λ m n o → assocl* {m} {n} {o} ;
  ∙-cong = _×c_
  }

cauchyPlusIsCM : IsCommutativeMonoid _cauchy≃_ _+_ 0
cauchyPlusIsCM = record {
  isSemigroup = cauchyPlusIsSG ;
  identityˡ = λ m → 1C ;
  comm = λ m n → swap+cauchy n m
  }

cauchyTimesIsCM : IsCommutativeMonoid _cauchy≃_ _*_ 1
cauchyTimesIsCM = record {
  isSemigroup = cauchyTimesIsSG ;
  identityˡ = λ m → uniti* {m} ;
  comm = λ m n → swap⋆cauchy n m
  }

cauchyIsCSR : IsCommutativeSemiring _cauchy≃_ _+_ _*_ 0 1
cauchyIsCSR = record {
  +-isCommutativeMonoid = cauchyPlusIsCM ;
  *-isCommutativeMonoid = cauchyTimesIsCM ;
  distribʳ = λ o m n → factor*+ {m} {n} {o} ;
  zeroˡ = λ m → 0C
  }

cauchyCSR : CommutativeSemiring Level.zero Level.zero
cauchyCSR = record {
  Carrier = ℕ ;
  _≈_ = _cauchy≃_ ;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = cauchyIsCSR
  }

------------------------------------------------------------------------------
-- Groupoid structure

open import Groupoid

private
  postulate linv : {m n : ℕ} (c : FinVec m n) → (sym-iso c) ∘̂ c ≡ 1C
  postulate rinv : {m n : ℕ} (c : FinVec m n) → c ∘̂ (sym-iso c) ≡ 1C

G : 1Groupoid
G = record {
  set = ℕ ;
  _↝_ = _cauchy≃_ ;
  _≈_ = _≡_ ;
  id  = id-iso ;
  _∘_ = λ c₁ c₂ → trans-iso c₂ c₁ ;
  _⁻¹ = sym-iso ;
  lneutr = ∘̂-lid ;
  rneutr = ∘̂-rid ;
  assoc  = λ c₁ c₂ c₃ → sym (∘̂-assoc c₁ c₂ c₃) ;
  equiv = record {
            refl  = refl ;
            sym   = sym ;
            trans = trans
          } ;
  linv = linv ;
  rinv = rinv ;
  ∘-resp-≈ = cong₂ _∘̂_
  }
--}

------------------------------------------------------------------------------


text:
open import Lemmachine
module Lemmachine.Lemmas (hooks : Hooks) where
import Lemmachine.Resolve
open import Data.Empty
open import Data.String
open import Data.Maybe
open import Data.Function
open import Data.Product hiding (map)
open import Data.List.Any hiding (map) renaming (any to any₂)
open import Relation.Nullary
open Membership-≡ public
open import Relation.Binary.PropositionalEquality public
open import Relation.Binary.PropositionalEquality.TrustMe
private
  resource : Resource
  resource = toResource hooks
open Request public
open Resource resource public
open Lemmachine.Resolve resource public

private
  eqMethod-refl : ∀ m → eqMethod m m ≡ true
  eqMethod-refl HEAD = refl
  eqMethod-refl GET = refl
  eqMethod-refl PUT = refl
  eqMethod-refl DELETE = refl
  eqMethod-refl POST = refl
  eqMethod-refl TRACE = refl
  eqMethod-refl CONNECT = refl
  eqMethod-refl OPTIONS = refl

  methodIsMember : ∀ r → (methods : List Method)
                   → method r ∈ methods
                   → any (eqMethod (method r))
                         methods ≡ true
  methodIsMember _ [] ()
  methodIsMember _ (x ∷ _) (here p) rewrite p with eqMethod-refl x
  ... | p₂ rewrite p₂ = refl
  methodIsMember r (x ∷ xs) (there ps) with eqMethod (method r) x | methodIsMember r xs ps
  ... | true | _ = refl
  ... | false | p rewrite p = refl

methodIsKnown : ∀ r → method r ∈ knownMethods r
                    → any (eqMethod (method r))
                          (knownMethods r) ≡ true
methodIsKnown r p = methodIsMember r (knownMethods r) p

methodIsAllowed : ∀ r → method r ∈ allowedMethods r
                      → any (eqMethod (method r))
                            (allowedMethods r) ≡ true
methodIsAllowed r p = methodIsMember r (allowedMethods r) p

postulate
  methodIsntAllowed : ∀ r → method r ∉ allowedMethods r
                          → any (eqMethod (method r))
                                (allowedMethods r) ≡ false

notOptions : ∀ r → method r ≢ OPTIONS
                 → eqMethod (method r) OPTIONS ≡ false
notOptions r p with method r
... | HEAD = refl
... | GET = refl
... | PUT = refl
... | DELETE = refl
... | POST = refl
... | TRACE = refl
... | CONNECT = refl
... | OPTIONS = ⊥-elim (p refl)

private
  ==-refl : ∀ s → (s == s) ≡ true
  ==-refl s = trustMe

  headerIsMember : (header : String)
                   → (headers : RequestHeaders)
                   → header ∈ map headerKey headers
                   → ∃ λ v → fetchHeader header headers ≡ just v
  headerIsMember _ [] ()
  headerIsMember _ ((k , v) ∷ _) (here p) rewrite p with ==-refl k
  ... | p₂ rewrite p₂ = v , refl
  headerIsMember header ((k , v) ∷ xs) (there ps) with header ≟ k | headerIsMember header xs ps
  ... | yes _ | _ = v , refl
  ... | no _ | v₂ , p with any₂ (_≟_ header ∘ headerKey) xs
  ... | yes _ rewrite p = v₂ , refl
  ... | no _ =  v₂ , p

acceptIsHeader : ∀ r → "Accept" ∈ map headerKey (headers r)
                     → ∃ λ v → fetchHeader "Accept" (headers r) ≡ just v
acceptIsHeader r p with headerIsMember "Accept" (headers r) p
... | v , p₂ with fetchHeader "Accept" (headers r) | p₂
... | ._ | refl = v , refl

acceptLanguageIsHeader : ∀ r → "Accept-Language" ∈ map headerKey (headers r)
                             → ∃ λ v → fetchHeader "Accept-Language" (headers r) ≡ just v
acceptLanguageIsHeader r p with headerIsMember "Accept-Language" (headers r) p
... | v , p₂ with fetchHeader "Accept-Language" (headers r) | p₂
... | ._ | refl = v , refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --without-K --safe #-}

module Categories.Category.Equivalence.Properties where

open import Level

open import Categories.Adjoint.Equivalence using (⊣Equivalence)
open import Categories.Adjoint.TwoSided using (_⊣⊢_; withZig)
open import Categories.Category.Core
open import Categories.Category.Equivalence using (WeakInverse; StrongEquivalence)
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties using ([_]-resp-Iso)
open import Categories.NaturalTransformation using (ntHelper; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃
  using (NaturalIsomorphism ; unitorˡ; unitorʳ; associator; _ⓘᵥ_; _ⓘˡ_; _ⓘʳ_)

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

module _ {F : Functor C D} {G : Functor D C} (W : WeakInverse F G) where
  open WeakInverse W

  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  -- adjoint equivalence
  F⊣⊢G : F ⊣⊢ G
  F⊣⊢G = withZig record
    { unit   = ≃.sym G∘F≈id
    ; counit =
      let open D
          open HomReasoning
          open MR D
          open MP D
      in record
        { F⇒G = ntHelper record
          { η       = λ X → F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
          ; commute = λ {X Y} f → begin
            (F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ Y))) ∘ F.F₁ (G.F₁ f)
              ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G.F₁ f))) ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X)))
              ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y) C.∘ G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G.F₁ f)) ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G.F₁ f C.∘ G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η Y ∘ (F.F₁ (G.F₁ f) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute f) Equiv.refl ⟩
            (f ∘ F∘G≈id.⇒.η X) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ assoc ⟩
            f ∘ F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ∎
          }
        ; F⇐G = ntHelper record
          { η       = λ X → (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
          ; commute = λ {X Y} f → begin
            ((F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F∘G≈id.⇐.η Y) ∘ f
              ≈⟨ pullʳ (F∘G≈id.⇐.commute f) ⟩
            (F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F.F₁ (G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ center (⟺ F.homomorphism) ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y) C.∘ G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇐.commute (G.F₁ f)) ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G.F₁ (F.F₁ (G.F₁ f)) C.∘ G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute _) Equiv.refl ⟩
            (F.F₁ (G.F₁ f) ∘ F∘G≈id.⇒.η (F.F₀ (G.F₀ X))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ center Equiv.refl ⟩
            F.F₁ (G.F₁ f) ∘ (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ∎
          }
        ; iso = λ X → Iso-∘ (Iso-∘ (Iso-swap (F∘G≈id.iso _)) ([ F ]-resp-Iso (G∘F≈id.iso _)))
                            (F∘G≈id.iso X)
        }
    ; zig    = λ {A} →
      let open D
          open HomReasoning
          open MR D
      in begin
      (F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ (F.F₀ A))))
        ∘ F.F₁ (G∘F≈id.⇐.η A)
        ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G∘F≈id.⇐.η A))) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘
        F.F₁ (G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A)) C.∘ G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G∘F≈id.⇐.η A)) ⟩∘⟨refl ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇐.η A C.∘ G∘F≈id.⇒.η A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl⟩∘⟨ elimˡ ((F.F-resp-≈ (G∘F≈id.iso.isoˡ _)) ○ F.identity) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ F∘G≈id.iso.isoʳ _ ⟩
      id
        ∎
    }

  module F⊣⊢G = _⊣⊢_ F⊣⊢G

module _ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (SE : StrongEquivalence C D) where
  open StrongEquivalence SE

  C≅D : ⊣Equivalence C D
  C≅D = record
    { L    = F
    ; R    = G
    ; L⊣⊢R = F⊣⊢G weak-inverse
    }

  module C≅D = ⊣Equivalence C≅D

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

import Level

open import Data.Empty
open import Data.Product
open import Data.List using (_∷_; []; _++_)
open import Data.List.Properties using (∷-injectiveʳ)

open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst)

open import Common

module Semantics {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import HasTrace message
open import TraceSet message
open import SessionType message
open import Transitions message

record Semantics (X : TraceSet) : Set where
  field
    closed   : PrefixClosed X
    coherent : Coherent X
open Semantics public

data Classification : TraceSet -> Set where
  emp : ∀{X}   -> X ⊆ ∅        -> Classification X
  eps : ∀{X}   -> X ⊆⊇ ｛ [] ｝ -> Classification X
  inp : ∀{X x} -> I x ∷ [] ∈ X -> Classification X
  out : ∀{X x} -> O x ∷ [] ∈ X -> Classification X

is-emp : ∀{X} -> Semantics X -> [] ∉ X -> X ⊆ ∅
is-emp sem nxε xφ with closed sem none xφ
... | xε = ⊥-elim (nxε xε)

is-eps :
  ∀{X} ->
  Semantics X ->
  (¬ (∃[ x ] (I x ∷ [] ∈ X))) ->
  (¬ (∃[ x ] (O x ∷ [] ∈ X))) ->
  X ⊆ ｛ [] ｝
is-eps sem nix nox {[]} xφ = refl
is-eps sem nix nox {I x ∷ φ} xφ with closed sem (some none) xφ
... | ix = ⊥-elim (nix (x , ix))
is-eps sem nix nox {O x ∷ φ} xφ with closed sem (some none) xφ
... | ox = ⊥-elim (nox (x , ox))

kind? : ∀{X} -> Semantics X -> Classification X
kind? {X} sem with excluded-middle {∃[ x ] (I x ∷ [] ∈ X)}
... | yes (_ , ix) = inp ix
... | no nix with excluded-middle {∃[ x ] (O x ∷ [] ∈ X)}
... | yes (_ , ox) = out ox
... | no nox with excluded-middle {[] ∈ X}
... | yes xε = eps (is-eps sem nix nox , λ { refl -> xε })
... | no nxε = emp (is-emp sem nxε)

sem-sound : (T : SessionType) -> Semantics ⟦ T ⟧
closed (sem-sound T) = ⊑-has-trace
coherent (sem-sound T) = trace-coherence

derive-semantics : ∀{X} -> Semantics X -> (α : Action) -> Semantics (X ∂ α)
closed (derive-semantics sem _) pre hasφ = closed sem (some pre) hasφ
coherent (derive-semantics {X} sem γ) {φ} {α} {β} hasφα hasφβ = coherent {X} sem {γ ∷ φ} hasφα hasφβ

co-semantics : ∀{X} -> Semantics X -> Semantics (CoSet X)
closed (co-semantics sem) le coφ = closed sem (⊑-co-trace le) coφ
coherent (co-semantics sem) {φ} {ψ₁} {ψ₂} {x} {y} iφx oφx
  rewrite co-trace-++ φ (I x ∷ ψ₁) | co-trace-++ φ (O y ∷ ψ₂) =
  coherent sem {co-trace φ} {co-trace ψ₂} {co-trace ψ₁} {y} {x} oφx iφx

non-empty-semantics-contains-[] : ∀{X : TraceSet}{φ} -> Semantics X -> φ ∈ X -> [] ∈ X
non-empty-semantics-contains-[] sem w = closed sem none w

decode : ∀{X} -> Semantics X -> ∞SessionType
force (decode sem) with kind? sem
... | emp _ = nil
... | eps _ = win
... | inp _ = inp λ x -> decode (derive-semantics sem (I x))
... | out _ = out λ x -> decode (derive-semantics sem (O x))

decode-sub : ∀{X} (sem : Semantics X) -> ⟦ decode sem .force ⟧ ⊆ X
decode-sub sem tφ with kind? sem
decode-sub _ (_ , () , refl) | emp _
decode-sub _ (_ , _ , step () _) | emp _
decode-sub _ (_ , _ , refl) | eps (_ , sup) = sup refl
decode-sub _ (_ , _ , step (out ()) _) | eps _
decode-sub sem (_ , _ , refl) | inp w = non-empty-semantics-contains-[] sem w
decode-sub sem (_ , def , step inp tr) | inp w =
  decode-sub (derive-semantics sem (I _)) (_ , def , tr)
decode-sub sem (_ , _ , refl) | out w = non-empty-semantics-contains-[] sem w
decode-sub sem (_ , def , step (out !x) tr) | out w =
  decode-sub (derive-semantics sem (O _)) (_ , def , tr)

decode-sup : ∀{X} (sem : Semantics X) -> X ⊆ ⟦ decode sem .force ⟧
decode-sup sem {φ} hasφ with kind? sem
... | emp sub = ⊥-elim (sub hasφ)
... | eps (sub , _) rewrite sym (sub hasφ) = _ , out , refl
decode-sup sem {[]} hasφ | inp _ = _ , inp , refl
decode-sup sem {I _ ∷ _} hasφ | inp _ =
  let _ , def , tr = decode-sup (derive-semantics sem (I _)) hasφ in
  _ , def , step inp tr
decode-sup sem {O _ ∷ _} hasφ | inp w = ⊥-elim (coherent sem {[]} w hasφ)
decode-sup sem {[]} hasφ | out _ = _ , out , refl
decode-sup sem {I _ ∷ _} hasφ | out w = ⊥-elim (coherent sem {[]} hasφ w)
decode-sup sem {O _ ∷ _} hasφ | out _ =
  let _ , def , tr = decode-sup (derive-semantics sem (O _)) hasφ in
  _ , def , step (out (transitions+defined->defined tr def)) tr

decode+maximal->win :
  ∀{X φ}
  (sem : Semantics X)
  (rφ : decode sem .force HasTrace φ) ->
  φ ∈ Maximal X ->
  Win (after rφ)
decode+maximal->win sem rφ comp with kind? sem
decode+maximal->win sem (_ , () , refl) comp | emp sub
decode+maximal->win sem (_ , _ , step () _) comp | emp sub
decode+maximal->win sem (_ , _ , refl) comp | eps _ = Win-win
decode+maximal->win sem (_ , _ , step (out ()) _) comp | eps _
decode+maximal->win sem (_ , def , refl) (maximal _ F) | inp w with F none w
... | ()
decode+maximal->win sem (_ , def , step inp tr) comp | inp _ =
  decode+maximal->win (derive-semantics sem (I _)) (_ , def , tr) (derive-maximal comp)
decode+maximal->win sem (_ , def , refl) (maximal _ F) | out w with F none w
... | ()
decode+maximal->win sem (_ , def , step (out !x) tr) comp | out w =
  decode+maximal->win (derive-semantics sem (O _)) (_ , def , tr) (derive-maximal comp)

win->maximal :
  ∀{T φ ψ} ->
  φ ⊑ ψ ->
  (tφ : T HasTrace φ) ->
  T HasTrace ψ ->
  Win (after tφ) ->
  φ ≡ ψ
win->maximal le (_ , tdef , refl) (_ , sdef , refl) w = refl
win->maximal le (_ , tdef , refl) (_ , sdef , step (out !x) sr) (out U) = ⊥-elim (U _ !x)
win->maximal (some le) (_ , tdef , step inp tr) (_ , sdef , step inp sr) w
  rewrite win->maximal le (_ , tdef , tr) (_ , sdef , sr) w = refl
win->maximal (some le) (_ , tdef , step (out _) tr) (_ , sdef , step (out _) sr) w
  rewrite win->maximal le (_ , tdef , tr) (_ , sdef , sr) w = refl

decode+win->maximal :
  ∀{X φ}
  (sem : Semantics X)
  (rφ : decode sem .force HasTrace φ) ->
  Win (after rφ) ->
  φ ∈ Maximal X
decode+win->maximal {X} {φ} sem rφ w =
  maximal (decode-sub sem rφ) λ le xψ -> let rψ = decode-sup sem xψ in
                                          sym (win->maximal le rφ rψ w)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Lemmachine.Response.Status where
{-# IMPORT Lemmachine.FFI #-}
open import Data.Nat

data Status : Set where
  -- 1xx: Informational - Request received, continuing process
  -- 2xx: Success - The action was successfully received, understood, and accepted
  OK Created Accepted NoContent : Status
  -- 3xx: Redirection - Further action must be taken in order to complete the request
  MultipleChoices MovedPermanently SeeOther NotModified MovedTemporarily : Status
  -- 4xx: Client Error - The request contains bad syntax or cannot be fulfilled
  BadRequest Unauthorized Forbidden NotFound MethodNotAllowed : Status
  NotAcceptable Conflict Gone PreconditionFailed : Status
  RequestEntityTooLarge RequestURItooLong UnsupportedMediaType : Status
  -- 5xx: Server Error - The server failed to fulfill an apparently valid request
  NotImplemented ServiceUnavailable : Status