rules.txt

THIS IS ALSO PRETTY OLD NOW


TODO:
- harmonize notation with implementation everywhere
- add newest coe Glue (old/notes), look at hcom fib unfolding optimization
- write hcom Glue

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

Interval vars: i,j,k

Cofibrations:
  - A cof is a list of atomic cofs, viewed as a *conjunction*.
  - Atomic cofs: i=0 | i=1 | i=j
  - Cof vars: α, β, γ

Context:
  - Γ + interval cxt + one cofibration
  - In notation, we can just extend Γ with either i:I or α:Cof,
    but formally we mean extending the appropriate part of the cxt.
    Extending the cof is just conjunction.

Systems:
  - list of (cof, term) pairs, can be empty
  - notation: [α₀ ↦ t₀, α₁ ↦ t₁, ... αᵢ ↦ tᵢ]
  - typing:

    Γ ⊢ A : U    Γ, αᵢ ⊢ tᵢ : A    Γ, αᵢ ∧ αⱼ ⊢ tᵢ ≡ tⱼ
    ───────────────────────────────────────────────────
             Γ ⊢ [αᵢ ↦ tᵢ] is a system

Cubical extension judgement:

    Γ ⊢ t : A[α ↦ u]  means  Γ ⊢ t : A  and  Γ,α ⊢ t ≡ u

Coercion

         Γ,i ⊢ A : U   Γ ⊢ t : A r
    ────────────────────────────────────
    Γ ⊢ coeⁱ r r' A t : (A r') [r=r' ↦ t]

Homogeneous composition


    Γ ⊢ α cof  Γ ⊢ A : U   Γ, α, i ⊢ t : A    Γ ⊢ b : A    Γ, α ⊢ t r ≡ b
    ──────────────────────────────────────────────────────────────────────
         Γ ⊢ hcomⁱ r r' A [α ↦ t] b : A [r=r' ↦ b, α ↦ t r')

Composition (derived)

    Γ ⊢ α cof   Γ, i ⊢ A : U   Γ, α, i ⊢ t : A   Γ ⊢ b : A r   Γ, α ⊢ t r ≡ b
    ────────────────────────────────────────────────────────────────────────
       Γ ⊢ comⁱ r r' A [α ↦ t] b : (A r') [r=r' ↦ b, α ↦ t r']
           com r r' (i. A i) [α i. t] b :=
             hcom r r' (A r') [α i. coe i r' (j. A j) t] (coe r r' (i. A i) b)


-- filling
--------------------------------------------------------------------------------

Γ, i ⊢ coeFillⁱ r A t : A [i=r ↦ t, i=r' ↦ coeⁱ r r' A t ]
       coeFillⁱ r A t := coe r i A t

Γ, i ⊢ coeFill⁻¹ⁱ r A t : A [i=r ↦ coe r r' A t, i=r' ↦ t]
       coeFill⁻¹ⁱ r A t := coe i r' A t


-- Equivalences
--------------------------------------------------------------------------------

isEquiv : (A → B) → U
isEquiv f :=
    (f⁻¹  : B → A)
  × (linv : ∀ a → f⁻¹ (f a) = a)
  × (rinv : ∀ b → f (f⁻¹ b) = b)
  × (coh  : ∀ a →
            Pathⁱ (f (linv a i) = f a) (rinv (f a)) (refl (f a)))

idIsEquiv : (A : U) → isEquiv (λ (a:A). a)
  _⁻¹  = λ a. a
  linv = λ a i. a
  rinv = λ b i. b
  coh  = λ a i j. a

isEquivCoe : (Γ, i ⊢ A : U) (r r' : I) → Γ ⊢ isEquiv (coeⁱ r r' A : Ar → Ar')
isEquivCoe A r r' =

  _⁻¹ := coeⁱ r' r A

  linvFill : ∀ s a → a = coeⁱ s r A (coeⁱ r s A a)
  linvFill s a = λ j. hcomᵏ r s (A r) [j=0 ↦ coeⁱ k r A (coeⁱ r k A a), j=1 ↦ a] a

  linv := linvFill r'

  rinvFill : ∀ s b → coeⁱ s r' A (coeⁱ r' s A b) = b
  rinvFill s b = λ j. hcomᵏ r' s (A r') [j=0 ↦ coeⁱ k r' A (coeⁱ r' k A b), j=1 ↦ b] b

  rinv := rinvFill r

  coh : ∀ a → PathPⁱ (f (linv a i) = f a)
                     (refl (f a)) (rinv (f a)))

  coh = TODO

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

Glue

    Γ ⊢ B : U   Γ, α ⊢ eqv : (A : U) × (f : A → B) × isEquiv f
    ──────────────────────────────────────────────────────────
                  Γ ⊢ Glue [α ↦ eqv] B : U
                 Γ, α ⊢ Glue [α ↦ eqv] B ≡ A


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

isEquiv : (A → B) → U
isEquiv A B f :=
    (g      : B → A)
  × (linv   : (x : A) → Path A (g (f x)) x)
  × (rinv   : (x : B) → Path B (f (g x)) x)
  × (coh    : (x : A) →
            PathP i (Path B (f (linv x {x}{g (f x)} i)) (f x))
                    (rinv (f x))
                    (refl B (f x)))

coeIsEquiv : (A : I → U) → (r r' : I) → isEquiv (coeⁱ r r' A : A r → A r')
coeIsEquiv A r r' =
  _⁻¹  := λ x. coe r' r A x
  linv := λ x. λ j. hcom r r' (A r)  [j=0 k. coe k r A (coe r k A x); j=1 k. x] x
  rinv := λ x. λ j. hcom r' r (A r') [j=0 k. coe k r' A (coe r' k A x); j=1 k. x] x
  coh  := TODO

-- coh :

--             PathP i (Path B (f (linv x {x}{g (f x)} i)) (f x))
--                     (rinv (f x)))
--                     (λ _. coe r r' A



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


coeⁱ r r' ((a : A) × B a) t =
  (coeⁱ r r' A t.1, coeⁱ r r' (B (coeFillⁱ r r' A t.1)) t.2)

coeⁱ r r' ((a : A) → B a) t =
  (λ (a' : A r'). coeⁱ r r' (B (coeFill⁻¹ⁱ r r' A a')) (t (coeⁱ r' r A a')))

coeⁱ r r' (Pathʲ A t u) p =
  (λ j. comⁱ r r' (A i j) [j=0 ↦ t i, j=1 ↦ u i] (p @ j))
  : Pathʲ (A[i↦r']) (t[i↦r']) (u[i↦r'])

coe r r' (i. t i ={j. A i j} u i) p =
  λ {t r'}{u r'} j. com r r' (i. A i j) [j=0 i. t i; j=1 i. u i] (p j)

coeⁱ r r' ((j : I) → A j) p =
  (λ j. coeⁱ r r' (i. A i j) (p @ j))

coeⁱ r r' ℕ t = t
coeⁱ r r' U t = t
coeⁱ r r' (Glue [α ↦ (T, f)] A) gr = TODO

hcom r r' ((a : A) × B a) [α i. t i] b =
  (  hcom r r' A [α i. (t i).1] b.1
   , com r r' (i. B (hcom r i A [α j. (t j).1] b.1)) [α i. (t i).2] b.2)

hcomⁱ r r' ((a : A) → B a) [α ↦ t] b =
  λ a. hcomⁱ r r' (B a) [α ↦ t i a] (b a)

hcom r r' (lhs ={j.A j} rhs) [α i. t i] base =
  λ j. hcom r r' (A j) [j=0 i. lhs i; j=1 i. rhs i; α i. t i j] (base j)


hcom r r' ((i : I) → B i) [α j. t] b =
  (λ arg. hcom r r' (A arg) [α i. ↦ t arg] (base arg))

hcomⁱ r r' ℕ [α ↦ zero]  zero    = zero
hcomⁱ r r' ℕ [α ↦ suc t] (suc b) = suc (hcomⁱ r r' ℕ [α ↦ t] b)
hcomⁱ r r' U [α ↦ t] b = Glue [α ↦ (t r', (coeⁱ r' r (t i), _)), r=r' ↦ (b, idEqv)] b

hcomⁱ r r' (Glue [α ↦ (T, f)] A) [β ↦ t] gr =
  glue [α ↦ hcomⁱ r r' T [β ↦ t] gr]
       (hcomⁱ r r' A [β ↦ unglue t, α ↦ f (hfillⁱ r r' T [β ↦ t] gr)] (unglue gr))


-- System
--------------------------------------------------------------------------------
- CCTT, coe, hcom, no cof disjunction
- no (∀i.α), in coeGlue we compute ∀i.α extended systems on the stop
- parameterized (strict) inductives, HITs, all single-sorted
- no indexed inductives

-- Eval
--------------------------------------------------------------------------------

- Defunctionalized closures
- Lambdas, path lambdas are closures
- CBV except for system components which are lazy
- binders that we have to match on are not closures
  - hcom and coe types are not closures
  - system components are not closures
- delayed isubst
  - no sharing of isubst forcing computation
  - eager isubst composition: isubst of isubst collapses
- in the closed eval case, hcom can lazily peel off strict inductive constructors
   (because of canonicity!!!)

-- Neutrals
--------------------------------------------------------------------------------

- Neutrals store a bitmask of blocking ivars + delayed isubst
- we collect blocking ivars during eval/forcing
- forcing a neutral:
  - if forcing sub is an injective renaming on blocking vars, then remain blocked
  - otherwise force the whole thing

NOTE:
  - Right now I don't want to collect more precise blocking info, e.g. blocking cofs.
    (potential TODO)
  - In open eval, if I get to actually force the whole hcom system because of
    a strict inductive hcom rule, I gather all base+tube blocking ivars


-- Delayed unfoldings
--------------------------------------------------------------------------------