text:
-- {-# OPTIONS --without-K #-}
module kripke where
open import common

infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_
infixr 1 _‘‘→’’_
infixr 1 _ww‘‘‘→’’’_
infixl 3 _‘’ₐ_
infixl 3 _w‘‘’’ₐ_
infixr 2 _‘∘’_
infixr 2 _‘×’_
infixr 2 _‘‘×’’_
infixr 2 _w‘‘×’’_

mutual
  data Context : Set where
    ε : Context
    _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
    W : ∀ {Γ A} → Type Γ → Type (Γ ▻ A)
    W1 : ∀ {Γ A B} → Type (Γ ▻ B) → Type (Γ ▻ A ▻ (W {Γ = Γ} {A = A} B))
    _‘’_ : ∀ {Γ A} → Type (Γ ▻ A) → Term {Γ} A → Type Γ
    ‘Type’ : ∀ Γ → Type Γ
    ‘Term’ : ∀ {Γ} → Type (Γ ▻ ‘Type’ Γ)
    _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
    _‘×’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
    Quine : ∀ {Γ} → Type (Γ ▻ ‘Type’ Γ) → Type Γ
    ‘⊤’ : ∀ {Γ} → Type Γ
    ‘⊥’ : ∀ {Γ} → Type Γ

  data Term : {Γ : Context} → Type Γ → Set where
    ⌜_⌝ : ∀ {Γ} → Type Γ → Term {Γ} (‘Type’ Γ)
    ⌜_⌝t : ∀ {Γ T} → Term {Γ} T → Term {Γ} (‘Term’ ‘’ ⌜ T ⌝)
    ‘⌜‘VAR₀’⌝t’ : ∀ {Γ T} → Term {Γ ▻ ‘Term’ ‘’ ⌜ T ⌝} (W (‘Term’ ‘’ ⌜ ‘Term’ ‘’ ⌜ T ⌝ ⌝))
    ‘⌜‘VAR₀’⌝’ : ∀ {Γ} → Term {Γ ▻ ‘Type’ Γ} (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))
    ‘λ∙’ : ∀ {Γ A B} → Term {Γ ▻ A} (W B) → Term {Γ} (A ‘→’ B)
    ‘VAR₀’ : ∀ {Γ T} → Term {Γ ▻ T} (W T)
    _‘’ₐ_ : ∀ {Γ A B} → Term {Γ} (A ‘→’ B) → Term {Γ} A → Term {Γ} B
    ‘‘×'’’ : ∀ {Γ} → Term {Γ} (‘Type’ Γ ‘→’ ‘Type’ Γ ‘→’ ‘Type’ Γ)
    quine→ : ∀ {Γ φ} → Term {Γ} (Quine φ        ‘→’ φ ‘’ ⌜ Quine φ ⌝)
    quine← : ∀ {Γ φ} → Term {Γ} (φ ‘’ ⌜ Quine φ ⌝ ‘→’ Quine φ)
    ‘tt’ : ∀ {Γ} → Term {Γ} ‘⊤’
    SW : ∀ {Γ X A} {a : Term A} → Term {Γ} (W X ‘’ a) → Term X
    →SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} (T ‘→’ (W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x)
      → Term {Γ} (T ‘→’ A ‘’ x ‘→’ B)
    ←SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} ((W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x ‘→’ T)
      → Term {Γ} ((A ‘’ x ‘→’ B) ‘→’ T)
    →SW1SV→SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} (T ‘→’ (W1 A ‘’ ‘VAR₀’ ‘→’ W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x)
      → Term {Γ} (T ‘→’ A ‘’ x ‘→’ A ‘’ x ‘→’ B)
    ←SW1SV→SW1SV→W : ∀ {Γ T X A B} {x : Term X}
      → Term {Γ} ((W1 A ‘’ ‘VAR₀’ ‘→’ W1 A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x ‘→’ T)
      → Term {Γ} ((A ‘’ x ‘→’ A ‘’ x ‘→’ B) ‘→’ T)
    w : ∀ {Γ A T} → Term {Γ} A → Term {Γ ▻ T} (W A)
    w→ : ∀ {Γ A B X} → Term {Γ ▻ X} (W (A ‘→’ B)) → Term {Γ ▻ X} (W A ‘→’ W B)
    →w : ∀ {Γ A B X} → Term {Γ ▻ X} (W A ‘→’ W B) → Term {Γ ▻ X} (W (A ‘→’ B))
    ww→ : ∀ {Γ A B X Y} → Term {Γ ▻ X ▻ Y} (W (W (A ‘→’ B))) → Term {Γ ▻ X ▻ Y} (W (W A) ‘→’ W (W B))
    →ww : ∀ {Γ A B X Y} → Term {Γ ▻ X ▻ Y} (W (W A) ‘→’ W (W B)) → Term {Γ ▻ X ▻ Y} (W (W (A ‘→’ B)))
    _‘∘’_ : ∀ {Γ A B C} → Term {Γ} (B ‘→’ C) → Term {Γ} (A ‘→’ B) → Term {Γ} (A ‘→’ C)
    _w‘‘’’ₐ_ : ∀ {Γ A B T} → Term {Γ ▻ T} (W (‘Term’ ‘’ ⌜ A ‘→’ B ⌝)) → Term {Γ ▻ T} (W (‘Term’ ‘’ ⌜ A ⌝)) → Term {Γ ▻ T} (W (‘Term’ ‘’ ⌜ B ⌝))
    ‘‘’ₐ’ : ∀ {Γ A B} → Term {Γ} (‘Term’ ‘’ ⌜ A ‘→’ B ⌝ ‘→’ ‘Term’ ‘’ ⌜ A ⌝ ‘→’ ‘Term’ ‘’ ⌜ B ⌝)
    -- _w‘‘’’_ : ∀ {Γ A B T} → Term {Γ ▻ T} (‘Type’ (Γ ▻ T)) → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ T ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Type’ Γ)))
    ‘‘□’’ : ∀ {Γ A B} → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Type’ Γ)))
    -- ‘‘’’' : ∀ {Γ A} → Term {Γ ▻ A} (‘Type’ (Γ ▻ A) ‘→’ W (‘Term’ ‘’ ⌜ A ⌝) ‘→’ W (‘Type’ Γ))
    _‘‘→’’_ : ∀ {Γ} → Term {Γ} (‘Type’ Γ) → Term {Γ} (‘Type’ Γ) → Term {Γ} (‘Type’ Γ)
    _ww‘‘‘→’’’_ : ∀ {Γ A B} → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝)))
    _ww‘‘‘×’’’_ : ∀ {Γ A B} → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝)))

□ : Type ε → Set _
□ = Term {ε}

‘□’ : ∀ {Γ} → Type Γ → Type Γ
‘□’ T = ‘Term’ ‘’ ⌜ T ⌝

_‘‘×’’_ : ∀ {Γ} → Term {Γ} (‘Type’ Γ) → Term {Γ} (‘Type’ Γ) → Term {Γ} (‘Type’ Γ)
A ‘‘×’’ B = ‘‘×'’’ ‘’ₐ A ‘’ₐ B

max-level : Level
max-level = lzero

mutual
  Context⇓ : (Γ : Context) → Set (lsuc max-level)
  Context⇓ ε = ⊤
  Context⇓ (Γ ▻ T) = Σ (Context⇓ Γ) (Type⇓ {Γ} T)

  Type⇓ : {Γ : Context} → Type Γ → Context⇓ Γ → Set max-level
  Type⇓ (W T) Γ⇓ = Type⇓ T (Σ.proj₁ Γ⇓)
  Type⇓ (W1 T) Γ⇓ = Type⇓ T ((Σ.proj₁ (Σ.proj₁ Γ⇓)) , (Σ.proj₂ Γ⇓))
  Type⇓ (T ‘’ x) Γ⇓ = Type⇓ T (Γ⇓ , Term⇓ x Γ⇓)
  Type⇓ (‘Type’ Γ) Γ⇓ = Lifted (Type Γ)
  Type⇓ ‘Term’ Γ⇓ = Lifted (Term (lower (Σ.proj₂ Γ⇓)))
  Type⇓ (A ‘→’ B) Γ⇓ = Type⇓ A Γ⇓ → Type⇓ B Γ⇓
  Type⇓ (A ‘×’ B) Γ⇓ = Type⇓ A Γ⇓ × Type⇓ B Γ⇓
  Type⇓ ‘⊤’ Γ⇓ = ⊤
  Type⇓ ‘⊥’ Γ⇓ = ⊥
  Type⇓ (Quine φ) Γ⇓ = Type⇓ φ (Γ⇓ , (lift (Quine φ)))

  Term⇓ : ∀ {Γ : Context} {T : Type Γ} → Term T → (Γ⇓ : Context⇓ Γ) → Type⇓ T Γ⇓
  Term⇓ ⌜ x ⌝ Γ⇓ = lift x
  Term⇓ ⌜ x ⌝t Γ⇓ = lift x
  Term⇓ ‘⌜‘VAR₀’⌝t’ Γ⇓ = lift ⌜ (lower (Σ.proj₂ Γ⇓)) ⌝t
  Term⇓ ‘⌜‘VAR₀’⌝’ Γ⇓ = lift ⌜ (lower (Σ.proj₂ Γ⇓)) ⌝
  Term⇓ (f ‘’ₐ x) Γ⇓ = Term⇓ f Γ⇓ (Term⇓ x Γ⇓)
  Term⇓ ‘tt’ Γ⇓ = tt
  Term⇓ (quine→ {φ}) Γ⇓ x = x
  Term⇓ (quine← {φ}) Γ⇓ x = x
  Term⇓ (‘λ∙’ f) Γ⇓ x = Term⇓ f (Γ⇓ , x)
  Term⇓ ‘VAR₀’ Γ⇓ = Σ.proj₂ Γ⇓
  Term⇓ (SW t) = Term⇓ t
  Term⇓ (←SW1SV→W f) = Term⇓ f
  Term⇓ (→SW1SV→W f) = Term⇓ f
  Term⇓ (←SW1SV→SW1SV→W f) = Term⇓ f
  Term⇓ (→SW1SV→SW1SV→W f) = Term⇓ f
  Term⇓ (w x) Γ⇓ = Term⇓ x (Σ.proj₁ Γ⇓)
  Term⇓ (w→ f) Γ⇓ = Term⇓ f Γ⇓
  Term⇓ (→w f) Γ⇓ = Term⇓ f Γ⇓
  Term⇓ (ww→ f) Γ⇓ = Term⇓ f Γ⇓
  Term⇓ (→ww f) Γ⇓ = Term⇓ f Γ⇓
  Term⇓ ‘‘×'’’ Γ⇓ A B = lift (lower A ‘×’ lower B)
  Term⇓ (g ‘∘’ f) Γ⇓ x = Term⇓ g Γ⇓ (Term⇓ f Γ⇓ x)
  Term⇓ (f w‘‘’’ₐ x) Γ⇓ = lift (lower (Term⇓ f Γ⇓) ‘’ₐ lower (Term⇓ x Γ⇓))
  Term⇓ ‘‘’ₐ’ Γ⇓ f x = lift (lower f ‘’ₐ lower x)
  -- Term⇓ (f w‘‘’’ x) Γ⇓ = lift {!!} --(lower (Term⇓ f Γ⇓) ‘’ lower (Term⇓ x Γ⇓))
  Term⇓ (‘‘□’’ {Γ} T) Γ⇓ = lift (‘Term’ ‘’ lower (Term⇓ T Γ⇓))
  Term⇓ (A ‘‘→’’ B) Γ⇓ = lift ((lower (Term⇓ A Γ⇓)) ‘→’ (lower (Term⇓ B Γ⇓)))
  Term⇓ (A ww‘‘‘→’’’ B) Γ⇓ = lift ((lower (Term⇓ A Γ⇓)) ‘‘→’’ (lower (Term⇓ B Γ⇓)))
  Term⇓ (A ww‘‘‘×’’’ B) Γ⇓ = lift ((lower (Term⇓ A Γ⇓)) ‘‘×’’ (lower (Term⇓ B Γ⇓)))

module inner (‘X’ : Type ε) (‘f’ : Term {ε} (‘□’ ‘X’ ‘→’ ‘X’)) where
  ‘H’ : Type ε
  ‘H’ = Quine (W1 ‘Term’ ‘’ ‘VAR₀’ ‘→’ W ‘X’)

  ‘toH’ : □ ((‘□’ ‘H’ ‘→’ ‘X’) ‘→’ ‘H’)
  ‘toH’ = ←SW1SV→W quine←

  ‘fromH’ : □ (‘H’ ‘→’ (‘□’ ‘H’ ‘→’ ‘X’))
  ‘fromH’ = →SW1SV→W quine→

  ‘□‘H’→□‘X’’ : □ (‘□’ ‘H’ ‘→’ ‘□’ ‘X’)
  ‘□‘H’→□‘X’’ = ‘λ∙’ (w ⌜ ‘fromH’ ⌝t w‘‘’’ₐ ‘VAR₀’ w‘‘’’ₐ ‘⌜‘VAR₀’⌝t’)

  ‘h’ : Term ‘H’
  ‘h’ = ‘toH’ ‘’ₐ (‘f’ ‘∘’ ‘□‘H’→□‘X’’)

  Lӧb : □ ‘X’
  Lӧb = ‘fromH’ ‘’ₐ ‘h’ ‘’ₐ ⌜ ‘h’ ⌝t

Lӧb : ∀ {X} → Term {ε} (‘□’ X ‘→’ X) → Term {ε} X
Lӧb {X} f = inner.Lӧb X f

⌞_⌟ : Type ε → Set _
⌞ T ⌟ = Type⇓ T tt

‘¬’_ : ∀ {Γ} → Type Γ → Type Γ
‘¬’ T = T ‘→’ ‘⊥’

_w‘‘×’’_ : ∀ {Γ X} → Term {Γ ▻ X} (W (‘Type’ Γ)) → Term {Γ ▻ X} (W (‘Type’ Γ)) → Term {Γ ▻ X} (W (‘Type’ Γ))
A w‘‘×’’ B = w→ (w→ (w ‘‘×'’’) ‘’ₐ A) ‘’ₐ B

lӧb : ∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’) → ⌞ ‘X’ ⌟
lӧb f = Term⇓ (Lӧb f) tt

incompleteness : ¬ □ (‘¬’ (‘□’ ‘⊥’))
incompleteness = lӧb

soundness : ¬ □ ‘⊥’
soundness x = Term⇓ x tt

non-emptyness : Σ (Type ε) (λ T → □ T)
non-emptyness = ‘⊤’ , ‘tt’

module helpers where
  Wₕ : ∀ {Γ A} → Type Γ → Type (Γ ▻ A)
  Wₕ ‘⊤’ = ‘⊤’
  Wₕ ‘⊥’ = ‘⊥’
  Wₕ (T ‘→’ T₂) = Wₕ T ‘→’ Wₕ T₂
  Wₕ (T ‘×’ T₂) = Wₕ T ‘×’ Wₕ T₂
  Wₕ (W T₂) = W (Wₕ T₂)
  Wₕ T = W T

  _‘’ₕ_ : ∀ {Γ A} → Type (Γ ▻ A) → Term A → Type Γ
  ‘⊤’ ‘’ₕ x₁ = ‘⊤’
  ‘⊥’ ‘’ₕ x₁ = ‘⊥’
  W f ‘’ₕ x₁ = f
  ‘Term’ ‘’ₕ ⌜ ‘⊤’ ⌝ = ‘⊤’
  (f ‘→’ f₁) ‘’ₕ x₁ = (f ‘’ₕ x₁) ‘→’ (f₁ ‘’ₕ x₁)
  (f ‘×’ f₁) ‘’ₕ x₁ = (f ‘’ₕ x₁) ‘×’ (f₁ ‘’ₕ x₁)
  f ‘’ₕ x = f ‘’ x

  _‘→’ₕ_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
  ‘⊤’ ‘→’ₕ B = B
  ‘⊥’ ‘→’ₕ B = ‘⊤’
  A ‘→’ₕ ‘⊤’ = ‘⊤’
  A ‘→’ₕ B = A ‘→’ B

  _‘×’ₕ_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
  ‘⊤’ ‘×’ₕ B = B
  ‘⊥’ ‘×’ₕ B = ‘⊥’
  A ‘×’ₕ ‘⊤’ = A
  A ‘×’ₕ ‘⊥’ = ‘⊥’
  A ‘×’ₕ B = A ‘×’ B

open helpers

mutual
  simplify-type : ∀ {Γ} → Type Γ → Type Γ
  simplify-type ‘⊤’ = ‘⊤’
  simplify-type ‘⊥’ = ‘⊥’
  simplify-type (T ‘→’ T₁) = simplify-type T ‘→’ₕ simplify-type T₁
  simplify-type (T ‘×’ T₁) = simplify-type T ‘×’ₕ simplify-type T₁
  simplify-type (T₁ ‘’ x) = simplify-type T₁ ‘’ₕ simplify-term x
  simplify-type (W T₁) = Wₕ (simplify-type T₁)
  simplify-type (W1 T₂) = W1ₕ (simplify-type T₂)
    where W1ₕ : ∀ {Γ A B} → Type (Γ ▻ A) → Type (Γ ▻ B ▻ W A)
          W1ₕ ‘⊤’ = ‘⊤’
          W1ₕ ‘⊥’ = ‘⊥’
          W1ₕ (T ‘→’ T₂) = W1ₕ T ‘→’ W1ₕ T₂
          W1ₕ (T ‘×’ T₂) = W1ₕ T ‘×’ W1ₕ T₂
          W1ₕ (W T₂) = W (Wₕ T₂)
          W1ₕ (W1 T₂) = W1 (W1ₕ T₂)
          W1ₕ T = W1 T
  simplify-type (‘Type’ Γ) = ‘Type’ Γ
  simplify-type ‘Term’ = ‘Term’
  simplify-type (Quine T) = Quine (simplify-type T)

  simplify-term : ∀ {Γ T} → Term {Γ} T → Term T
  simplify-term ⌜ x ⌝ = ⌜ simplify-type x ⌝
  simplify-term ⌜ t ⌝t = ⌜ simplify-term t ⌝t
  simplify-term ‘⌜‘VAR₀’⌝t’ = ‘⌜‘VAR₀’⌝t’
  simplify-term ‘⌜‘VAR₀’⌝’ = ‘⌜‘VAR₀’⌝’
  simplify-term (‘λ∙’ t) = ‘λ∙’ (simplify-term t)
  simplify-term ‘VAR₀’ = ‘VAR₀’
  simplify-term (t ‘’ₐ t₁) = simplify-term t ‘’ₐₕ simplify-term t₁
    where _‘’ₐₕ_ : ∀ {Γ A T} → Term {Γ} (A ‘→’ T) → Term A → Term T
          ‘λ∙’ ‘⌜‘VAR₀’⌝t’ ‘’ₐₕ x = ⌜ x ⌝t
          ‘λ∙’ ‘⌜‘VAR₀’⌝’ ‘’ₐₕ x = ⌜ x ⌝t
          ‘λ∙’ ‘VAR₀’ ‘’ₐₕ x = x
          ‘λ∙’ (f ‘’ₐ f₁) ‘’ₐₕ x = ‘λ∙’ (f ‘’ₐₕ f₁) ‘’ₐ x
          ‘λ∙’ (w f) ‘’ₐₕ x = f
          (f ‘’ₐ f₁) ‘’ₐₕ x = (f ‘’ₐₕ f₁) ‘’ₐ x
          (f ‘∘’ f₁) ‘’ₐₕ x = f ‘’ₐₕ (f₁ ‘’ₐₕ x)
          f ‘’ₐₕ x = f ‘’ₐ x
  simplify-term ‘‘×'’’ = ‘‘×'’’
  simplify-term quine→ = quine→
  simplify-term quine← = quine←
  simplify-term ‘tt’ = ‘tt’
  simplify-term (SW t₁) = SW (simplify-term t₁)
  simplify-term (→SW1SV→W t₁) = →SW1SV→W (simplify-term t₁)
  simplify-term (←SW1SV→W t₁) = ←SW1SV→W (simplify-term t₁)
  simplify-term (→SW1SV→SW1SV→W t₁) = →SW1SV→SW1SV→W (simplify-term t₁)
  simplify-term (←SW1SV→SW1SV→W t₁) = ←SW1SV→SW1SV→W (simplify-term t₁)
  simplify-term (w t) = w (simplify-term t)
  simplify-term (w→ t) = w→ (simplify-term t)
  simplify-term (→w t) = →w (simplify-term t)
  simplify-term (ww→ t) = ww→ (simplify-term t)
  simplify-term (→ww t) = →ww (simplify-term t)
  simplify-term (t ‘∘’ t₁) = simplify-term t ‘∘’ simplify-term t₁
  simplify-term (t w‘‘’’ₐ t₁) = simplify-term t w‘‘’’ₐ simplify-term t₁
  simplify-term ‘‘’ₐ’ = ‘‘’ₐ’
  simplify-term (‘‘□’’ t) = ‘‘□’’ (simplify-term t)
  simplify-term (t ‘‘→’’ t₁) = simplify-term t ‘‘→’’ simplify-term t₁
  simplify-term (t ww‘‘‘→’’’ t₁) = simplify-term t ww‘‘‘→’’’ simplify-term t₁
  simplify-term (t ww‘‘‘×’’’ t₁) = simplify-term t ww‘‘‘×’’’ simplify-term t₁
{-
mutual
  simplify-type⇓→ : ∀ {Γ T Γ⇓} → Type⇓ {Γ} T Γ⇓ → Type⇓ {Γ} (simplify-type T) Γ⇓
  simplify-type⇓→ {T = T ‘→’ T₁} T⇓ = {!!}
  simplify-type⇓→ {T = W T₁} T⇓ = {!!}
  simplify-type⇓→ {T = W1 T₂} T⇓ = {!!}
  simplify-type⇓→ {T = T₁ ‘’ x} T⇓ = {!!}
  simplify-type⇓→ {T = ‘Type’ ._} T⇓ = {!!}
  simplify-type⇓→ {T = ‘Term’} T⇓ = {!!}
  simplify-type⇓→ {T = T ‘×’ T₁} T⇓ = {!!}
  simplify-type⇓→ {T = Quine T} T⇓ = {!!}
  simplify-type⇓→ {T = ‘⊤’} T⇓ = tt
  simplify-type⇓→ {T = ‘⊥’} T⇓ = T⇓

  simplify-type⇓← : ∀ {Γ T Γ⇓} → Type⇓ {Γ} (simplify-type T) Γ⇓ → Type⇓ {Γ} T Γ⇓
  simplify-type⇓← {T = W T₁} T⇓ = {!!}
  simplify-type⇓← {T = W1 T₂} T⇓ = {!!}
  simplify-type⇓← {T = T₁ ‘’ x} T⇓ = {!!}
  simplify-type⇓← {T = ‘Type’ ._} T⇓ = {!!}
  simplify-type⇓← {T = ‘Term’} T⇓ = {!!}
  simplify-type⇓← {T = T ‘→’ T₁} T⇓ x = {!!}
  simplify-type⇓← {Γ} {T ‘×’ T₁} {Γ⇓} T⇓ = helper {Γ} {simplify-type T} {simplify-type T₁} {T} {T₁} {Γ⇓} (simplify-type⇓← {T = T}) (simplify-type⇓← {T = T₁}) T⇓
    where helper : ∀ {Γ A B A' B'} {Γ⇓ : Context⇓ Γ}
                 → (Type⇓ A Γ⇓ → Type⇓ A' Γ⇓)
                 → (Type⇓ B Γ⇓ → Type⇓ B' Γ⇓)
                 → Type⇓ (A ‘×’ₕ B) Γ⇓
                 → Type⇓ (A' ‘×’ B') Γ⇓
          helper {A = ‘⊤’} f g x = f tt , g x
          helper {A = ‘⊥’} f g ()
          helper {A = W A₁} {‘⊤’} f g x = f x , g tt
          helper {A = W1 A₂} {‘⊤’} f g x = f x , g tt
          helper {A = A₁ ‘’ x} {‘⊤’} f g x₁ = f x₁ , g tt
          helper {A = ‘Type’ ._} {‘⊤’} f g x = f x , g tt
          helper {A = ‘Term’} {‘⊤’} f g x = f x , g tt
          helper {A = A ‘→’ A₁} {‘⊤’} f g x = f x , g tt
          helper {A = A ‘×’ A₁} {‘⊤’} f g x = f x , g tt
          helper {A = Quine A} {‘⊤’} f g x = f x , g tt
          helper {A = W A₁} {‘⊥’} {Γ⇓ = proj₁ , proj₂} f g ()
          helper {A = W1 A₂} {‘⊥’} {Γ⇓ = proj₁ , proj₂ , proj₃} f g ()
          helper {A = A₁ ‘’ x} {‘⊥’} f g ()
          helper {A = ‘Type’ ._} {‘⊥’} f g ()
          helper {A = ‘Term’} {‘⊥’} {Γ⇓ = proj₁ , proj₂} f g ()
          helper {A = A ‘→’ A₁} {‘⊥’} f g ()
          helper {A = A ‘×’ A₁} {‘⊥’} f g ()
          helper {A = Quine A} {‘⊥’} f g ()
          helper {A = W A₁} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = W1 A₂} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = A₂ ‘’ _} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = {!f (Σ.proj₁ x) , g (Σ.proj₂ x)!}
          helper {A = ‘Type’ ._} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = ‘Term’} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = A₁ ‘→’ A₂} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = A₁ ‘×’ A₂} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {A = Quine A₁} {W B₁} {Γ⇓ = proj₁ , proj₂} f g x = f (Σ.proj₁ x) , g (Σ.proj₂ x)
          helper {B = W1 B₂} f g x = {!!}
          helper {B = B₁ ‘’ x} f g x₁ = {!!}
          helper {B = ‘Type’ ._} f g x = {!!}
          helper {B = ‘Term’} f g x = {!!}
          helper {B = B ‘→’ B₁} f g x = {!!}
          helper {B = B ‘×’ B₁} f g x = {!!}
          helper {B = Quine B} f g x = {!!} {-
          helper {A = W A₁} f g x = {!!}
          helper {A = W1 A₂} f g x = {!!}
          helper {A = A₁ ‘’ x} f g x₁ = {!!}
          helper {A = ‘Type’ ._} f g x = {!!}
          helper {A = ‘Term’} f g x = {!!}
          helper {A = A ‘→’ A₁} f g x = {!!}
          helper {A = A ‘×’ A₁} f g x = {!!}
          helper {A = Quine A} f g x = {!!} -}
  simplify-type⇓← {T = Quine T} T⇓ = {!!}
  simplify-type⇓← {T = ‘⊤’} T⇓ = tt
  simplify-type⇓← {T = ‘⊥’} T⇓ = T⇓
-}

module modal-fixpoint where
  context-to-term : Context → Set
  context-to-term ε = ⊤
  context-to-term (Γ ▻ x) = Σ (context-to-term Γ) (λ _ → Term x)

  context-to-term⇓ : ∀ {Γ} → context-to-term Γ → Context⇓ Γ
  context-to-term⇓ {ε} v = tt
  context-to-term⇓ {Γ ▻ x} v = (context-to-term⇓ (Σ.proj₁ v)) , (Term⇓ (Σ.proj₂ v) (context-to-term⇓ (Σ.proj₁ v)))

  Type-in : ∀ {Γ} → Type Γ → context-to-term Γ → Type ε
  Type-in {ε} T v = T
  Type-in (T ‘→’ T₁) v = (Type-in T v) ‘→’ (Type-in T₁ v)
  Type-in ‘⊤’ v = ‘⊤’
  Type-in ‘⊥’ v = ‘⊥’
  Type-in {Γ ▻ x} T v = Type-in (T ‘’ Σ.proj₂ v) (Σ.proj₁ v)

  postulate hold : ∀ {Γ} → ℕ → Type Γ → Type Γ
  postulate hold-t : ∀ {Γ T} → ℕ → Term {Γ} T → Term T

  helper-ikf : ∀ {Γ A} world (T₁ : Type (Γ ▻ A)) (x : Term A) → Type Γ
  helper-ikf zero ‘Term’ x₁ = ‘⊤’
  helper-ikf world f (x₁ ‘‘→’’ x₂) = helper-ikf world f x₁ ‘→’ helper-ikf world f x₂
  helper-ikf (suc world) ‘Term’ ⌜ x₁ ⌝ = x₁
  helper-ikf (suc world) ‘Term’ (x₁ ‘’ₐ x₂) = hold (suc world) (‘Term’ ‘’ (x₁ ‘’ₐ x₂))
  helper-ikf (suc world) ‘Term’ (SW x₂) = hold (suc world) (‘Term’ ‘’ SW x₂)
  helper-ikf world (W T₂) x₁ = T₂
  helper-ikf world (W1 T₄) x₁ = hold world (W1 T₄ ‘’ x₁)
  helper-ikf world (T₃ ‘’ x₁) x₂ = hold world (T₃ ‘’ x₁ ‘’ x₂)
  helper-ikf world (‘Type’ ._) x₁ = hold world (‘Type’ _ ‘’ x₁)
  helper-ikf world (T₂ ‘→’ T₃) x₁ = helper-ikf world T₂ x₁ ‘→’ helper-ikf world T₃ x₁
  helper-ikf world (T₂ ‘×’ T₃) x₁ = helper-ikf world T₂ x₁ ‘×’ helper-ikf world T₃ x₁
  helper-ikf world (Quine T₂) x₁ = hold world (Quine T₂ ‘’ x₁)
  helper-ikf world ‘⊤’ x₁ = ‘⊤’
  helper-ikf world ‘⊥’ x₁ = ‘⊥’

  mutual
{-    _‘’ₐₕ_ : ∀ {Γ A B} {world} (f : Term {Γ} (A ‘→’ B)) (x : Term A) → Term B
    ‘λ∙’ ‘⌜‘VAR₀’⌝t’ ‘’ₐₕ x₂ = ⌜ x₂ ⌝t
    ‘λ∙’ ‘⌜‘VAR₀’⌝’ ‘’ₐₕ x₂ = ⌜ x₂ ⌝t
    ‘λ∙’ ‘VAR₀’ ‘’ₐₕ x₂ = x₂
    ‘λ∙’ (f ‘’ₐ f₁) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (SW f₁) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (w f) ‘’ₐₕ x₂ = f
    ‘λ∙’ (→w (‘λ∙’ ‘VAR₀’)) ‘’ₐₕ x₂ = ‘λ∙’ ‘VAR₀’
    ‘λ∙’ (→w (‘λ∙’ (f ‘’ₐ f₁))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (‘λ∙’ (SW f₁))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (‘λ∙’ (w f))) ‘’ₐₕ x₂ = ‘λ∙’ (w (‘λ∙’ f ‘’ₐₕ x₂))
    ‘λ∙’ (→w (‘λ∙’ (→ww f))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (‘λ∙’ (‘‘□’’ f))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (‘λ∙’ (f ww‘‘‘→’’’ f₁))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (‘λ∙’ (f ww‘‘‘×’’’ f₁))) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (f ‘’ₐ f₁)) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (SW f₁)) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (w→ f)) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (ww→ f)) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→w (f ‘∘’ f₁)) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (→ww f) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (f w‘‘’’ₐ f₁) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (‘‘□’’ f) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (f ww‘‘‘→’’’ f₁) ‘’ₐₕ x₂ = {!!}
    ‘λ∙’ (f ww‘‘‘×’’’ f₁) ‘’ₐₕ x₂ = {!!}
    _‘’ₐₕ_ {world = world} (f ‘’ₐ f₁) x₂ = hold-t world ((_‘’ₐₕ_ {world = world} f f₁) ‘’ₐ x₂)
    _‘’ₐₕ_ {world = world} ‘‘×'’’ x₂ = {!!}
    _‘’ₐₕ_ {world = world} quine→ x₂ = {!!}
    _‘’ₐₕ_ {world = world} quine← x₂ = {!!}
    _‘’ₐₕ_ {world = world} (SW f₁) x₂ = {!!}
    _‘’ₐₕ_ {world = world} (→SW1SV→W f₁) x₂ = {!!}
    _‘’ₐₕ_ {world = world} (←SW1SV→W f₁) x₂ = {!!}
    →SW1SV→SW1SV→W (‘λ∙’ f₁) ‘’ₐₕ x₂ = {!!}
    →SW1SV→SW1SV→W (f₁ ‘’ₐ f₂) ‘’ₐₕ x₂ = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ⌜ x ⌝) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ⌜ x₃ ⌝t) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘⌜‘VAR₀’⌝t’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘⌜‘VAR₀’⌝’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ ‘⌜‘VAR₀’⌝t’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ ‘⌜‘VAR₀’⌝’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ ‘VAR₀’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (x₃ ‘’ₐ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (SW x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (w x₃)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ ‘VAR₀’))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (x₃ ‘’ₐ x₄)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (SW x₄)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w ‘⌜‘VAR₀’⌝t’)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w ‘⌜‘VAR₀’⌝’)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w ‘VAR₀’)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (x₃ ‘’ₐ x₄))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (SW x₄))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (‘λ∙’ x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ x₃ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (SW x₃ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→W (‘λ∙’ x₃) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→W (x₃ ‘’ₐ x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→W (SW x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→W (x₃ ‘∘’ x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W (‘λ∙’ x₃) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W (x₃ ‘’ₐ x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W quine← ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))) = ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W (SW x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W (x₃ ‘∘’ x₄) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₁ ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ ((x₂ ‘∘’ x₃) ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x ⌝))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ⌜ x₃ ⌝t))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘⌜‘VAR₀’⌝t’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘⌜‘VAR₀’⌝’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (‘λ∙’ x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘VAR₀’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ ‘’ₐ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘‘×'’’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w quine→))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w quine←))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘tt’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (SW x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (→SW1SV→W x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (←SW1SV→W x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (→SW1SV→SW1SV→W x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (←SW1SV→SW1SV→W x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (w x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (w→ x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (→w x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (ww→ x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (→ww x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ ‘∘’ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ w‘‘’’ₐ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w ‘‘’ₐ’))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (‘‘□’’ x₃)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ ‘‘→’’ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ ww‘‘‘→’’’ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (w (x₃ ww‘‘‘×’’’ x₄)))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (→w x₃))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (→ww x₃))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (x₃ w‘‘’’ₐ x₄))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (‘‘□’’ x₃))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (x₃ ww‘‘‘→’’’ x₄))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (w (x₃ ww‘‘‘×’’’ x₄))))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (→ww x₃)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (‘‘□’’ x₃)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (x₃ ww‘‘‘→’’’ x₄)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (‘λ∙’ (x₃ ww‘‘‘×’’’ x₄)))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (x₃ ‘’ₐ x₄))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (SW x₄))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (w→ x₃))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (ww→ x₃))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→w (x₃ ‘∘’ x₄))) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (→ww x₃)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (x₃ w‘‘’’ₐ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (‘‘□’’ x₃)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (x₃ ww‘‘‘→’’’ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘λ∙’ (x₃ ww‘‘‘×’’’ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘VAR₀’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ (x₃ ‘’ₐ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘‘×'’’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ quine→) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ quine←) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘tt’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ SW x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ →SW1SV→W x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ←SW1SV→W x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ →SW1SV→SW1SV→W x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ←SW1SV→SW1SV→W x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ w x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ w→ x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ →w x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ww→ x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ →ww x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ (x₃ ‘∘’ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ (x₃ w‘‘’’ₐ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘‘’ₐ’) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ ‘‘□’’ x₃) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ (x₃ ‘‘→’’ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ (x₃ ww‘‘‘→’’’ x₄)) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (x₂ ‘’ₐ x₃ ww‘‘‘×’’’ x₄) = {!!}
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ SW x₃ = {!!}
    →SW1SV→SW1SV→W (SW f₂) ‘’ₐₕ x₂ = {!!}
    →SW1SV→SW1SV→W (←SW1SV→W f₂) ‘’ₐₕ x₂ = {!!}
    →SW1SV→SW1SV→W (←SW1SV→SW1SV→W f₂) ‘’ₐₕ x₂ = {!!}
    →SW1SV→SW1SV→W (f₁ ‘∘’ f₂) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W (‘λ∙’ f₁) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W (f₁ ‘’ₐ f₂) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W quine← ‘’ₐₕ x₂ = {!!} -- ←SW1SV→SW1SV→W quine← ‘’ₐ x₂
    ←SW1SV→SW1SV→W (SW f₂) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W (→SW1SV→W f₂) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W (→SW1SV→SW1SV→W f₂) ‘’ₐₕ x₂ = {!!}
    ←SW1SV→SW1SV→W (f₁ ‘∘’ f₂) ‘’ₐₕ x₂ = {!!}
    _‘’ₐₕ_ {world = world} (w→ f) x₂ = w→ f ‘’ₐ x₂
    _‘’ₐₕ_ {world = world} (ww→ f) x₂ = {!!}
    _‘’ₐₕ_ {world = world} (f ‘∘’ f₁) x₂ = _‘’ₐₕ_ {world = world} f (_‘’ₐₕ_ {world = world} f₁ x₂)
    _‘’ₐₕ_ {world = world} ‘‘’ₐ’ x₂ = {!!}

    ‘‘□’’ₕ : ∀ {Γ A B} → Term {Γ ▻ A ▻ B} (W (W (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝))) → Term {Γ ▻ A ▻ B} (W (W (‘Type’ Γ)))
    ‘‘□’’ₕ t = ‘‘□’’ t

    _‘∘’ₕ_ : ∀ {Γ A B C} {world} (g : Term {Γ} (B ‘→’ C)) (f : Term (A ‘→’ B)) → Term (A ‘→’ C)
    f ‘∘’ₕ g = f ‘∘’ g-}

    in-kripke-frame-c : ∀ (world : ℕ) → Context → Context
    in-kripke-frame : ∀ {Γ} (world : ℕ) → Type Γ → Type (in-kripke-frame-c world Γ)
    in-kripke-frame-t : ∀ {Γ} (world : ℕ) {T : Type Γ} → Term T → Term (in-kripke-frame world T)

    in-kripke-frame-c world ε = ε
    in-kripke-frame-c world (Γ ▻ x) = in-kripke-frame-c world Γ ▻ in-kripke-frame world x

    _‘’ₐₕ_ : ∀ {Γ A B} → Term {Γ} (A ‘→’ B) → Term {Γ} A → Term {Γ} B
    (f₁ ‘’ₐ f₂) ‘’ₐₕ x₁ = (f₁ ‘’ₐₕ f₂) ‘’ₐ x₁
    →SW1SV→SW1SV→W quine→ ‘’ₐₕ (←SW1SV→SW1SV→W quine← ‘’ₐ f) = f
    f ‘’ₐₕ x = {!!}

    in-kripke-frame world (T ‘→’ T₁) = (in-kripke-frame world T) ‘→’ (in-kripke-frame world T₁)
    in-kripke-frame world (‘Type’ Γ) = ‘Type’ (in-kripke-frame-c world Γ)
    in-kripke-frame world (W T₁) = W (in-kripke-frame world T₁)
    in-kripke-frame world (W1 T₂) = W1 (in-kripke-frame world T₂)
    in-kripke-frame zero (‘Term’ ‘’ x) = ‘⊤’
    in-kripke-frame {Γ = Γ} (suc world) (‘Term’ ‘’ (f ‘’ₐ x)) = helper helper'
      where helper' : Term (in-kripke-frame world (‘Type’ Γ))
            helper' = simplify-term (in-kripke-frame-t world f) ‘’ₐₕ simplify-term (in-kripke-frame-t world x)

            helper : ∀ {Γ} → Term (in-kripke-frame world (‘Type’ Γ)) → Type (in-kripke-frame-c (suc world) Γ)
            helper x = {!!}
    in-kripke-frame (suc world) (‘Term’ ‘’ x) = {!in-kripke-frame world x!}
    in-kripke-frame world (T₁ ‘’ x) = {!!}
    in-kripke-frame world ‘Term’ = {!!}
    in-kripke-frame world (T ‘×’ T₁) = {!!}
    in-kripke-frame world (Quine T) = {!!}
    in-kripke-frame world ‘⊤’ = ‘⊤’
    in-kripke-frame world ‘⊥’ = ‘⊥’

    in-kripke-frame-t world ⌜ x ⌝ = ⌜ (in-kripke-frame world x) ⌝
    in-kripke-frame-t zero ⌜ t ⌝t = ‘tt’
    in-kripke-frame-t (suc world) ⌜ t ⌝t = {!!}
    in-kripke-frame-t world ‘⌜‘VAR₀’⌝t’ = {!!}
    in-kripke-frame-t world ‘⌜‘VAR₀’⌝’ = {!!}
    in-kripke-frame-t world (‘λ∙’ t) = ‘λ∙’ (in-kripke-frame-t world t)
    in-kripke-frame-t world ‘VAR₀’ = ‘VAR₀’
    in-kripke-frame-t world (t ‘’ₐ t₁) = in-kripke-frame-t world t ‘’ₐₕ in-kripke-frame-t world t₁
    in-kripke-frame-t world ‘‘×'’’ = {!!}
    in-kripke-frame-t world quine→ = {!!}
    in-kripke-frame-t world quine← = {!!}
    in-kripke-frame-t world ‘tt’ = ‘tt’
    in-kripke-frame-t world (SW t₁) = {!!}
    in-kripke-frame-t world (→SW1SV→W t₁) = {!!}
    in-kripke-frame-t world (←SW1SV→W t₁) = {!!}
    in-kripke-frame-t world (→SW1SV→SW1SV→W t₁) = {!!}
    in-kripke-frame-t world (←SW1SV→SW1SV→W t₁) = {!!}
    in-kripke-frame-t world (w t) = w (in-kripke-frame-t world t)
    in-kripke-frame-t world (w→ t) = w→ (in-kripke-frame-t world t)
    in-kripke-frame-t world (→w t) = →w (in-kripke-frame-t world t)
    in-kripke-frame-t world (ww→ t) = ww→ (in-kripke-frame-t world t)
    in-kripke-frame-t world (→ww t) = →ww (in-kripke-frame-t world t)
    in-kripke-frame-t world (t ‘∘’ t₁) = {!!}
    in-kripke-frame-t world (t w‘‘’’ₐ t₁) = {!!}
    in-kripke-frame-t world ‘‘’ₐ’ = {!!}
    in-kripke-frame-t zero (‘‘□’’ t) = w (w ⌜ ‘⊤’ ⌝)
    in-kripke-frame-t {Γ = Γ ▻ A ▻ B} (suc world) (‘‘□’’ t) = helper {lzero} (‘‘□’’ₕ (in-kripke-frame-t world t))
      where ‘‘□’’ₕ : ∀ {Γ A B} → Term {in-kripke-frame-c world Γ ▻ A ▻ B} (W (W (in-kripke-frame world (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝)))) → Term {in-kripke-frame-c world Γ ▻ A ▻ B} (W (W (‘Type’ (in-kripke-frame-c world Γ))))
            ‘‘□’’ₕ T = {!!}

            helper : ∀ {ℓ ℓ′} {A : Set ℓ} {B : Set ℓ′} → A → B
            helper t = {!!}
    in-kripke-frame-t world (t ‘‘→’’ t₁) = {!!}
    in-kripke-frame-t world (t ww‘‘‘→’’’ t₁) = {!!}
    in-kripke-frame-t world (t ww‘‘‘×’’’ t₁) = {!!}
{-
    in-kripke-frame zero ‘Term’ = ‘⊤’
    in-kripke-frame {Γ} world (T ‘→’ T₁) = simplify-type (in-kripke-frame world T ‘→’ in-kripke-frame world T₁)
    in-kripke-frame {Γ} world (T ‘×’ T₁) = simplify-type (in-kripke-frame world T ‘×’ in-kripke-frame world T₁)
    in-kripke-frame world (W T) = simplify-type (W (in-kripke-frame world T))
    in-kripke-frame world (W1 T) = simplify-type (W1 (in-kripke-frame world T))
    in-kripke-frame world (T₁ ‘’ x) = simplify-type (helper-ikf world (simplify-type (in-kripke-frame world T₁)) (simplify-term (in-kripke-frame-t world x)))
    in-kripke-frame world ‘⊤’ = ‘⊤’
    in-kripke-frame world ‘⊥’ = ‘⊥’
    in-kripke-frame world (‘Type’ Γ) = hold world (‘Type’ Γ)
    in-kripke-frame world (Quine T) = hold world (Quine T)
    in-kripke-frame {Γ ▻ .(‘Type’ Γ)} (suc world) ‘Term’ = ‘Term’  {-helper (in-kripke-frame-t world T v) v
      where
        helper : ∀ {Γ} → Term (‘Type’ Γ) → context-to-term Γ → Type ε
        helper ⌜ x ⌝ v = Type-in x v
        helper (t ‘‘→’’ t₁) v = helper t v ‘→’ helper t₁ v
        helper (t ‘’ₐ t₁) v = {!!}
        helper (SW t₁) v = {!!}-}

    in-kripke-frame-t : ∀ {Γ} (world : ℕ) → {T : Type Γ} → Term T → Term (in-kripke-frame world T)
    in-kripke-frame-t world ⌜ x ⌝ = ⌜ in-kripke-frame world x ⌝
    in-kripke-frame-t world ⌜ x ⌝t = ⌜ in-kripke-frame-t world x ⌝t
    in-kripke-frame-t world ‘⌜‘VAR₀’⌝t’ = ‘⌜‘VAR₀’⌝t’
    in-kripke-frame-t world ‘⌜‘VAR₀’⌝’ = ‘⌜‘VAR₀’⌝’
    in-kripke-frame-t world (‘λ∙’ x) = ‘λ∙’ (in-kripke-frame-t world x)
    in-kripke-frame-t world ‘VAR₀’ = ‘VAR₀’
    in-kripke-frame-t world (x ‘’ₐ x₁) = _‘’ₐₕ_ {world = world} (simplify-term (in-kripke-frame-t world x)) (simplify-term (in-kripke-frame-t world x₁))
    in-kripke-frame-t world ‘‘×'’’ = ‘‘×'’’
    in-kripke-frame-t world quine→ = quine→
    in-kripke-frame-t world quine← = quine←
    in-kripke-frame-t world ‘tt’ = ‘tt’
    in-kripke-frame-t world (SW x₁) = SW (in-kripke-frame-t world x₁)
    in-kripke-frame-t world (→SW1SV→W x₁) = →SW1SV→W (in-kripke-frame-t world x₁)
    in-kripke-frame-t world (←SW1SV→W x₁) = ←SW1SV→W (in-kripke-frame-t world x₁)
    in-kripke-frame-t world (→SW1SV→SW1SV→W x₁) = →SW1SV→SW1SV→W (in-kripke-frame-t world x₁)
    in-kripke-frame-t world (←SW1SV→SW1SV→W x₁) = ←SW1SV→SW1SV→W (in-kripke-frame-t world x₁)
    in-kripke-frame-t world (w x) = w (in-kripke-frame-t world x)
    in-kripke-frame-t world (w→ x) = w→ (in-kripke-frame-t world x)
    in-kripke-frame-t world (→w x) = →w (in-kripke-frame-t world x)
    in-kripke-frame-t world (ww→ x) = ww→ (in-kripke-frame-t world x)
    in-kripke-frame-t world (→ww x) = →ww (in-kripke-frame-t world x)
    in-kripke-frame-t world (x ‘∘’ x₁) = _‘∘’ₕ_ {world = world} (simplify-term (in-kripke-frame-t world x)) (simplify-term (in-kripke-frame-t world x₁))
    in-kripke-frame-t world (x w‘‘’’ₐ x₁) = simplify-term (in-kripke-frame-t world x) w‘‘’’ₐ simplify-term (in-kripke-frame-t world x₁)
    in-kripke-frame-t world ‘‘’ₐ’ = ‘‘’ₐ’
    in-kripke-frame-t zero (‘‘□’’ x) = w (w ⌜ ‘⊤’ ⌝)
    in-kripke-frame-t (suc world) (‘‘□’’ x) = ‘‘□’’ₕ (simplify-term (in-kripke-frame-t world x))
    in-kripke-frame-t world (x ‘‘→’’ x₁) = {!!}
    in-kripke-frame-t world (x ww‘‘‘→’’’ x₁) = {!!}
    in-kripke-frame-t world (x ww‘‘‘×’’’ x₁) = {!!}
-}
  kripke-reduce : ∀ {Γ} → Type Γ → context-to-term Γ → Type ε
  kripke-reduce (W x₁) v = kripke-reduce x₁ (Σ.proj₁ v)
  kripke-reduce (W1 x₂) v = kripke-reduce x₂ ((Σ.proj₁ (Σ.proj₁ v)) , (‘λ∙’ (Σ.proj₂ v) ‘’ₐ Σ.proj₂ (Σ.proj₁ v)))
  kripke-reduce (T₁ ‘’ x) v = kripke-reduce T₁ (v , x)
  kripke-reduce (‘Type’ Γ) v = Type-in (‘Type’ Γ) v
  -- kripke-reduce ‘TVAR₀’ v = {!!}
  kripke-reduce ‘Term’ (v , T) = {!!} {- Type-in (lower (Term⇓ (Σ.proj₂ v) (context-to-term⇓ (Σ.proj₁ v)))) (Σ.proj₁ v) -}
  kripke-reduce (T ‘→’ T₁) v = kripke-reduce T v ‘→’ kripke-reduce T₁ v
  kripke-reduce (T ‘×’ T₁) v = kripke-reduce T v ‘×’ kripke-reduce T₁ v
  kripke-reduce (Quine x) v = {!!}
  kripke-reduce ‘⊤’ v = ‘⊤’
  kripke-reduce ‘⊥’ v = ‘⊥’

  kripke-eval' : ∀ {Γ} → ℕ → Type Γ → context-to-term Γ → Type ε
  kripke-eval' 0 T v = Type-in T v
  kripke-eval' (suc n) T v = kripke-eval' n (kripke-reduce T v) tt

  kripke-finalize : ∀ {Γ} → Type Γ → context-to-term Γ → Type ε
  kripke-finalize (W x₁) v = kripke-finalize x₁ (Σ.proj₁ v)
  kripke-finalize (W1 x₂) v = kripke-finalize x₂ ((Σ.proj₁ (Σ.proj₁ v)) , (‘λ∙’ (Σ.proj₂ v) ‘’ₐ Σ.proj₂ (Σ.proj₁ v)))
  kripke-finalize (T₁ ‘’ x) v = kripke-finalize T₁ (v , x)
  kripke-finalize (‘Type’ Γ) v = Type-in (‘Type’ Γ) v
  -- kripke-finalize ‘TVAR₀’ v = {!!}
  kripke-finalize ‘Term’ v = ‘⊤’
  kripke-finalize (T ‘→’ T₁) v = kripke-finalize T v ‘→’ kripke-finalize T₁ v
  kripke-finalize (T ‘×’ T₁) v = kripke-finalize T v ‘×’ kripke-finalize T₁ v
  kripke-finalize (Quine x) v = {!!}
  kripke-finalize ‘⊤’ v = ‘⊤’
  kripke-finalize ‘⊥’ v = ‘⊥’

  mutual
    kripke-count : ∀ {Γ} → Type Γ → ℕ
    kripke-count (W T₁) = kripke-count T₁
    kripke-count (W1 T₂) = kripke-count T₂
    kripke-count (T₁ ‘’ x) = kripke-count T₁ + kripke-count-t x
    kripke-count (‘Type’ Γ) = 0
    -- kripke-count ‘TVAR₀’ = 0
    kripke-count ‘Term’ = 1
    kripke-count (T ‘→’ T₁) = kripke-count T + kripke-count T₁
    kripke-count (T ‘×’ T₁) = kripke-count T + kripke-count T₁
    kripke-count (Quine T) = kripke-count T
    kripke-count ‘⊤’ = 0
    kripke-count ‘⊥’ = 0

    kripke-count-t : ∀ {Γ T} → Term {Γ} T → ℕ
    kripke-count-t ⌜ x ⌝ = kripke-count x
    kripke-count-t (x ‘’ₐ x₁) = kripke-count-t x + kripke-count-t x₁
    kripke-count-t ⌜ x ⌝t = kripke-count-t x
    kripke-count-t ‘⌜‘VAR₀’⌝t’ = 0
    kripke-count-t ‘⌜‘VAR₀’⌝’ = 0
    kripke-count-t (‘λ∙’ x) = kripke-count-t x
    kripke-count-t ‘VAR₀’ = 0
    kripke-count-t quine→ = 0
    kripke-count-t quine← = 0
    kripke-count-t ‘tt’ = 0
    kripke-count-t (SW x₁) = kripke-count-t x₁
    kripke-count-t (→SW1SV→W x₁) = kripke-count-t x₁
    kripke-count-t (←SW1SV→W x₁) = kripke-count-t x₁
    kripke-count-t (→SW1SV→SW1SV→W x₁) = kripke-count-t x₁
    kripke-count-t (←SW1SV→SW1SV→W x₁) = kripke-count-t x₁
    kripke-count-t (w x) = kripke-count-t x
    kripke-count-t (w→ x) = kripke-count-t x
    kripke-count-t (→w x) = kripke-count-t x
    kripke-count-t (ww→ x) = kripke-count-t x
    kripke-count-t (→ww x) = kripke-count-t x
    kripke-count-t ‘‘×'’’ = 0
    kripke-count-t (x ‘∘’ x₁) = kripke-count-t x + kripke-count-t x₁
    kripke-count-t (x w‘‘’’ₐ x₁) = kripke-count-t x + kripke-count-t x₁
    kripke-count-t ‘‘’ₐ’ = 0
    -- kripke-count-t (f w‘‘’’ x) = kripke-count-t f + kripke-count-t x
    kripke-count-t (‘‘□’’ T) = 1 + kripke-count-t T
    kripke-count-t (x ‘‘→’’ x₁) = kripke-count-t x + kripke-count-t x₁
    kripke-count-t (x ww‘‘‘→’’’ x₁) = kripke-count-t x + kripke-count-t x₁
    kripke-count-t (x ww‘‘‘×’’’ x₁) = kripke-count-t x + kripke-count-t x₁

  kripke-normalize' : ∀ {Γ} → Type Γ → context-to-term Γ → Type ε
  kripke-normalize' T v = kripke-eval' (kripke-count T) T v

  kripke-normalize'' : ∀ {Γ} → (T : Type Γ) → Type (in-kripke-frame-c (kripke-count T) Γ)
  kripke-normalize'' T = in-kripke-frame (kripke-count T) T

open modal-fixpoint

‘Bot’ : ∀ {Γ} → Type Γ
‘Bot’ {Γ} = Quine (W1 ‘Term’ ‘’ ‘VAR₀’ ‘→’ W1 ‘Term’ ‘’ ‘VAR₀’ ‘→’ W (‘Type’ Γ)) {- a bot takes in the source code for itself, for another bot, and spits out the assertion that it cooperates with this bot -}

_cooperates-with_ : □ ‘Bot’ → □ ‘Bot’ → Type ε
b1 cooperates-with b2 = lower (Term⇓ b1 tt (lift b1) (lift b2))

‘eval-bot'’ : ∀ {Γ} → Term {Γ} (‘Bot’ ‘→’ (‘□’ ‘Bot’ ‘→’ ‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))
‘eval-bot'’ = →SW1SV→SW1SV→W quine→

‘‘eval-bot'’’ : ∀ {Γ} → Term {Γ} (‘□’ ‘Bot’ ‘→’ ‘□’ ({- other -} ‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))
‘‘eval-bot'’’ = ‘λ∙’ (w ⌜ ‘eval-bot'’ ⌝t w‘‘’’ₐ ‘VAR₀’ w‘‘’’ₐ ‘⌜‘VAR₀’⌝t’)

‘other-cooperates-with’ : ∀ {Γ} → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ ‘Bot’)) ‘→’ W (W (‘□’ (‘Type’ Γ))))
‘other-cooperates-with’ {Γ} = ‘eval-other'’ ‘∘’ w→ (w (w→ (w (‘λ∙’ ‘⌜‘VAR₀’⌝t’))))
  where
    ‘eval-other’ : Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ (‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))))
    ‘eval-other’ = w→ (w (w→ (w ‘‘eval-bot'’’))) ‘’ₐ ‘VAR₀’

    ‘eval-other'’ : Term (W (W (‘□’ (‘□’ ‘Bot’))) ‘→’ W (W (‘□’ (‘Type’ Γ))))
    ‘eval-other'’ = ww→ (w→ (w (w→ (w ‘‘’ₐ’))) ‘’ₐ ‘eval-other’)

‘self’ : ∀ {Γ} → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ ‘Bot’)))
‘self’ = w ‘VAR₀’

‘other’ : ∀ {Γ} → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ ‘Bot’)))
‘other’ = ‘VAR₀’

make-bot : ∀ {Γ} → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘Type’ Γ))) → Term {Γ} ‘Bot’
make-bot t = ←SW1SV→SW1SV→W quine← ‘’ₐ ‘λ∙’ (→w (‘λ∙’ t))

ww‘‘‘¬’’’_ : ∀ {Γ A B}
  → Term {Γ ▻ A ▻ B} (W (W (‘□’ (‘Type’ Γ))))
  → Term {Γ ▻ A ▻ B} (W (W (‘□’ (‘Type’ Γ))))
ww‘‘‘¬’’’ T = T ww‘‘‘→’’’ w (w ⌜ ⌜ ‘⊥’ ⌝ ⌝t)

‘DefectBot’ : □ ‘Bot’
‘CooperateBot’ : □ ‘Bot’
‘FairBot’ : □ ‘Bot’
‘PrudentBot’ : □ ‘Bot’

‘DefectBot’ = make-bot (w (w ⌜ ‘⊥’ ⌝))
‘CooperateBot’ = make-bot (w (w ⌜ ‘⊤’ ⌝))
‘FairBot’ = make-bot (‘‘□’’ (‘other-cooperates-with’ ‘’ₐ ‘self’))
‘PrudentBot’ = make-bot (‘‘□’’ (φ₀ ww‘‘‘×’’’ (¬□⊥ ww‘‘‘→’’’ other-defects-against-DefectBot)))
  where
    φ₀ : ∀ {Γ} → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ (‘Type’ Γ))))
    φ₀ = ‘other-cooperates-with’ ‘’ₐ ‘self’

    other-defects-against-DefectBot : Term {_ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)} (W (W (‘□’ (‘Type’ _))))
    other-defects-against-DefectBot = ww‘‘‘¬’’’ (‘other-cooperates-with’ ‘’ₐ w (w ⌜ ‘DefectBot’ ⌝t))

    ¬□⊥ : ∀ {Γ A B} → Term {Γ ▻ A ▻ B} (W (W (‘□’ (‘Type’ Γ))))
    ¬□⊥ = w (w ⌜ ⌜ ‘¬’ (‘□’ ‘⊥’) ⌝ ⌝t)

data KnownBot : Set where
  DefectBot : KnownBot
  CooperateBot : KnownBot
  FairBot : KnownBot
  PrudentBot : KnownBot

KnownBot⇓ : KnownBot → □ ‘Bot’
KnownBot⇓ DefectBot = ‘DefectBot’
KnownBot⇓ CooperateBot = ‘CooperateBot’
KnownBot⇓ FairBot = ‘FairBot’
KnownBot⇓ PrudentBot = ‘PrudentBot’

DB-defects : ∀ {b} → □ (‘¬’ (‘DefectBot’ cooperates-with b))
CB-cooperates : ∀ {b} → □ (‘CooperateBot’ cooperates-with b)

FB-spec : KnownBot → □ ‘Bot’ → Type ε
FB-spec DefectBot b = ‘¬’ (‘FairBot’ cooperates-with b)
FB-spec CooperateBot b = ‘FairBot’ cooperates-with b
FB-spec FairBot b = ‘FairBot’ cooperates-with b
FB-spec PrudentBot b = ‘FairBot’ cooperates-with b

FB-good : ∀ {b} → □ (FB-spec b (KnownBot⇓ b))

DB-defects {b} = ‘λ∙’ ‘VAR₀’
CB-cooperates {b} = ‘tt’
FB-good {DefectBot} = {!!}
FB-good {CooperateBot} = {!!}
FB-good {FairBot} = {!!}
FB-good {PrudentBot} = {!!}

{-
data Bot : Set where
  DefectBot : Bot
  CooperateBot : Bot
  FairBot : Bot
  PrudentBot : Bot

data Opponent : Set where
  Self : Opponent
  Other : Type ε → Opponent

_cooperates-with-me : ∀ {Γ} → Term {Γ} (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝ ‘→’ ‘Type’ Γ) → Term {Γ ▻ ‘Type’ Γ} (W ‘Type’ Γ)
x cooperates-with-me = w→ (w x) ‘’ₐ ‘⌜‘VAR₀’⌝’

{-
‘cooperates-with'’ : □ (‘Bot’ ‘→’ ‘Bot’ ‘→’ ‘Type’ Γ)
‘cooperates-with'’ = ‘λ∙’ (→w ((‘eval-bot’ ‘VAR₀’) ‘∘’ (w→ (w {!!}))))
  where ‘eval-bot'’ : Term (‘Bot’ ‘→’ (‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))
        ‘eval-bot'’ = →SW1SV→W quine→

        ‘eval-bot’_ : Term {ε ▻ ‘Bot’} (W ‘Bot’) → Term (W (‘□’ ‘Bot’) ‘→’ W ‘Type’ Γ)
        ‘eval-bot’ b = w→ (w→ (w ‘eval-bot'’) ‘’ₐ b)

        get-bot-source : Term {ε} (‘Bot’ ‘→’ ‘□’ ‘Bot’)
        get-bot-source = {!!}-}

_‘cooperates’ : Bot → Term {ε} (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝ ‘→’ ‘Type’ Γ)
DefectBot ‘cooperates’ = ‘λ∙’ (w ⌜ ‘⊥’ ⌝)
CooperateBot ‘cooperates’ = ‘λ∙’ (w ⌜ ‘⊤’ ⌝)
FairBot ‘cooperates’ = ‘λ∙’ {!!}
PrudentBot ‘cooperates’ = {!!}

_‘cooperates-with'’_ : Bot → Term {ε} (‘Term’ ‘’ ⌜ ‘Type’ Γ ⌝ ‘→’ ‘Type’ Γ) → Type ε
FairBot ‘cooperates-with'’ x = Quine (W1 ‘Term’ ‘’ (x cooperates-with-me))
DefectBot ‘cooperates-with'’ b2 = ‘⊥’
CooperateBot ‘cooperates-with'’ b2 = ‘⊤’
PrudentBot ‘cooperates-with'’ x = Quine (W1 ‘Term’ ‘’ (x cooperates-with-me w‘‘×’’ w ⌜ (‘¬’ (‘Term’ ‘’ ⌜ ‘⊥’ ⌝) ‘→’ ‘¬’ {!!}) ⌝))
-}

   {-

  box-free? : ∀ {Γ} → Type Γ → context-to-term Γ → Set
  box-free? (T₁ ‘’ x) v = box-free? T₁ (v , x)
  box-free? ‘Type’ Γ v = ⊤
  box-free? ‘Term’ v = ⊥
  box-free? (T ‘→’ T₁) v = box-free? T v × box-free? T₁ v
  box-free? ‘⊤’ v = ⊤
  box-free? ‘⊥’ v = ⊤

  mutual
    kripke-lift→ : ∀ (n : ℕ) (T : Type ε) → box-free? (kripke-eval' n T) tt
      → Term (kripke-eval' n T ‘→’ T)
    kripke-lift→ zero T H = ‘λx∙x’
    kripke-lift→ (suc n) (T₁ ‘’ x) H = {!!}
    kripke-lift→ (suc n) (T ‘→’ T₁) H = {!!} ‘∘’ (kripke-lift→ n (kripke-reduce (T ‘→’ T₁) tt) H)
    kripke-lift→ (suc n) ‘Type’ Γ H = kripke-lift→ n _ H
    kripke-lift→ (suc n) ‘⊤’ H = kripke-lift→ n _ H
    kripke-lift→ (suc n) ‘⊥’ H = kripke-lift→ n _ H

    kripke-lift← : ∀ (n : ℕ) (T : Type ε) → box-free? (kripke-eval' n T) tt
      → Term (kripke-eval' n T)
      → Term T
    kripke-lift← n T H t = {!!}
{-    kripke-lift : ∀ {Γ} (T : Type Γ) v → Term (kripke-reduce T v ‘→’ Type-in T v)
    kripke-lift (T₁ ‘’ x) = {!!}
    kripke-lift ‘Type’ Γ v = {!!}
    kripke-lift ‘Term’ v = {!!}
    kripke-lift {ε} (T ‘→’ T₁) v = {!!}
  kripke-lift {Γ ▻ x} (T ‘→’ T₁) v = {!!}
  kripke-lift ‘⊤’ v = {!!}
  kripke-lift ‘⊥’ v = {!!}-}

  Quine : Type (ε ▻ ‘Type’ Γ) → Type ε
  Quine φ = {!!}

  quine→ : ∀ {φ} → Term {ε} (Quine φ        ‘→’ φ ‘’ ⌜ Quine φ ⌝)
  quine← : ∀ {φ} → Term {ε} (φ ‘’ ⌜ Quine φ ⌝ ‘→’ Quine φ)

  quine→ = {!!}
  quine← = {!!}
-}

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Which Maybe type which calls out to Haskell via the FFI
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Foreign.Haskell.Maybe where

open import Level
open import Data.Maybe.Base as Data using (just; nothing)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- Definition

data Maybe (A : Set a) : Set a where
  just    : A → Maybe A
  nothing : Maybe A

{-# FOREIGN GHC type AgdaMaybe l a = Maybe a #-}
{-# COMPILE GHC Maybe = data AgdaMaybe (Just | Nothing) #-}

------------------------------------------------------------------------
-- Conversion

toForeign : Data.Maybe A → Maybe A
toForeign (just x) = just x
toForeign nothing = nothing

fromForeign : Maybe A → Data.Maybe A
fromForeign (just x) = just x
fromForeign nothing = nothing

ext: agda


text:
-- Andreas, 2017-01-18, issue #5 is fixed
-- reported by Ulf 2007-10-24

data Nat : Set where
  zero : Nat

data Vec : Nat -> Set where
  []   : Vec zero

f : (n : Nat) -> Vec n -> Nat
f n@._ [] = n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module function.extensionality.core where

open import level using (lsuc; _⊔_)
open import equality.core

Extensionality : ∀ i j → Set (lsuc (i ⊔ j))
Extensionality i j = {X : Set i}{Y : Set j}
                   → {f g : X → Y}
                   → ((x : X) → f x ≡ g x)
                   → f ≡ g

Extensionality' : ∀ i j → Set (lsuc (i ⊔ j))
Extensionality' i j = {X : Set i}{Y : X → Set j}
                    → {f g : (x : X) → Y x}
                    → ((x : X) → f x ≡ g x)
                    → f ≡ g

StrongExt : ∀ i j → Set (lsuc (i ⊔ j))
StrongExt i j = {X : Set i}{Y : X → Set j}
              → {f g : (x : X) → Y x}
              → (∀ x → f x ≡ g x) ≡ (f ≡ g)

funext-inv : ∀ {i j}{X : Set i}{Y : X → Set j}
        → {f g : (x : X) → Y x}
        → f ≡ g
        → (x : X) → f x ≡ g x
funext-inv refl x = refl

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
-- This file gives the definition of Gaussian Integers, and common
-- operations on them.

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

module GauInt.Base where

open import Data.Bool using (Bool ; true ; false ; T ; not ; _∧_)
open import Data.Nat using (ℕ ; _≡ᵇ_)
open import Data.Integer renaming (-_ to -ℤ_ ; _-_ to _-ℤ_ ; _+_ to _+ℤ_ ; _*_ to _*ℤ_ ) hiding (NonZero)

infix  4 _==_ -- boolean equality on 𝔾.
infix  4 _==ℤ_ -- boolean equality on ℤ.
infixl 6 _+_ _-_
infixl 7 _*_
infix 8  -_
infixl 9 _ᶜ  -- conjugation on 𝔾.

-- A Gaussian integer is a pair of integers.
infix 5 _+_i
data 𝔾 : Set where
  _+_i : ℤ -> ℤ -> 𝔾

-- Addition.
_+_ : 𝔾 -> 𝔾 -> 𝔾
(a + b i) + (c + d i) = x + y i where
  x = a +ℤ c
  y = b +ℤ d

-- Additive identity.
0𝔾 : 𝔾
0𝔾 = 0ℤ + 0ℤ i

-- Additive inverse.
-_ : 𝔾 -> 𝔾
- (a + b i) = (-ℤ a) + (-ℤ b) i

-- Subtraction.
_-_ : 𝔾 -> 𝔾 -> 𝔾
_-_ x y = x + (- y)

-- Multiplication.
_*_ : 𝔾 -> 𝔾 -> 𝔾
(a + b i) * (c + d i) = x + y i where
  x = a *ℤ c -ℤ b *ℤ d
  y = (a *ℤ d) +ℤ b *ℤ c

-- Multiplicative identity.
1𝔾 : 𝔾
1𝔾 = 1ℤ + 0ℤ i

-- imaginary unit i.
iG : 𝔾
iG = 0ℤ + 1ℤ i

-- Real and imaginary part.
Re : 𝔾 -> ℤ
Re (a + b i) = a

Im : 𝔾 -> ℤ
Im (a + b i) = b

-- Conjugation of complex numbers retricted to Gaussian integers.
_ᶜ : 𝔾 -> 𝔾
_ᶜ (a + b i) = a + (-ℤ b) i

-- Rank.
rank : 𝔾 -> ℕ
rank (a + b i) = ∣ a *ℤ a +ℤ b *ℤ b ∣

-- Boolean equality on ℤ.
_==ℤ_ : ℤ -> ℤ -> Bool
+_ n ==ℤ +_ m = n ≡ᵇ m
+_ n ==ℤ -[1+_] n₁ = false
-[1+_] n ==ℤ +_ n₁ = false
-[1+_] n ==ℤ -[1+_] m = n ≡ᵇ m

-- Boolean equality on 𝔾.
_==_ : 𝔾 -> 𝔾 -> Bool
a + b i == c + d i = (a ==ℤ c) ∧ (b ==ℤ d)

-- NonZero predicate. Intended to use as implicit argument to deal
-- with the zero divisor case.
record NonZero (x : 𝔾) : Set where
  field
    nonZero : T (not ( x == 0𝔾))

-- ----------------------------------------------------------------------
-- Injections

-- I don't have good notation for this.
infix 5 _+0i'
_+0i' : ℤ -> 𝔾
_+0i' n = n + 0ℤ i

-- Injection of naturals are used more often.
infix 5 _+0i
_+0i : ℕ -> 𝔾
_+0i n = + n +0i'

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
module Category.Instance where

open import Level
open import Category.Core

𝟙 : Category _ _
𝟙 = record
    { Objects = record
        { Carrier = ⊤
        ; _≈_ = λ _ _ → ⊤
        ; isEquivalence = _
        }
    ; Morphisms = record
        { Carrier = λ x → ⊤
        ; _≈_ = λ _ _ → ⊤
        ; isEquivalence = _
        ; _∘_ = λ _ _ → tt
        ; id = λ a → tt
        ; isMorphism = _
        }
    }
    where
        open import Data.Unit

-- "pointing" an element with a functor from 𝟙
point : ∀ {𝒸 ℓ} → {C : Category 𝒸 ℓ} → Category.Object C → Functor 𝟙 C
point {_} {_} {C} c = record
    { mapObject = λ _ → c
    ; mapMorphism = λ _ → id c
    ; isFunctor = record
        { preserve-id = λ a → MorphEq.refl
        ; preserve-∘ = λ _ _ → MorphEq.sym (left-identity (id c))
        }
    }
    where
        open Category C
        open import Relation.Binary.Indexed
        module MorphEq = IsEquivalence (MorphismStructure.isEquivalence Morphisms)

        open IsMorphism isMorphism

-- the identity functo
identity : ∀ {𝒸 ℓ} → (C : Category 𝒸 ℓ) → Functor C C
identity C = record
    { mapObject = λ x → x
    ; mapMorphism = λ x → x
    ; isFunctor = record
        { preserve-id = λ a → MorphEq.refl
        ; preserve-∘ = λ f g → MorphEq.refl
        }
    }
    where
        open Category C
        open import Relation.Binary.Indexed
        module MorphEq = IsEquivalence (MorphismStructure.isEquivalence Morphisms)

        open IsMorphism isMorphism

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


text:
{-# OPTIONS --enable-prop #-}

data TestProp : Prop where
  p₁ p₂ : TestProp

data _≡Prop_ {A : Prop} (x : A) : A → Set where
  refl : x ≡Prop x

p₁≢p₂ : {P : Prop} → p₁ ≡Prop p₂ → P
p₁≢p₂ ()

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak.Up-to {ℓ} (lts : LTS ℓ) where

open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bisimilarity.Weak lts
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
open import Expansion lts as E using (Expansion; _≲_; ≳:_)
import Expansion.Equational-reasoning-instances
open import Indexed-container
open import Relation
import Similarity.Weak lts as S
import Up-to

open LTS lts

import Similarity.Step lts _[_]⇒̂_ as SS

------------------------------------------------------------------------
-- The general up-to machinery, instantiated with the StepC container

open Up-to StepC public

------------------------------------------------------------------------
-- Up to expansion

-- Up to expansion.
--
-- I took this definition from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi.

Up-to-expansion : Trans₂ ℓ Proc
Up-to-expansion R = Expansion ∞ ⊙ R ⊙ Expansion ∞ ⁻¹

-- Up to expansion is monotone.

up-to-expansion-monotone : Monotone Up-to-expansion
up-to-expansion-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- Up to expansion is size-preserving.

up-to-expansion-size-preserving : Size-preserving Up-to-expansion
up-to-expansion-size-preserving =
  _⇔_.from (monotone→⇔ up-to-expansion-monotone)
    (λ where
       {x = p , q} (r , p≳r , s , r≈s , s≲q) →
         p  ∼⟨ p≳r ⟩
         r  ∼′⟨ r≈s ⟩ ≳:
         s  ∽⟨ s≲q ⟩■
         q)

------------------------------------------------------------------------
-- A generalisation of up to expansion

mutual

  -- A monolithic implementation of a non-symmetric variant of up to
  -- expansion, based on the technique presented in Section 6.5.2.4 of
  -- "Enhancements of the bisimulation proof method" by Pous and
  -- Sangiorgi.
  --
  -- It is at the time of writing not clear to me if there is some
  -- size-preserving proof that matches this technique.

  6-5-2-4 :
    {R : Rel₂ ℓ Proc} →
    (∀ {P P′ Q μ} →
     R (P , Q) → P [ μ ]⟶ P′ →
     ∃ λ Q′ → Q [ μ ]⇒̂ Q′ ×
       (Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞) (P′ , Q′)) →
    (∀ {P Q Q′ μ} →
     R (P , Q) → Q [ μ ]⟶ Q′ →
     ∃ λ P′ → P [ μ ]⇒̂ P′ ×
       (Weak-bisimilarity ∞ ⊙ R ⊙ Expansion ∞ ⁻¹) (P′ , Q′)) →
    R ⊆ Weak-bisimilarity ∞
  6-5-2-4 {R} lr⟶ rl⟶ =
    6-5-2-4′ (λ PRQ → S.⟨ lr⟶ PRQ ⟩)
             (λ PR⁻¹Q → S.⟨ Σ-map id (Σ-map id lemma) ∘ rl⟶ PR⁻¹Q ⟩)
    where
    lemma :
      Weak-bisimilarity ∞ ⊙ R ⊙ Expansion ∞ ⁻¹ ⊆
      (Expansion ∞ ⊙ R ⁻¹ ⊙ Weak-bisimilarity ∞) ⁻¹
    lemma (_ , P₁≈P₂ , _ , P₂RP₃ , P₃≲P₄) =
      (_ , P₃≲P₄ , _ , P₂RP₃ , symmetric P₁≈P₂)

  -- A variant of 6-5-2-4.

  6-5-2-4′ :
    let Prog = λ (R : Rel₂ ℓ Proc) →
          R ⊆ ⟦ S.StepC ⟧ (Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞) in
    ∀ {R} → Prog R → Prog (R ⁻¹) → R ⊆ Weak-bisimilarity ∞
  6-5-2-4′ {R} lr⟶ rl⟶ =
    R                    ⊆⟨ ⊆≈≈ ⟩
    ≈ R ≈                ⊆⟨ unfold _ (λ P≈R≈Q →
                                        StepC.⟨ SS.Step.challenge (lemma lr⟶ P≈R≈Q)
                                              , Σ-map id (Σ-map id ≈≈-sym) ∘
                                                  SS.Step.challenge (lemma rl⟶ (≈≈-sym P≈R≈Q))
                                              ⟩) ⟩∎
    Weak-bisimilarity ∞  ∎
    where
    ≈_≈ : Rel₂ ℓ Proc → Rel₂ ℓ Proc
    ≈ R ≈ = Weak-bisimilarity ∞ ⊙ R ⊙ Weak-bisimilarity ∞

    ⊆≈≈ : ∀ {R} → R ⊆ ≈ R ≈
    ⊆≈≈ r = _ , reflexive , _ , r , reflexive

    ≳_≈ : Rel₂ ℓ Proc → Rel₂ ℓ Proc
    ≳ R ≈ = Expansion ∞ ⊙ R ⊙ Weak-bisimilarity ∞

    ⊆≳≈ : ∀ {R} → R ⊆ ≳ R ≈
    ⊆≳≈ r = _ , reflexive , _ , r , reflexive

    ≈≈-sym : ∀ {R} → ≈ R ≈ ⊆ ≈ R ⁻¹ ≈ ⁻¹
    ≈≈-sym (_ , P₁≈P₂ , _ , P₂RP₃ , P₃≈P₄) =
      (_ , symmetric P₃≈P₄ , _ , P₂RP₃ , symmetric P₁≈P₂)

    lemma : ∀ {R} → R ⊆ ⟦ S.StepC ⟧ ≳ R ≈ → ≈ R ≈ ⊆ SS.Step ≈ R ≈
    lemma {R} lr⟶ = λ where
        (P₁ , P≈P₁ , Q₁ , P₁RQ₁ , Q₁≈Q) .SS.Step.challenge P⟶P₁ →
          let P₁′ , P₁⟶̂P₁′ , P′≈′P₁′ = left-to-right P≈P₁ P⟶P₁
              Q₁′ , Q₁⇒̂Q₁′ , P₁″ ,
                P₁′≳P₁″ , Q₁″ ,
                P₁″RQ₁″ , Q₁″≈Q₁′    = lr≳≈⇒̂ (⊆≳≈ P₁RQ₁) P₁⟶̂P₁′
              Q′ , Q⇒̂Q′  , Q₁′≈Q′    = weak-is-weak⇒̂ Q₁≈Q Q₁⇒̂Q₁′
          in Q′ , Q⇒̂Q′ , P₁″
           , transitive′ {a = ℓ} (force P′≈′P₁′) P₁′≳P₁″
           , Q₁″ , P₁″RQ₁″ , transitive {a = ℓ} Q₁″≈Q₁′ Q₁′≈Q′
      where
      lr⟶̂ :
        ∀ {P P′ Q μ} →
        R (P , Q) → P [ μ ]⟶̂ P′ → ∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
      lr⟶̂ PRQ (done s)    = _ , silent s done , ⊆≳≈ PRQ
      lr⟶̂ PRQ (step P⟶P′) = S.challenge (lr⟶ PRQ) P⟶P′

      lr≳≈⟶ :
        ∀ {P P′ Q μ} →
        ≳ R ≈ (P , Q) → P [ μ ]⟶ P′ →
        ∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
      lr≳≈⟶ (P₁ , P≳P₁ , Q₁ , P₁RQ₁ , Q₁≈Q) P⟶P′ =
        let P₁′ , P₁⟶̂P₁′ , P′≳P₁′          = E.left-to-right P≳P₁ P⟶P′
            Q₁′ , Q₁⇒̂Q₁′ , P₁″ , P₁′≳P₁″ ,
              Q₁″ , P₁″RQ₁″ , Q₁″≈Q₁′      = lr⟶̂ P₁RQ₁ P₁⟶̂P₁′
            Q′ , Q⇒̂Q′ , Q₁′≈Q′             = weak-is-weak⇒̂ Q₁≈Q Q₁⇒̂Q₁′
        in Q′ , Q⇒̂Q′ ,
           P₁″ , transitive {a = ℓ} P′≳P₁′ P₁′≳P₁″ ,
           Q₁″ , P₁″RQ₁″ , transitive {a = ℓ} Q₁″≈Q₁′ Q₁′≈Q′

      lr≳≈⇒ :
        ∀ {P P′ Q} →
        ≳ R ≈ (P , Q) → P ⇒ P′ → ∃ λ Q′ → Q ⇒ Q′ × ≳ R ≈ (P′ , Q′)
      lr≳≈⇒ P≳R≈Q done                = _ , done , P≳R≈Q
      lr≳≈⇒ P≳R≈Q (step s P⟶P′ P′⇒P″) =
        let Q′ , Q⇒̂Q′  , P′≳R≈Q′ = lr≳≈⟶ P≳R≈Q P⟶P′
            Q″ , Q′⇒Q″ , P″≳R≈Q″ = lr≳≈⇒ P′≳R≈Q′ P′⇒P″
        in Q″ , ⇒-transitive (⇒̂→⇒ s Q⇒̂Q′) Q′⇒Q″ , P″≳R≈Q″

      lr≳≈[]⇒ :
        ∀ {P P′ Q μ} →
        ¬ Silent μ →
        ≳ R ≈ (P , Q) → P [ μ ]⇒ P′ →
        ∃ λ Q′ → Q [ μ ]⇒ Q′ × ≳ R ≈ (P′ , Q′)
      lr≳≈[]⇒ ¬s P≳R≈Q (steps P⇒P′ P′⟶P″ P″⇒P‴) =
        let Q′ , Q⇒Q′  , P′≳R≈Q′ = lr≳≈⇒ P≳R≈Q P⇒P′
            Q″ , Q′⇒̂Q″ , P″≳R≈Q″ = lr≳≈⟶ P′≳R≈Q′ P′⟶P″
            Q‴ , Q″⇒Q‴ , P‴≳R≈Q‴ = lr≳≈⇒ P″≳R≈Q″ P″⇒P‴
        in Q‴
         , []⇒⇒-transitive (⇒[]⇒-transitive Q⇒Q′ (⇒̂→[]⇒ ¬s Q′⇒̂Q″)) Q″⇒Q‴
         , P‴≳R≈Q‴

      lr≳≈⇒̂ :
        ∀ {P P′ Q μ} →
        ≳ R ≈ (P , Q) → P [ μ ]⇒̂ P′ →
        ∃ λ Q′ → Q [ μ ]⇒̂ Q′ × ≳ R ≈ (P′ , Q′)
      lr≳≈⇒̂ PRQ = λ where
        (silent s P⇒P′)      → Σ-map id (Σ-map (silent s)      id)
                                 (lr≳≈⇒ PRQ P⇒P′)
        (non-silent ¬s P⇒P′) → Σ-map id (Σ-map (non-silent ¬s) id)
                                 (lr≳≈[]⇒ ¬s PRQ P⇒P′)

------------------------------------------------------------------------
-- Up to weak bisimilarity

-- Up to weak bisimilarity.
--
-- I based this definition on Definition 4.2.13 in Milner's
-- "Operational and Algebraic Semantics of Concurrent Processes".

Up-to-weak-bisimilarity : Trans₂ ℓ Proc
Up-to-weak-bisimilarity R =
  Weak-bisimilarity ∞ ⊙ R ⊙ Weak-bisimilarity ∞

-- Up to weak bisimilarity is monotone.

up-to-weak-bisimilarity-monotone : Monotone Up-to-weak-bisimilarity
up-to-weak-bisimilarity-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- If transitivity of weak bisimilarity is size-preserving in the
-- first argument, then "up to weak bisimilarity" is size-preserving.

size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving :
  (∀ {i x y z} → [ i ] x ≈ y → [ ∞ ] y ≈ z → [ i ] x ≈ z) →
  Size-preserving Up-to-weak-bisimilarity
size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving
  trans =
  _⇔_.from (monotone→⇔ up-to-weak-bisimilarity-monotone) λ where
    {x = p , q} (r , p≈r , s , r≈s , s≈q) →
      p  ≈∞⟨ p≈r ⟩
      r  ≈⟨ r≈s ⟩∞
      s  ∼⟨ s≈q ⟩■
      q
  where
  infixr -2 _≈⟨_⟩∞_ _≈∞⟨_⟩_

  _≈⟨_⟩∞_ : ∀ {i} x {y z} → [ i ] x ≈ y → [ ∞ ] y ≈ z → [ i ] x ≈ z
  _ ≈⟨ p ⟩∞ q = trans p q

  _≈∞⟨_⟩_ : ∀ {i} x {y z} → [ ∞ ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z
  _ ≈∞⟨ p ⟩ q = symmetric (trans (symmetric q) (symmetric p))

-- If transitivity of weak bisimilarity is size-preserving in both
-- arguments, then weak bisimulations up to weak bisimilarity are
-- contained in weak bisimilarity.

size-preserving-transitivity→up-to-weak-bisimilarity-up-to :
  (∀ {i x y z} → [ i ] x ≈ y → [ i ] y ≈ z → [ i ] x ≈ z) →
  Up-to-technique Up-to-weak-bisimilarity
size-preserving-transitivity→up-to-weak-bisimilarity-up-to =
  size-preserving→up-to ∘
  size-preserving-transitivity→up-to-weak-bisimilarity-size-preserving

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.FGIdeal where
open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal renaming (generatedIdeal to generatedIdealCommRing)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Ideal

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
  open CommAlgebraStr (snd A)

  generatedIdeal : {n : ℕ} → FinVec (fst A) n → IdealsIn A
  generatedIdeal = generatedIdealCommRing (CommAlgebra→CommRing A)

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}

record ⊤ : Set where
  constructor tt

data I : Set where
  i : ⊤ → I

data D : I → Set where
  d : D (i tt)

postulate
  P : (x : I) → D x → Set

foo : (y : _) → P _ y
foo d = {!!}


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

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

open import Cubical.Data.Unit

import Cubical.Algebra.Magma.Construct.Unit as ⊤Magma
open ⊤Magma public hiding (⊤-isMagma; ⊤-Magma)

◯-assoc : Associative _◯_
◯-assoc _ _ _ = refl

⊤-isSemigroup : IsSemigroup ⊤ _◯_
⊤-isSemigroup = record
  { isMagma = ⊤Magma.⊤-isMagma
  ; assoc   = ◯-assoc
  }

⊤-Semigroup : Semigroup ℓ-zero
⊤-Semigroup = record { isSemigroup = ⊤-isSemigroup }


text:
------------------------------------------------------------------------
-- Some properties that hold for Erased do not hold for every
-- accessible modality
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Erased.Counterexamples.Cubical
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
open import Erased.Cubical eq
  using (Σ-closed-reflective-subuniverse; Accessible)
open import Equality.Decision-procedures equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Path-split equality-with-J as PS
  using (_-Null_; Is-∞-extendable-along-[_])
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T
  using (∥_∥; ∣_∣; Axiom-of-choice)
open import Preimage equality-with-J using (_⁻¹_)

private
  variable
    a b ℓ ℓ′ p : Level
    A          : Type a

-- A type is modal with respect to the modality ∥_∥ if it is a
-- proposition.

∥∥-modal : Type ℓ → Type ℓ
∥∥-modal = Is-proposition

-- Propositional truncation is a Σ-closed reflective subuniverse.
--
-- This proof is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

∥∥-modality : Σ-closed-reflective-subuniverse ℓ
∥∥-modality {ℓ = ℓ} = λ where
    .◯                      → ∥_∥
    .η                      → ∣_∣
    .Is-modal               → ∥∥-modal
    .Is-modal-propositional → λ ext → H-level-propositional ext 1
    .Is-modal-◯             → T.truncation-is-proposition
    .Is-modal-respects-≃    → H-level-cong _ 1
    .extendable-along-η     → extendable
    .Σ-closed               → Σ-closure 1
  where
  open Σ-closed-reflective-subuniverse

  extendable :
    {A B : Type ℓ} →
    Is-proposition B →
    Is-∞-extendable-along-[ ∣_∣ ] (λ (_ : ∥ A ∥) → B)
  extendable {A = A} {B = B} =
    Is-proposition B                                   →⟨ (λ prop →
                                                             _≃_.is-equivalence $
                                                             Eq.↔→≃
                                                               _
                                                               (T.rec prop)
                                                               refl
                                                               (λ f → ⟨ext⟩ $
                                                                  T.elim
                                                                    _
                                                                    (λ _ → ⇒≡ 1 prop)
                                                                    (λ _ → refl _))) ⟩
    Is-equivalence (λ (f : ∥ A ∥ → B) → f ∘ ∣_∣)       ↔⟨ inverse $ PS.Is-∞-extendable-along≃Is-equivalence ext ⟩□
    Is-∞-extendable-along-[ ∣_∣ ] (λ (_ : ∥ A ∥) → B)  □

-- The propositional truncation modality is accessible.
--
-- This proof is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

∥∥-accessible : Accessible ℓ′ (∥∥-modality {ℓ = ℓ})
∥∥-accessible {ℓ′ = ℓ′} {ℓ = ℓ} =
    ↑ ℓ′ ⊤
  , (λ _ → ↑ ℓ′ Bool)
  , (λ A →
       Is-proposition A                                  ↝⟨ record { from = from; to = to } ⟩
       (λ _ → ↑ ℓ′ Bool) -Null A                         ↔⟨ inverse $ PS.Π-Is-∞-extendable-along≃Null ext ⟩□
       (↑ ℓ′ ⊤ → Is-∞-extendable-along-[ _ ] (λ _ → A))  □)

  where
  to : Is-proposition A → (λ _ → ↑ ℓ′ Bool) -Null A
  to prop _ =
    _≃_.is-equivalence $
    Eq.⇔→≃
      prop
      (Π-closure ext 1 λ _ → prop)
      _
      (_$ lift true)

  from : (λ _ → ↑ ℓ′ Bool) -Null A → Is-proposition A
  from {A = A} null x y =
    x                                      ≡⟨⟩
    case true ⦂ Bool of if_then x else y   ≡⟨ cong (_$ true) $ sym $ E.right-inverse-of _ ⟩
    E.to (E.from (if_then x else y)) true  ≡⟨⟩
    E.from (if_then x else y)              ≡⟨⟩
    E.to (E.from (if_then x else y)) false ≡⟨ cong (_$ false) $ E.right-inverse-of _ ⟩
    case false ⦂ Bool of if_then x else y  ≡⟨⟩
    y                                      ∎
    where
    ≃Bool→ : A ≃ (Bool → A)
    ≃Bool→ =
      A                ↝⟨ Eq.⟨ _ , null _ ⟩ ⟩
      (↑ ℓ′ Bool → A)  ↝⟨ Eq.↔→≃ (_∘ lift) (_∘ lower) refl refl ⟩□
      (Bool → A)       □

    module E = _≃_ ≃Bool→

-- It is not the case that, for all types A and B and functions
-- f : A → B, "f is ∥∥-connected" implies ∥ Is-equivalence f ∥.

¬[∥∥-connected→∥Is-equivalence∥] :
  ¬ ({A : Type a} {B : Type b} {f : A → B} →
     (∀ y → Contractible ∥ f ⁻¹ y ∥) → ∥ Is-equivalence f ∥)
¬[∥∥-connected→∥Is-equivalence∥] hyp =
                                                                   $⟨ (λ _ → ∣ lift true , refl _ ∣) ⟩

  ((y : ↑ _ ⊤) → ∥ (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ⁻¹ y ∥)  →⟨ (∀-cong _ λ _ →
                                                                       propositional⇒inhabited⇒contractible T.truncation-is-proposition) ⟩
  ((y : ↑ _ ⊤) →
   Contractible ∥ (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ⁻¹ y ∥)   →⟨ hyp ⟩

  ∥ Is-equivalence (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤)) ∥        ↔⟨ T.∥∥↔ (Eq.propositional ext _) ⟩

  Is-equivalence (const (lift tt) ⦂ (↑ _ Bool → ↑ _ ⊤))            →⟨ Eq.⟨ _ ,_⟩ ⟩

  ↑ _ Bool ≃ ↑ _ ⊤                                                 →⟨ (λ eq → Eq.↔⇒≃ B.↑↔ F.∘ eq F.∘ Eq.↔⇒≃ (inverse B.↑↔)) ⟩

  Bool ≃ ⊤                                                         →⟨ (λ eq → H-level-cong _ 1 (inverse eq) (mono₁ 0 ⊤-contractible)) ⟩

  Is-proposition Bool                                              →⟨ ¬-Bool-propositional ⟩□

  ⊥                                                                □

-- It is not the case that, for all types A and B and functions
-- f : A → B, "f is ∥∥-connected" is equivalent to
-- ∥ Is-equivalence f ∥.
--
-- Compare with
-- Erased.Level-1.[]-cong₂-⊔.Erased-connected↔Erased-Is-equivalence.

¬[∥∥-connected≃∥Is-equivalence∥] :
  ¬ ({A : Type a} {B : Type b} {f : A → B} →
     (∀ y → Contractible ∥ f ⁻¹ y ∥) ≃ ∥ Is-equivalence f ∥)
¬[∥∥-connected≃∥Is-equivalence∥] hyp =
  ¬[∥∥-connected→∥Is-equivalence∥] (_≃_.to hyp)

-- If (x : A) → ∥ P x ∥ implies ∥ ((x : A) → P x) ∥ for all types A
-- and type families P over A, then the axiom of choice holds.

[Π∥∥→∥Π∥]→Axiom-of-choice :
  ({A : Type a} {P : A → Type p} →
   ((x : A) → ∥ P x ∥) → ∥ ((x : A) → P x) ∥) →
  Axiom-of-choice a p
[Π∥∥→∥Π∥]→Axiom-of-choice hyp = λ _ → hyp

-- If ∥ ((x : A) → P x) ∥ is isomorphic to (x : A) → ∥ P x ∥ for all
-- types A and type families P over A, then the axiom of choice holds.
--
-- Compare with Erased.Level-1.Erased-Π↔Π.

[∥Π∥↔Π∥∥]→Axiom-of-choice :
  ({A : Type a} {P : A → Type p} →
   ∥ ((x : A) → P x) ∥ ↔ ((x : A) → ∥ P x ∥)) →
  Axiom-of-choice a p
[∥Π∥↔Π∥∥]→Axiom-of-choice hyp =
  [Π∥∥→∥Π∥]→Axiom-of-choice (_↔_.from hyp)

-- If ∥ A ∥ → ∥ B ∥ implies ∥ (A → B) ∥ for all types A and B in the
-- same universe, then ∥ (∥ A ∥ → A) ∥ holds for every type A in this
-- universe. This is a variant of the axiom of choice of which Kraus
-- et al. state that "We expect that this makes it possible to show
-- that, in MLTT with weak propositional truncation, [a logically
-- equivalent variant of the axiom] is not derivable" (see "Notions of
-- Anonymous Existence in Martin-Löf Type Theory").

[[∥∥→∥∥]→∥→∥]→Axiom-of-choice :
  ({A B : Type a} → (∥ A ∥ → ∥ B ∥) → ∥ (A → B) ∥) →
  ({A : Type a} → ∥ (∥ A ∥ → A) ∥)
[[∥∥→∥∥]→∥→∥]→Axiom-of-choice hyp {A = A} =
                       $⟨ T.rec T.truncation-is-proposition id ⟩
  (∥ ∥ A ∥ ∥ → ∥ A ∥)  →⟨ hyp ⟩□
  ∥ (∥ A ∥ → A) ∥      □

-- If ∥ (A → B) ∥ is isomorphic to ∥ A ∥ → ∥ B ∥ for all types A and B
-- in the same universe, then ∥ (∥ A ∥ → A) ∥ holds for every type A
-- in this universe. This is a variant of the axiom of choice of which
-- Kraus et al. state that "We expect that this makes it possible to
-- show that, in MLTT with weak propositional truncation, [a logically
-- equivalent variant of the axiom] is not derivable" (see "Notions of
-- Anonymous Existence in Martin-Löf Type Theory").
--
-- Compare with Erased.Level-1.Erased-Π↔Π-Erased.

[∥→∥↔[∥∥→∥∥]]→Axiom-of-choice :
  ({A B : Type a} → ∥ (A → B) ∥ ↔ (∥ A ∥ → ∥ B ∥)) →
  ({A : Type a} → ∥ (∥ A ∥ → A) ∥)
[∥→∥↔[∥∥→∥∥]]→Axiom-of-choice hyp =
  [[∥∥→∥∥]→∥→∥]→Axiom-of-choice (_↔_.from hyp)

-- It is not the case that, for every type A, if A is ∥∥-modal, then A
-- is (λ (A : Type a) → ∥∥-modal A)-null.

¬[∥∥-modal→∥∥-modal-Null] :
  ¬ ({A : Type a} → ∥∥-modal A → (λ (A : Type a) → ∥∥-modal A) -Null A)
¬[∥∥-modal→∥∥-modal-Null] hyp =                                 $⟨ ⊥-propositional ⟩
  Is-proposition ⊥                                              →⟨ hyp ⟩
  (∀ A → Is-equivalence (const ⦂ (⊥ → Is-proposition A → ⊥)))   →⟨ _$ _ ⟩
  Is-equivalence (const ⦂ (⊥ → Is-proposition (↑ _ Bool) → ⊥))  →⟨ Eq.⟨ _ ,_⟩ ⟩
  ⊥ ≃ (Is-proposition (↑ _ Bool) → ⊥)                           →⟨ →-cong ext
                                                                     (Eq.↔⇒≃ $ inverse $
                                                                      B.⊥↔uninhabited (¬-Bool-propositional ∘ ↑⁻¹-closure 1))
                                                                     Eq.id F.∘_ ⟩
  ⊥ ≃ (⊥₀ → ⊥)                                                  →⟨ Π⊥↔⊤ ext F.∘_ ⟩
  ⊥ ≃ ⊤                                                         →⟨ (λ eq → ⊥-elim $ _≃_.from eq _) ⟩□
  ⊥                                                             □

-- It is not the case that, for every type A, there is an equivalence
-- between "A is ∥∥-modal" and (λ (A : Type a) → ∥∥-modal A) -Null A.
--
-- Compare with Erased.Stability.Very-stable≃Very-stable-Null.

¬[∥∥-modal≃∥∥-modal-Null] :
  ¬ ({A : Type a} → ∥∥-modal A ≃ (λ (A : Type a) → ∥∥-modal A) -Null A)
¬[∥∥-modal≃∥∥-modal-Null] hyp =
  ¬[∥∥-modal→∥∥-modal-Null] (_≃_.to hyp)

-- It is not the case that, for every type A : Type a and proof of
-- Extensionality a a, there is an equivalence between "A is ∥∥-modal"
-- and (λ (A : Type a) → ∥∥-modal A) -Null A.
--
-- Compare with Erased.Stability.Very-stable≃Very-stable-Null.

¬[∥∥-modal≃∥∥-modal-Null]′ :
  ¬ ({A : Type a} →
     Extensionality a a →
     ∥∥-modal A ≃ (λ (A : Type a) → ∥∥-modal A) -Null A)
¬[∥∥-modal≃∥∥-modal-Null]′ hyp =
  ¬[∥∥-modal≃∥∥-modal-Null] (hyp ext)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
data U : Set
T : U → Set

{-# NO_UNIVERSE_CHECK #-}
data U where
  pi : (A : Set)(b : A → U) → U

T (pi A b) = (x : A) → T (b x)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Examples.TrafficLight where

open import Data.Bool
open import Data.Empty
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit
open import Relation.Binary.PropositionalEquality

open import Library
open import FStream.Core
open import FStream.FVec
open import FStream.Containers

open import CTL.Modalities
open import CTL.Proof

data Colour : Set where
  red   : Colour
  green : Colour

_<$>_ = fmap

boolToColour : Bool → Colour
boolToColour false = green
boolToColour true = red

trafficLight : FStream (ReaderC Bool) Colour
trafficLight = ⟨ returnReader green ▻ (boolToColour <$> ask) ▻ returnReader green ▻ returnReader red ⟩ ▻⋯
-- TODO Consider replacing Colour by Bool for simplification

boolLight : FStream (ReaderC Bool) Bool
boolLight = ⟨ returnReader true ▻ returnReader true ▻ returnReader false ⟩ ▻⋯

-- TODO This only proves that right now (in the first tick), liveness is satisfied, but not in the later ticks!
isLive : AF (map (_≡ green) trafficLight)
isLive p = alreadyA refl

trafficLight₂ : FStream (ReaderC Bool) Colour
trafficLight₂ = ⟨ returnReader red ▻ (boolToColour <$> ask) ▻ returnReader red ▻ returnReader green ⟩ ▻⋯
boolLight₂ : FStream (ReaderC Bool) Bool
boolLight₂ = ⟨ returnReader false ▻ returnReader false ▻ returnReader true ⟩ ▻⋯

-- FIND-OUT how to call this / what this actually means
isLive₂ : EF (map (_≡ true) boolLight₂)
isLive₂ p = notYetE (true , (notYetE (true , (alreadyE refl))))
-- notYetE (true , (notYetE (true , (alreadyE (false , refl)))))

trafficLight₃ : ∀ {i} → FStream {i} (ReaderC Bool) Colour
trafficLight₃ = ⟨ returnReader green ▻ (boolToColour <$> ask) ▻ returnReader red ▻ returnReader green ⟩ ▻⋯
boolLight₃ : FStream (ReaderC Bool) Bool
boolLight₃ = ⟨ returnReader true ▻ returnReader false ▻ returnReader true ⟩ ▻⋯

isLive₄ : ∀ {i} → AG {i} (AFₛ (map (_≡ green) (trafficLight₃)))
nowA (isLive₄ p) = alreadyA refl
nowA (laterA (isLive₄ p) false) = alreadyA refl
nowA (laterA (isLive₄ p) true) = notYetA (const (notYetA (const (alreadyA refl))))
nowA (laterA (laterA (isLive₄ p) p₁) p₂) = notYetA (λ p₃ → alreadyA refl)
nowA (laterA (laterA (laterA (isLive₄ p) p₁) p₂) p₃) = alreadyA refl
laterA (laterA (laterA (laterA (isLive₄ p) p₁) p₂) p₃) p₄ = isLive₄ true

mutual
  -- This fellow switches between false and true every time a "true" is entered as input
  trueEgde : ∀ {i} → FStream {i} (ReaderC Bool) Bool
  proj₁ (inF trueEgde) = tt
  head (proj₂ (inF trueEgde) true) = false
  tail (proj₂ (inF trueEgde) true) = falseEgde
  head (proj₂ (inF trueEgde) false) = true
  tail (proj₂ (inF trueEgde) false) = trueEgde
  falseEgde : ∀ {i} → FStream {i} (ReaderC Bool) Bool
  proj₁ (inF falseEgde) = tt
  head (proj₂ (inF falseEgde) true) = true
  tail (proj₂ (inF falseEgde) true) = trueEgde
  head (proj₂ (inF falseEgde) false) = false
  tail (proj₂ (inF falseEgde) false) = falseEgde

-- At every point in time, it is possible (by correct input) to output true
mutual
  edgeResponsive : ∀ {i} → AG {i} (EFₛ (map (_≡ true) trueEgde ))
  nowA (edgeResponsive false) = alreadyE refl
  nowA (edgeResponsive true) = notYetE (true , alreadyE refl)
  laterA (edgeResponsive false) = edgeResponsive
  laterA (edgeResponsive true) = edgeResponsive'
  edgeResponsive' : ∀ {i} → AG {i} (EFₛ (map (_≡ true) falseEgde))
  edgeResponsive' = {!   !}
  -- Exercise for you, dear reader!

frob : ∀ {i} → Bool → FStream {i} (ReaderC Bool) Bool
proj₁ (inF (frob b)) = tt
head (proj₂ (inF (frob b)) false) = b
tail (proj₂ (inF (frob b)) false) = frob b
head (proj₂ (inF (frob b)) true) = not b
tail (proj₂ (inF (frob b)) true) = frob (not b)

frobResponsive : ∀ {i} → (b : Bool) → AG {i} (EFₛ (map (_≡ true) (frob b) ))
nowA (frobResponsive false false) = notYetE (true , alreadyE refl)
nowA (frobResponsive false true) = alreadyE refl
nowA (frobResponsive true false) = alreadyE refl
nowA (frobResponsive true true) = notYetE (true , (alreadyE refl))
laterA (frobResponsive b false) = frobResponsive b
laterA (frobResponsive b true) = frobResponsive (not b)

-- Prove that a series of ⊤ is always true, under any circumstance
tautology : AG ⟨ returnReader ⊤ ⟩ ▻⋯
-- We create a cyclical stream of proofs
tautology = ⟨ const tt ⟩AG ▻AG

tautology₂ : ∀ {i} → AG {i} ⟨ returnReader ⊤ ⟩ ▻⋯
nowA (tautology₂ p) = tt
laterA (tautology₂ p) = tautology₂
-- p is the position of the first side effect

-- TODO Find something that this satisfies
identity : ∀ {A} → FStream (ReaderC A) A
identity = ⟨ ask ⟩ ▻⋯

alwaysGreen : ∀ {i} → FStream {i} (ReaderC Bool) Colour
alwaysGreen = ⟨ (returnReader green) ▻ returnReader green ⟩ ▻⋯

isAlwaysGreen : ∀ {i} → AG {i} (map (_≡ green) alwaysGreen)
nowA (isAlwaysGreen p) = refl
nowA (laterA (isAlwaysGreen p) p₁) = refl
laterA (laterA (isAlwaysGreen p) p₁) p₂ = isAlwaysGreen p
{-
nowA isAlwaysGreen _ = refl
nowA (laterA isAlwaysGreen _) _ = refl
laterA (laterA isAlwaysGreen _) _ = isAlwaysGreen
-}

isAlwaysGreen' : ∀ {i} → AG {i} (map (_≡ green) alwaysGreen)
isAlwaysGreen' = {!   !} -- TODO Would like to use bisimulation

isGreenOrRed : ∀ {i} → AG {i} (map (λ x → (x ≡ green) ⊎ (x ≡ red)) ⟨ returnReader green ▻ returnReader red ⟩ ▻⋯)
nowA (isGreenOrRed p) = inj₁ refl
nowA (laterA (isGreenOrRed p) p₁) = inj₂ refl
laterA (laterA (isGreenOrRed p) p₁) p₂ = isGreenOrRed p

trafficLight₄ : ∀ {i} → FStream {i} (ReaderC Bool) Bool
trafficLight₄ = ⟨ returnReader true ▻ ask ⟩ ▻⋯

liveness₄ : ∀ {i} → AG {i} (AFₛ (map (true ≡_) trafficLight₄))
nowA (liveness₄ p) = alreadyA refl
nowA (laterA (liveness₄ p) p₁) = notYetA (λ p₂ → alreadyA refl)
laterA (laterA (liveness₄ p) p₁) = liveness₄

responsivity : ∀ {i} → EG {i} (map (true ≡_) trafficLight₄)
proj₁ responsivity = false
nowE (proj₂ responsivity) = refl
proj₁ (laterE (proj₂ responsivity)) = true
nowE (proj₂ (laterE (proj₂ responsivity))) = refl
laterE (proj₂ (laterE (proj₂ responsivity))) = responsivity

responsivity₁ : ∀ {i} → EG {i} (map (true ≡_) trafficLight₄)
responsivity₁ = mapEG ⟨ refl ⟩EGᵢ ▻EG

responsivity₁' : ∀ {i} → EG {i} (map (true ≡_) trafficLight₄)
responsivity₁' = mapEG ⟨ refl ▻EGᵢ refl ⟩EGᵢ ▻EG

responsivity₂ : ∀ {i} → EG {i} (⟨ vmap (true ≡_) (returnReader true ▻ ask ⟩) ▻⋯)
proj₁ responsivity₂ = false
nowE (proj₂ responsivity₂) = refl
proj₁ (laterE (proj₂ responsivity₂)) = true
nowE (proj₂ (laterE (proj₂ responsivity₂))) = refl
laterE (proj₂ (laterE (proj₂ responsivity₂))) = responsivity₂

responsoSmall : EN (⟨ vmap (true ≡_) (returnReader true ▻ ask ⟩) ▻⋯)
proj₁ responsoSmall = true
proj₁ (proj₂ responsoSmall) = true
proj₂ (proj₂ responsoSmall) = refl

responso : AG (ENₛ (⟨ vmap (true ≡_) (returnReader true ▻ ask ⟩) ▻⋯))
nowA (responso p) with fmap EN'ₛ (inF ⟨ FCons (fmap (vmap' (λ section → true ≡ section)) (fmap (λ x → x , ask ⟩) (returnReader true))) ▻⋯)
nowA (responso p) | proj₃ , proj₄ with EN' (_aux_ ((true ≡ true) , FCons (tt , (λ x → (true ≡ x) , FNil))) (FCons (tt , (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))))))
...   | bla = {!   !}
nowA (laterA (responso p) p₁) = {!   !}
laterA (laterA (responso p) p₁) p₂ = {!   !}

{-
head
      (EN'ₛ
       (((true ≡ true) , FCons (tt , (λ x → (true ≡ x) , FNil))) aux
        FCons
        (tt ,
         (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))))))
EN'
 (((true ≡ true) , FCons (tt , (λ x → (true ≡ x) , FNil))) aux
  FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil)))))
EPred head (inF (tail
 (((true ≡ true) , FCons (tt , (λ x → (true ≡ x) , FNil))) aux
  FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil)))))))
EPred head (inF
 (( FCons (tt , (λ x → (true ≡ x) , FNil))) pre⟨
  FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))) ▻⋯ )))
EPred head (fmap (_aux
  (FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))) ▻⋯ ))) (tt , (λ x → (true ≡ x) , FNil)) )
EPred head (tt , (λ x → (true ≡ x) , FNil) aux
  FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))) ▻⋯ ) )
∃ p → head ((λ x → (true ≡ x) , FNil) aux
  FCons
  (tt ,
   (λ x → (true ≡ true) , FCons (tt , (λ x₁ → (true ≡ x₁) , FNil))) ▻⋯ ) )
-}

tautology₄ : EG ⟨ returnReader ⊤ ⟩ ▻⋯
tautology₄ = ⟨ ConsEG (23 , tt , []EG) ▻EG

tautology₅ : EG ⟨ returnReader ⊤ ⟩ ▻⋯
tautology₅ = ⟨ (23 , tt) ⟩EG ▻EG

tautology₆ : EG ⟨ returnReader ⊤ ▻ returnReader ⊤ ⟩ ▻⋯
tautology₆ = ⟨ (23 , tt) ▻EG (42 , tt) ⟩EG ▻EG

-- In lots of cases, Agda can infer the input that will validate the proof
easy : EG ⟨ (true ≡_) <$> ask ▻ returnReader ⊤ ⟩ ▻⋯
easy = ⟨ refl ▻EGᵢ tt ⟩EGᵢ ▻EG

timesTwo : ∀ {i} → FStream {i} (ReaderC ℕ) ℕ
timesTwo = map (_* 2) ⟨ ask ⟩ ▻⋯

even : ℕ → Set
even n = ∃ λ m → n ≡ m * 2

alwaysEven : ∀ {i} → AG {i} (map even timesTwo)
nowA (alwaysEven p) = p , refl
laterA (alwaysEven p) = alwaysEven

alwaysEven₁ : ∀ {i} → AG {i} (map even timesTwo)
-- alwaysEven₁ = mapAG ([]AG pre⟨ {!   !} ▻AG) -- TODO Report internal error on refining
alwaysEven₁ = mapAG ⟨ (λ p → p) ⟩AG ▻AG

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.S2.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

data S² : Type₀ where
  base : S²
  surf : PathP (λ i → base ≡ base) refl refl

S²ToSetRec : ∀ {ℓ} {A : S² → Type ℓ}
           → ((x : S²) → isSet (A x))
           → A base
           → (x : S²) → A x
S²ToSetRec set b base = b
S²ToSetRec set b (surf i j) =
  isOfHLevel→isOfHLevelDep 2 set b b {a0 = refl} {a1 = refl} refl refl surf i j

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.
   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-2 as ECP-LBFT-OBM-Diff-2
import      LibraBFT.Impl.Storage.DiemDB.LedgerStore.LedgerStore    as LedgerStore
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Storage.DiemDB.DiemDB where

------------------------------------------------------------------------------
getEpochEndingLedgerInfosImpl
  : DiemDB → Epoch → Epoch → Epoch {-Usize-}
  → Either ErrLog (List LedgerInfoWithSignatures × Bool)
getLatestLedgerInfo
  : DiemDB
  → Either ErrLog LedgerInfoWithSignatures
------------------------------------------------------------------------------

mAX_NUM_EPOCH_ENDING_LEDGER_INFO : Epoch -- Usize
mAX_NUM_EPOCH_ENDING_LEDGER_INFO = 100

------------------------------------------------------------------------------
-- impl DiemDB

-- Returns ledger infos for epoch changes starting with the given epoch.
-- If there are less than `MAX_NUM_EPOCH_ENDING_LEDGER_INFO` results, it returns all of them.
-- Otherwise the first `MAX_NUM_EPOCH_ENDING_LEDGER_INFO` results are returned
-- and a flag is set to True to indicate there are more.
getEpochEndingLedgerInfos
  : DiemDB → Epoch → Epoch
  → Either ErrLog (List LedgerInfoWithSignatures × Bool)
getEpochEndingLedgerInfos self startEpoch endEpoch =
  getEpochEndingLedgerInfosImpl self startEpoch endEpoch mAX_NUM_EPOCH_ENDING_LEDGER_INFO

-- TODO-2: provide EitherD variants before writing proofs about this function;
-- TODO-2: then use `whenD` in place of the two `if`s below
getEpochEndingLedgerInfosImpl self startEpoch endEpoch limit = do
  if (not ⌊ (startEpoch ≤? endEpoch) ⌋)
    then
    (Left fakeErr {-here ["bad epoch range", lsE startEpoch, lsE endEpoch]-})
    else pure unit
  -- the latest epoch can be the same as the current epoch (in most cases), or
  -- current_epoch + 1 (when the latest ledger_info carries next validator set)
  latestEpoch ← getLatestLedgerInfo self >>= pure ∘ (_^∙  liwsLedgerInfo ∙ liNextBlockEpoch)
  if (not ⌊ (endEpoch ≤? latestEpoch) ⌋)
    then
    (Left fakeErr) -- [ "unable to provide epoch change ledger info for still open epoch"
                   -- , "asked upper bound", lsE endEpoch
                   -- , "last sealed epoch", lsE (latestEpoch - 1) ])))
                   -- -1 is OK because genesis LedgerInfo has .next_block_epoch() == 1
    else pure unit

  let (pagingEpoch , more) =
        ECP-LBFT-OBM-Diff-2.e_DiemDB_getEpochEndingLedgerInfosImpl_limit startEpoch endEpoch limit
  lis0    ← LedgerStore.getEpochEndingLedgerInfoIter (self ^∙ ddbLedgerStore) startEpoch pagingEpoch
  let lis = LedgerStore.obmEELIICollect lis0
  if -- genericLength lis /= (pagingEpoch^.eEpoch) - (startEpoch^.eEpoch)
    length lis + (startEpoch {-^∙ eEpoch-}) /= (pagingEpoch {-^∙ eEpoch-}) -- rewritten to avoid monus
    then Left fakeErr -- [ "DB corruption: missing epoch ending ledger info"
                      -- , lsE startEpoch, lsE endEpoch, lsE pagingEpoch ]
    else pure (lis , more)
{-
 where
  here t = "DiemDB":"getEpochEndingLedgerInfosImpl":t
-}

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

-- impl DbReader for DiemDB

getLatestLedgerInfo self =
  maybeS (self ^∙ ddbLedgerStore ∙ lsLatestLedgerInfo)
         (Left fakeErr {-["DiemDB.Lib", "getLatestLedgerInfo", "Nothing"]-})
         pure

getEpochEndingLedgerInfo : DiemDB → Version → Either ErrLog LedgerInfoWithSignatures
getEpochEndingLedgerInfo = LedgerStore.getEpochEndingLedgerInfo ∘ _ddbLedgerStore

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

-- impl DbWriter for DiemDB

-- LBFT-OBM-DIFF : entire impl
module saveTransactions (self  : DiemDB)
                        {- → [TransactionToCommit] → Version-}
                        (mliws : Maybe LedgerInfoWithSignatures) where
  VariantFor : ∀ {ℓ} EL → EL-func {ℓ} EL
  VariantFor EL = EL ErrLog DiemDB

  step₁ : LedgerInfoWithSignatures → VariantFor EitherD

  step₀ : VariantFor EitherD
  step₀ = maybeSD mliws (LeftD fakeErr) step₁

  step₁ liws = do
         -- TODO-2: Make an EitherD variant of putLedgerInfo and make D version default
    ls ← fromEither $ LedgerStore.putLedgerInfo (self ^∙ ddbLedgerStore) liws
    RightD (self & ddbLedgerStore ∙~ (ls & lsLatestLedgerInfo ?~ liws))

  E : VariantFor Either
  E = toEither step₀

  D : VariantFor EitherD
  D = fromEither E

saveTransactions = saveTransactions.D


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

module Cubical.Data.FinSet.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Empty renaming (rec to EmptyRec)
open import Cubical.Data.Sigma

open import Cubical.Data.Fin
open import Cubical.Data.SumFin renaming (Fin to SumFin) hiding (discreteFin)
open import Cubical.Data.FinSet.Base

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.Relation.Nullary.HLevels

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    B : Type ℓ'

-- infix operator to more conveniently compose equivalences

_⋆_ = compEquiv

infixr 30 _⋆_

-- useful implications

EquivPresIsFinSet : A ≃ B → isFinSet A → isFinSet B
EquivPresIsFinSet e = rec isPropIsFinSet (λ (n , p) → ∣ n , compEquiv (invEquiv e) p ∣)

isFinSetFin : {n : ℕ} → isFinSet (Fin n)
isFinSetFin = ∣ _ , pathToEquiv refl ∣

isFinSetUnit : isFinSet Unit
isFinSetUnit = ∣ 1 , Unit≃Fin1 ∣

isFinSet→Discrete : isFinSet A → Discrete A
isFinSet→Discrete = rec isPropDiscrete (λ (_ , p) → EquivPresDiscrete (invEquiv p) discreteFin)

isContr→isFinSet : isContr A → isFinSet A
isContr→isFinSet h = ∣ 1 , isContr→≃Unit* h ⋆ invEquiv (Unit≃Unit* ) ⋆ Unit≃Fin1 ∣

isDecProp→isFinSet : isProp A → Dec A → isFinSet A
isDecProp→isFinSet h (yes p) = isContr→isFinSet (inhProp→isContr p h)
isDecProp→isFinSet h (no ¬p) = ∣ 0 , uninhabEquiv ¬p ¬Fin0 ∣

{-

Alternative definition of finite sets

A set is finite if it is merely equivalent to `Fin n` for some `n`. We
can translate this to code in two ways: a truncated sigma of a nat and
an equivalence, or a sigma of a nat and a truncated equivalence. We
prove that both formulations are equivalent.

-}

isFinSet' : Type ℓ → Type ℓ
isFinSet' A = Σ[ n ∈ ℕ ] ∥ A ≃ Fin n ∥

FinSet' : (ℓ : Level) → Type (ℓ-suc ℓ)
FinSet' ℓ = TypeWithStr _ isFinSet'

isPropIsFinSet' : isProp (isFinSet' A)
isPropIsFinSet' {A = A} (n , equivn) (m , equivm) =
  Σ≡Prop (λ _ → isPropPropTrunc) n≡m
  where
    Fin-n≃Fin-m : ∥ Fin n ≃ Fin m ∥
    Fin-n≃Fin-m = rec
      isPropPropTrunc
      (rec
        (isPropΠ λ _ → isPropPropTrunc)
        (λ hm hn → ∣ Fin n ≃⟨ invEquiv hn ⟩ A ≃⟨ hm ⟩ Fin m ■ ∣)
        equivm
      )
      equivn

    Fin-n≡Fin-m : ∥ Fin n ≡ Fin m ∥
    Fin-n≡Fin-m = rec isPropPropTrunc (∣_∣ ∘ ua) Fin-n≃Fin-m

    ∥n≡m∥ : ∥ n ≡ m ∥
    ∥n≡m∥ = rec isPropPropTrunc (∣_∣ ∘ Fin-inj n m) Fin-n≡Fin-m

    n≡m : n ≡ m
    n≡m = rec (isSetℕ n m) (λ p → p) ∥n≡m∥

-- logical equivalence of two definitions

isFinSet→isFinSet' : isFinSet A → isFinSet' A
isFinSet→isFinSet' ∣ n , equiv ∣ = n , ∣ equiv ∣
isFinSet→isFinSet' (squash p q i) = isPropIsFinSet' (isFinSet→isFinSet' p) (isFinSet→isFinSet' q) i

isFinSet'→isFinSet : isFinSet' A → isFinSet A
isFinSet'→isFinSet (n , ∣ isFinSet-A ∣) = ∣ n , isFinSet-A ∣
isFinSet'→isFinSet (n , squash p q i) = isPropIsFinSet (isFinSet'→isFinSet (n , p)) (isFinSet'→isFinSet (n , q)) i

isFinSet≡isFinSet' : isFinSet A ≡ isFinSet' A
isFinSet≡isFinSet' {A = A} = hPropExt isPropIsFinSet isPropIsFinSet' isFinSet→isFinSet' isFinSet'→isFinSet

FinSet→FinSet' : FinSet ℓ → FinSet' ℓ
FinSet→FinSet' (A , isFinSetA) = A , isFinSet→isFinSet' isFinSetA

FinSet'→FinSet : FinSet' ℓ → FinSet ℓ
FinSet'→FinSet (A , isFinSet'A) = A , isFinSet'→isFinSet isFinSet'A

FinSet≃FinSet' : FinSet ℓ ≃ FinSet' ℓ
FinSet≃FinSet' =
  isoToEquiv
    (iso FinSet→FinSet' FinSet'→FinSet
        (λ _ → Σ≡Prop (λ _ → isPropIsFinSet') refl)
        (λ _ → Σ≡Prop (λ _ → isPropIsFinSet) refl))

FinSet≡FinSet' : FinSet ℓ ≡ FinSet' ℓ
FinSet≡FinSet' = ua FinSet≃FinSet'

-- cardinality of finite sets

card : FinSet ℓ → ℕ
card = fst ∘ snd ∘ FinSet→FinSet'

-- definitions to reduce problems about FinSet to SumFin

≃Fin : Type ℓ → Type ℓ
≃Fin A = Σ[ n ∈ ℕ ] A ≃ Fin n

≃SumFin : Type ℓ → Type ℓ
≃SumFin A = Σ[ n ∈ ℕ ] A ≃ SumFin n

≃Fin→SumFin : ≃Fin A → ≃SumFin A
≃Fin→SumFin (n , e) = n , compEquiv e (invEquiv (SumFin≃Fin _))

≃SumFin→Fin : ≃SumFin A → ≃Fin A
≃SumFin→Fin (n , e) = n , compEquiv e (SumFin≃Fin _)

transpFamily :
    {A : Type ℓ}{B : A → Type ℓ'}
  → ((n , e) : ≃SumFin A) → (x : A) → B x ≃ B (invEq e (e .fst x))
transpFamily {B = B} (n , e) x = pathToEquiv (λ i → B (retEq e x (~ i)))

max_stars_repo_name: FernandoLarrain/cubical


text:
open import Data.Boolean
open import Type

module Data.List.Sorting.SelectionSort {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

import      Lvl
open import Data.List
open import Data.List.Functions as List using (_++_)
import      Data.List.Functions.Multi as List
open import Data.List.Sorting.Functions(_≤?_)
open import Data.Option
open import Data.Tuple
import      Numeral.Finite.Conversions as 𝕟
open import Functional using (_∘_)

{-# TERMINATING #-}
selectionSort : List(T) → List(T)
selectionSort l with extractMinimal l
... | Some(x , xs) = x ⊰ selectionSort(xs)
... | None         = l

module Proofs where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Induct where

open import Data.Nat
open import Data.Sum
open import Relation.Binary.PropositionalEquality

{- The downward closure of a set. -}
data downset : (ℕ → Set) → ℕ → Set where
  downset-lit : {φ : ℕ → Set} → {x : ℕ} → φ x → downset φ x
  downset-pred : {φ : ℕ → Set} → {x : ℕ} → downset φ (suc x) → downset φ x

{- Example 1: The downset of a downset is itself. Simple induction. -}
downset-downset : ∀ {φ} → ∀ {x} → downset (downset φ) x → downset φ x
downset-downset (downset-lit p) = p
downset-downset (downset-pred p) = downset-pred (downset-downset p)

{- Example 2: Downsets are downward closed. Needs lemmata. -}
lemma-larger : ∀ x y → x ≤ y → (suc x ≤ y) ⊎ (x ≡ y)
lemma-larger 0 0 z≤n = inj₂ refl
lemma-larger 0 (suc y) z≤n = inj₁ (s≤s z≤n)
lemma-larger (suc x) (suc y) (s≤s x-leq-y) with lemma-larger x y x-leq-y
lemma-larger (suc x) (suc y) (s≤s x-leq-y) | inj₁ sx-leq-y = inj₁ (s≤s sx-leq-y)
lemma-larger (suc x) (suc y) (s≤s x-leq-y) | inj₂ x-eq-y = inj₂ (cong suc x-eq-y)

downset-zero : ∀ {φ} → ∀ y → downset φ y → downset φ zero
downset-zero zero d-phi-y = d-phi-y
downset-zero (suc y) d-phi-y = downset-zero y (downset-pred d-phi-y)

downset-downward-closed : ∀ {φ} → ∀ x y → downset φ y → x ≤ y → downset φ x
downset-downward-closed 0 y d-phi-y x-leq-y = downset-zero y d-phi-y
downset-downward-closed
  (suc x) (suc y) d-phi-y (s≤s x-leq-y) with lemma-larger x y x-leq-y
... | inj₁ sx-leq-y = downset-downward-closed (suc x) y (downset-pred d-phi-y) sx-leq-y
... | inj₂ refl = d-phi-y

max_stars_repo_name: zaklogician/induct-agda-isabelle

max_issues_repo_name: zaklogician/induct-agda-isabelle

max_forks_repo_name: zaklogician/induct-agda-isabelle


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Data.Nat

module Cubical.Data.W.Indexed where

open _≅_

private
  variable
    ℓX ℓS ℓP : Level

module Types {X : Type ℓX} (S : X → Type ℓS) (P : ∀ x → S x → Type ℓP) (inX : ∀ x (s : S x) → P x s → X) where
  data IW (x : X) : Type (ℓ-max ℓX (ℓ-max ℓS ℓP)) where
    node : (s : S x) → (subtree : (p : P x s) → IW (inX x s p)) → IW x

  Subtree : ∀ {x} → (s : S x) → Type (ℓ-max (ℓ-max ℓX ℓS) ℓP)
  Subtree {x} s = (p : P x s) → IW (inX x s p)

  RepIW : (x : X) → Type (ℓ-max (ℓ-max ℓX ℓS) ℓP)
  RepIW x = Σ[ s ∈ S x ] Subtree s

open Types public

module _ {X : Type ℓX} {S : X → Type ℓS} {P : ∀ x → S x → Type ℓP} {inX : ∀ x (s : S x) → P x s → X} where

  getShape : ∀ {x} → IW S P inX x → S x
  getShape (node s subtree) = s

  getSubtree : ∀ {x} → (w : IW S P inX x) → (p : P x (getShape w)) → IW S P inX (inX x (getShape w) p)
  getSubtree (node s subtree) = subtree

  wExt : ∀ {x} (w w' : IW S P inX x)
    → (ps : getShape w ≡ getShape w')
    → (pw : PathP (λ i → Subtree S P inX (ps i)) (getSubtree w) (getSubtree w'))
    → w ≡ w'
  wExt (node s subtree) (node s' subtree') ps psubtree = cong₂ node ps psubtree

  isoRepIW : (x : X) → IW S P inX x ≅ RepIW S P inX x
  fun (isoRepIW x) (node s subtree) = s , subtree
  inv (isoRepIW x) (s , subtree) = node s subtree
  rightInv (isoRepIW x) (s , subtree) = refl
  leftInv (isoRepIW x) (node s subtree) = refl

  equivRepIW : (x : X) → IW S P inX x ≃ RepIW S P inX x
  equivRepIW x = isoToEquiv (isoRepIW x)

  pathRepIW : (x : X) → IW S P inX x ≡ RepIW S P inX x
  pathRepIW x = ua (equivRepIW x)

  isPropIW : (∀ x → isProp (S x)) → ∀ x → isProp (IW S P inX x)
  isPropIW isPropS x (node s subtree) (node s' subtree') =
    cong₂ node (isPropS x s s') (toPathP (funExt λ p → isPropIW isPropS _ _ (subtree' p)))

module IWPathTypes {X : Type ℓX} (S : X → Type ℓS) (P : ∀ x → S x → Type ℓP) (inX : ∀ x (s : S x) → P x s → X) where

  --somewhat inspired by https://github.com/jashug/IWTypes , but different.

  IndexCover : Type (ℓ-max (ℓ-max ℓX ℓS) ℓP)
  IndexCover = Σ[ x ∈ X ] IW S P inX x × IW S P inX x

  ShapeCover : IndexCover → Type ℓS
  ShapeCover (x , w , w') = getShape w ≡ getShape w'

  ArityCover : ∀ xww' → ShapeCover xww' → Type ℓP
  ArityCover (x , w , w') ps = P x (getShape w')

  inXCover : ∀ xww' → (ps : ShapeCover xww') → ArityCover xww' ps → IndexCover
  inXCover (x , w , w') ps p = (inX x (getShape w') p) , (subst (Subtree S P inX) ps (getSubtree w) p , getSubtree w' p)

  Cover : ∀ {x : X} → (w w' : IW S P inX x) → Type (ℓ-max (ℓ-max ℓX ℓS) ℓP)
  Cover {x} w w' = IW ShapeCover ArityCover inXCover (x , w , w')

module IWPath {X : Type ℓX} {S : X → Type ℓS} {P : ∀ x → S x → Type ℓP} {inX : ∀ x (s : S x) → P x s → X} where
  open IWPathTypes S P inX

  isoEncode : ∀ {x} (w w' : IW S P inX x) → (w ≡ w') ≅ Cover w w'
  isoEncodeSubtree : ∀ {x} (w w' : IW S P inX x) (ps : ShapeCover (x , w , w'))
    → (PathP (λ i → Subtree S P inX (ps i)) (getSubtree w) (getSubtree w'))
       ≅
       (∀ (p : P x (getShape w')) → IW ShapeCover ArityCover inXCover (inXCover (x , w , w') ps p))

  isoEncodeSubtree w w'@(node s' subtree') ps =
    PathPIsoPath (λ i → Subtree S P inX (ps i)) (getSubtree w) (getSubtree w') ⟫
    invIso (funExtIso) ⟫
    codomainIsoDep (λ p → isoEncode _ (subtree' p))
    where _⟫_ = compIso
          infixr 10 _⟫_
  fun (isoEncode w@(node s subtree) w'@(node s' subtree')) pw =
    node (cong getShape pw) (fun (isoEncodeSubtree w w' (cong getShape pw)) (cong getSubtree pw))
  inv (isoEncode w@(node s subtree) w'@(node s' subtree')) cw@(node ps csubtree) =
    cong₂ node ps (inv (isoEncodeSubtree w w' ps) csubtree)
  rightInv (isoEncode w@(node s subtree) w'@(node s' subtree')) cw@(node ps csubtree) =
    cong (node ps) (
      fun (isoEncodeSubtree w w' ps) (inv (isoEncodeSubtree w w' ps) csubtree)
        ≡⟨ rightInv (isoEncodeSubtree w w' ps) csubtree ⟩
      csubtree ∎
    )
  leftInv (isoEncode w@(node s subtree) w'@(node s' subtree')) pw =
    cong₂ node (cong getShape pw)
      (inv (isoEncodeSubtree w w' (cong getShape pw))
        (fun (isoEncodeSubtree w w' (cong getShape pw))
          (cong getSubtree pw)
        )
      )
      ≡⟨ cong (cong₂ node (cong getShape pw)) (leftInv (isoEncodeSubtree w w' (cong getShape pw)) (cong getSubtree pw)) ⟩
    cong₂ node (cong getShape pw) (cong getSubtree pw)
      ≡⟨ flipSquare (λ i → wExt (node (getShape (pw i)) (getSubtree (pw i))) (pw i) refl refl) ⟩
    pw ∎

  encode : ∀ {x} (w w' : IW S P inX x) → w ≡ w' → Cover w w'
  encode w w' = fun (isoEncode w w')

  decode : ∀ {x} (w w' : IW S P inX x) → Cover w w' → w ≡ w'
  decode w w' = inv (isoEncode w w')

  decodeEncode : ∀ {x} (w w' : IW S P inX x) → (pw : w ≡ w') → decode w w' (encode w w' pw) ≡ pw
  decodeEncode w w' = leftInv (isoEncode w w')

  encodeDecode : ∀ {x} (w w' : IW S P inX x) → (cw : Cover w w') → encode w w' (decode w w' cw) ≡ cw
  encodeDecode w w' = rightInv (isoEncode w w')

  equivEncode : ∀ {x} (w w' : IW S P inX x) → (w ≡ w') ≃ Cover w w'
  equivEncode w w' = isoToEquiv (isoEncode w w')

  pathEncode : ∀ {x} (w w' : IW S P inX x) → (w ≡ w') ≡ Cover w w'
  pathEncode w w' = ua (equivEncode w w')

open IWPathTypes
open IWPath

isOfHLevelSuc-IW : {X : Type ℓX} {S : X → Type ℓS} {P : ∀ x → S x → Type ℓP} {inX : ∀ x (s : S x) → P x s → X} →
  (n : HLevel) → (∀ x → isOfHLevel (suc n) (S x)) → ∀ x → isOfHLevel (suc n) (IW S P inX x)
isOfHLevelSuc-IW zero isHS x = isPropIW isHS x
isOfHLevelSuc-IW (suc n) isHS x w w' =
  subst (isOfHLevel (suc n)) (λ i → pathEncode w w' (~ i))
    (isOfHLevelSuc-IW n
      (λ (y , v , v') → isHS y (getShape v) (getShape v'))
      (x , w , w')
    )

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)

open import Setoids.Setoids
open import Setoids.Subset
open import Setoids.Functions.Definition
open import LogicalFormulae
open import Functions
open import Lists.Lists
open import Setoids.Orders
open import Rings.Orders.Partial.Definition
open import Rings.Definition

module LectureNotes.MetAndTop.Chapter2 {a b c : _} {R : Set a} {S : Setoid {a} {b} R} {_<_ : Rel {a} {c} R} {_+_ _*_ : R → R → R} {ring : Ring S _+_ _*_} {ps : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing ring ps) where

open Setoid S renaming (_∼_ to _∼R_)
open Ring ring

record Metric {d1 e : _} {A : Set d1} {T : Setoid {d1} {e} A} (d : A → A → R) : Set (a ⊔ b ⊔ c ⊔ d1 ⊔ e) where
  open Setoid T
  field
    dWellDefined : (x y v w : A) → x ∼ y → v ∼ w → (d x v) ∼R (d w y)
    dZero : (x y : A) → (d x y) ∼R 0R → x ∼ y
    dZero' : (x y : A) → x ∼ y → (d x y) ∼R 0R
    dSymmetric : (x y : A) → (d x y) ∼R (d y x)
    dTriangle : (x y z : A) → ((d x z) < ((d x y) + (d y z))) || ((d x z) ∼R ((d x y) + (d y z)))
  dNonnegative : (x y : A) → (0R < d x y) || (0R ∼R (d x y))
  dNonnegative x y = {!!}