text:
module CombinatoryLogic.Syntax where

open import Data.String using (String; _++_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 1
infixl 6 _∙_

data Combinator : Set where
  -- Kapitel 1, Abschnitt C, §3 (Die formalen Grundbegriffe)
  B C W K Q Π P ∧ : Combinator
  -- Kapitel 1, Abschnitt C, §2, c (Anwendung)
  _∙_ : (X Y : Combinator) → Combinator

-- NOTE: for the (intensional) equality defined by Kapitel 1, Abschnitt C, §4
-- (Symbolische Festsetzungen), Festsetzung 2, we use the propositional equality
-- _≡_.

toString : Combinator → String
toString (X ∙ Y@(_ ∙ _)) = toString X ++ "(" ++ toString Y ++ ")"
toString (X ∙ Y) = toString X ++ toString Y
toString B = "B"
toString C = "C"
toString W = "W"
toString K = "K"
toString Q = "Q"
toString Π = "Π"
toString P = "P"
toString ∧ = "∧"

_ : toString (K ∙ Q ∙ (W ∙ C)) ≡ "KQ(WC)"
_ = refl

_ : toString (K ∙ ∧ ∙ (Q ∙ Π) ∙ (W ∙ C)) ≡ "K∧(QΠ)(WC)"
_ = refl

_ : toString (K ∙ ∧ ∙ ((Q ∙ Π) ∙ (W ∙ C))) ≡ "K∧(QΠ(WC))"
_ = refl

_ : toString (K ∙ K ∙ K) ≡ "KKK"
_ = refl

infix 5 _==_

-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 2
_==_ : (X Y : Combinator) → Combinator
X == Y = Q ∙ X ∙ Y

-- Kapitel 1, Abschnitt C, §4 (Symbolische Festsetzungen), Def. 3
I : Combinator
I = W ∙ K

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
open import Sec4

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

-- Now ≥ relation
_≥_ : ∀ (m : ℕ) → ∀ (n : ℕ) → Prop
Z ≥ Z = ⊤
S m ≥ Z = ⊤
Z ≥ S n = ⊥
S m ≥ S n = m ≥ n

-- Example proof
-- eqqr : ((S (S (S Z))) ≥ (S (S Z))) → ((S (S Z)) ≥ (S (S (S Z))))
-- eqqr ()

-- -- Now is ≥ equivalence relation?
-- relfexivity
reflexivity : ∀ (m : ℕ) → (m ≥ m)
reflexivity  Z = ⋆
reflexivity  (S m) = reflexivity m

-- -- -- Now symmetry
-- sym : ∀ (m : ℕ) → ∀ (n : ℕ) → m ≥ n → n ≥ m
-- sym Z Z p = ⋆
-- sym Z (S n) p = ⋆
-- sym (S m) Z ⋆ = {!!}
-- sym (S m) (S n) p = sym m n p

-- -- -- Now transitivity
trans'' : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → m ≥ n → n ≥ p → m ≥ p
trans'' Z Z p p0 p1 = p1
trans'' Z (S n) p () p1
trans'' (S m) n Z p0 p1 = ⋆
trans'' (S m) Z (S p) p0 ()
trans'' (S m) (S n) (S p) p0 p1 = trans'' m n p p0 p1

-- Given the above three are satisfied, we know that it is an
-- equivalence relation!

-- Now let us try strictly greater than (>)

-- Definition of >
_>_ : ∀ (m : ℕ) → ∀ (n : ℕ) → Prop
Z > Z =  ⊥
Z > S n = ⊥
S m > Z = ⊤
S m > S n = m > n

-- Now let us see of > is an equivalence relation

-- reflixvity of > not possible!
-- refl-> : ∀ (m : ℕ) → m > m
-- refl-> Z = {!!}
-- refl-> (S m) = refl-> m

-- equality
_==_ : ∀ (m : ℕ) → ∀ (n : ℕ) → Prop
Z == Z =  ⊤
Z == S n = ⊥
S m == Z = ⊥
S m == S n = m == n

-- Is equiality an equivalence relation?

-- reflexivity
refl-≡ : ∀ (m : ℕ) → m == m
refl-≡ Z = ⋆
refl-≡ (S m) = refl-≡ m

-- Symmetry
sym-≡ : ∀ (m : ℕ) → ∀ (n : ℕ) → m == n → n == m
sym-≡ Z Z h = ⋆
sym-≡ Z (S n) ()
sym-≡ (S m) Z ()
sym-≡ (S m) (S n) h = sym-≡ m n h

-- Transitivity
trans-≡ : ∀ (m n p : ℕ) → m == n → n == p → m == p
trans-≡ Z n Z h0 h1 = ⋆
trans-≡ Z Z (S p) h0 h1 = h1
trans-≡ Z (S n) (S p) () h1
trans-≡ (S m) Z Z () h1
trans-≡ (S m) (S n) Z h0 ()
trans-≡ (S m) Z (S p) () h1
trans-≡ (S m) (S n) (S p) h0 h1 = trans-≡ m n p h0 h1

-- Homework ≤ on natural numbers

-- Addition of natural numbers
_+_ : ∀ (m n : ℕ) → ℕ
Z + n = n
S m + n = S (m + n)

-- Use equality, 2 + 3 == 3 + 2
eqq : ((S (S Z)) + (S ( S ( S Z)))) == ((S ( S ( S Z))) + (S (S Z)))
eqq = ⋆

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

eqq2 : ((S (S Z)) + (S ( S ( S Z)))) ≡ ((S ( S ( S Z))) + (S (S Z)))
eqq2 = refl

cong : ∀ (n m : ℕ) → n ≡ m → S n ≡ S m
cong n .n refl = refl

-lemma-+ : ∀ (n : ℕ) → n ≡ (n + Z)
-lemma-+ Z = refl
-lemma-+ (S n) with -lemma-+ n
-lemma-+ (S n) | h = cong n (n + Z) h

lem2 : ∀ (m n : ℕ) → (m + S n) ≡ S (m + n)
lem2 Z n = refl
lem2 (S m) n = cong (m + S n) (S (m + n)) (lem2 m n)

-- Now prove commutativity of addition
commute-+ : ∀ (m n : ℕ) → (m + n) ≡ (n + m)
commute-+ Z n = -lemma-+ n
commute-+ (S m) n with (n + S m) | (lem2 n m)
commute-+ (S m) n | .(S (n + m)) | refl = cong (m + n) (n + m) (commute-+ m n)

_<_ : ∀ (m n : ℕ) → Prop
Z < Z = ⊥
Z < S n = ⊥
S m < Z = ⊤
S m < S n = m < n

-- refl-< : ∀ (m : ℕ) → m < m
-- refl-< Z = !!
-- refl-< (S m) = !!

-- Define booleans
data 𝔹 : Set where
 True : 𝔹
 False : 𝔹

-- Define &&
_&&_ : ∀ (A B : 𝔹) → 𝔹
True && True = True
True && False = False
False && B = False

-- Define ||
_||_ : ∀ (A B : 𝔹) → 𝔹
True || B = True
False || True = True
False || False = False

-- Prove equivalence of two hardware functions g and f
g : ∀ (A B C : 𝔹) → 𝔹
g A B C = B && (A || C)

ff : ∀ (A B C : 𝔹) → 𝔹
ff A B C = (A && B) || ((B && C) && (B || C))

-- Equality of booleans
_==̰_ : ∀ (A B : 𝔹) → Prop
True ==̰ True = ⊤
True ==̰ False = ⊥
False ==̰ True = ⊥
False ==̰ False = ⊤

-- Now prove that for any input A B C, g ≡ ff
g≃ff : ∀ (A B C : 𝔹) → (g A B C) ==̰ (ff A B C)
g≃ff True True True = ⋆
g≃ff True True False = ⋆
g≃ff True False C = ⋆
g≃ff False True True = ⋆
g≃ff False True False = ⋆
g≃ff False False C = ⋆

_≤_ : ∀ (m n : ℕ) → Prop
Z ≤ n = ⊤
S m ≤ Z = ⊥
S m ≤ S n = m ≤ n

-- Symmetry on ≤
-- sym-≤ : ∀ (m n : ℕ) → (m ≤ n) → (n ≤ m)
-- sym-≤ Z Z ⋆ = ⋆
-- sym-≤ Z (S n) ⋆ = {!!}
-- sym-≤ (S m) Z ()
-- sym-≤ (S m) (S n) p = sym-≤ m n p

-- ≠
_≠_ : ∀ (m n : ℕ) → Prop
Z ≠ Z = ⊥
Z ≠ S n = ⊤
S m ≠ Z = ⊤
S m ≠ S n = m ≠ n

-- -- Is ≠ an equivalence relation?
-- ≠-refl
-- ≠-relf : ∀ (m : ℕ) → (m ≠ m)
-- ≠-relf Z = {!!}
-- ≠-relf (S m) = ≠-relf m

-- -- Symmetry
≠-sym : ∀ (m n : ℕ) → (m ≠ n) → (n ≠ m)
≠-sym Z Z ()
≠-sym Z (S n) p = ⋆
≠-sym (S m) Z p = ⋆
≠-sym (S m) (S n) p = ≠-sym m n p

-- -- Transitivity
-- ≠-trans : ∀ (m n p : ℕ) → (m ≠ n) → (n ≠ p) → (m ≠ p)
-- ≠-trans Z Z Z h0 ()
-- ≠-trans Z (S n) Z ⋆ ⋆ = {!!}
-- ≠-trans Z n (S p) h0 h1 = ⋆
-- ≠-trans (S m) n Z h0 h1 = ⋆
-- ≠-trans (S m) Z (S p) ⋆ ⋆ = {!!}
-- ≠-trans (S m) (S n) (S p) h0 h1 = ≠-trans m n p h0 h1

de1 : {A B : Prop} → ((¬ A) ∨ (¬ B)) ⇒ ¬ (A ∧ B)
de1 = impl (λ x → neg (impl (λ x₁ →
                               let y = elim1-∧ x₁
                                   z = elim2-∧ x₁
                               in
                               elim-∨ x (λ x₃ → elim-neg y x₃) (λ x₂ → elim-neg z x₂))))

de2 : {A B : Prop} → ((¬ A) ∧ (¬ B)) ⇒ (¬ (A ∨ B))
de2 = impl (λ x → neg (impl (λ x₁ → elim-∨ x₁ (λ x₂ → elim-neg x₂ (elim1-∧ x))
                                             (λ x₂ → elim-neg x₂ (elim2-∧ x)))))

-- Multiplication of naturals
_*_ : ∀ (m n : ℕ) → ℕ
Z * n = Z
S m * n = n + (m * n)

-- Square relation on two naturals
_r²_ : ∀ (m n : ℕ) → Prop
m r² n = (m * m) ≡ (n * n)

-- reflexivity of r²
refl-r² : ∀ (m : ℕ) → (m r² m)
refl-r² Z = refl
refl-r² (S m) = refl

sym-r² : ∀ (m n : ℕ) → (m r² n) → (n r² m)
sym-r² Z Z p = refl
sym-r² Z (S n) ()
sym-r² (S m) Z ()
sym-r² (S m) (S n) p rewrite p = refl

trans-r² : ∀ (m n p : ℕ) → (m r² n) → (n r² p) → (m r² p)
trans-r² Z n Z h0 h1 = refl
trans-r² Z Z (S p) refl ()
trans-r² Z (S n) (S p) () h1
trans-r² (S m) Z Z () h1
trans-r² (S m) (S n) Z h0 ()
trans-r² (S m) Z (S p) () h1
trans-r² (S m) (S n) (S p) h0 h1 rewrite h0
                                        | h1 = refl

ext: agda


text:
module Schedule where

open import Data.Bool
open import Data.Fin
open import Data.Empty
open import Data.List
open import Data.List.All
open import Data.Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Function using (_$_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session

-- outcomes of step
data Event : Set where
  Terminated Forked Restarted Halted New Closed NotClosed WaitSkipped : Event
  SendSkipped Received NotReceived : Event
  Stuck : Event
  Selected NotSelected : Event
  NSelected NotNSelected BranchSkipped NBranchSkipped : Event

data NextPool : Set where
  _,_ : ∀ {G} → Event → ThreadPool G → NextPool

module Alternative where
  step : ∀ {Gtop G1 G2} → SSplit Gtop G1 G2 → ThreadPool G1 → ThreadPool G2 → NextPool
  step ss-top (tnil ina) tp2@(tnil _) = Terminated , tp2

  step ss-top (tnil ina) tp2 = Stuck , tp2

  step ss-top (tcons ss (Fork{G₁ = G₁}{G₂ = G₂} ss₁ κ₁ κ₂) tp) tp2
    with ssplit-compose ss ss₁
  ... | Gi , ss₁₃ , ss₂₄ with ssplit-refl-right G₁ | ssplit-refl-right G₂
  ... | Gunit , ss-G1GunitG1 | G2unit , ss-G2GuG2 =
    Forked , (tappend ss-top ((tcons ss₁₃ (apply-cont ss-G1GunitG1 κ₁ (VUnit (ssplit-inactive-right ss-G1GunitG1)))
                             (tcons ss₂₄ (Ready ss-G2GuG2 (VUnit (ssplit-inactive-right ss-G2GuG2)) κ₂) tp))) tp2)

  step ss-top (tcons ss (Ready ss₁ v κ) tp) tp2 =
    Restarted , (tappend ss-top (tsnoc ss tp (apply-cont ss₁ κ v)) tp2)

  step ss-top (tcons ss (Halt inaG x₁ x₂) tp) tp2
    rewrite inactive-left-ssplit ss inaG = Halted , (tappend ss-top tp tp2)

  step ss-top (tcons{G₁} ss (New s κ) tp) tp2
    with ssplit-refl-right G₁
  ... | Gi , ss-GiG1
    with ssplit-inactive-right ss-GiG1
  ... | ina-Gi = New , (tappend (ss-left ss-top) ((tcons (ss-left ss)
           (Ready (ss-left ss-GiG1) (VPair (ss-posneg (inactive-ssplit-trivial ina-Gi)) (VChan POS (here-pos ina-Gi (subF-refl _))) (VChan NEG (here-neg ina-Gi (subF-refl _)))) (lift-cont κ))
           (lift-threadpool tp))) (lift-threadpool tp2))

  step ss-top (tcons{G₁}{G₂} ss cmd@(Close ss-vκ v κ) tp) tp2
    with ssplit-compose ss-top ss
  ... | Gi , ss-top1 , ss-top2
    with ssplit-refl-left-inactive Gi
  ... | G' , ina-G' , ss-GG'
    with matchWaitAndGo ss-top1 (ss-vκ , v , κ) ss-GG' (tappend ss-top2 tp tp2) (tnil ina-G')
  ... | just (Gnext , tpnext) = Closed , tpnext
  ... | nothing
    with ssplit-compose5 ss-top ss
  ... | Gi' , ss-top1' , ss-top2' = step ss-top1' tp (tsnoc ss-top2' tp2 cmd)

  step ss-top (tcons ss cmd@(Wait ss₁ v κ) tp) tp2
    with ssplit-compose5 ss-top ss
  ... | Gi , ss-top1 , ss-top2 =
    step ss-top1 tp (tsnoc ss-top2 tp2 cmd)

  step ss-top (tcons ss cmd@(Send ss₁ ss-args vch v κ) tp) tp2
    with ssplit-compose5 ss-top ss
  ... | Gi , ss-top1 , ss-top2 =
    step ss-top1 tp (tsnoc ss-top2 tp2 cmd)

  step ss-top (tcons{G₁}{G₂} ss cmd@(Recv ss-vκ vch κ) tp) tp2
    with ssplit-compose ss-top ss
  ... | Gi , ss-top1 , ss-top2
    with ssplit-refl-left-inactive Gi
  ... | G' , ina-G' , ss-GG'
    with matchSendAndGo ss-top1 (ss-vκ , vch , κ) ss-GG' (tappend ss-top2 tp tp2) (tnil ina-G')
  ... | just (G-next , tp-next) =
    Received , tp-next
  ... | nothing
    with ssplit-compose5 ss-top ss
  ... | Gi' , ss-top1' , ss-top2' =
    step ss-top1' tp (tsnoc ss-top2' tp2 cmd)

  step ss-top (tcons{G₁}{G₂} ss cmd@(Select ss-vκ lab vch κ) tp) tp2
    with ssplit-compose ss-top ss
  ... | Gi , ss-top1 , ss-top2
    with ssplit-refl-left-inactive Gi
  ... | G' , ina-G' , ss-GG'
    with matchBranchAndGo ss-top1 (ss-vκ , lab , vch , κ) ss-GG' (tappend ss-top2 tp tp2) (tnil ina-G')
  ... | just (G-next , tp-next) =
    Selected , tp-next
  ... | nothing
    with ssplit-compose5 ss-top ss
  ... | Gi' , ss-top1' , ss-top2' =
    step ss-top1' tp (tsnoc ss-top2' tp2 cmd)

  step ss-top (tcons ss cmd@(Branch ss₁ vch dcont) tp) tp2
    with ssplit-compose5 ss-top ss
  ... | Gi , ss-top1 , ss-top2 =
    step ss-top1 tp (tsnoc ss-top2 tp2 cmd)

  step ss-top (tcons{G₁}{G₂} ss cmd@(NSelect ss-vκ lab vch κ) tp) tp2
    with ssplit-compose ss-top ss
  ... | Gi , ss-top1 , ss-top2
    with ssplit-refl-left-inactive Gi
  ... | G' , ina-G' , ss-GG'
    with matchNBranchAndGo ss-top1 (ss-vκ , lab , vch , κ) ss-GG' (tappend ss-top2 tp tp2) (tnil ina-G')
  ... | just (G-next , tp-next) = NSelected , tp-next
  ... | nothing
    with ssplit-compose5 ss-top ss
  ... | Gi' , ss-top1' , ss-top2' =
    step ss-top1' tp (tsnoc ss-top2' tp2 cmd)

  step ss-top (tcons ss cmd@(NBranch ss₁ vch dcont) tp) tp2
    with ssplit-compose5 ss-top ss
  ... | Gi , ss-top1 , ss-top2 =
    step ss-top1 tp (tsnoc ss-top2 tp2 cmd)

module Original where
  step : ∀ {G} → ThreadPool G → NextPool
  step (tnil ina) =
    Terminated , tnil ina
  step (tcons ss (Fork{G₁ = G₁}{G₂ = G₂} ss₁ κ₁ κ₂) tp) with ssplit-compose ss ss₁
  ... | Gi , ss₁₃ , ss₂₄ with ssplit-refl-right G₁ | ssplit-refl-right G₂
  ... | Gunit , ss-G1GunitG1 | G2unit , ss-G2GuG2 =
    Forked , (tcons ss₁₃ (apply-cont ss-G1GunitG1 κ₁ (VUnit (ssplit-inactive-right ss-G1GunitG1)))
                    (tcons ss₂₄ (apply-cont ss-G2GuG2 κ₂ (VUnit (ssplit-inactive-right ss-G2GuG2))) tp))
  step (tcons ss (Ready ss₁ v κ) tp) =
    Restarted , (tsnoc ss tp (apply-cont ss₁ κ v))
  step (tcons ss (Halt inaG x₁ x₂) tp) rewrite inactive-left-ssplit ss inaG =
    Halted , tp
  step (tcons{G₁} ss (New s κ) tp) with ssplit-refl-right G₁
  ... | Gi , ss-GiG1 with ssplit-inactive-right ss-GiG1
  ... | ina-Gi =
    New , (tcons (ss-left ss)
             (apply-cont (ss-left ss-GiG1) (lift-cont κ) (VPair (ss-posneg (inactive-ssplit-trivial ina-Gi)) (VChan POS (here-pos ina-Gi (subF-refl _))) (VChan NEG (here-neg ina-Gi (subF-refl _)))))
             (lift-threadpool tp))
  step (tcons{G₁}{G₂} ss cmd@(Close ss-vκ v κ) tp) with ssplit-refl-left-inactive G₂
  ... | G' , ina-G' , ss-GG' with matchWaitAndGo ss (ss-vκ , v , κ) ss-GG' tp (tnil ina-G')
  ... | just (Gnext , tpnext) = Closed , tpnext
  ... | nothing = NotClosed , (tsnoc ss tp cmd)
  step (tcons ss cmd@(Wait ss₁ v κ) tp) =
    WaitSkipped , (tsnoc ss tp cmd)
  step (tcons ss cmd@(Send ss₁ ss-args vch v κ) tp) =
    SendSkipped , (tsnoc ss tp cmd)
  step (tcons{G₁}{G₂} ss cmd@(Recv ss-vκ vch κ) tp) with ssplit-refl-left-inactive G₂
  ... | G' , ina-G' , ss-GG' with matchSendAndGo ss (ss-vκ , vch , κ) ss-GG' tp (tnil ina-G')
  ... | just (G-next , tp-next) = Received , tp-next
  ... | nothing = NotReceived , (tsnoc ss tp cmd)
  step (tcons{G₁}{G₂} ss cmd@(Select ss-vκ lab vch κ) tp) with ssplit-refl-left-inactive G₂
  ... | G' , ina-G' , ss-GG' with matchBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp (tnil ina-G')
  ... | just (G-next , tp-next) = Selected , tp-next
  ... | nothing = NotSelected , (tsnoc ss tp cmd)
  step (tcons ss cmd@(Branch ss-vκ vch dcont) tp) =
    BranchSkipped , (tsnoc ss tp cmd)
  step (tcons{G₁}{G₂} ss cmd@(NSelect ss-vκ lab vch κ) tp) with ssplit-refl-left-inactive G₂
  ... | G' , ina-G' , ss-GG' with matchNBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp (tnil ina-G')
  ... | just (G-next , tp-next) = NSelected , tp-next
  ... | nothing = NotNSelected , (tsnoc ss tp cmd)
  step (tcons ss cmd@(NBranch ss-vκ vch dcont) tp) =
    NBranchSkipped , (tsnoc ss tp cmd)

open Alternative

single-step : (∃ λ G → ThreadPool G) → Event × (∃ λ G → ThreadPool G)
single-step (G , tp)
  with ssplit-refl-left-inactive G
... | G' , ina-G' , ss-GG'
  with step ss-GG' tp (tnil ina-G')
... | ev , tp' = ev , ( _ , tp')

-- stuff to run ...
data Gas : Set where
  Empty : Gas
  More  : Gas → Gas

-- outcomes of scheduling
data Outcome : Set where
  Terminated : Outcome
  _,_ : Event → Outcome → Outcome
  OutOfGas : ∀ {G} → ThreadPool G → Outcome

-- thread scheduling
schedule : {G : SCtx} → Gas → ThreadPool G → Outcome
schedule Empty tp = OutOfGas tp
schedule{G} (More gas) tp
  with single-step (_ , tp)
... | Terminated , _ , tp' = Terminated
... | ev , _ , tp' = ev , (schedule gas tp')

-- start main thread
start : Gas → Expr [] TUnit → Outcome
start f e =
  schedule f (tcons ss-[] (run [] ss-[] e (vnil []-inactive) (halt []-inactive UUnit)) (tnil []-inactive))

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


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

module Dodo.Unary.Empty where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Data.Product using (∃-syntax)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)

-- # Definitions

Empty₁ : ∀ {a ℓ : Level} {A : Set a} → Pred A ℓ → Set (a ⊔ ℓ)
Empty₁ {A = A} P = ∀ (x : A) → ¬ P x

NonEmpty₁ : ∀ {a ℓ : Level} {A : Set a} → Pred A ℓ → Set (a ⊔ ℓ)
NonEmpty₁ P = ∃[ x ] P x

¬₁_ : ∀ {a ℓ : Level} {A : Set a} → Pred A ℓ → Pred A ℓ
¬₁_ P x = ¬ P x

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.BiInvInt.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat hiding (_+_; +-comm)
open import Cubical.Data.Int
open import Cubical.Data.Bool

open import Cubical.HITs.Ints.BiInvInt.Base

-- addition

_+ᴮ_ : BiInvInt → BiInvInt → BiInvInt
m +ᴮ zero          = m
m +ᴮ suc n         = suc (m +ᴮ n)
m +ᴮ predr n       = predr (m +ᴮ n)
m +ᴮ predl n       = predl (m +ᴮ n)
m +ᴮ suc-predr n i = suc-predr (m +ᴮ n) i
m +ᴮ predl-suc n i = predl-suc (m +ᴮ n) i

-- properties of addition

+ᴮ-assoc : ∀ l m n → (l +ᴮ m) +ᴮ n ≡ l +ᴮ (m +ᴮ n)
+ᴮ-assoc l m zero i            = l +ᴮ m
+ᴮ-assoc l m (suc n) i         = suc (+ᴮ-assoc l m n i)
+ᴮ-assoc l m (predr n) i       = predr (+ᴮ-assoc l m n i)
+ᴮ-assoc l m (predl n) i       = predl (+ᴮ-assoc l m n i)
+ᴮ-assoc l m (suc-predr n i) j = suc-predr (+ᴮ-assoc l m n j) i
+ᴮ-assoc l m (predl-suc n i) j = predl-suc (+ᴮ-assoc l m n j) i

+ᴮ-unitʳ : ∀ n → n +ᴮ zero ≡ n
+ᴮ-unitʳ n i = n

+ᴮ-unitˡ : ∀ n → zero +ᴮ n ≡ n
+ᴮ-unitˡ zero i            = zero
+ᴮ-unitˡ (suc n) i         = suc (+ᴮ-unitˡ n i)
+ᴮ-unitˡ (predr n) i       = predr (+ᴮ-unitˡ n i)
+ᴮ-unitˡ (predl n) i       = predl (+ᴮ-unitˡ n i)
+ᴮ-unitˡ (suc-predr n i) j = suc-predr (+ᴮ-unitˡ n j) i
+ᴮ-unitˡ (predl-suc n i) j = predl-suc (+ᴮ-unitˡ n j) i

-- TODO: a direct proof of commutatitivty
-- (for now, we use Data.Int)

fwd-+≡+ᴮ : ∀ m n → fwd (m + n) ≡ (fwd m) +ᴮ (fwd n)
fwd-+≡+ᴮ m (pos zero)       = refl
fwd-+≡+ᴮ m (pos (suc n))    = fwd-sucInt (m +pos n) ∙ cong suc (fwd-+≡+ᴮ m (pos n))
fwd-+≡+ᴮ m (negsuc zero)    = fwd-predInt m
fwd-+≡+ᴮ m (negsuc (suc n)) = fwd-predInt (m +negsuc n) ∙ cong pred (fwd-+≡+ᴮ m (negsuc n))

+ᴮ≡+ : ∀ m n → m +ᴮ n ≡ fwd ((bwd m) + (bwd n))
+ᴮ≡+ m n = sym (fwd-+≡+ᴮ (bwd m) (bwd n) ∙ (λ i → (fwd-bwd m i) +ᴮ (fwd-bwd n i)))

+ᴮ-comm : ∀ m n → m +ᴮ n ≡ n +ᴮ m
+ᴮ-comm m n = +ᴮ≡+ m n ∙ cong fwd (+-comm (bwd m) (bwd n)) ∙ sym (+ᴮ≡+ n m)

-- some of the lemmas needed for a direct proof +ᴮ-comm are corollaries of +ᴮ-comm

suc-+ᴮ : ∀ m n → (suc m) +ᴮ n ≡ suc (m +ᴮ n)
suc-+ᴮ m n = +ᴮ-comm (suc m) n ∙ (λ i → suc (+ᴮ-comm n m i))
-- suc-+ᴮ m zero i    = suc m
-- suc-+ᴮ m (suc n) i = suc (suc-+ᴮ m n i)
-- suc-+ᴮ m (predr n) = cong predr (suc-+ᴮ m n) ∙ predr-suc (m +ᴮ n) ∙ sym (suc-predr (m +ᴮ n))
-- suc-+ᴮ m (predl n) = cong predl (suc-+ᴮ m n) ∙ predl-suc (m +ᴮ n) ∙ sym (suc-predl (m +ᴮ n))
-- suc-+ᴮ m (suc-predr n i) j = {!!}
-- suc-+ᴮ m (predl-suc n i) j = {!!}

predr-+ᴮ : ∀ m n → (predr m) +ᴮ n ≡ predr (m +ᴮ n)
predr-+ᴮ m n = +ᴮ-comm (predr m) n ∙ (λ i → predr (+ᴮ-comm n m i))

predl-+ᴮ : ∀ m n → (predl m) +ᴮ n ≡ predl (m +ᴮ n)
predl-+ᴮ m n = +ᴮ-comm (predl m) n ∙ (λ i → predl (+ᴮ-comm n m i))

-- +ᴮ-comm : ∀ m n → n +ᴮ m ≡ m +ᴮ n
-- +ᴮ-comm m zero              = +ᴮ-unitˡ m
-- +ᴮ-comm m (suc n)           =   suc-+ᴮ n m ∙ cong suc   (+ᴮ-comm m n)
-- +ᴮ-comm m (predr n)         = predr-+ᴮ n m ∙ cong predr (+ᴮ-comm m n)
-- +ᴮ-comm m (predl n)         = predl-+ᴮ n m ∙ cong predl (+ᴮ-comm m n)
-- +ᴮ-comm m (suc-predr n i) j = {!!}
-- +ᴮ-comm m (predl-suc n i) j = {!!}

-- negation / subtraction

-ᴮ_ : BiInvInt → BiInvInt
-ᴮ zero          = zero
-ᴮ suc n         = predl (-ᴮ n)
-ᴮ predr n       = suc (-ᴮ n)
-ᴮ predl n       = suc (-ᴮ n)
-ᴮ suc-predr n i = predl-suc (-ᴮ n) i
-ᴮ predl-suc n i = suc-predl (-ᴮ n) i

_-ᴮ_ : BiInvInt → BiInvInt → BiInvInt
m -ᴮ n = m +ᴮ (-ᴮ n)

-- TODO: properties of negation

-- +ᴮ-invˡ : ∀ n → (-ᴮ n) +ᴮ n ≡ zero
-- +ᴮ-invˡ zero              = refl
-- +ᴮ-invˡ (suc n)           = (λ i → suc (predl-+ᴮ (-ᴮ n) n i)) ∙ (λ i → suc-pred (+ᴮ-invˡ n i) i)
-- +ᴮ-invˡ (predr n)         = (λ i → predr (suc-+ᴮ (-ᴮ n) n i)) ∙ (λ i → predr-suc (+ᴮ-invˡ n i) i)
-- +ᴮ-invˡ (predl n)         = (λ i → predl (suc-+ᴮ (-ᴮ n) n i)) ∙ (λ i → predl-suc (+ᴮ-invˡ n i) i)
-- +ᴮ-invˡ (suc-predr n i) j = {!!}
-- +ᴮ-invˡ (predl-suc n i) j = {!!}

-- +ᴮ-invʳ : ∀ n → n +ᴮ (-ᴮ n) ≡ zero
-- +ᴮ-invʳ n = {!!}

-- natural injections from ℕ

posᴮ : ℕ → BiInvInt
posᴮ zero = zero
posᴮ (suc n) = suc (posᴮ n)

negᴮ : ℕ → BiInvInt
negᴮ zero = zero
negᴮ (suc n) = pred (negᴮ n)

-- absolute value and sign
-- (Note that there doesn't appear to be any way around using
--  bwd here! Any direct proof ends up doing the same work...)

absᴮ : BiInvInt → ℕ
absᴮ n = abs (bwd n)

sgnᴮ : BiInvInt → Bool
sgnᴮ n = sgn (bwd n)

-- TODO: a direct definition of multiplication using +ᴮ-invˡ/ʳ
-- (for now we use abs and sgn, as in agda's stdlib)

_*ᴮ_ : BiInvInt → BiInvInt → BiInvInt
m *ᴮ n = caseBool posᴮ negᴮ (sgnᴮ m and sgnᴮ n) (absᴮ m * absᴮ n)
-- m *ᴮ zero = zero
-- m *ᴮ suc n = (m *ᴮ n) +ᴮ m
-- m *ᴮ predr n = (m *ᴮ n) -ᴮ m
-- m *ᴮ predl n = (m *ᴮ n) -ᴮ m
-- m *ᴮ suc-predr n i = ( +ᴮ-assoc (m *ᴮ n) (-ᴮ m) m
--                      ∙ cong ((m *ᴮ n) +ᴮ_) (+ᴮ-invˡ m)
--                      ∙ +ᴮ-unitʳ (m *ᴮ n)) i
-- m *ᴮ predl-suc n i = ( +ᴮ-assoc (m *ᴮ n) m (-ᴮ m)
--                      ∙ cong ((m *ᴮ n) +ᴮ_) (+ᴮ-invʳ m)
--                      ∙ +ᴮ-unitʳ (m *ᴮ n)) i

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
-- Useless abstract
module Issue476b where

abstract
  data A : Set

data A where

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Compiler correctness
------------------------------------------------------------------------

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

module Lambda.Simplified.Partiality-monad.Inductive.Compiler-correctness
  where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints hiding (comp; app)
open import Partiality-monad.Inductive.Monad

open import Lambda.Simplified.Compiler
open import Lambda.Simplified.Partiality-monad.Inductive.Interpreter
open import Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine
open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

private
  module C = Closure Code
  module T = Closure Tm

open Partial
open Trans-⊑

-- Some abbreviations.

evalⁿ : ∀ {n} → Tm n → T.Env n → ℕ → T.Value ⊥
evalⁿ t ρ n = app→ eval n (_ , t , ρ)

_∙ⁿ_ : T.Value → T.Value → ℕ → T.Value ⊥
(v₁ ∙ⁿ v₂) n = function (v₁ ∙ v₂) (app→ eval n)

execⁿ : State → ℕ → Maybe C.Value ⊥
execⁿ s n = app→ (transformer execP) n s

-- Compiler correctness.

mutual

  ⟦⟧-correct :
    ∀ {n} t {ρ : T.Env n} {c s}
      {k : ℕ → T.Value → Maybe C.Value ⊥} {n} →
    (∀ v → execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
           λ n → k n v) →
    execⁿ ⟨ comp t c , s , comp-env ρ ⟩ ≳[ n ]
    λ n → evalⁿ t ρ (suc n) >>= k n
  ⟦⟧-correct (var x) {ρ} {c} {s} {k} hyp =
    execⁿ ⟨ var x ∷ c , s , comp-env ρ ⟩                 ≳⟨ step⇓ ⟩
    execⁿ ⟨ c , val (comp-val (ρ x)) ∷ s , comp-env ρ ⟩  ≳⟨ hyp (ρ x) ⟩
    (λ n → k n (ρ x))                                    ≡⟨ sym now->>= ⟩≳
    (λ n → evalⁿ (var x) ρ (suc n) >>= k n)              ∎≳

  ⟦⟧-correct (ƛ t) {ρ} {c} {s} {k} hyp =
    execⁿ ⟨ clo (comp t (ret ∷ [])) ∷ c , s , comp-env ρ ⟩   ≳⟨ step⇓ ⟩
    execⁿ ⟨ c , val (comp-val (T.ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≳⟨ hyp (T.ƛ t ρ) ⟩
    (λ n → k n (T.ƛ t ρ))                                    ≡⟨ sym now->>= ⟩≳
    (λ n → evalⁿ (ƛ t) ρ (suc n) >>= k n)                    ∎≳

  ⟦⟧-correct (t₁ · t₂) {ρ} {c} {s} {k} {n} hyp =
    execⁿ ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩    ≳⟨ (⟦⟧-correct t₁ {n = n} λ v₁ → ⟦⟧-correct t₂ λ v₂ → ∙-correct v₁ v₂ hyp) ⟩

    (λ n → evalⁿ t₁ ρ (suc n) >>=′ λ v₁ →
           evalⁿ t₂ ρ (suc n) >>=′ λ v₂ →
           (v₁ ∙ⁿ v₂) n >>=
           k n)                                               ≡⟨ cong (evalⁿ t₁ ρ (suc n) >>=′_)
                                                                      (⟨ext⟩ λ _ → associativity (evalⁿ t₂ ρ (suc n)) _ _) ⟩≳
    (λ n → evalⁿ t₁ ρ (suc n) >>=′ λ v₁ →
           (evalⁿ t₂ ρ (suc n) >>=′ λ v₂ → (v₁ ∙ⁿ v₂) n) >>=
           k n)                                               ≡⟨ associativity (evalⁿ t₁ ρ (suc n)) _ _ ⟩≳

    (λ n → evalⁿ (t₁ · t₂) ρ (suc n) >>= k n)                 ∎≳

  ∙-correct :
    ∀ {n} v₁ v₂ {ρ : T.Env n} {c s}
      {k : ℕ → T.Value → Maybe C.Value ⊥} {n} →
    (∀ v → execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
           λ n → k n v) →
    execⁿ ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
          , comp-env ρ
          ⟩ ≳[ n ]
    λ n → (v₁ ∙ⁿ v₂) n >>= k n

  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {zero} hyp =
    execⁿ ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
          , comp-env ρ
          ⟩                                                     ≡⟨ refl ⟩≳

    const never                                                 ≡⟨ sym never->>= ⟩≳

    (λ n → (T.ƛ t₁ ρ₁ ∙ⁿ v₂) n >>= k n)                         ∎≳

  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {suc n} hyp = later (
    execⁿ ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
          , comp-env ρ
          ⟩ ∘ suc                                               ≳⟨⟩

    execⁿ ⟨ comp t₁ (ret ∷ [])
          , ret c (comp-env ρ) ∷ s
          , cons (comp-val v₂) (comp-env ρ₁)
          ⟩                                                     ∀≡⟨ (λ n → cong (λ ρ′ → execⁿ ⟨ comp t₁ (ret ∷ []) , ret c (comp-env ρ) ∷ s , ρ′ ⟩ n)
                                                                                (sym comp-cons)) ⟩≳
    execⁿ ⟨ comp t₁ (ret ∷ [])
          , ret c (comp-env ρ) ∷ s
          , comp-env (cons v₂ ρ₁)
          ⟩                                                     ≳⟨ (⟦⟧-correct t₁ {n = n} λ v →

        execⁿ ⟨ ret ∷ []
              , val (comp-val v) ∷ ret c (comp-env ρ) ∷ s
              , comp-env (cons v₂ ρ₁)
              ⟩                                                       ≳⟨ step⇓ ⟩

        execⁿ ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩               ≳⟨ hyp v ⟩

        (λ n → k n v)                                                 ≳⟨ step⇓ ⟩

        (λ n → k (suc n) v)                                           ∎≳) ⟩

    (λ n → evalⁿ t₁ (cons v₂ ρ₁) (suc n) >>= k (suc n))         ≳⟨⟩

    (λ n → (T.ƛ t₁ ρ₁ ∙ⁿ v₂) (suc n) >>= k (suc n))             ∎≳)

-- Note that the equality that is used here is syntactic.

correct :
  ∀ t →
  exec ⟨ comp t [] , [] , nil ⟩ ≡
  (⟦ t ⟧ nil >>= λ v → return (just (comp-val v)))
correct t =
  exec ⟨ comp t [] , [] , nil ⟩                            ≡⟨ cong (λ ρ → exec ⟨ comp t [] , [] , ρ ⟩) $ sym comp-nil ⟩

  exec ⟨ comp t [] , [] , comp-env nil ⟩                   ≡⟨⟩

  ⨆ ( execⁿ ⟨ comp t [] , [] , comp-env nil ⟩
    , _
    )                                                      ≡⟨ ≳→⨆≡⨆ 1 (⟦⟧-correct t $ λ v →

      execⁿ ⟨ [] , val (comp-val v) ∷ [] , comp-env nil ⟩       ≳⟨ step⇓ ⟩
      const (return (just (comp-val v)))                        ∎≳) ⟩

  ⨆ ( (λ n → evalⁿ t nil n >>= λ v →
             return (just (comp-val v)))
    , _
    )                                                      ≡⟨ sym ⨆->>= ⟩

  (⟦ t ⟧ nil >>= λ v → return (just (comp-val v)))         ∎

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


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

-- In this module, we define F<:⁻, F<:ᵈ (F<: deterministic defined in Pierce92) and
-- show that F<:⁻ subtyping is undecidable.
module FsubMinus where

open import Data.List as List
open import Data.Nat
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Vec as Vec renaming (_∷_ to _‼_ ; [] to nil) hiding (_++_)
open import Function
open import Data.Empty renaming (⊥ to False)

open import Relation.Nullary
open import Relation.Unary using () renaming (Decidable to UDecidable)
open import Relation.Binary using () renaming (Decidable to BDecidable)
open import Relation.Binary.PropositionalEquality as ≡

open import Data.Nat.Properties as ℕₚ
open import Data.Maybe.Properties as Maybeₚ
open import Utils

-- Definition of F<:⁻
--
-- F<:⁻ is defined by removing function types (_⟶_ in the paper) from F<:.
module FsubMinus where
  infix 6 var_
  infixr 6 Π<:_∙_

  -- Types
  --
  -- * ⊤ is a supertype of all types.
  -- * (var n) represents a type variable.
  -- * (Π<: S ∙ U) represent a universal type (∀ X <: S . U).
  data Ftyp : Set where
    ⊤       : Ftyp
    var_    : ℕ → Ftyp
    Π<:_∙_  : Ftyp → Ftyp → Ftyp

  -- typing context
  Env : Set
  Env = List Ftyp

  -- shifting operation of de Bruijn indices
  infixl 7 _↑_
  _↑_ : Ftyp → ℕ → Ftyp
  ⊤ ↑ n           = ⊤
  (var x) ↑ n with n ≤? x
  ... | yes p     = var (suc x)
  ... | no ¬p     = var x
  (Π<: S ∙ U) ↑ n = Π<: S ↑ n ∙ U ↑ suc n

  infix 4 _<:_∈_
  data _<:_∈_ : ℕ → Ftyp → Env → Set where
    hd : ∀ {T Γ} → 0 <: T ↑ 0 ∈ T ∷ Γ
    tl : ∀ {n T T′ Γ} → n <: T ∈ Γ → suc n <: T ↑ 0 ∈ T′ ∷ Γ

  -- subtyping judgment of F<:⁻
  -- The statement of the rules should be self-explanatory.
  infix 4 _⊢F_<:_
  data _⊢F_<:_ : Env → Ftyp → Ftyp → Set where
    ftop   : ∀ {Γ T} →
      Γ ⊢F T <: ⊤
    fvrefl : ∀ {Γ n} →
      Γ ⊢F var n <: var n
    fbinds : ∀ {Γ n T U} →
      n <: T ∈ Γ →
      Γ ⊢F T <: U →
      Γ ⊢F var n <: U
    fall   : ∀ {Γ S₁ S₂ U₁ U₂} →
      Γ ⊢F S₂ <: S₁ →
      Γ ‣ S₂ ! ⊢F U₁ <: U₂ →
      Γ ⊢F Π<: S₁ ∙ U₁ <: Π<: S₂ ∙ U₂

  -- The remaining are some technical setup.
  env-lookup : Env → ℕ → Maybe Ftyp
  env-lookup [] n = nothing
  env-lookup (T ∷ Γ) zero = just $ T ↑ 0
  env-lookup (T ∷ Γ) (suc n) = Maybe.map (_↑ 0) $ env-lookup Γ n

  lookup⇒<:∈ : ∀ {Γ n T} → env-lookup Γ n ≡ just T → n <: T ∈ Γ
  lookup⇒<:∈ {[]} {n} ()
  lookup⇒<:∈ {T ∷ Γ} {zero} refl = hd
  lookup⇒<:∈ {T ∷ Γ} {suc n} eq with env-lookup Γ n | lookup⇒<:∈ {Γ} {n}
  ... | nothing | rec with eq
  ... | ()
  lookup⇒<:∈ {T ∷ Γ} {suc n} refl | just T′ | rec = tl (rec refl)

  <:∈⇒lookup : ∀ {Γ n T} → n <: T ∈ Γ → env-lookup Γ n ≡ just T
  <:∈⇒lookup hd            = refl
  <:∈⇒lookup (tl <:∈)
    rewrite <:∈⇒lookup <:∈ = refl

  env-lookup′ : Env → ℕ → Maybe Ftyp
  env-lookup′ Γ n = Maybe.map (repeat (suc n) (_↑ 0)) (lookupOpt Γ n)

  env-lookup-same : ∀ Γ n → env-lookup Γ n ≡ env-lookup′ Γ n
  env-lookup-same [] n          = refl
  env-lookup-same (T ∷ Γ) zero  = refl
  env-lookup-same (T ∷ Γ) (suc n)
    rewrite env-lookup-same Γ n = sym $ Maybeₚ.map-compose (lookupOpt Γ n)

  <:∈-map : ∀ {a} {A : Set a} {n T} {f : A → Ftyp} {_↑′_ : A → ℕ → A} Γ →
              (∀ a n → f a ↑ n ≡ f (a ↑′ n)) →
              n <: T ∈ List.map f Γ → ∃ λ a → T ≡ f a
  <:∈-map {f = f} Γ comm d = aux _ d refl
    where aux : ∀ {n T Γ*} Γ → n <: T ∈ Γ* → Γ* ≡ List.map f Γ → ∃ λ a → T ≡ f a
          aux [] hd ()
          aux (T ∷ Γ) hd refl = -, comm _ _
          aux [] (tl <:∈) ()
          aux (T ∷ Γ) (tl <:∈) refl with aux Γ <:∈ refl
          ... | a , refl      = -, comm _ _

  <:∈-func : ∀ {x T T′ Γ} → x <: T ∈ Γ → x <: T′ ∈ Γ → T ≡ T′
  <:∈-func hd hd              = refl
  <:∈-func (tl T∈Γ) (tl T′∈Γ) = cong (_↑ 0) (<:∈-func T∈Γ T′∈Γ)

  Ftyp-measure : Ftyp → ℕ
  Ftyp-measure ⊤           = 1
  Ftyp-measure (var x)     = 1
  Ftyp-measure (Π<: S ∙ U) = Ftyp-measure S + Ftyp-measure U

  Ftyp-measure≥1 : ∀ T → Ftyp-measure T ≥ 1
  Ftyp-measure≥1 ⊤           = s≤s z≤n
  Ftyp-measure≥1 (var _)     = s≤s z≤n
  Ftyp-measure≥1 (Π<: S ∙ U) = ≤-trans (Ftyp-measure≥1 S) (≤-stepsʳ _ ≤-refl)

  ↑-idx : ℕ → ℕ → ℕ
  ↑-idx x n with n ≤? x
  ... | yes p = suc x
  ... | no ¬p = x

  ↑-var : ∀ x n → (var x) ↑ n ≡ var (↑-idx x n)
  ↑-var x n with n ≤? x
  ... | yes p = refl
  ... | no ¬p = refl

  Ftyp-measure-↑ : ∀ T m → Ftyp-measure (T ↑ m) ≡ Ftyp-measure T
  Ftyp-measure-↑ ⊤ m                 = refl
  Ftyp-measure-↑ (var x) m
    rewrite ↑-var x m                = refl
  Ftyp-measure-↑ (Π<: S ∙ U) m
    rewrite Ftyp-measure-↑ S m
          | Ftyp-measure-↑ U (suc m) = refl

  F-measure : ∀ {Γ S U} → Γ ⊢F S <: U → ℕ
  F-measure ftop         = 1
  F-measure fvrefl       = 1
  F-measure (fbinds _ D) = 1 + F-measure D
  F-measure (fall D₁ D₂) = 1 + F-measure D₁ + F-measure D₂

  F-deriv = Σ (Env × Ftyp × Ftyp) λ { (Γ , S , U) → Γ ⊢F S <: U }

  env : F-deriv → Env
  env ((Γ , _) , _) = Γ

  typ₁ : F-deriv → Ftyp
  typ₁ ((_ , S , U) , _) = S

  typ₂ : F-deriv → Ftyp
  typ₂ ((_ , S , U) , _) = U

  F-measure-packed : F-deriv → ℕ
  F-measure-packed (_ , D) = F-measure D

  ≡⊤-dec : UDecidable (_≡ ⊤)
  ≡⊤-dec ⊤           = yes refl
  ≡⊤-dec (var _)     = no (λ ())
  ≡⊤-dec (Π<: _ ∙ _) = no (λ ())

  Π<:-injective : ∀ {S U S′ U′} → Π<: S ∙ U ≡ Π<: S′ ∙ U′ → S ≡ S′ × U ≡ U′
  Π<:-injective refl = refl , refl

  Ftyp-≡-dec : BDecidable (_≡_ {A = Ftyp})
  Ftyp-≡-dec ⊤ ⊤                  = yes refl
  Ftyp-≡-dec ⊤ (var _)            = no (λ ())
  Ftyp-≡-dec ⊤ (Π<: _ ∙ _)        = no (λ ())
  Ftyp-≡-dec (var _) ⊤            = no (λ ())
  Ftyp-≡-dec (var x) (var y) with x ≟ y
  ... | yes x≡y                   = yes (cong var_ x≡y)
  ... | no x≢y                    = no (λ { refl → x≢y refl })
  Ftyp-≡-dec (var _) (Π<: _ ∙ _)  = no (λ ())
  Ftyp-≡-dec (Π<: _ ∙ _) ⊤        = no (λ ())
  Ftyp-≡-dec (Π<: _ ∙ _) (var _)  = no (λ ())
  Ftyp-≡-dec (Π<: S ∙ U) (Π<: S′ ∙ U′)
    with Ftyp-≡-dec S S′ | Ftyp-≡-dec U U′
  ... | yes S≡S′ | yes U≡U′       = yes (cong₂ Π<:_∙_ S≡S′ U≡U′)
  ... | yes S≡S′ | no U≢U′        = no λ Π<:≡ → U≢U′ (proj₂ (Π<:-injective Π<:≡))
  ... | no S≢S′  | yes U≡U′       = no (λ Π<:≡ → S≢S′ (proj₁ (Π<:-injective Π<:≡)))
  ... | no S≢S′  | no U≢U′        = no (λ Π<:≡ → S≢S′ (proj₁ (Π<:-injective Π<:≡)))

-- Definition of F<:
--
-- Here we also define full F<:. We do not use it anywhere.
module Full where

  infix 6 var_
  infixr 6 _⇒_ Π<:_∙_

  -- Types
  --
  -- * ⊤ is a supertype of all types.
  -- * (var n) represent a type variable.
  -- * (S ⇒ U) represents a function type (S ⟶ U).
  -- * (Π<: S ∙ U) represents a universal type (∀ X <: S . U).
  data Ftyp : Set where
    ⊤       : Ftyp
    var_    : ℕ → Ftyp
    _⇒_     : Ftyp → Ftyp → Ftyp
    Π<:_∙_  : Ftyp → Ftyp → Ftyp

  Env : Set
  Env = List Ftyp

  infixl 7 _↑_
  _↑_ : Ftyp → ℕ → Ftyp
  ⊤ ↑ n           = ⊤
  (var x) ↑ n with n ≤? x
  ... | yes p     = var (suc x)
  ... | no ¬p     = var x
  (S ⇒ U) ↑ n     = S ↑ n ⇒ U ↑ n
  (Π<: S ∙ U) ↑ n = Π<: S ↑ n ∙ U ↑ suc n

  infix 4 _<:_∈_
  data _<:_∈_ : ℕ → Ftyp → Env → Set where
    hd : ∀ {T Γ} → 0 <: T ↑ 0 ∈ T ∷ Γ
    tl : ∀ {n T T′ Γ} → n <: T ∈ Γ → suc n <: T ↑ 0 ∈ T′ ∷ Γ

  infix 4 _⊢F_<:_

  data _⊢F_<:_ : Env → Ftyp → Ftyp → Set where
    ftop   : ∀ {Γ T} → Γ ⊢F T <: ⊤
    fvrefl : ∀ {Γ n} → Γ ⊢F var n <: var n
    fbinds : ∀ {Γ n T U} →
               n <: T ∈ Γ →
               Γ ⊢F T <: U →
               Γ ⊢F var n <: U
    ffun   : ∀ {Γ S₁ S₂ U₁ U₂} →
               Γ ⊢F S₂ <: S₁ →
               Γ ⊢F U₁ <: U₂ →
               Γ ⊢F S₁ ⇒ U₁ <: S₂ ⇒ U₂
    fall   : ∀ {Γ S₁ S₂ U₁ U₂} →
               Γ ⊢F S₂ <: S₁ →
               S₂ ∷ Γ ⊢F U₁ <: U₂ →
               Γ ⊢F Π<: S₁ ∙ U₁ <: Π<: S₂ ∙ U₂

  env-lookup : Env → ℕ → Maybe Ftyp
  env-lookup [] n = nothing
  env-lookup (T ∷ Γ) zero = just $ T ↑ 0
  env-lookup (T ∷ Γ) (suc n) = Maybe.map (_↑ 0) $ env-lookup Γ n

  lookup⇒<:∈ : ∀ {Γ n T} → env-lookup Γ n ≡ just T → n <: T ∈ Γ
  lookup⇒<:∈ {[]} {n} ()
  lookup⇒<:∈ {T ∷ Γ} {zero} refl = hd
  lookup⇒<:∈ {T ∷ Γ} {suc n} eq with env-lookup Γ n | lookup⇒<:∈ {Γ} {n}
  ... | nothing | rec with eq
  ... | ()
  lookup⇒<:∈ {T ∷ Γ} {suc n} refl | just T′ | rec = tl (rec refl)

  <:∈⇒lookup : ∀ {Γ n T} → n <: T ∈ Γ → env-lookup Γ n ≡ just T
  <:∈⇒lookup hd            = refl
  <:∈⇒lookup (tl <:∈)
    rewrite <:∈⇒lookup <:∈ = refl

  env-lookup′ : Env → ℕ → Maybe Ftyp
  env-lookup′ Γ n = Maybe.map (repeat (suc n) (_↑ 0)) (lookupOpt Γ n)

  env-lookup-same : ∀ Γ n → env-lookup Γ n ≡ env-lookup′ Γ n
  env-lookup-same [] n          = refl
  env-lookup-same (T ∷ Γ) zero  = refl
  env-lookup-same (T ∷ Γ) (suc n)
    rewrite env-lookup-same Γ n = sym $ Maybeₚ.map-compose (lookupOpt Γ n)

open FsubMinus

-- Undecidability of F<:
--
-- Here we show a reduction proof from F<:⁻ to F<:. Assuming F<:⁻ subtyping being
-- undecidable (which is about to be shown below), we formalize that F<: subtyping is
-- undecidable.
module FsubUndec where

  -- the interpretation function of types from F<:⁻ to F<:
  infixl 5 _*
  _* : Ftyp → Full.Ftyp
  ⊤ *           = Full.⊤
  var x *       = Full.var x
  Π<: T₁ ∙ T₂ * = Full.Π<: T₁ * ∙ (T₂ *)

  *-↑-comm : ∀ (T : Ftyp) n → (T *) Full.↑ n ≡ (T ↑ n) *
  *-↑-comm ⊤ n = refl
  *-↑-comm (var x) n with n ≤? x
  ... | yes p  = refl
  ... | no ¬p  = refl
  *-↑-comm (Π<: S ∙ U) n rewrite *-↑-comm S n | *-↑-comm U (suc n)
               = refl

  repeat*-↑-comm : ∀ T n m → repeat n (Full._↑ m) (T *) ≡ (repeat n (_↑ m) T) *
  repeat*-↑-comm T zero m        = refl
  repeat*-↑-comm T (suc n) m
    rewrite repeat*-↑-comm T n m = *-↑-comm (repeat n (_↑ m) T) m

  *-injective : ∀ {S U} → S * ≡ U * → S ≡ U
  *-injective {⊤} {⊤} refl            = refl
  *-injective {⊤} {var x} ()
  *-injective {⊤} {Π<: _ ∙ _} ()
  *-injective {var x} {⊤} ()
  *-injective {var x} {var .x} refl   = refl
  *-injective {var _} {Π<: _ ∙ _} ()
  *-injective {Π<: S ∙ S₁} {⊤} ()
  *-injective {Π<: _ ∙ _} {var x} ()
  *-injective {Π<: S ∙ S₁} {Π<: U ∙ U₁} eq
    with S * | U * | *-injective {S} {U} | S₁ * | U₁ * | *-injective {S₁} {U₁}
  ... | S* | U* | r | S₁* | U₁* | r₁ with eq
  ... | refl rewrite r refl | r₁ refl = refl

  Full<:∈⇒<:∈ : ∀ {Γ n T} → n Full.<: T * ∈ List.map _* Γ → n <: T ∈ Γ
  Full<:∈⇒<:∈ {Γ} {n} <:∈
    with Full.<:∈⇒lookup <:∈
  ...  | eq rewrite Full.env-lookup-same (List.map _* Γ) n
    with lookupOpt (List.map _* Γ) n | lookupOpt-map-inv {f = _*} Γ {n}
  ...  | just T  | inv
       with inv refl
  ...     | T′ , refl , lk
          with just-injective eq
  ...        | eq′
    rewrite repeat*-↑-comm T′ n 0 | *-↑-comm (repeat n (_↑ 0) T′) 0
    with *-injective eq′
  ...  | refl = lookup⇒<:∈ (trans (env-lookup-same Γ n) aux)
    where aux : env-lookup′ Γ n ≡ just (repeat n (_↑ 0) T′ ↑ 0)
          aux rewrite lk = refl
  Full<:∈⇒<:∈ {Γ} {n} <:∈ | () | nothing | _

  <:∈⇒Full<:∈ : ∀ {Γ n T} → n <: T ∈ Γ → n Full.<: T * ∈ List.map _* Γ
  <:∈⇒Full<:∈ (hd {T})
    rewrite sym $ *-↑-comm T 0 = Full.hd
  <:∈⇒Full<:∈ (tl {T = T} <:∈)
    rewrite sym $ *-↑-comm T 0 = Full.tl (<:∈⇒Full<:∈ <:∈)

  full⇒minus-gen : ∀ {Γ* S* U*} → Γ* Full.⊢F S* <: U* →
               ∀ {Γ S U} → Γ* ≡ List.map _* Γ → S* ≡ (S *) → U* ≡ (U *) →
                 Γ ⊢F S <: U
  full⇒minus-gen Full.ftop {Γ} {S} {⊤} eqΓ eqS refl             = ftop
  full⇒minus-gen Full.ftop {Γ} {S} {var x} eqΓ eqS ()
  full⇒minus-gen Full.ftop {Γ} {S} {Π<: U ∙ U₁} eqΓ eqS ()
  full⇒minus-gen Full.fvrefl {Γ} {⊤} {⊤} eqΓ () eqU
  full⇒minus-gen Full.fvrefl {Γ} {var x} {⊤} eqΓ refl ()
  full⇒minus-gen Full.fvrefl {Γ} {Π<: S ∙ S₁} {⊤} eqΓ () eqU
  full⇒minus-gen Full.fvrefl {Γ} {⊤} {var x} eqΓ () eqU
  full⇒minus-gen Full.fvrefl {Γ} {var x} {var .x} eqΓ refl refl = fvrefl
  full⇒minus-gen Full.fvrefl {Γ} {Π<: S ∙ S₁} {var x} eqΓ () eqU
  full⇒minus-gen Full.fvrefl {Γ} {⊤} {Π<: U ∙ U₁} eqΓ () eqU
  full⇒minus-gen Full.fvrefl {Γ} {var x} {Π<: U ∙ U₁} eqΓ refl ()
  full⇒minus-gen Full.fvrefl {Γ} {Π<: S ∙ S₁} {Π<: U ∙ U₁} eqΓ () eqU
  full⇒minus-gen (Full.fbinds T∈Γ* Dfull) {Γ} {⊤} {U} eqΓ () eqU
  full⇒minus-gen (Full.fbinds {n = n} T∈Γ* Dfull)
             {Γ} {var x} {U} eqΓ refl eqU       = aux
    where T′∈Γ : ∀ {Γ* T} → n Full.<: T ∈ Γ* → Γ* ≡ List.map _* Γ → ∃[ T′ ] (T ≡ T′ *)
          T′∈Γ <:∈ refl with Full.<:∈⇒lookup <:∈
          ... | eq rewrite Full.env-lookup-same (List.map _* Γ) n
            with lookupOpt (List.map _* Γ) n | inspect (lookupOpt (List.map _* Γ)) n
          ... | just T | [ lk ]
            with lookupOpt-map-inv Γ lk | just-injective eq
          ... | T′ , refl , lkeq | eq′
            rewrite repeat*-↑-comm T′ n 0
              | *-↑-comm (repeat n (_↑ 0) T′) 0 = -, sym eq′
          T′∈Γ <:∈ refl | () | nothing | _
          aux : Γ ⊢F var n <: U
          aux with T′∈Γ T∈Γ* eqΓ
          ... | T′ , refl rewrite eqΓ           = fbinds (Full<:∈⇒<:∈ T∈Γ*) (full⇒minus-gen Dfull refl refl eqU)
  full⇒minus-gen (Full.fbinds T∈Γ* Dfull) {Γ} {Π<: S ∙ S₁} {U} eqΓ () eqU
  full⇒minus-gen (Full.ffun _ _) {Γ} {⊤} {U} eqΓ () eqU
  full⇒minus-gen (Full.ffun _ _) {Γ} {var x₂} {U} eqΓ () eqU
  full⇒minus-gen (Full.ffun _ _) {Γ} {Π<: S ∙ S₁} {U} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {⊤} {⊤} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {⊤} {var x} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {⊤} {Π<: U ∙ U₁} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {var x} {⊤} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {var x} {var x₁} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {var x} {Π<: U ∙ U₁} eqΓ () eqU
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {Π<: S ∙ S₁} {⊤} eqΓ refl ()
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {Π<: S ∙ S₁} {var x} eqΓ refl ()
  full⇒minus-gen (Full.fall Dp Dbody) {Γ} {Π<: S₁ ∙ U₁} {Π<: S₂ ∙ U₂}
                 eqΓ refl refl = fall (full⇒minus-gen Dp eqΓ refl refl)
                                      (full⇒minus-gen Dbody (aux eqΓ) refl refl)
    where aux : ∀ {Γ*} → Γ* ≡ List.map _* Γ → (S₂ *) ∷ Γ* ≡ (S₂ *) ∷ List.map _* Γ
          aux refl             = refl

  -- The following two functions accomplish the reduction proof.
  full⇒minus : ∀ {Γ S U} → List.map _* Γ Full.⊢F S * <: U * → Γ ⊢F S <: U
  full⇒minus Dfull = full⇒minus-gen Dfull refl refl refl

  minus⇒full : ∀ {Γ S U} → Γ ⊢F S <: U → List.map _* Γ Full.⊢F S * <: U *
  minus⇒full ftop                    = Full.ftop
  minus⇒full fvrefl                  = Full.fvrefl
  minus⇒full {Γ} (fbinds T∈Γ Dminus) = Full.fbinds (<:∈⇒Full<:∈ T∈Γ) (minus⇒full Dminus)
  minus⇒full (fall Dp Db)            = Full.fall (minus⇒full Dp) (minus⇒full Db)

-- Definition of F<:ᵈ
--
-- Definition of F<:ᵈ F<:ᵈ (F<: deterministic) is an intermediate construction in
-- Pierce92 towards the undecidability proof of F<: subtyping. This intermediate
-- construction is also shown undecidable and we directly use that result here.
module DeterministicFsubSized where

  open import Induction.Nat
  import Relation.Binary.EqReasoning as Eq

  infix 6 var⁻_
  infixr 6 Π⁺<:_∙¬_ Π⁻<:⊤∙¬_

  -- Types
  --
  -- Types in F<:ᵈ are divided into two parts and the two parts are mutually defined.
  -- The two parts are positive types [Ftyp⁺] and negative types [Ftyp⁻] and defined
  -- as follows.
  mutual
  -- Positive types
  -- * ⊤⁺ corresponds to ⊤ in F<:⁻.
  -- * (Π⁺<: Ts ∙¬ U) represents a universal type where all types involved are negative types (∀ X₁ <: T₁ ... ∀ Xₙ <: Tₙ . ∀ X <: U . X).
    data Ftyp⁺ (n : ℕ) : Set where
      ⊤⁺       : Ftyp⁺ n
      Π⁺<:_∙¬_ : Vec (Ftyp⁻ n) n → Ftyp⁻ n → Ftyp⁺ n

  -- Negative types
  -- * (var⁻ n) corresponds to a type variable in F<:⁻.
  -- * (Π⁻<:⊤∙¬_ T) represents a universal type where all parameter types are ⊤ and T is positive (∀ X₁ <: ⊤ ... ∀ Xₙ <: ⊤ . ∀ X <: T . X).
    data Ftyp⁻ (n : ℕ) : Set where
      var⁻_    : ℕ → Ftyp⁻ n
      Π⁻<:⊤∙¬_ : Ftyp⁺ n → Ftyp⁻ n

  -- shifting operation for both positive and negative types
  infixl 7 _↑⁺_ _↑⁺_ ⟦_↑⁻_⟧
  mutual
    _↑⁺_ : ∀ {n} → Ftyp⁺ n → ℕ → Ftyp⁺ n
    ⊤⁺ ↑⁺ n                  = ⊤⁺
    _↑⁺_ {m} (Π⁺<: S ∙¬ U) n = Π⁺<: ⟦ S ↑⁻ n ⟧ ∙¬ (U ↑⁻ (m + n))

    _↑⁻_ : ∀ {n} → Ftyp⁻ n → ℕ → Ftyp⁻ n
    (var⁻ x) ↑⁻ n with n ≤? x
    ... | yes p            = var⁻ (suc x)
    ... | no ¬p            = var⁻ x
    _↑⁻_ {m} (Π⁻<:⊤∙¬ T) n = Π⁻<:⊤∙¬ (T ↑⁺ (m + n))

    ⟦_↑⁻_⟧ : ∀ {n m} → Vec (Ftyp⁻ n) m → ℕ → Vec (Ftyp⁻ n) m
    ⟦ nil ↑⁻ n ⟧   = nil
    ⟦ T ‼ S ↑⁻ n ⟧ = T ↑⁻ n ‼ ⟦ S ↑⁻ suc n ⟧

  -- In F<:ᵈ, typing contexts consist only of negative types.
  NEnv : ℕ → Set
  NEnv n = List (Ftyp⁻ n)

  nenv-lookup : ∀ {n} → NEnv n → ℕ → Maybe (Ftyp⁻ n)
  nenv-lookup Γ n = Maybe.map (repeat (suc n) (_↑⁻ 0)) (lookupOpt Γ n)

  -- subtyping judgment of F<:ᵈ
  --
  -- For a fixed n, a subtyping judgment of F<:ᵈ is a ternary predicate, among a
  -- typing context (consisting of negative types), a negative type and a positive
  -- type.  A subtyping judgment in F<:ᵈ asserts that a negative type is a subtype of
  -- a positive type in the given context. Notice that there is no subtyping relation
  -- between two negative types or two positive types.
  infix 4 [_]_⊢FD_<:_
  data [_]_⊢FD_<:_ (n : ℕ) : NEnv n → Ftyp⁻ n → Ftyp⁺ n → Set where
    fdtop : ∀ {Γ T} → [ n ] Γ ⊢FD T <: ⊤⁺
    fdvar : ∀ {Γ m T S U} →
              nenv-lookup Γ m ≡ just T →
              [ n ] Γ ⊢FD T <: Π⁺<: S ∙¬ U →
              [ n ] Γ ⊢FD var⁻ m <: Π⁺<: S ∙¬ U
    fdall : ∀ {Γ T S U} →
              [ n ] Vec.foldl (λ _ → _) (flip _∷_) Γ S ⊢FD U <: T →
              [ n ] Γ ⊢FD Π⁻<:⊤∙¬ T <: Π⁺<: S ∙¬ U

  infix 5 _*⁺ _*⁻
  infix 6 Π⁻[_]∙_ Π⁺_∙_

  -- the interpretation function of types from F<:ᵈ to F<:⁻
  mutual
    _*⁺ : ∀ {n} → Ftyp⁺ n → Ftyp
    ⊤⁺ *⁺         = ⊤
    Π⁺<: S ∙¬ U *⁺ = Π⁻[ S ]∙ U

    Π⁻[_]∙_ : ∀ {n m} → Vec (Ftyp⁻ n) m → Ftyp⁻ n → Ftyp
    Π⁻[ nil ]∙ U    = Π<: U *⁻ ∙ var zero
    Π⁻[ S ‼ Ss ]∙ U = Π<: S *⁻ ∙ Π⁻[ Ss ]∙ U

    _*⁻ : ∀ {n} → Ftyp⁻ n → Ftyp
    var⁻ n *⁻          = var n
    _*⁻ {n} (Π⁻<:⊤∙¬ T) = Π⁺ n ∙ T

    Π⁺_∙_ : ∀ {n} → ℕ → Ftyp⁺ n → Ftyp
    Π⁺ zero ∙ T  = Π<: T *⁺ ∙ var zero
    Π⁺ suc n ∙ T = Π<: ⊤ ∙ Π⁺ n ∙ T

  module _ where
    open Eq (setoid ℕ)

    mutual
      *-↑-comm⁺ : ∀ {m} (T : Ftyp⁺ m) n → (T *⁺) ↑ n ≡ (T ↑⁺ n) *⁺
      *-↑-comm⁺ ⊤⁺ n            = refl
      *-↑-comm⁺ (Π⁺<: S ∙¬ U) n = Π-↑-comm⁻ S U n

      Π-↑-comm⁻ : ∀ {i j} (S : Vec (Ftyp⁻ i) j) (U : Ftyp⁻ i) n →
                    (Π⁻[ S ]∙ U) ↑ n ≡ Π⁻[ ⟦ S ↑⁻ n ⟧ ]∙ (U ↑⁻ (j + n))
      Π-↑-comm⁻ nil U n
        rewrite *-↑-comm⁻ U n = refl
      Π-↑-comm⁻ {j = suc j} (T ‼ S) U n
        rewrite *-↑-comm⁻ T n
              | Π-↑-comm⁻ S U (suc n)
              | +-suc j n     = refl

      *-↑-comm⁻ : ∀ {m} (T : Ftyp⁻ m) n → (T *⁻) ↑ n ≡ (T ↑⁻ n) *⁻
      *-↑-comm⁻ (var⁻ x) n with n ≤? x
      ... | yes p             = refl
      ... | no ¬p             = refl
      *-↑-comm⁻ (Π⁻<:⊤∙¬ T) n = Π-↑-comm⁺ _ T n

      Π-↑-comm⁺ : ∀ {i} j (T : Ftyp⁺ i) n →
                    (Π⁺ j ∙ T) ↑ n ≡ Π⁺ j ∙ (T ↑⁺ (j + n))
      Π-↑-comm⁺ zero T n
        rewrite *-↑-comm⁺ T n = refl
      Π-↑-comm⁺ (suc j) T n
        rewrite Π-↑-comm⁺ j T (suc n)
              | +-suc j n     = refl

  repeat*-↑-comm⁻ : ∀ {i} (T : Ftyp⁻ i) n m →
                      repeat n (_↑ m) (T *⁻) ≡ (repeat n (_↑⁻ m) T) *⁻
  repeat*-↑-comm⁻ T zero m        = refl
  repeat*-↑-comm⁻ T (suc n) m
    rewrite repeat*-↑-comm⁻ T n m = *-↑-comm⁻ (repeat n (_↑⁻ m) T) m

  mutual
    *-injective⁺ : ∀ {n} {S U : Ftyp⁺ n} → S *⁺ ≡ U *⁺ → S ≡ U
    *-injective⁺ {n} {⊤⁺} {⊤⁺} eq = refl
    *-injective⁺ {.0} {⊤⁺} {Π⁺<: nil ∙¬ _} ()
    *-injective⁺ {.(suc _)} {⊤⁺} {Π⁺<: _ ‼ _ ∙¬ _} ()
    *-injective⁺ {n} {Π⁺<: S ∙¬ U} {⊤⁺} eq = ⊥-elim $ aux eq
      where aux : ∀ {n m} {S : Vec (Ftyp⁻ n) m} {U} → ¬ Π⁻[ S ]∙ U ≡ ⊤
            aux {S = nil} ()
            aux {S = _ ‼ S} ()
    *-injective⁺ {n} {Π⁺<: S₁ ∙¬ U₁} {Π⁺<: S₂ ∙¬ U₂} eq with Π-injective⁻ eq
    ... | refl , refl = refl

    Π-injective⁻ : ∀ {n m} {S₁ S₂ : Vec (Ftyp⁻ n) m} {U₁ U₂ : Ftyp⁻ n} →
                     Π⁻[ S₁ ]∙ U₁ ≡ Π⁻[ S₂ ]∙ U₂ →
                     S₁ ≡ S₂ × U₁ ≡ U₂
    Π-injective⁻ {S₁ = nil} {nil} {U₁} {U₂} eq
      with U₁ *⁻ | U₂ *⁻ | *-injective⁻ {S = U₁} {U₂}
    ...  | U₁* | U₂* | rec with eq
    ...  | refl = refl , rec refl
    Π-injective⁻ {S₁ = S ‼ S₁} {S′ ‼ S₂} {U₁} {U₂} eq
      with S *⁻ | S′ *⁻ | Π⁻[ S₁ ]∙ U₁ | Π⁻[ S₂ ]∙ U₂
         | *-injective⁻ {S = S} {S′}
         | Π-injective⁻ {S₁ = S₁} {S₂} {U₁} {U₂}
    ...  | S* | S′* | Π₁ | Π₂ | recS | rec with eq
    ...  | refl with recS refl | rec refl
    ...  | refl | refl , eqU = refl , eqU

    *-injective⁻ : ∀ {n} {S U : Ftyp⁻ n} → S *⁻ ≡ U *⁻ → S ≡ U
    *-injective⁻ {n} {var⁻ x} {var⁻ .x} refl = refl
    *-injective⁻ {zero} {var⁻ _} {Π⁻<:⊤∙¬ _} ()
    *-injective⁻ {suc n} {var⁻ _} {Π⁻<:⊤∙¬ _} ()
    *-injective⁻ {n} {Π⁻<:⊤∙¬ T} {var⁻ x} eq = ⊥-elim $ aux _ eq
      where aux : ∀ {n x} {T : Ftyp⁺ n} m → ¬ Π⁺ m ∙ T ≡ var x
            aux zero ()
            aux (suc m) ()
    *-injective⁻ {n} {Π⁻<:⊤∙¬ T₁} {Π⁻<:⊤∙¬ T₂} eq with Π-injective⁺ n eq
    ... | refl = refl

    Π-injective⁺ : ∀ {n} {T₁ T₂ : Ftyp⁺ n} m →
                     Π⁺ m ∙ T₁ ≡ Π⁺ m ∙ T₂ →
                     T₁ ≡ T₂
    Π-injective⁺ {T₁ = T₁} {T₂} zero eq
      with T₁ *⁺ | T₂ *⁺ | *-injective⁺ {S = T₁} {T₂}
    ...  | T₁* | T₂* | rec with eq
    ...  | refl = rec refl
    Π-injective⁺ {T₁ = T₁} {T₂} (suc m) eq
      with Π⁺ m ∙ T₁ | Π⁺ m ∙ T₂ | Π-injective⁺ {T₁ = T₁} {T₂} m
    ...  | Π₁ | Π₂ | rec with eq
    ...  | refl = rec refl

  data Pi (P Q : Ftyp → Set) : ℕ → Ftyp → Set where
    pzero : ∀ {U} → Q U → Pi P Q zero (Π<: U ∙ var zero)
    psuc  : ∀ {n S T} → P S → Pi P Q n T -> Pi P Q (suc n) (Π<: S ∙ T)

  -- two predicates that capture the images of the interpretation functions
  mutual
    -- Covar captures the image of the interpretation function from positive types to F<:.
    data Covar (n : ℕ) : Ftyp → Set where
      cvtop : Covar n ⊤
      cvΠ   : ∀ {T} → Pi (Contra n) (Contra n) n T → Covar n T

    -- Contra captures the image of the interpretation function from negative types to F<:.
    data Contra (n : ℕ) : Ftyp → Set where
      cnvar : ∀ m → Contra n (var m)
      cnΠ   : ∀ {T} → Pi (⊤ ≡_) (Covar n) n T → Contra n T

  infix 5 ⟦_⟧⁺ ⟦_⟧⁻

  -- the inverse functions of the interpretation functions
  mutual
    ⟦_⟧⁺ : ∀ {n T} → Covar n T → Ftyp⁺ n
    ⟦ cvtop ⟧⁺ = ⊤⁺
    ⟦ cvΠ P ⟧⁺ = Π⁺<: ∥ P ∥⁺₁ ∙¬ ∥ P ∥⁺₂

    ∥_∥⁺₁ : ∀ {n m T} → Pi (Contra n) (Contra n) m T → Vec (Ftyp⁻ n) m
    ∥ pzero U ∥⁺₁  = nil
    ∥ psuc S P ∥⁺₁ = ⟦ S ⟧⁻ ‼ ∥ P ∥⁺₁

    ∥_∥⁺₂ : ∀ {n m T} → Pi (Contra n) (Contra n) m T → Ftyp⁻ n
    ∥ pzero U ∥⁺₂  = ⟦ U ⟧⁻
    ∥ psuc S P ∥⁺₂ = ∥ P ∥⁺₂

    ⟦_⟧⁻ : ∀ {n T} → Contra n T → Ftyp⁻ n
    ⟦ cnvar m ⟧⁻ = var⁻ m
    ⟦ cnΠ P ⟧⁻   = Π⁻<:⊤∙¬ ∥ P ∥⁻

    ∥_∥⁻ : ∀ {n m T} → Pi (⊤ ≡_) (Covar n) m T → Ftyp⁺ n
    ∥ pzero T ∥⁻  = ⟦ T ⟧⁺
    ∥ psuc S P ∥⁻ = ∥ P ∥⁻

  mutual
    ⟦⟧⁺*⁺⇒id : ∀ {n T} (cT : Covar n T) → (⟦ cT ⟧⁺ *⁺) ≡ T
    ⟦⟧⁺*⁺⇒id cvtop   = refl
    ⟦⟧⁺*⁺⇒id (cvΠ P) = ∥∥⁻Π⇒id P

    ∥∥⁻Π⇒id : ∀ {n m T} (P : Pi (Contra n) (Contra n) m T) →
                Π⁻[ ∥ P ∥⁺₁ ]∙ ∥ P ∥⁺₂ ≡ T
    ∥∥⁻Π⇒id (pzero U)
      rewrite ⟦⟧⁻*⁻⇒id U             = refl
    ∥∥⁻Π⇒id (psuc S P)
      rewrite ⟦⟧⁻*⁻⇒id S | ∥∥⁻Π⇒id P = refl

    ⟦⟧⁻*⁻⇒id : ∀ {n T} (cT : Contra n T) → (⟦ cT ⟧⁻ *⁻) ≡ T
    ⟦⟧⁻*⁻⇒id (cnvar m) = refl
    ⟦⟧⁻*⁻⇒id (cnΠ P)   = ∥∥⁺Π⇒id P

    ∥∥⁺Π⇒id : ∀ {n m T} (P : Pi (⊤ ≡_) (Covar n) m T) → Π⁺ m ∙ ∥ P ∥⁻ ≡ T
    ∥∥⁺Π⇒id (pzero U) rewrite ⟦⟧⁺*⁺⇒id U    = refl
    ∥∥⁺Π⇒id (psuc refl P) rewrite ∥∥⁺Π⇒id P = refl

  infix 5 *⟦_⟧⁺ *⟦_⟧⁻ *∥_,_∥⁺

  mutual

    *⟦_⟧⁺ : ∀ {n} (T : Ftyp⁺ n) → Covar n (T *⁺)
    *⟦ ⊤⁺ ⟧⁺          = cvtop
    *⟦ Π⁺<: S ∙¬ U ⟧⁺ = cvΠ *∥ S , U ∥⁺

    *∥_,_∥⁺ : ∀ {n m} (S : Vec (Ftyp⁻ n) m) (U : Ftyp⁻ n) →
              Pi (Contra n) (Contra n) m (Π⁻[ S ]∙ U)
    *∥ nil , U ∥⁺    = pzero *⟦ U ⟧⁻
    *∥ S ‼ Ss , U ∥⁺ = psuc *⟦ S ⟧⁻ *∥ Ss , U ∥⁺

    *⟦_⟧⁻ : ∀ {n} (T : Ftyp⁻ n) → Contra n (T *⁻)
    *⟦ var⁻ x ⟧⁻    = cnvar x
    *⟦ Π⁻<:⊤∙¬ T ⟧⁻ = cnΠ *∥ _ , T ∥⁻

    *∥_,_∥⁻ : ∀ {n} m (T : Ftyp⁺ n) → Pi (⊤ ≡_) (Covar n) m (Π⁺ m ∙ T)
    *∥ zero , T ∥⁻  = pzero *⟦ T ⟧⁺
    *∥ suc m , T ∥⁻ = psuc refl *∥ m , T ∥⁻

  mutual
    *⁺⟦⟧⁺⇒id : ∀ {n} (T : Ftyp⁺ n) → ⟦ *⟦ T ⟧⁺ ⟧⁺ ≡ T
    *⁺⟦⟧⁺⇒id ⊤⁺                           = refl
    *⁺⟦⟧⁺⇒id (Π⁺<: S ∙¬ U)
      rewrite *∥∥⁺₁⇒id S U | *∥∥⁺₂⇒id S U = refl

    *∥∥⁺₁⇒id : ∀ {n m} (S : Vec (Ftyp⁻ n) m) (U : Ftyp⁻ n) → ∥ *∥ S , U ∥⁺ ∥⁺₁ ≡ S
    *∥∥⁺₁⇒id nil U                       = refl
    *∥∥⁺₁⇒id (S ‼ Ss) U
      rewrite *⁻⟦⟧⁻⇒id S | *∥∥⁺₁⇒id Ss U = refl

    *∥∥⁺₂⇒id : ∀ {n m} (S : Vec (Ftyp⁻ n) m) (U : Ftyp⁻ n) → ∥ *∥ S , U ∥⁺ ∥⁺₂ ≡ U
    *∥∥⁺₂⇒id nil U      = *⁻⟦⟧⁻⇒id U
    *∥∥⁺₂⇒id (S ‼ Ss) U = *∥∥⁺₂⇒id Ss U

    *⁻⟦⟧⁻⇒id : ∀ {n} (T : Ftyp⁻ n) → ⟦ *⟦ T ⟧⁻ ⟧⁻ ≡ T
    *⁻⟦⟧⁻⇒id (var⁻ x)     = refl
    *⁻⟦⟧⁻⇒id {n} (Π⁻<:⊤∙¬ T)
      rewrite *∥∥⁻⇒id n T = refl

    *∥∥⁻⇒id : ∀ {n} m (T : Ftyp⁺ n) → ∥ *∥ m , T ∥⁻ ∥⁻ ≡ T
    *∥∥⁻⇒id zero T    = *⁺⟦⟧⁺⇒id T
    *∥∥⁻⇒id (suc m) T = *∥∥⁻⇒id m T

  open Measure <-wellFounded F-measure-packed renaming (wfRec to F-rec)

  minus⇒deterministic-gen : ∀ (D : F-deriv) →
                            ∀ n {Γ} (S : Contra n (typ₁ D)) (U : Covar n (typ₂ D)) →
                              env D ≡ List.map _*⁻ Γ →
                              [ n ] Γ ⊢FD ⟦ S ⟧⁻ <: ⟦ U ⟧⁺
  minus⇒deterministic-gen D = F-rec (λ D → prop D) pf D
    where prop : F-deriv → Set
          prop D = ∀ n {Γ} (S : Contra n (typ₁ D)) (U : Covar n (typ₂ D)) →
                     env D ≡ List.map _*⁻ Γ →
                     [ n ] Γ ⊢FD ⟦ S ⟧⁻ <: ⟦ U ⟧⁺
          open ≤-Reasoning

          pf : ∀ (D : F-deriv) →
                 (∀ D′ → F-measure-packed D′ < F-measure-packed D → prop D′) → prop D
          pf ((Γ , S* , .⊤) , ftop) rec n S cvtop eq                       = fdtop
          pf ((Γ , S* , .⊤) , ftop) rec n S (cvΠ ()) eq
          pf ((Γ , .(var _) , .(var _)) , fvrefl) rec n S (cvΠ ()) eq
          pf ((Γ , .(var m) , .⊤) , fbinds T∈Γ D) rec n (cnvar m) cvtop eq = fdtop

          pf ((Γ , .(var m) , U*) , fbinds T∈Γ D) rec n {Γ′} (cnvar m) (cvΠ P) refl
            with trans (sym $ env-lookup-same (List.map _*⁻ Γ′) m) $ <:∈⇒lookup T∈Γ
          ... | eq with lookupOpt (List.map _*⁻ Γ′) m | inspect (lookupOpt (List.map _*⁻ Γ′)) m
          pf ((Γ , .(var m) , U*) , fbinds T∈Γ D) rec n {Γ′} (cnvar m) (cvΠ P) refl | refl | just T | [ lk ]
            with lookupOpt-map-inv Γ′ lk
          ...  | T′ , refl , lk′
            rewrite repeat*-↑-comm⁻ T′ m 0
               | *-↑-comm⁻ (repeat m (_↑⁻ 0) T′) 0
            with rec (-, D) ≤-refl n *⟦ repeat m (_↑⁻ 0) T′ ↑⁻ 0 ⟧⁻ (cvΠ P) refl
          ...  | Drec rewrite *⁻⟦⟧⁻⇒id (repeat m (_↑⁻ 0) T′ ↑⁻ 0)
            = fdvar (cong (Maybe.map (repeat (suc m) (_↑⁻ 0))) lk′) Drec
          pf ((Γ , .(var m) , U*) , fbinds T∈Γ D) rec n {Γ′} (cnvar m) (cvΠ P) refl | () | nothing | [ lk ]

          pf ((Γ , .(var _) , U*) , fbinds T∈Γ D) rec n (cnΠ ()) U eq
          pf ((Γ , .(Π<: _ ∙ _) , .(Π<: _ ∙ _)) , Dtop@(fall S₂<:S₁ U₁<:U₂))
             rec n (cnΠ Ps) (cvΠ Pu) refl                                  = fdall (aux _ n (fall S₂<:S₁ U₁<:U₂) Ps Pu ≤-refl)
            where transport : ∀ {Γ T₁ T₂ S*} (S : Contra n S*)
                                (D : S* ∷ Γ ⊢F T₁ <: T₂) →
                                Σ ((⟦ S ⟧⁻ *⁻) ∷ Γ ⊢F T₁ <: T₂) (λ D′ → F-measure D′ ≡ F-measure D)
                  transport {Γ} {T₁} {T₂} S D
                    = subst (λ S → Σ (S ∷ Γ ⊢F T₁ <: T₂) (λ D′ → F-measure D′ ≡ F-measure D))
                            (sym $ ⟦⟧⁻*⁻⇒id S) (D , refl)

                  aux : ∀ {T₁ T₂} Γ m (D : List.map _*⁻ Γ ⊢F T₁ <: T₂)
                          (Ps : Pi (_≡_ ⊤) (Covar n) m T₁)
                          (Pu : Pi (Contra n) (Contra n) m T₂) →
                          F-measure D ≤ F-measure Dtop →
                          [ n ] Vec.foldl (λ _ → _) (flip _∷_) Γ ∥ Pu ∥⁺₁ ⊢FD ∥ Pu ∥⁺₂ <: ∥ Ps ∥⁻
                  aux Γ zero (fall <:₁ <:₂) (pzero S₁) (pzero S₂) ≤
                    = rec (-, <:₁) (≤-trans shrinks ≤) n S₂ S₁ refl
                    where shrinks : (F-measure <:₁) < suc (F-measure <:₁ + F-measure <:₂)
                          shrinks = begin-strict
                            F-measure <:₁                       ≤⟨ ≤-stepsʳ (F-measure <:₂) ≤-refl ⟩
                            F-measure <:₁ + F-measure <:₂       <⟨ ≤-refl ⟩
                            suc (F-measure <:₁ + F-measure <:₂) ∎
                  aux Γ (suc m) (fall <:₁ <:₂) (psuc refl Ps) (psuc S₂ Pu) ≤
                    with transport S₂ <:₂
                  ... | <:₂′ , eq = aux (⟦ S₂ ⟧⁻ ∷ Γ) m <:₂′ Ps Pu $
                    begin
                      F-measure <:₂′                            ≡⟨ eq ⟩
                      F-measure <:₂                             ≤⟨ ≤-stepsˡ (F-measure <:₁) ≤-refl ⟩
                      F-measure <:₁ + F-measure <:₂             <⟨ ≤ ⟩
                      suc (F-measure S₂<:S₁ + F-measure U₁<:U₂) ∎

  -- The following two functions conclude the reduction proof from F<:ᵈ to F<:⁻.
  minus⇒deterministic : ∀ n {Γ : NEnv n} {S U} → List.map _*⁻ Γ ⊢F S *⁻ <: U *⁺ → [ n ] Γ ⊢FD S <: U
  minus⇒deterministic n {Γ} {S} {U} D with minus⇒deterministic-gen (-, D) n *⟦ S ⟧⁻ *⟦ U ⟧⁺ refl
  ... | D′ rewrite *⁻⟦⟧⁻⇒id S | *⁺⟦⟧⁺⇒id U = D′

  deterministic⇒minus : ∀ n {Γ : NEnv n} {S U} → [ n ] Γ ⊢FD S <: U → List.map _*⁻ Γ ⊢F S *⁻ <: U *⁺
  deterministic⇒minus n fdtop             = ftop
  deterministic⇒minus n {Γ} (fdvar {m = m} T∈Γ D)
    with lookupOpt Γ m | inspect (lookupOpt Γ) m
  deterministic⇒minus n {Γ} (fdvar {m = m} refl D) | just T | [ eq ]
    = fbinds (lookup⇒<:∈ $ begin
                env-lookup (List.map _*⁻ Γ) m       ≡⟨ env-lookup-same (List.map _*⁻ Γ) m ⟩
                env-lookup′ (List.map _*⁻ Γ) m      ≡⟨ cong (Maybe.map (repeat (suc m) (_↑ 0)))
                                                            (lookupOpt-map Γ _*⁻ eq) ⟩
                just (repeat m (_↑ 0) (T *⁻) ↑ 0)   ≡⟨ cong (just ∘ (_↑ 0))
                                                            (repeat*-↑-comm⁻ T m 0) ⟩
                just ((repeat m (_↑⁻ 0) T *⁻) ↑ 0)  ≡⟨ cong just $ *-↑-comm⁻ (repeat m (_↑⁻ 0) T) 0 ⟩
                just ((repeat m (_↑⁻ 0) T ↑⁻ 0) *⁻) ∎)
             (deterministic⇒minus n D)
    where open Eq (setoid (Maybe Ftyp))
  deterministic⇒minus n {Γ} (fdvar {m = m} () D) | nothing | _
  deterministic⇒minus n {Γ} (fdall D)     = aux n _ _ _ D
    where aux : ∀ {n} m {Γ} (S : Vec (Ftyp⁻ n) m) U T →
                  [ n ] Vec.foldl (λ _ → _) (flip _∷_) Γ S ⊢FD U <: T →
                  List.map _*⁻ Γ ⊢F Π⁺ m ∙ T <: Π⁻[ S ]∙ U
          aux .0 nil U T D                = fall (deterministic⇒minus _ D) fvrefl
          aux .(suc _) (x ‼ S) U T D      = fall ftop (aux _ S U T D)


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

open import Categories.Category

-- The core of a category.
-- See https://ncatlab.org/nlab/show/core

module Categories.Category.Construction.Core {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level using (_⊔_)
open import Function using (flip)

open import Categories.Category.Groupoid using (Groupoid; IsGroupoid)
open import Categories.Morphism 𝒞
open import Categories.Morphism.IsoEquiv 𝒞

open Category 𝒞
open _≃_

Core : Category o (ℓ ⊔ e) e
Core = record
  { Obj       = Obj
  ; _⇒_       = _≅_
  ; _≈_       = _≃_
  ; id        = ≅.refl
  ; _∘_       = flip ≅.trans
  ; assoc     = ⌞ assoc     ⌟
  ; sym-assoc = ⌞ sym-assoc ⌟
  ; identityˡ = ⌞ identityˡ ⌟
  ; identityʳ = ⌞ identityʳ ⌟
  ; identity² = ⌞ identity² ⌟
  ; equiv     = ≃-isEquivalence
  ; ∘-resp-≈  = λ where ⌞ eq₁ ⌟ ⌞ eq₂ ⌟ → ⌞ ∘-resp-≈ eq₁ eq₂ ⌟
  }

Core-isGroupoid : IsGroupoid Core
Core-isGroupoid = record
  { _⁻¹ = ≅.sym
  ; iso = λ {_ _ f} → record { isoˡ = ⌞ isoˡ f ⌟ ; isoʳ = ⌞ isoʳ f ⌟ }
  }
  where open _≅_

CoreGroupoid : Groupoid o (ℓ ⊔ e) e
CoreGroupoid = record { category = Core; isGroupoid = Core-isGroupoid }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
open import Issue2229Reexport2

B = A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Algebra.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Module

open import Cubical.Algebra.Algebra.Base

open Iso

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

module AlgebraTheory (R : Ring ℓ) (A : Algebra R ℓ') where
  open RingStr (snd R) renaming (_+_ to _+r_ ; _·_ to _·r_)
  open AlgebraStr (A .snd)

  0-actsNullifying : (x : ⟨ A ⟩) → 0r ⋆ x ≡ 0a
  0-actsNullifying x =
    let idempotent-+ = 0r ⋆ x              ≡⟨ cong (λ u → u ⋆ x) (sym (RingTheory.0Idempotent R)) ⟩
                       (0r +r 0r) ⋆ x      ≡⟨ ⋆DistL+ 0r 0r x ⟩
                       (0r ⋆ x) + (0r ⋆ x) ∎
    in RingTheory.+Idempotency→0 (Algebra→Ring A) (0r ⋆ x) idempotent-+

  ⋆Dist· : (x y : ⟨ R ⟩) (a b : ⟨ A ⟩) → (x ·r y) ⋆ (a · b) ≡ (x ⋆ a) · (y ⋆ b)
  ⋆Dist· x y a b = (x ·r y) ⋆ (a · b) ≡⟨ ⋆AssocR _ _ _ ⟩
                   a · ((x ·r y) ⋆ b) ≡⟨ cong (a ·_) (⋆Assoc _ _ _) ⟩
                   a · (x ⋆ (y ⋆ b)) ≡⟨ sym (⋆AssocR _ _ _) ⟩
                   x ⋆ (a · (y ⋆ b)) ≡⟨ sym (⋆AssocL _ _ _) ⟩
                   (x ⋆ a) · (y ⋆ b) ∎

module AlgebraHoms {R : Ring ℓ} where
  open IsAlgebraHom

  idAlgebraHom : (A : Algebra R ℓ') → AlgebraHom A A
  fst (idAlgebraHom A) x = x
  pres0 (snd (idAlgebraHom A)) = refl
  pres1 (snd (idAlgebraHom A)) = refl
  pres+ (snd (idAlgebraHom A)) x y = refl
  pres· (snd (idAlgebraHom A)) x y = refl
  pres- (snd (idAlgebraHom A)) x = refl
  pres⋆ (snd (idAlgebraHom A)) r x = refl

  compIsAlgebraHom : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
    {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩}
    → IsAlgebraHom (B .snd) g (C .snd)
    → IsAlgebraHom (A .snd) f (B .snd)
    → IsAlgebraHom (A .snd) (g ∘ f) (C .snd)
  compIsAlgebraHom {g = g} {f} gh fh .pres0 = cong g (fh .pres0) ∙ gh .pres0
  compIsAlgebraHom {g = g} {f} gh fh .pres1 = cong g (fh .pres1) ∙ gh .pres1
  compIsAlgebraHom {g = g} {f} gh fh .pres+ x y = cong g (fh .pres+ x y) ∙ gh .pres+ (f x) (f y)
  compIsAlgebraHom {g = g} {f} gh fh .pres· x y = cong g (fh .pres· x y) ∙ gh .pres· (f x) (f y)
  compIsAlgebraHom {g = g} {f} gh fh .pres- x = cong g (fh .pres- x) ∙ gh .pres- (f x)
  compIsAlgebraHom {g = g} {f} gh fh .pres⋆ r x = cong g (fh .pres⋆ r x) ∙ gh .pres⋆ r (f x)

  _∘≃a_ : {A B C : Algebra R ℓ'}
         → AlgebraEquiv B C → AlgebraEquiv A B → AlgebraEquiv A C
  _∘≃a_  g f .fst = compEquiv (fst f) (fst g)
  _∘≃a_  g f .snd = compIsAlgebraHom (g .snd) (f .snd)

  compAlgebraHom : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
              → AlgebraHom A B → AlgebraHom B C → AlgebraHom A C
  compAlgebraHom f g .fst = g .fst ∘ f .fst
  compAlgebraHom f g .snd = compIsAlgebraHom (g .snd) (f .snd)

  syntax compAlgebraHom f g = g ∘a f

  compIdAlgebraHom : {A B : Algebra R ℓ'} (φ : AlgebraHom A B) → compAlgebraHom (idAlgebraHom A) φ ≡ φ
  compIdAlgebraHom φ = AlgebraHom≡ refl

  idCompAlgebraHom : {A B : Algebra R ℓ'} (φ : AlgebraHom A B) → compAlgebraHom φ (idAlgebraHom B) ≡ φ
  idCompAlgebraHom φ = AlgebraHom≡ refl

  compAssocAlgebraHom : {A B C D : Algebra R ℓ'}
                        (φ : AlgebraHom A B) (ψ : AlgebraHom B C) (χ : AlgebraHom C D)
                      → compAlgebraHom (compAlgebraHom φ ψ) χ ≡ compAlgebraHom φ (compAlgebraHom ψ χ)
  compAssocAlgebraHom _ _ _ = AlgebraHom≡ refl

module AlgebraEquivs {R : Ring ℓ} where
  open IsAlgebraHom
  open AlgebraHoms

  compIsAlgebraEquiv : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
    {g : ⟨ B ⟩ ≃ ⟨ C ⟩} {f : ⟨ A ⟩ ≃ ⟨ B ⟩}
    → IsAlgebraEquiv (B .snd) g (C .snd)
    → IsAlgebraEquiv (A .snd) f (B .snd)
    → IsAlgebraEquiv (A .snd) (compEquiv f g) (C .snd)
  compIsAlgebraEquiv {g = g} {f} gh fh = compIsAlgebraHom {g = g .fst} {f .fst} gh fh

  compAlgebraEquiv : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
                → AlgebraEquiv A B → AlgebraEquiv B C → AlgebraEquiv A C
  fst (compAlgebraEquiv f g) = compEquiv (f .fst) (g .fst)
  snd (compAlgebraEquiv f g) = compIsAlgebraEquiv {g = g .fst} {f = f .fst} (g .snd) (f .snd)

-- the Algebra version of uaCompEquiv
module AlgebraUAFunctoriality {R : Ring ℓ} where
 open AlgebraStr
 open AlgebraEquivs

 Algebra≡ : (A B : Algebra R ℓ') → (
   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
   Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
   Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
   Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
   Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
   PathP (λ i → IsAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isAlgebra (snd A))
                                                                     (isAlgebra (snd B)))
   ≃ (A ≡ B)
 Algebra≡ A B = isoToEquiv theIso
   where
   open Iso
   theIso : Iso _ _
   fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
                 , algebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
   inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
                , cong (isAlgebra ∘ snd) x
   rightInv theIso _ = refl
   leftInv theIso _ = refl

 caracAlgebra≡ : {A B : Algebra R ℓ'} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
 caracAlgebra≡ {A = A} {B = B} p q P =
   sym (transportTransport⁻ (ua (Algebra≡ A B)) p)
                                    ∙∙ cong (transport (ua (Algebra≡ A B))) helper
                                    ∙∙ transportTransport⁻ (ua (Algebra≡ A B)) q
     where
     helper : transport (sym (ua (Algebra≡ A B))) p ≡ transport (sym (ua (Algebra≡ A B))) q
     helper = Σ≡Prop
                (λ _ → isPropΣ
                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isOfHLevelPathP 1 (isPropIsAlgebra _ _ _ _ _ _ _) _ _)
               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

 uaCompAlgebraEquiv : {A B C : Algebra R ℓ'} (f : AlgebraEquiv A B) (g : AlgebraEquiv B C)
                  → uaAlgebra (compAlgebraEquiv f g) ≡ uaAlgebra f ∙ uaAlgebra g
 uaCompAlgebraEquiv f g = caracAlgebra≡ _ _ (
   cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g))
     ≡⟨ uaCompEquiv _ _ ⟩
   cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g)
     ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩
   cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Agda.Primitive public
open import Agda.Builtin.Nat public renaming (Nat to ℕ) hiding (_==_; _+_)
open import Agda.Builtin.Bool public

{- Basic datatypes and propositions -}

record ⊤ : Prop where
  instance constructor tt

record Unit : Set where
  instance constructor tt

data ⊥ : Prop where

data Empty : Set where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_ public

infixr 42 _×_
infixl 4 _,_

record ΣP (A : Prop) (B : A → Prop) : Prop where
  constructor _,_
  field
    fst : A
    snd : B fst
open ΣP public

instance
  pairP : {A : Prop} {B : A → Prop} {{a : A}} {{b : B a}} → ΣP A B
  pairP {{a}} {{b}} = a , b

record ΣS (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open ΣS public

{-
Literal notation for natural numbers and similar things.
Later on we will use notation with literal natural numbers for things that are not always defined,
so we need to use [fromNat] and a constraint. The idea is that if we have an instance of
[Number A], that means that we can potentially use literals to denote elements of [A], as long as
instance search can figure out that the constraint is satisfied.
We need the constraint to be a set as we will pattern match on it.
-}

record Number (A : Set) : Set₁ where
  field
    Constraint : ℕ → Set
    fromNat : (n : ℕ) {{_ : Constraint n}} → A
open Number {{...}} public
{-# BUILTIN FROMNAT fromNat #-}

instance
  NumNat : Number ℕ
  Number.Constraint NumNat _ = Unit
  Number.fromNat NumNat n = n

{- Equality -}

data _≡_ {l} {A : Set l} (x : A) : A → Prop l where
  instance refl : x ≡ x
--{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REWRITE _≡_ #-}

infix 4 _≡_

ap : {A B : Set} (f : A → B) {a b : A} → a ≡ b → f a ≡ f b
ap f refl = refl

ap2 : {A B C : Set} (f : A → B → C) {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → f a b ≡ f a' b'
ap2 f refl refl = refl

ap3 : {A B C D : Set} (f : A → B → C → D) {a a' : A} {b b' : B} {c c' : C} → a ≡ a' → b ≡ b' → c ≡ c' → f a b c ≡ f a' b' c'
ap3 f refl refl refl = refl

ap4 : {A B C D E : Set} (f : A → B → C → D → E) {a a' : A} {b b' : B} {c c' : C} {d d' : D} → a ≡ a' → b ≡ b' → c ≡ c' → d ≡ d' → f a b c d ≡ f a' b' c' d'
ap4 f refl refl refl refl = refl

_∙_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
refl ∙ refl = refl

infixr 4 _∙_

! : {A : Set} {a b : A} → a ≡ b → b ≡ a
! refl = refl

{- Lifting from Prop/Set to Set₁ -}

record Box (P : Prop) : Set where
  constructor box
  field
    unbox : P
open Box public

{- Monads -}

record Monad {ℓ ℓ'} (M : Set ℓ → Set ℓ') : Set (lsuc ℓ ⊔ ℓ') where
  field
    return : {A : Set ℓ} → A → M A
    _>>=_ : {A B : Set ℓ} → M A → (A → M B) → M B

  _>>_ : {A B : Set ℓ} → M A → M B → M B
  a >> b = a >>= (λ _ → b)

  infixr 20 _>>_

open Monad {{…}} public

-- {- For the partiality monad, we use (dependent) lists of propositions in order to get rid of useless ⊤s -}

-- data ListProp : Set₁
-- pf : ListProp → Prop

-- data ListProp where
--   [] : ListProp
--   [_] : Prop → ListProp
--   _,_ : (l : ListProp) → (pf l → ListProp) → ListProp

-- pf [] = ⊤
-- pf [ p ] = p
-- pf ([] , p) = pf (p tt)
-- pf (l , q) = ΣP (pf l) (λ x → pf (q x))

-- lemma : {l : ListProp} {p : pf l → ListProp} → pf (l , p) → ΣP (pf l) (λ x → pf (p x))

-- lemma {[]} q = tt , q
-- lemma {[ p ]} q = q
-- lemma {l , p} {r} q = (fst q , snd q)

{- The partiality monad -}

record Partial (A : Set) : Set₁ where
  field
    isDefined : Prop
    _$_ : isDefined → A
  infix 5 _$_
open Partial public

instance
  PartialityMonad : Monad Partial
  isDefined (Monad.return PartialityMonad x) = ⊤
  Monad.return PartialityMonad x Partial.$ tt = x
  isDefined (Monad._>>=_ PartialityMonad a f) = ΣP (isDefined a) (λ x → isDefined (f (a $ x)))
  Monad._>>=_ PartialityMonad a f Partial.$ x = f (a $ fst x) $ snd x

assume : (P : Prop) → Partial (Box P)
isDefined (assume P) = P
assume P $ x = box x

fail : {A : Set} → Partial A
isDefined fail = ⊥

{- Properties of the natural numbers -}

data _≤_ : (n m : ℕ) → Set where
  instance ≤r : {n : ℕ} → n ≤ n
  ≤S : {n m : ℕ} → n ≤ m → n ≤ suc m

≤P : {n m : ℕ} → suc n ≤ suc m → n ≤ m
≤P ≤r = ≤r
≤P {n} {suc m} (≤S p) = ≤S (≤P p)

_+_ : ℕ → ℕ → ℕ
n + zero = n
n + suc m = suc (n + m)

infixl 20 _+_

instance
  ≤-+ : {n m : ℕ} → n ≤ (n + m)
  ≤-+ {m = zero} = ≤r
  ≤-+ {m = suc m} = ≤S (≤-+ {m = m})

  -- ≤-+S : {m : ℕ} (n : ℕ) → m ≤ (m + suc n)
  -- ≤-+S _ = ≤S ≤-+

instance
  -- ≤S0 : {n : ℕ} → n ≤ suc n
  -- ≤S0 = ≤S ≤r

  0≤ : {n : ℕ} → 0 ≤ n
  0≤ {zero} = ≤r
  0≤ {suc n} = ≤S (0≤ {n})

≤SS : {n m : ℕ} {{_ : n ≤ m}} → suc n ≤ suc m
≤SS ⦃ ≤r ⦄ = ≤r
≤SS ⦃ ≤S p ⦄ = ≤S (≤SS {{p}})

≤+ : (l : ℕ) {n m : ℕ} {{_ : n ≤ m}} → (n + l) ≤ (m + l)
-- ≤+ l {{≤r}} = ≤r
-- ≤+ zero {{ ≤S p }} = ≤S p
-- ≤+ (suc l) {{ ≤S p }} = ≤SS {{≤+ l {{≤S p}}}}
≤+ zero {{p}} = p
≤+ (suc l) = ≤SS {{≤+ l}}

≤tr : {n m k : ℕ} {{_ : n ≤ m}} {{_ : m ≤ k}} → n ≤ k
≤tr ⦃ ≤r ⦄ ⦃ q ⦄ = q
≤tr ⦃ ≤S p ⦄ ⦃ ≤r ⦄ = ≤S p
≤tr ⦃ ≤S p ⦄ ⦃ ≤S q ⦄ = ≤S (≤tr {{≤S p}} {{q}})

{- Rewrite rules for the natural numbers (!!!) -}

+O-rewrite : {n : ℕ} → 0 + n ≡ n
+O-rewrite {zero} = refl
+O-rewrite {suc n} = ap suc +O-rewrite
-- {-# REWRITE +O-rewrite #-}

+S-rewrite : {n m : ℕ} → suc m + n ≡ suc (m + n)
+S-rewrite {zero} = refl
+S-rewrite {suc n} {m} = ap suc (+S-rewrite {n} {m})
-- {-# REWRITE +S-rewrite #-}

assoc : {n m k : ℕ} → (n + m) + k ≡ n + (m + k)
assoc {k = zero} = refl
assoc {n} {m} {k = suc k} = ap suc (assoc {n} {m} {k = k})
-- {-# REWRITE assoc #-}

data _===_ {l} {A : Set l} (x : A) : A → Set l where
  instance refl : x === x
{-# BUILTIN EQUALITY _===_ #-}

infix 4 _===_

-- transport : {A : Set} {P : A → Set} {a b : A} → a === b → P a → P b
-- transport refl u = u

-- transport! : {A : Set} {P : A → Set} {a b : A} → a === b → P b → P a
-- transport! refl u = u

{- Instance arguments -}

⟨⟩ : {A : Prop} {{a : A}} → A
⟨⟩ {{a}} = a

{- This is the sorts that we use for the syntax, two sorts: types and terms -}

data SyntaxSort : Set where
  Ty : SyntaxSort
  Tm : SyntaxSort

{- Positions of variables in a context -}

data VarPos : ℕ → Set where
  last : {n : ℕ} → VarPos (suc n)
  prev : {n : ℕ} → VarPos n → VarPos (suc n)

-- Size of the context before (and excluding) that variable
_-VarPos'_ : (n : ℕ) → VarPos n → ℕ
(suc n) -VarPos' last = n
(suc n) -VarPos' prev k = n -VarPos' k

-- Size of the context before (and including) that variable
_-VarPos_ : (n : ℕ) → VarPos n → ℕ
n -VarPos k = suc (n -VarPos' k)

--instance
suc-VarPos'≤ : {n : ℕ} {p : VarPos (suc n)} → (suc n -VarPos' p) ≤ n
suc-VarPos'≤ {n} {last} = ≤r
suc-VarPos'≤ {suc n} {prev p} = ≤tr {{suc-VarPos'≤ {n} {p}}} {{≤S ≤r}}

{- Positions of weakening spots in a context -}

data WeakPos : ℕ → Set where
  last : {n : ℕ} → WeakPos n
  prev : {n : ℕ} → WeakPos n → WeakPos (suc n)

weakenPos : {n m : ℕ} → n ≤ m → WeakPos n → WeakPos m
weakenPos ≤r k = k
weakenPos (≤S p) k = prev (weakenPos p k)

{- Weakening by a group of variable in the middle of a context -}

weakenV : {n m : ℕ} {{_ : n ≤ m}} (p : WeakPos n) → VarPos n → VarPos m
weakenV {m = suc m} ⦃ r ⦄ (prev p) last = last
weakenV ⦃ ≤r ⦄ p x = x
weakenV ⦃ ≤S r ⦄ last x = prev (weakenV {{r}} last x)
weakenV ⦃ ≤S r ⦄ (prev p) (prev x) = prev (weakenV {{≤P (≤S r)}} p x)

weakenV≤r : {n : ℕ} {p : WeakPos n} {v : VarPos n} → weakenV {{≤r}} p v ≡ v
weakenV≤r {p = last} {last} = refl
weakenV≤r {p = prev p} {last} = refl
weakenV≤r {p = last} {prev v} = refl
weakenV≤r {p = prev p} {prev v} = refl

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
{-# OPTIONS --without-K #-}
module Univalence where

open import Equivalence
open import Types

postulate
  ua : ∀ {ℓ} {A : Set ℓ} {B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

open import HoTT

{-
This file contains three proofs of Ω(S¹) = ℤ and the fact that the circle is
a 1-type:
- Something closely related to Mike’s original proof
- Dan’s encode-decode proof
- Guillaume’s proof using the flattening lemma.
This file is divided in a lot of different parts so that common parts can be
factored:

1. Definition of the universal cover and the encoding map (this part is common
   to all three proofs)
2. Proof that [encode (loop^ n) == n] (this part is common to Mike’s proof and
   the encode-decode proof)
3. Dan’s encode-decode proof that [Ω S¹ ≃ ℤ]
4. Mike’s proof that [Σ S¹ Cover] is contractible
5. Proof with the flattening lemma that [Σ S¹ S¹Cover] is contractible
6. Proof of [Ω S¹ ≃ ℤ] using the fact that [Σ S¹ S¹Cover] is contractible (common
   to Mike’s proof and the flattening lemma proof)
7. Encode-decode proof of the whole equivalence
8. Proof that the circle is a 1-type (common to all three proofs)

Keep
- 1, 2, 3    for the encode-decode proof    (+ 7, 8 for S¹ is a 1-type)
- 1, 2, 4, 6 for Mike’s proof               (+ 8)
- 1, 5, 6    for the flattening lemma proof (+ 8)
-}

{- 2017/02/09 favonia:

  1. [loop^] is defined in terms of [Group.exp], and the lemma
     [encode'-decode] is changed accordingly.  Although the original
     [encode-decode] can be proved without the generalized [encode'],
     [encode'] seems useful in proving the isomorphism (not just
     type equivalence) without flipping the two sides [Ω S¹] and [ℤ].

  2. Part 9 is added for further results.
-}

module homotopy.LoopSpaceCircle where

{- 1. Universal cover and encoding map (common to all three proofs) -}

module S¹Cover = S¹RecType ℤ succ-equiv

S¹Cover : S¹ → Type₀
S¹Cover = S¹Cover.f

encode' : {x₁ x₂ : S¹} (p : x₁ == x₂) → S¹Cover x₁ → S¹Cover x₂
encode' p n = transport S¹Cover p n

encode : {x : S¹} (p : base == x) → S¹Cover x
encode p = encode' p 0

{- 2. Encoding [loop^ n] (common to Mike’s proof and the encode-decode proof) -}

ΩS¹-group-structure : GroupStructure (base == base)
ΩS¹-group-structure = Ω^S-group-structure 0 ⊙S¹

module ΩS¹GroupStruct = GroupStructure ΩS¹-group-structure

-- We define the element of [Ω S¹] which is supposed to correspond to an
-- integer [n], this is the loop winding around the circle [n] times.
loop^ : (n : ℤ) → base == base
loop^ = ΩS¹GroupStruct.exp loop

-- Compatibility of [loop^] with the addition function
abstract
  loop^+ : (n₁ n₂ : ℤ) → loop^ (n₁ ℤ+ n₂) == loop^ n₁ ∙ loop^ n₂
  loop^+ = ΩS¹GroupStruct.exp-+ loop

-- Now we check that encoding [loop^ n] gives indeed [n], again by induction
-- on [n]
abstract
  encode'-∙ : ∀ {x₀ x₁ x₂} (p₀ : x₀ == x₁) (p₁ : x₁ == x₂) n
    → encode' (p₀ ∙ p₁) n == encode' p₁ (encode' p₀ n)
  encode'-∙ idp _ _ = idp

  encode'-loop : ∀ n → encode' loop n == succ n
  encode'-loop = S¹Cover.coe-loop-β

  encode'-!loop : ∀ n → encode' (! loop) n == pred n
  encode'-!loop n = coe-ap-! S¹Cover loop n ∙ S¹Cover.coe!-loop-β n

abstract
  encode'-loop^ : (n₁ n₂ : ℤ) → encode' (loop^ n₁) n₂ == n₁ ℤ+ n₂
  encode'-loop^ (pos 0) n₂ = idp
  encode'-loop^ (pos 1) n₂ = encode'-loop n₂
  encode'-loop^ (pos (S (S n₁))) n₂ =
    encode' (loop ∙ loop^ (pos (S n₁))) n₂
         =⟨ encode'-∙ loop (loop^ (pos (S n₁))) n₂ ⟩
    encode' (loop^ (pos (S n₁))) (encode' loop n₂)
         =⟨ encode'-loop n₂ |in-ctx encode' (loop^ (pos (S n₁))) ⟩
    encode' (loop^ (pos (S n₁))) (succ n₂)
         =⟨ encode'-loop^ (pos (S n₁)) (succ n₂) ⟩
    pos (S n₁) ℤ+ succ n₂
         =⟨ ℤ+-succ (pos (S n₁)) n₂ ⟩
    pos (S (S n₁)) ℤ+ n₂ =∎
  encode'-loop^ (negsucc 0) n₂ = encode'-!loop n₂
  encode'-loop^ (negsucc (S n₁)) n₂ =
    encode' (! loop ∙ loop^ (negsucc n₁)) n₂
         =⟨ encode'-∙ (! loop) (loop^ (negsucc n₁)) n₂ ⟩
    encode' (loop^ (negsucc n₁)) (encode' (! loop) n₂)
         =⟨ encode'-!loop n₂ |in-ctx encode' (loop^ (negsucc n₁)) ⟩
    encode' (loop^ (negsucc n₁)) (pred n₂)
         =⟨ encode'-loop^ (negsucc n₁) (pred n₂) ⟩
    negsucc n₁ ℤ+ pred n₂
         =⟨ ℤ+-pred (negsucc n₁) n₂ ⟩
    negsucc (S n₁) ℤ+ n₂
         =∎

  encode-loop^ : (n : ℤ) → encode (loop^ n) == n
  encode-loop^ n = encode'-loop^ n 0 ∙ ℤ+-unit-r n

{- 3. Dan’s encode-decode proof -}

-- The decoding function at [base] is [loop^], but we extend it to the whole
-- of [S¹] so that [decode-encode] becomes easier (and we need [loop^+] to
-- be able to extend it)
decode : (x : S¹) → (S¹Cover x → base == x)
decode =
  S¹-elim loop^ (↓-→-in λ {n} q →
                 ↓-cst=idf-in' $
                   ! (loop^+ n 1) ∙ ap loop^ (ℤ+-comm n 1 ∙ S¹Cover.↓-loop-out q))

abstract
  decode-encode : (x : S¹) (p : base == x) → decode x (encode p) == p
  decode-encode _ idp = idp  -- Magic!

-- And we get the theorem
ΩS¹≃ℤ : (base == base) ≃ ℤ
ΩS¹≃ℤ = equiv encode (decode base) encode-loop^ (decode-encode base)

{- 4. Mike’s proof that [Σ S¹ Cover] is contractible -}

-- We want to prove that every point of [Σ S¹ S¹Cover] is equal to [(base , O)]
paths-mike : (xt : Σ S¹ S¹Cover) → (base , 0) == xt
paths-mike (x , t) = paths-mike-c x t where

  abstract
    -- We do it by circle-induction on the first component. When it’s [base],
    -- we use the [↓-loop^] below (which is essentially [encode-loop^]) and
    -- for [loop] we use [loop^+] and the fact that [ℤ] is a set.
    paths-mike-c : (x : S¹) (t : S¹Cover x) → (base , 0) == (x , t) :> Σ S¹ S¹Cover
    paths-mike-c = S¹-elim
      (λ n → pair= (loop^ n) (↓-loop^ n))
      (↓-Π-in (λ {n} {n'} q →
       ↓-cst=idf-in'
         (pair= (loop^ n) (↓-loop^ n) ∙ pair= loop q
                    =⟨ Σ-∙ (↓-loop^ n) q ⟩
          pair= (loop^ n ∙ loop) (↓-loop^ n ∙ᵈ q)
                    =⟨ pair== (! (loop^+ n 1) ∙ ap loop^ (ℤ+-comm n 1 ∙ S¹Cover.↓-loop-out q))
                              (set-↓-has-all-paths-↓ ℤ-is-set) ⟩
          pair= (loop^ n') (↓-loop^ n') ∎))) where

      ↓-loop^ : (n : ℤ) → 0 == n [ S¹Cover ↓ loop^ n ]
      ↓-loop^ n = from-transp _ _ (encode-loop^ n)

abstract
  contr-mike : is-contr (Σ S¹ S¹Cover)
  contr-mike = ((base , 0) , paths-mike)

{- 5. Flattening lemma proof that [Σ S¹ Cover] is contractible -}

--We import the flattening lemma for the universal cover of the circle
--open FlatteningS¹ ℤ succ-equiv
open S¹Cover using (module Wt; Wt; cct; ppt; flattening-S¹)

-- We prove that the flattened HIT corresponding to the universal cover of the
-- circle (the real line) is contractible
Wt-is-contr : is-contr Wt
Wt-is-contr = (cct tt 0 , Wt.elim (base* ∘ snd) (loop* ∘ snd)) where

  -- This is basically [loop^] using a different composition order
  base* : (n : ℤ) → cct tt 0 == cct tt n
  base* (pos 0) = idp
  base* (pos 1) = ppt tt 0
  base* (pos (S (S n))) = base* (pos (S n)) ∙ ppt tt (pos (S n))
  base* (negsucc 0) = ! (ppt tt (negsucc O))
  base* (negsucc (S n)) = base* (negsucc n) ∙ ! (ppt tt (negsucc (S n)))

  abstract
    loop* : (n : ℤ)
      → base* n == base* (succ n) [ (λ x → cct tt 0 == x) ↓ ppt tt n ]
    loop* n = ↓-cst=idf-in' (aux n) where

      -- This is basically [loop^+ 1 n]
      aux : (n : ℤ) → base* n ∙ ppt tt n == base* (succ n)
      aux (pos 0) = idp
      aux (pos (S n)) = idp
      aux (negsucc 0) = !-inv-l (ppt tt (negsucc O))
      aux (negsucc (S n)) =
        base* (negsucc (S n)) ∙ ppt tt (negsucc (S n))
                  =⟨ idp ⟩
        (base* (negsucc n) ∙ ! (ppt tt (negsucc (S n)))) ∙ ppt tt (negsucc (S n))
                  =⟨ ∙-assoc (base* (negsucc n)) _ _ ⟩
        base* (negsucc n) ∙ (! (ppt tt (negsucc (S n))) ∙ ppt tt (negsucc (S n)))
                  =⟨ !-inv-l (ppt tt (negsucc (S n)))
                         |in-ctx (λ u → base* (negsucc n) ∙ u) ⟩
        base* (negsucc n) ∙ idp
                  =⟨ ∙-unit-r _ ⟩
        base* (negsucc n) ∎

-- Then, using the flattening lemma we get that the total space of [Cover] is
-- contractible
abstract
  contr-flattening : is-contr (Σ S¹ S¹Cover)
  contr-flattening = transport! is-contr flattening-S¹ Wt-is-contr

{- 6. Proof that [Ω S¹ ≃ ℤ] using the fact that [Σ S¹ Cover] is contractible -}

tot-encode : Σ S¹ (λ x → base == x) → Σ S¹ S¹Cover
tot-encode (x , y) = (x , encode y)

-- The previous map induces an equivalence on the total spaces, because both
-- total spaces are contractible
abstract
  total-is-equiv : is-equiv tot-encode
  total-is-equiv = contr-to-contr-is-equiv _ (pathfrom-is-contr base) contr-flattening

-- Hence it’s an equivalence fiberwise
abstract
  encode-is-equiv : (x : S¹) → is-equiv (encode {x})
  encode-is-equiv = total-equiv-is-fiber-equiv (λ _ → encode) total-is-equiv

-- We can then conclude that the loop space of the circle is equivalent to [ℤ]
ΩS¹≃ℤ' : (base == base) ≃ ℤ
ΩS¹≃ℤ' = (encode {base} , encode-is-equiv base)

{- 7. Encode-decode proof of the whole fiberwise equivalence -}

-- This is quite similar to [paths-mike], we’re doing it by circle-induction,
-- the base case is [encode-loop^] and the loop case is using the fact that [ℤ]
-- is a set (and [loop^+] is already used in [decode])
encode-decode : (x : S¹) (t : S¹Cover x) → encode (decode x t) == t
encode-decode =
  S¹-elim {P = λ x → (t : S¹Cover x) → encode (decode x t) == t}
    encode-loop^ (↓-Π-in (λ q → prop-has-all-paths-↓ (ℤ-is-set _ _)))

encode-is-equiv' : (x : S¹) → is-equiv (encode {x})
encode-is-equiv' x = is-eq encode (decode x) (encode-decode x) (decode-encode x)

{- 8. Proof that the circle is a 1-type -}

abstract
  S¹Cover-is-set : {y : S¹} → is-set (S¹Cover y)
  S¹Cover-is-set {y} = S¹-elim {P = λ y → is-set (S¹Cover y)}
    ℤ-is-set (prop-has-all-paths-↓ is-set-is-prop) y

  ΩS¹-is-set : {y : S¹} → is-set (base == y)
  ΩS¹-is-set {y} = equiv-preserves-level ((encode {y} , encode-is-equiv y) ⁻¹)
                                         (S¹Cover-is-set {y})

S¹-level : has-level 1 S¹
S¹-level =
  S¹-elim (λ _ → ΩS¹-is-set) (prop-has-all-paths-↓ (Π-level (λ x → is-set-is-prop)))

{- 9. More stuff -}

ΩS¹-iso-ℤ : Ω^S-group 0 ⊙S¹ S¹-level ≃ᴳ ℤ-group
ΩS¹-iso-ℤ = ≃-to-≃ᴳ ΩS¹≃ℤ encode-pres-∙ where
  abstract
    encode-∙ : ∀ {x₁ x₂} (loop₁ : base == x₁) (loop₂ : x₁ == x₂)
      → encode (loop₁ ∙ loop₂) == encode' loop₂ (encode loop₁)
    encode-∙ idp _ = idp

    encode-pres-∙ : ∀ (loop₁ loop₂ : base == base)
      → encode (loop₁ ∙ loop₂) == encode loop₁ ℤ+ encode loop₂
    encode-pres-∙ loop₁ loop₂ =
        encode (loop₁ ∙ loop₂)
          =⟨ encode'-∙ loop₁ loop₂ 0 ⟩
        encode' loop₂ (encode loop₁)
          =⟨ ! $ decode-encode _ loop₂ |in-ctx (λ loop₂ → encode' loop₂ (encode loop₁)) ⟩
        encode' (loop^ (encode loop₂)) (encode loop₁)
          =⟨ encode'-loop^ (encode loop₂) (encode loop₁) ⟩
        encode loop₂ ℤ+ encode loop₁
          =⟨ ℤ+-comm (encode loop₂) (encode loop₁) ⟩
        encode loop₁ ℤ+ encode loop₂
          =∎

abstract
  ΩS¹-is-abelian : is-abelian (Ω^S-group 0 ⊙S¹ S¹-level)
  ΩS¹-is-abelian = iso-preserves-abelian (ΩS¹-iso-ℤ ⁻¹ᴳ) ℤ-group-is-abelian

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
------------------------------------------------------------------------
-- Normalization/simplification of kinding in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Simple.Normalization where

open import Data.Fin using (Fin; zero; suc; raise; lift)
open import Data.Fin.Substitution using (module VarSubst)
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.List using ([]; _∷_; _∷ʳ_; map)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product as Prod using (_,_)
open import Data.Vec as Vec using ([]; _∷_)
import Data.Vec.Properties as VecProp
open import Function using (flip; _∘_)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
  renaming (sub to hsub; _↑ to _H↑)
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Syntax.WeakEquality
open import FOmegaInt.Kinding.Simple as Simple
open import FOmegaInt.Kinding.Simple.EtaExpansion
open import FOmegaInt.Kinding.Declarative as Declarative

------------------------------------------------------------------------
-- Normalization/simplification of kinded types to simply kinded
-- types.
--
-- TODO: explain the point of this and how "simple" kinding differs
-- from "canonical" kinding.

open Syntax
open TermCtx
open SimpleCtx    using (kd; tp; ⌊_⌋Asc; kd-inj′)
open Substitution hiding (subst)
open ContextConversions
open RenamingCommutesNorm
open WeakHereditarySubstitutionEquality
open WeakEqEtaExpansion
open WeakEqNormalization
open KindedHereditarySubstitution
open Simple.Kinding
open Declarative.Kinding

private
  module S where
    open Simple.Kinding public
    open SimpleCtx      public
    open SimplyWfCtx    public
  module D where
    open Declarative.Kinding public
    open TermCtx             public
  module E = ElimCtx

mutual

  -- Normalization and simultaneous simplification of kinding:
  -- well-kinded types normalize to simply kinded normal forms.
  nf-Tp∈ : ∀ {n} {Γ : Ctx n} {a k} →
           let Γ′ = nfCtx Γ in Γ ⊢Tp a ∈ k → ⌊ Γ′ ⌋Ctx ⊢Nf nf Γ′ a ∈ ⌊ k ⌋
  nf-Tp∈ {_} {Γ} (∈-var {j} x Γ-ctx Γ[x]≡kd-k)
    with E.lookup (nfCtx Γ) x | nfCtx-lookup-kd x Γ Γ[x]≡kd-k
  nf-Tp∈ {_} {Γ} (∈-var {j} x Γ-ctx Γ[x]≡kd-j) | kd ._ | refl =
    subst (_ ⊢Nf η-exp (nfKind _ j) (var∙ x) ∈_) (⌊⌋-nf _)
          (η-exp-Var∈ (lookup-kd x (nf-ctx Γ-ctx) nf-Γ[x]≡kd-nf-j)
                      (∈-var x (⌊⌋-lookup (nfCtx Γ) x nf-Γ[x]≡kd-nf-j)))
    where
      open WfsCtxOps using (lookup-kd)
      nf-Γ[x]≡kd-nf-j = nfCtx-lookup-kd x Γ Γ[x]≡kd-j
  nf-Tp∈ (∈-var x Γ-ctx Γ[x]≡kd-k) | tp _  | ()
  nf-Tp∈ (∈-⊥-f Γ-ctx)    = ∈-⊥-f
  nf-Tp∈ (∈-⊤-f Γ-ctx)    = ∈-⊤-f
  nf-Tp∈ (∈-∀-f k-kd a∈*) = ∈-∀-f (nf-kd k-kd) (nf-Tp∈ a∈*)
  nf-Tp∈ (∈-→-f a∈* b∈*)  = ∈-→-f (nf-Tp∈ a∈*) (nf-Tp∈ b∈*)
  nf-Tp∈ (∈-Π-i {j} {a} j-kd a∈k k-kd) =
    let j′ = nfKind _ j
    in subst (λ l → _ ⊢Nf Λ∙ j′ (nf (kd j′ ∷ _) a) ∈ l ⇒ _) (⌊⌋-nf j)
             (∈-Π-i (nf-kd j-kd) (nf-Tp∈ a∈k))
  nf-Tp∈ (∈-Π-e {a} {b} a∈Πjk b∈j _ _) =
    subst (_ ⊢Nf nf _ a ↓⌜·⌝ nf _ b ∈_) (sym (⌊⌋-Kind/ _))
          (Nf∈-Π-e′ (nf-Tp∈ a∈Πjk) (nf-Tp∈ b∈j))
  nf-Tp∈ (∈-s-i a∈a⋯b)  = nf-Tp∈ a∈a⋯b
  nf-Tp∈ (∈-⇑ a∈j j<∷k) = subst (_ ⊢Nf _ ∈_) (<∷-⌊⌋ j<∷k) (nf-Tp∈ a∈j)

  -- Normalization and simultaneous simplification of kind
  -- well-formedness: well-formed kinds normalize to simply
  -- well-formed kinds.
  nf-kd : ∀ {n} {Γ : Ctx n} {k} →
          let Γ′ = nfCtx Γ in Γ ⊢ k kd → ⌊ Γ′ ⌋Ctx ⊢ nfKind Γ′ k kds
  nf-kd (kd-⋯ a∈* b∈*)   = kds-⋯ (nf-Tp∈ a∈*) (nf-Tp∈ b∈*)
  nf-kd (kd-Π j-kd k-kd) = kds-Π (nf-kd j-kd) (nf-kd k-kd)

  -- Normalization and simultaneous simplification of contexts:
  -- well-formed contexts normalize to simply well-formed simple
  -- contexts.

  nf-wf : ∀ {n} {Γ : Ctx n} {a} →
          let Γ′ = nfCtx Γ in Γ ⊢ a wf → ⌊ Γ′ ⌋Ctx ⊢ nfAsc Γ′ a wfs
  nf-wf (wf-kd k-kds) = wfs-kd (nf-kd k-kds)
  nf-wf (wf-tp a∈*)   = wfs-tp (nf-Tp∈ a∈*)

  nf-ctx : ∀ {n} {Γ : Ctx n} → Γ ctx → nfCtx Γ ctxs
  nf-ctx D.[]             = S.[]
  nf-ctx (a-wf D.∷ Γ-ctx) = nf-wf a-wf S.∷ nf-ctx Γ-ctx

-- Normal forms of type operators are η-long.
≈-η-nf : ∀ {n} {Γ : Ctx n} {a j k} → Γ ⊢Tp a ∈ Π j k →
         let nf-Γ = nfCtx Γ
         in nf nf-Γ (Λ j (weaken a · var zero)) ≈ nf nf-Γ a
≈-η-nf a∈Πjk with Nf∈-⇒-inv (nf-Tp∈ a∈Πjk)
≈-η-nf {_} {Γ} {a} {j} {k} a∈Πjk
  | l , b , l-kds , b∈⌊k⌋ , ⌊l⌋≡⌊j⌋ , nf-a≡Λlb =
  begin
    nf nf-Γ (Λ j (weaken a · var zero))
  ≈⟨ ≈-Λ∙ ⌊nf-j⌋≡⌊l⌋ (begin
        nf-a′ ↓⌜·⌝ η-exp (weakenKind′ nf-j) (var∙ zero)
      ≡⟨ cong (_↓⌜·⌝ η-exp (weakenKind′ nf-j) (var∙ zero))
              (trans (sym (nf-weaken (kd nf-j) a)) (cong weakenElim nf-a≡Λlb)) ⟩
        weakenElim (Λ∙ l b) ↓⌜·⌝ η-exp (weakenKind′ nf-j) (var∙ zero)
      ≡⟨⟩
        b Elim/Var (VarSubst.wk VarSubst.↑) /⟨ ⌊ weakenKind′ l ⌋ ⟩
          hsub (η-exp (weakenKind′ nf-j) (var∙ zero))
      ≈⟨ ≈-[∈] (≈-refl (b Elim/Var (VarSubst.wk VarSubst.↑)))
               (≈-η-exp ⌊nf-j/wk⌋≡⌊l/wk⌋ (≈-var∙ zero)) ⟩
        b Elim/Var (VarSubst.wk VarSubst.↑) /⟨ ⌊ weakenKind′ l ⌋ ⟩
          hsub (η-exp (weakenKind′ l) (var∙ zero))
      ≈⟨ Nf∈-[]-η-var [] l-kds
                      (subst (λ l → kd l ∷ _ ⊢Nf b ∈ _) (sym ⌊l⌋≡⌊j⌋) b∈⌊k⌋) ⟩
        b
      ∎) ⟩
    Λ∙ l b
  ≡⟨ sym nf-a≡Λlb ⟩
    nf nf-Γ a
  ∎
  where
    nf-Γ   = nfCtx Γ
    nf-j   = nfKind nf-Γ j
    nf-j∷Γ = kd nf-j ∷ nf-Γ
    nf-a′  = nf nf-j∷Γ (weaken a)
    ⌊nf-j⌋≡⌊l⌋ = begin
      ⌊ nf-j ⌋ ≡⟨ ⌊⌋-nf j ⟩
      ⌊ j ⌋    ≡⟨ sym ⌊l⌋≡⌊j⌋ ⟩
      ⌊ l ⌋    ∎
      where open ≡-Reasoning
    ⌊nf-j/wk⌋≡⌊l/wk⌋ = begin
      ⌊ weakenKind′ nf-j ⌋   ≡⟨ ⌊⌋-Kind′/Var nf-j ⟩
      ⌊ nf-j ⌋               ≡⟨ ⌊nf-j⌋≡⌊l⌋ ⟩
      ⌊ l ⌋                  ≡⟨ sym (⌊⌋-Kind′/Var l) ⟩
      ⌊ weakenKind′ l ⌋      ∎
      where open ≡-Reasoning
    open ≈-Reasoning

-- Well-kinded hereditary substitions.

infix 4 _⊢/Tp⟨_⟩_∈_

data _⊢/Tp⟨_⟩_∈_ : ∀ {m n} → Ctx n → SKind → SVSub m n → Ctx m → Set where
  ∈-hsub : ∀ {n} {Γ : Ctx n} {k a} →
           Γ ⊢Tp a ∈ k → Γ ⊢/Tp⟨ ⌊ k ⌋ ⟩ hsub ⌜ a ⌝ ∈ kd k ∷ Γ
  ∈-H↑   : ∀ {m n Δ k Γ} {σ : SVSub m n} {a} →
           Δ ⊢/Tp⟨ k ⟩ σ ∈ Γ → (a TermAsc/ toSub σ) ∷ Δ ⊢/Tp⟨ k ⟩ σ H↑ ∈ a ∷ Γ

-- Normalize and simplify a well-kinded hereditary substitution.

nf-/⟨⟩∈ : ∀ {m n k Δ} {σ : SVSub m n} {Γ} → Δ ⊢/Tp⟨ k ⟩ σ ∈ Γ →
          ⌊ nfCtx Δ ⌋Ctx ⊢/⟨ k ⟩ nfSVSub (nfCtx Δ) σ ∈ ⌊ nfCtx Γ ⌋Ctx
nf-/⟨⟩∈ (∈-hsub {Γ = Γ} {k} {a} a∈k) =
  subst₂ (⌊ nfCtx Γ ⌋Ctx ⊢/⟨ ⌊ k ⌋ ⟩_∈_)
         (cong (hsub ∘ nf (nfCtx Γ)) (sym (⌞⌟∘⌜⌝-id a)))
         (cong (λ j → kd j ∷ ⌊ nfCtx Γ ⌋Ctx) (sym (⌊⌋-nf k)))
         (∈-hsub (nf-Tp∈ a∈k))
nf-/⟨⟩∈ (∈-H↑ {Δ = Δ} {k} {Γ} {σ} {a} σ∈Γ) =
  subst (_⊢/⟨ k ⟩ nfSVSub (nfCtx (a/σ ∷ Δ)) (σ H↑) ∈ ⌊ nfCtx (a ∷ Γ) ⌋Ctx)
        (cong (_∷ ⌊ nfCtx Δ ⌋Ctx) (begin
          ⌊ nfAsc (nfCtx Γ) a ⌋Asc                     ≡⟨ ⌊⌋Asc-nf a ⟩
          ⌊ a ⌋Asc                                     ≡˘⟨ S.⌊⌋-TermAsc/ a ⟩
          ⌊ a TermAsc/ toSub σ ⌋Asc                    ≡˘⟨ ⌊⌋Asc-nf _ ⟩
          ⌊ nfAsc (nfCtx Δ) (a TermAsc/ toSub σ) ⌋Asc  ∎))
        (∈-H↑ (nf-/⟨⟩∈ σ∈Γ))
  where
    open ≡-Reasoning
    a/σ = a TermAsc/ toSub σ

open ≈-Reasoning
private module P = ≡-Reasoning

mutual

  -- Substitution (weakly) commutes with normalization.

  nf-/⟨⟩ : ∀ {m n Δ k Γ} {σ : SVSub m n} {a j} →
           Γ ⊢Tp a ∈ j → Δ ⊢/Tp⟨ k ⟩ σ ∈ Γ →
           nf (nfCtx Δ) (a / toSub σ)  ≈
             nf (nfCtx Γ) a /⟨ k ⟩ nfSVSub (nfCtx Δ) σ
  nf-/⟨⟩ {Γ = Γ} (∈-var x Γ-ctx Γ[x]≡kd-j) σ∈Γ
    with E.lookup (nfCtx Γ) x | nfCtx-lookup-kd x Γ Γ[x]≡kd-j
  nf-/⟨⟩ {Δ = Δ} {k} {Γ} {σ} {_} {j} (∈-var x Γ-ctx Γ[x]≡kd-j) σ∈Γ
    | kd nf-j | refl with hit? σ x
  ... | hit a hitP =
    let open WfsCtxOps using (lookup-kd)
        nf-Γ-ctxs       = nf-ctx Γ-ctx
        nf-Γ[x]≡kd-nf-j = nfCtx-lookup-kd x Γ Γ[x]≡kd-j
        nf-j-kds  = lookup-kd x nf-Γ-ctxs nf-Γ[x]≡kd-nf-j
        hitP-nf-σ = nf-Hit (nfCtx Δ) hitP
        x∈⌊j⌋     = ∈-var x (⌊⌋-lookup (nfCtx Γ) x nf-Γ[x]≡kd-nf-j)
    in begin
      nf (nfCtx Δ) (Vec.lookup (toSub σ) x)
    ≡⟨ cong (nf (nfCtx Δ)) (lookup-toSub σ x) ⟩
      nf (nfCtx Δ) (⌞ toElim (lookupSV σ x) ⌟)
    ≡⟨ cong (nf (nfCtx Δ) ∘ ⌞_⌟ ∘ toElim) (lookup-Hit hitP) ⟩
      nf (nfCtx Δ) ⌞ a ⌟
    ≡˘⟨ cong (_?∙∙⟨ k ⟩ []) (lookup-Hit hitP-nf-σ) ⟩
      var∙ x /⟨ k ⟩ nfSVSub (nfCtx Δ) σ
    ≈˘⟨ η-exp-var-Hit-/⟨⟩ hitP-nf-σ nf-j-kds x∈⌊j⌋ (nf-/⟨⟩∈ σ∈Γ) ⟩
      η-exp (nfKind (nfCtx Γ) j) (var∙ x) /⟨ k ⟩ nfSVSub (nfCtx Δ) σ
    ∎
  ... | miss y missP =
    let open WfsCtxOps using (lookup-kd)
        nf-Γ-ctxs       = nf-ctx Γ-ctx
        nf-Γ[x]≡kd-nf-j = nfCtx-lookup-kd x Γ Γ[x]≡kd-j
        nf-j-kds   = lookup-kd x nf-Γ-ctxs nf-Γ[x]≡kd-nf-j
        missP-nf-σ = nf-Miss (nfCtx Δ) missP
        x∈⌊j⌋      = ∈-var x (⌊⌋-lookup (nfCtx Γ) x nf-Γ[x]≡kd-nf-j)
    in begin
      nf (nfCtx Δ) (Vec.lookup (toSub σ) x)
    ≡⟨ cong (nf (nfCtx Δ)) (lookup-toSub σ x) ⟩
      nf (nfCtx Δ) ⌞ toElim (lookupSV σ x) ⌟
    ≡⟨ cong (nf (nfCtx Δ) ∘ ⌞_⌟ ∘ toElim) (lookup-Miss missP) ⟩
      nf (nfCtx Δ) (var y)
    ≈⟨ nf-var-kd-⌊⌋ (nfCtx Δ) y (P.begin
          ⌊ E.lookup (nfCtx Δ) y ⌋Asc
        P.≡˘⟨ ⌊⌋Asc-lookup (nfCtx Δ) y ⟩
          S.lookup ⌊ nfCtx Δ ⌋Ctx y
        P.≡⟨ lookup-/⟨⟩∈-Miss (nf-/⟨⟩∈ σ∈Γ) x∈⌊j⌋ missP-nf-σ  ⟩
          S.lookup ⌊ nfCtx Γ ⌋Ctx x
        P.≡⟨ ⌊⌋-lookup (nfCtx Γ) x nf-Γ[x]≡kd-nf-j ⟩
          kd ⌊ nfKind (nfCtx Γ) j ⌋
        P.≡˘⟨ cong kd (⌊⌋-Kind/⟨⟩ (nfKind (nfCtx Γ) j)) ⟩
          kd ⌊ nfKind (nfCtx Γ) j Kind/⟨ k ⟩ nfSVSub (nfCtx Δ) σ ⌋
        P.∎) ⟩
      η-exp (nfKind (nfCtx Γ) j Kind/⟨ k ⟩ nfSVSub (nfCtx Δ) σ) (var∙ y)
    ≡˘⟨ η-exp-ne-Miss-/⟨⟩ x y [] (nfKind (nfCtx Γ) j) missP-nf-σ ⟩
      η-exp (nfKind (nfCtx Γ) j) (var∙ x) /⟨ k ⟩ nfSVSub (nfCtx Δ) σ
    ∎
  nf-/⟨⟩ (∈-var _ _ _) σ∈Γ | tp a | ()
  nf-/⟨⟩ (∈-⊥-f Γ-ctx) σ∈Γ = ≈-refl _
  nf-/⟨⟩ (∈-⊤-f Γ-ctx) σ∈Γ = ≈-refl _
  nf-/⟨⟩ (∈-∀-f {j} j-kd a∈*) σ∈Γ =
    ≈-∀∙ (nfKind-/⟨⟩ j-kd σ∈Γ) (nf-/⟨⟩ a∈* (∈-H↑ σ∈Γ))
  nf-/⟨⟩ (∈-→-f a∈* b∈*) σ∈Γ =
    ≈-⇒∙ (nf-/⟨⟩ a∈* σ∈Γ) (nf-/⟨⟩ b∈* σ∈Γ)
  nf-/⟨⟩ (∈-Π-i j-kd a∈k k-kd) σ∈Γ =
    ≈-Λ∙ (≋-⌊⌋ (nfKind-/⟨⟩ j-kd σ∈Γ)) (nf-/⟨⟩ a∈k (∈-H↑ σ∈Γ))
  nf-/⟨⟩ {Δ = Δ} {k} {Γ} {σ} {a · b} (∈-Π-e a∈Πjk b∈j _ _) σ∈Γ = begin
      nf (nfCtx Δ) (a / toSub σ) ↓⌜·⌝ nf (nfCtx Δ) (b / toSub σ)
    ≈⟨ ≈-↓⌜·⌝ (nf-/⟨⟩ a∈Πjk σ∈Γ) (nf-/⟨⟩ b∈j σ∈Γ) ⟩
      (nf (nfCtx Γ) a /⟨ k ⟩ nfSVSub (nfCtx Δ) σ) ↓⌜·⌝
        (nf (nfCtx Γ) b /⟨ k ⟩ nfSVSub (nfCtx Δ) σ)
    ≡⟨ sym (Nf∈-Π-e-/⟨⟩′ (nf-Tp∈ a∈Πjk) (nf-Tp∈ b∈j) (nf-/⟨⟩∈ σ∈Γ)) ⟩
      nf (nfCtx Γ) a ↓⌜·⌝ nf (nfCtx Γ) b /⟨ k ⟩ nfSVSub (nfCtx Δ) σ
    ∎
  nf-/⟨⟩ (∈-s-i a∈c⋯d)  σ∈Γ = nf-/⟨⟩ a∈c⋯d σ∈Γ
  nf-/⟨⟩ (∈-⇑ a∈j j<∷k) σ∈Γ = nf-/⟨⟩ a∈j σ∈Γ

  nfKind-/⟨⟩ : ∀ {m n Δ k Γ} {σ : SVSub m n} {j} →
               Γ ⊢ j kd → Δ ⊢/Tp⟨ k ⟩ σ ∈ Γ →
               nfKind (nfCtx Δ) (j Kind/ toSub σ)  ≋
                 nfKind (nfCtx Γ) j Kind/⟨ k ⟩ nfSVSub (nfCtx Δ) σ
  nfKind-/⟨⟩ (kd-⋯ a∈* b∈*)   σ∈Γ = ≋-⋯ (nf-/⟨⟩ a∈* σ∈Γ) (nf-/⟨⟩ b∈* σ∈Γ)
  nfKind-/⟨⟩ (kd-Π j-kd k-kd) σ∈Γ =
    ≋-Π (nfKind-/⟨⟩ j-kd σ∈Γ) (nfKind-/⟨⟩ k-kd (∈-H↑ σ∈Γ))

-- Shorthands.

nf-[] : ∀ {n} {Γ : Ctx n} {k a j b} →
        kd k ∷ Γ ⊢Tp a ∈ j → Γ ⊢Tp b ∈ k →
        nf (nfCtx Γ) (a [ b ])  ≈
          nf (nfCtx (kd k ∷ Γ)) a [ nf (nfCtx Γ) b ∈ ⌊ k ⌋ ]
nf-[] {_} {Γ} {k} {a} a∈j b∈k =
  subst (λ c → nf (nfCtx Γ) (a [ c ]) ≈
               (nf (nfCtx (kd k ∷ Γ)) a [ nf (nfCtx Γ) c ∈ ⌊ k ⌋ ]))
        (⌞⌟∘⌜⌝-id _) (nf-/⟨⟩ a∈j (∈-hsub b∈k))

nfKind-[] : ∀ {n} {Γ : Ctx n} {k j b} →
            kd k ∷ Γ ⊢ j kd → Γ ⊢Tp b ∈ k →
            nfKind (nfCtx Γ) (j Kind[ b ])  ≋
              nfKind (nfCtx (kd k ∷ Γ)) j Kind[ nf (nfCtx Γ) b ∈ ⌊ k ⌋ ]
nfKind-[] {_} {Γ} {k} {j} j-kd b∈k =
  subst (λ c → nfKind (nfCtx Γ) (j Kind[ c ]) ≋
               (nfKind (nfCtx (kd k ∷ Γ)) j Kind[ nf (nfCtx Γ) c ∈ ⌊ k ⌋ ]))
        (⌞⌟∘⌜⌝-id _) (nfKind-/⟨⟩ j-kd (∈-hsub b∈k))

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda