diff --git a/FFOLCompleteness.agda b/FFOLCompleteness.agda new file mode 100644 index 0000000..a1caac2 --- /dev/null +++ b/FFOLCompleteness.agda @@ -0,0 +1,330 @@ +{-# OPTIONS --prop --rewriting #-} + +open import PropUtil + +module FFOLCompleteness where + + open import Agda.Primitive + open import FinitaryFirstOrderLogic + open import ListUtil + + record Family : Set (lsuc (ℓ¹)) where + field + World : Set ℓ¹ + _≤_ : World → World → Prop + ≤refl : {w : World} → w ≤ w + ≤tran : {w w' w'' : World} → w ≤ w' → w' ≤ w'' → w ≤ w' + TM : World → Set ℓ¹ + TM≤ : {w w' : World} → w ≤ w' → TM w → TM w' + REL : (w : World) → TM w → TM w → Prop ℓ¹ + REL≤ : {w w' : World} → {t u : TM w} → (eq : w ≤ w') → REL w t u → REL w' (TM≤ eq t) (TM≤ eq u) + infixr 10 _∘_ + Con = World → Set ℓ¹ + Sub : Con → Con → Set ℓ¹ + Sub Δ Γ = (w : World) → Δ w → Γ w + _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + α ∘ β = λ w γ → α w (β w γ) + id : {Γ : Con} → Sub Γ Γ + id = λ w γ → γ + ◇ : Con -- The initial object of the category + ◇ = λ w → ⊤ₛ + ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object + ε w Γ = ttₛ + + -- Functor Con → Set called Tm + Tm : Con → Set ℓ¹ + Tm Γ = (w : World) → (Γ w) → TM w + _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms + t [ σ ]t = λ w → λ γ → t w (σ w γ) + + -- Tm⁺ + _▹ₜ : Con → Con + Γ ▹ₜ = λ w → (Γ w) × (TM w) + πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ + πₜ¹ σ = λ w → λ x → proj×₁ (σ w x) + πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ + πₜ² σ = λ w → λ x → proj×₂ (σ w x) + _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ) + σ ,ₜ t = λ w → λ x → (σ w x) ,× (t w x) + + -- Functor Con → Set called For + For : Con → Set (lsuc ℓ¹) + For Γ = (w : World) → (Γ w) → Prop ℓ¹ + _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms + F [ σ ]f = λ w → λ x → F w (σ w x) + + -- Formulas with relation on terms + R : {Γ : Con} → Tm Γ → Tm Γ → For Γ + R t u = λ w → λ γ → REL w (t w γ) (u w γ) + + + -- Proofs + _⊢_ : (Γ : Con) → For Γ → Prop ℓ¹ + Γ ⊢ F = ∀ w (γ : Γ w) → F w γ + _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms + prf [ σ ]p = λ w → λ γ → prf w (σ w γ) + -- Equalities below are useless because Γ ⊢ F is in prop + -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf + -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p + + -- → Prop⁺ + _▹ₚ_ : (Γ : Con) → For Γ → Con + Γ ▹ₚ F = λ w → (Γ w) ×'' (F w) + πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ¹ σ w δ = proj×''₁ (σ w δ) + πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) + πₚ² σ w δ = proj×''₂ (σ w δ) + _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + _,ₚ_ {F = F} σ pf w δ = (σ w δ) ,×'' pf w δ + + + + -- Implication + _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ + F ⇒ G = λ w → λ γ → (∀ w' → w ≤ w' → (F w γ) → (G w γ)) + + -- Forall + ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ + ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t) + + -- Lam & App + lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) + lam prf = λ w γ w' s h → prf w (γ ,×'' h) + app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G + app prf prf' = λ w γ → prf w γ w ≤refl (prf' w γ) + -- Again, we don't write the _[_]p equalities as everything is in Prop + + -- ∀i and ∀e + ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) + ∀i p w γ = λ t → p w (γ ,× t) + ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) + ∀e p {t} w γ = p w γ (t w γ) + + + tod : FFOL + tod = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; ∘-ass = refl + ; id = id + ; idl = refl + ; idr = refl + ; ◇ = ◇ + ; ε = ε + ; ε-u = refl + ; Tm = Tm + ; _[_]t = _[_]t + ; []t-id = refl + ; []t-∘ = refl + ; _▹ₜ = _▹ₜ + ; πₜ¹ = πₜ¹ + ; πₜ² = πₜ² + ; _,ₜ_ = _,ₜ_ + ; πₜ²∘,ₜ = refl + ; πₜ¹∘,ₜ = refl + ; ,ₜ∘πₜ = refl + ; ,ₜ∘ = refl + ; For = For + ; _[_]f = _[_]f + ; []f-id = refl + ; []f-∘ = refl + ; _⊢_ = _⊢_ + ; _[_]p = _[_]p + ; _▹ₚ_ = _▹ₚ_ + ; πₚ¹ = πₚ¹ + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ_ + ; ,ₚ∘πₚ = refl + ; πₚ¹∘,ₚ = refl + ; ,ₚ∘ = refl + ; _⇒_ = _⇒_ + ; []f-⇒ = refl + ; ∀∀ = ∀∀ + ; []f-∀∀ = refl + ; lam = lam + ; app = app + ; ∀i = ∀i + ; ∀e = ∀e + ; R = R + ; R[] = refl + } + + record Presheaf : Set (lsuc (ℓ¹)) where + field + World : Set ℓ¹ + Arr : World → World → Set ℓ¹ -- arrows + id-a : {w : World} → Arr w w -- id arrow + _∘a_ : {w w' w'' : World} → Arr w w' → Arr w' w'' → Arr w w'' -- arrow composition + ∘a-ass : {w w' w'' w''' : World}{a : Arr w w'}{b : Arr w' w''}{c : Arr w'' w'''} + → ((a ∘a b) ∘a c) ≡ (a ∘a (b ∘a c)) + idl-a : {w w' : World} → {a : Arr w w'} → (id-a {w}) ∘a a ≡ a + idr-a : {w w' : World} → {a : Arr w w'} → a ∘a (id-a {w'}) ≡ a + TM : World → Set ℓ¹ + TM≤ : {w w' : World} → Arr w w' → TM w' → TM w + REL : (w : World) → TM w → TM w → Prop ℓ¹ + REL≤ : {w w' : World} → {t u : TM w'} → (eq : Arr w w') → REL w' t u → REL w (TM≤ eq t) (TM≤ eq u) + infixr 10 _∘_ + Con = World → Set ℓ¹ + Sub : Con → Con → Set ℓ¹ + Sub Δ Γ = (w : World) → Δ w → Γ w + _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + α ∘ β = λ w γ → α w (β w γ) + id : {Γ : Con} → Sub Γ Γ + id = λ w γ → γ + ◇ : Con -- The initial object of the category + ◇ = λ w → ⊤ₛ + ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object + ε w Γ = ttₛ + + -- Functor Con → Set called Tm + Tm : Con → Set ℓ¹ + Tm Γ = (w : World) → (Γ w) → TM w + _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms + t [ σ ]t = λ w → λ γ → t w (σ w γ) + + -- Tm⁺ + _▹ₜ : Con → Con + Γ ▹ₜ = λ w → (Γ w) × (TM w) + πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ + πₜ¹ σ = λ w → λ x → proj×₁ (σ w x) + πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ + πₜ² σ = λ w → λ x → proj×₂ (σ w x) + _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ) + σ ,ₜ t = λ w → λ x → (σ w x) ,× (t w x) + + -- Functor Con → Set called For + For : Con → Set (lsuc ℓ¹) + For Γ = (w : World) → (Γ w) → Prop ℓ¹ + _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms + F [ σ ]f = λ w → λ x → F w (σ w x) + + -- Formulas with relation on terms + R : {Γ : Con} → Tm Γ → Tm Γ → For Γ + R t u = λ w → λ γ → REL w (t w γ) (u w γ) + + + -- Proofs + _⊢_ : (Γ : Con) → For Γ → Prop ℓ¹ + Γ ⊢ F = ∀ w (γ : Γ w) → F w γ + _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms + prf [ σ ]p = λ w → λ γ → prf w (σ w γ) + -- Equalities below are useless because Γ ⊢ F is in prop + -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf + -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p + + -- → Prop⁺ + _▹ₚ_ : (Γ : Con) → For Γ → Con + Γ ▹ₚ F = λ w → (Γ w) ×'' (F w) + πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ¹ σ w δ = proj×''₁ (σ w δ) + πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) + πₚ² σ w δ = proj×''₂ (σ w δ) + _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + _,ₚ_ {F = F} σ pf w δ = (σ w δ) ,×'' pf w δ + + + + -- Implication + _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ + F ⇒ G = λ w → λ γ → (∀ w' → Arr w w' → (F w γ) → (G w γ)) + + -- Forall + ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ + ∀∀ F = λ w → λ γ → ∀ t → F w (γ ,× t) + + -- Lam & App + lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) + lam prf = λ w γ w' s h → prf w (γ ,×'' h) + app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G + app prf prf' = λ w γ → prf w γ w id-a (prf' w γ) + -- Again, we don't write the _[_]p equalities as everything is in Prop +vv + -- ∀i and ∀e + ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) + ∀i p w γ = λ t → p w (γ ,× t) + ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) + ∀e p {t} w γ = p w γ (t w γ) + + + tod : FFOL + tod = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; ∘-ass = refl + ; id = id + ; idl = refl + ; idr = refl + ; ◇ = ◇ + ; ε = ε + ; ε-u = refl + ; Tm = Tm + ; _[_]t = _[_]t + ; []t-id = refl + ; []t-∘ = refl + ; _▹ₜ = _▹ₜ + ; πₜ¹ = πₜ¹ + ; πₜ² = πₜ² + ; _,ₜ_ = _,ₜ_ + ; πₜ²∘,ₜ = refl + ; πₜ¹∘,ₜ = refl + ; ,ₜ∘πₜ = refl + ; ,ₜ∘ = refl + ; For = For + ; _[_]f = _[_]f + ; []f-id = refl + ; []f-∘ = refl + ; _⊢_ = _⊢_ + ; _[_]p = _[_]p + ; _▹ₚ_ = _▹ₚ_ + ; πₚ¹ = πₚ¹ + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ_ + ; ,ₚ∘πₚ = refl + ; πₚ¹∘,ₚ = refl + ; ,ₚ∘ = refl + ; _⇒_ = _⇒_ + ; []f-⇒ = refl + ; ∀∀ = ∀∀ + ; []f-∀∀ = refl + ; lam = lam + ; app = app + ; ∀i = ∀i + ; ∀e = ∀e + ; R = R + ; R[] = refl + } + + -- Completeness proof + + -- We first build our universal Kripke model + + module ComplenessProof where + + -- We have a model, we construct the Universal Presheaf model of this model + import FFOLInitial as I + + UniversalPresheaf : Presheaf + UniversalPresheaf = record + { World = I.Con + ; Arr = I.Sub + ; id-a = I.id + ; _∘a_ = λ σ σ' → σ' I.∘ σ + ; ∘a-ass = ≡sym I.∘-ass + ; idl-a = I.idr + ; idr-a = I.idl + ; TM = λ Γ → I.Tm (I.Con.t Γ) + ; TM≤ = λ σ t → t I.[ I.Sub.t σ ]t + ; REL = λ Γ t u → I.Pf Γ (I.r t u) + ; REL≤ = λ σ pf → (pf I.[ I.Sub.t σ ]pₜ) I.[ I.Sub.p σ ]p + } + + -- I.xx are from initial, xx are from up + open Presheaf UniversalPresheaf + + -- Now we want to show universality of this model, that is + -- if you have a proof in UP, you have the same in I. + + q : {Γ : Con}{A : For Γ} → Γ ⊢ A → I.Pf {!!} {!!} + u : {Γ : Con}{A : For Γ} → I.Pf {!!} {!!} → Γ ⊢ A diff --git a/FFOLInitial.agda b/FFOLInitial.agda new file mode 100644 index 0000000..2bf0162 --- /dev/null +++ b/FFOLInitial.agda @@ -0,0 +1,550 @@ +{-# OPTIONS --prop --rewriting #-} + +open import PropUtil + +module FFOLInitial where + + open import FinitaryFirstOrderLogic + open import Agda.Primitive + open import ListUtil + + -- First definition of terms and term contexts -- + data Cont : Set₁ where + ◇t : Cont + _▹t⁰ : Cont → Cont + variable + Γₜ Δₜ Ξₜ : Cont + data TmVar : Cont → Set₁ where + tvzero : TmVar (Γₜ ▹t⁰) + tvnext : TmVar Γₜ → TmVar (Γₜ ▹t⁰) + + data Tm : Cont → Set₁ where + var : TmVar Γₜ → Tm Γₜ + + -- Now we can define formulæ + data For : Cont → Set₁ where + r : Tm Γₜ → Tm Γₜ → For Γₜ + _⇒_ : For Γₜ → For Γₜ → For Γₜ + ∀∀ : For (Γₜ ▹t⁰) → For Γₜ + + -- Then we define term substitutions, and the application of them on terms and formulæ + data Subt : Cont → Cont → Set₁ where + εₜ : Subt Γₜ ◇t + _,ₜ_ : Subt Δₜ Γₜ → Tm Δₜ → Subt Δₜ (Γₜ ▹t⁰) + + -- We subst on terms + _[_]t : Tm Γₜ → Subt Δₜ Γₜ → Tm Δₜ + var tvzero [ σ ,ₜ t ]t = t + var (tvnext tv) [ σ ,ₜ t ]t = var tv [ σ ]t + + -- We define liftings on term variables + -- A term of n variables is a term of n+1 variables + -- Same for a term array + wkₜt : Tm Γₜ → Tm (Γₜ ▹t⁰) + + wkₜt (var tv) = var (tvnext tv) + + -- From a substition into n variables, we get a substitution into n+1 variables which don't use the last one + wkₜσt : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) Γₜ + wkₜσt εₜ = εₜ + wkₜσt (σ ,ₜ t) = (wkₜσt σ) ,ₜ (wkₜt t) + wkₜσt-wkₜt : {tv : TmVar Γₜ} → {σ : Subt Δₜ Γₜ} → wkₜt (var tv [ σ ]t) ≡ var tv [ wkₜσt σ ]t + wkₜσt-wkₜt {tv = tvzero} {σ = σ ,ₜ x} = refl + wkₜσt-wkₜt {tv = tvnext tv} {σ = σ ,ₜ x} = wkₜσt-wkₜt {tv = tv} {σ = σ} + + -- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself + -- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1 + liftₜσ : Subt Δₜ Γₜ → Subt (Δₜ ▹t⁰) (Γₜ ▹t⁰) + liftₜσ σ = (wkₜσt σ) ,ₜ (var tvzero) + + + -- We subst on formulæ + _[_]f : For Γₜ → Subt Δₜ Γₜ → For Δₜ + (r t u) [ σ ]f = r (t [ σ ]t) (u [ σ ]t) + (A ⇒ B) [ σ ]f = (A [ σ ]f) ⇒ (B [ σ ]f) + (∀∀ A) [ σ ]f = ∀∀ (A [ liftₜσ σ ]f) + + -- We now can define identity on term substitutions + idₜ : Subt Γₜ Γₜ + idₜ {◇t} = εₜ + idₜ {Γₜ ▹t⁰} = liftₜσ (idₜ {Γₜ}) + + _∘ₜ_ : Subt Δₜ Γₜ → Subt Ξₜ Δₜ → Subt Ξₜ Γₜ + εₜ ∘ₜ β = εₜ + (α ,ₜ x) ∘ₜ β = (α ∘ₜ β) ,ₜ (x [ β ]t) + + + -- We have the access functions from the algebra, in restricted versions + πₜ¹ : Subt Δₜ (Γₜ ▹t⁰) → Subt Δₜ Γₜ + πₜ¹ (σₜ ,ₜ t) = σₜ + πₜ² : Subt Δₜ (Γₜ ▹t⁰) → Tm Δₜ + πₜ² (σₜ ,ₜ t) = t + + -- And their equalities (the fact that there are reciprocical) + πₜ²∘,ₜ : {σₜ : Subt Δₜ Γₜ} → {t : Tm Δₜ} → πₜ² (σₜ ,ₜ t) ≡ t + πₜ²∘,ₜ = refl + πₜ¹∘,ₜ : {σₜ : Subt Δₜ Γₜ} → {t : Tm Δₜ} → πₜ¹ (σₜ ,ₜ t) ≡ σₜ + πₜ¹∘,ₜ = refl + ,ₜ∘πₜ : {σₜ : Subt Δₜ (Γₜ ▹t⁰)} → (πₜ¹ σₜ) ,ₜ (πₜ² σₜ) ≡ σₜ + ,ₜ∘πₜ {σₜ = σₜ ,ₜ t} = refl + + -- We can also prove the substitution equalities + []t-id : {t : Tm Γₜ} → t [ idₜ {Γₜ} ]t ≡ t + []t-id {Γₜ ▹t⁰} {var tvzero} = refl + []t-id {Γₜ ▹t⁰} {var (tvnext tv)} = substP (λ t → t ≡ var (tvnext tv)) (wkₜσt-wkₜt {tv = tv} {σ = idₜ}) (substP (λ t → wkₜt t ≡ var (tvnext tv)) (≡sym ([]t-id {t = var tv})) refl) + []t-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {t : Tm Γₜ} → t [ β ∘ₜ α ]t ≡ (t [ β ]t) [ α ]t + []t-∘ {α = α} {β = β ,ₜ t} {t = var tvzero} = refl + []t-∘ {α = α} {β = β ,ₜ t} {t = var (tvnext tv)} = []t-∘ {t = var tv} + []f-id : {F : For Γₜ} → F [ idₜ {Γₜ} ]f ≡ F + []f-id {F = r t u} = cong₂ r []t-id []t-id + []f-id {F = F ⇒ G} = cong₂ _⇒_ []f-id []f-id + []f-id {F = ∀∀ F} = cong ∀∀ []f-id + wkₜσt-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → wkₜσt (β ∘ₜ α) ≡ (wkₜσt β ∘ₜ liftₜσ α) + wkₜt[] : {α : Subt Δₜ Γₜ} → {t : Tm Γₜ} → wkₜt (t [ α ]t) ≡ (wkₜt t [ liftₜσ α ]t) + wkₜσt-∘ {β = εₜ} = refl + wkₜσt-∘ {β = β ,ₜ t} = cong₂ _,ₜ_ wkₜσt-∘ (wkₜt[] {t = t}) + wkₜt[] {α = α ,ₜ t} {var tvzero} = refl + wkₜt[] {α = α ,ₜ t} {var (tvnext tv)} = wkₜt[] {t = var tv} + liftₜσ-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → liftₜσ (β ∘ₜ α) ≡ (liftₜσ β) ∘ₜ (liftₜσ α) + liftₜσ-∘ {α = α} {β = εₜ} = refl + liftₜσ-∘ {α = α} {β = β ,ₜ t} = cong₂ _,ₜ_ (cong₂ _,ₜ_ wkₜσt-∘ (wkₜt[] {t = t})) refl + []f-∘ : {α : Subt Ξₜ Δₜ} → {β : Subt Δₜ Γₜ} → {F : For Γₜ} → F [ β ∘ₜ α ]f ≡ (F [ β ]f) [ α ]f + []f-∘ {α = α} {β = β} {F = r t u} = cong₂ r ([]t-∘ {α = α} {β = β} {t = t}) ([]t-∘ {α = α} {β = β} {t = u}) + []f-∘ {F = F ⇒ G} = cong₂ _⇒_ []f-∘ []f-∘ + []f-∘ {F = ∀∀ F} = cong ∀∀ (≡tran (cong (λ σ → F [ σ ]f) liftₜσ-∘) []f-∘) + R[] : {σ : Subt Δₜ Γₜ} → {t u : Tm Γₜ} → (r t u) [ σ ]f ≡ r (t [ σ ]t) (u [ σ ]t) + R[] = refl + lem3 : {α : Subt Γₜ Δₜ} → {β : Subt Ξₜ Γₜ} → α ∘ₜ (wkₜσt β) ≡ wkₜσt (α ∘ₜ β) + lem3 {α = εₜ} = refl + lem3 {α = α ,ₜ var tv} = cong₂ _,ₜ_ (lem3 {α = α}) (≡sym (wkₜσt-wkₜt {tv = tv})) + wk[,] : {t : Tm Γₜ}{u : Tm Δₜ}{β : Subt Δₜ Γₜ} → (wkₜt t) [ β ,ₜ u ]t ≡ t [ β ]t + wk[,] {t = var tvzero} = refl + wk[,] {t = var (tvnext tv)} = refl + wk∘, : {α : Subt Γₜ Δₜ}{β : Subt Ξₜ Γₜ}{t : Tm Ξₜ} → (wkₜσt α) ∘ₜ (β ,ₜ t) ≡ (α ∘ₜ β) + wk∘, {α = εₜ} = refl + wk∘, {α = α ,ₜ t} {β = β} = cong₂ _,ₜ_ (wk∘, {α = α}) (wk[,] {t = t} {β = β}) + σ-idl : {α : Subt Δₜ Γₜ} → idₜ ∘ₜ α ≡ α + σ-idl {α = εₜ} = refl + σ-idl {α = α ,ₜ x} = cong₂ _,ₜ_ (≡tran wk∘, σ-idl) refl + σ-idr : {α : Subt Δₜ Γₜ} → α ∘ₜ idₜ ≡ α + σ-idr {α = εₜ} = refl + σ-idr {α = α ,ₜ x} = cong₂ _,ₜ_ σ-idr []t-id + ∘ₜ-ass : {Γₜ Δₜ Ξₜ Ψₜ : Cont}{α : Subt Γₜ Δₜ}{β : Subt Δₜ Ξₜ}{γ : Subt Ξₜ Ψₜ} → (γ ∘ₜ β) ∘ₜ α ≡ γ ∘ₜ (β ∘ₜ α) + ∘ₜ-ass {α = α} {β} {εₜ} = refl + ∘ₜ-ass {α = α} {β} {γ ,ₜ x} = cong₂ _,ₜ_ ∘ₜ-ass (≡sym ([]t-∘ {t = x})) + []f-∀∀ : {A : For (Γₜ ▹t⁰)} → {σₜ : Subt Δₜ Γₜ} → (∀∀ A) [ σₜ ]f ≡ (∀∀ (A [ (σₜ ∘ₜ πₜ¹ idₜ) ,ₜ πₜ² idₜ ]f)) + []f-∀∀ {A = A} = cong ∀∀ (cong (_[_]f A) (cong₂ _,ₜ_ (≡tran (cong wkₜσt (≡sym σ-idr)) (≡sym lem3)) refl)) + εₜ-u : {σₜ : Subt Γₜ ◇t} → σₜ ≡ εₜ + εₜ-u {σₜ = εₜ} = refl + + data Conp : Cont → Set₁ -- pu tit in Prop + variable + Γₚ Γₚ' : Conp Γₜ + Δₚ Δₚ' : Conp Δₜ + Ξₚ : Conp Ξₜ + + data Conp where + ◇p : Conp Γₜ + _▹p⁰_ : Conp Γₜ → For Γₜ → Conp Γₜ + + record Con : Set₁ where + constructor con + field + t : Cont + p : Conp t + + ◇ : Con + ◇ = con ◇t ◇p + + + _▹p_ : (Γ : Con) → For (Con.t Γ) → Con + Γ ▹p A = con (Con.t Γ) (Con.p Γ ▹p⁰ A) + + variable + Γ Δ Ξ : Con + + + + -- We can add term, that will not be used in the formulæ already present + -- (that's why we use wkₜσt) + _▹tp : Conp Γₜ → Conp (Γₜ ▹t⁰) + ◇p ▹tp = ◇p + (Γₚ ▹p⁰ A) ▹tp = (Γₚ ▹tp) ▹p⁰ (A [ wkₜσt idₜ ]f) + + _▹t : Con → Con + Γ ▹t = con ((Con.t Γ) ▹t⁰) (Con.p Γ ▹tp) + + data PfVar : (Γ : Con) → For (Con.t Γ) → Set₁ where + pvzero : {A : For (Con.t Γ)} → PfVar (Γ ▹p A) A + pvnext : {A B : For (Con.t Γ)} → PfVar Γ A → PfVar (Γ ▹p B) A + + data Pf : (Γ : Con) → For (Con.t Γ) → Prop₁ where + var : {A : For (Con.t Γ)} → PfVar Γ A → Pf Γ A + app : {A B : For (Con.t Γ)} → Pf Γ (A ⇒ B) → Pf Γ A → Pf Γ B + lam : {A B : For (Con.t Γ)} → Pf (Γ ▹p A) B → Pf Γ (A ⇒ B) + p∀∀e : {A : For ((Con.t Γ) ▹t⁰)} → {t : Tm (Con.t Γ)} → Pf Γ (∀∀ A) → Pf Γ (A [ idₜ ,ₜ t ]f) + p∀∀i : {A : For (Con.t (Γ ▹t))} → Pf (Γ ▹t) A → Pf Γ (∀∀ A) + + + data Subp : {Δₜ : Cont} → Conp Δₜ → Conp Δₜ → Set₁ where + εₚ : Subp Δₚ ◇p + _,ₚ_ : {A : For Δₜ} → (σ : Subp Δₚ Δₚ') → Pf (con Δₜ Δₚ) A → Subp Δₚ (Δₚ' ▹p⁰ A) + + + _[_]c : Conp Γₜ → Subt Δₜ Γₜ → Conp Δₜ + ◇p [ σₜ ]c = ◇p + (Γₚ ▹p⁰ A) [ σₜ ]c = (Γₚ [ σₜ ]c) ▹p⁰ (A [ σₜ ]f) + + []c-id : Γₚ [ idₜ ]c ≡ Γₚ + []c-id {Γₚ = ◇p} = refl + []c-id {Γₚ = Γₚ ▹p⁰ x} = cong₂ _▹p⁰_ []c-id []f-id + + []c-∘ : {α : Subt Δₜ Ξₜ} {β : Subt Γₜ Δₜ} {Ξₚ : Conp Ξₜ} → Ξₚ [ α ∘ₜ β ]c ≡ (Ξₚ [ α ]c) [ β ]c + []c-∘ {α = α} {β = β} {◇p} = refl + []c-∘ {α = α} {β = β} {Ξₚ ▹p⁰ A} = cong₂ _▹p⁰_ []c-∘ []f-∘ + + + record Sub (Γ : Con) (Δ : Con) : Set₁ where + constructor sub + field + t : Subt (Con.t Γ) (Con.t Δ) + p : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ t ]c) + + -- An order on contexts, where we can only change positions + infixr 5 _∈ₚ*_ + data _∈ₚ*_ : Conp Γₜ → Conp Γₜ → Set₁ where + zero∈ₚ* : ◇p ∈ₚ* Γₚ + next∈ₚ* : {A : For Δₜ} → PfVar (con Δₜ Δₚ) A → Δₚ' ∈ₚ* Δₚ → (Δₚ' ▹p⁰ A) ∈ₚ* Δₚ + -- Allows to grow ∈ₚ* to the right + right∈ₚ* :{A : For Δₜ} → Γₚ ∈ₚ* Δₚ → Γₚ ∈ₚ* (Δₚ ▹p⁰ A) + right∈ₚ* zero∈ₚ* = zero∈ₚ* + right∈ₚ* (next∈ₚ* x h) = next∈ₚ* (pvnext x) (right∈ₚ* h) + both∈ₚ* : {A : For Γₜ} → Γₚ ∈ₚ* Δₚ → (Γₚ ▹p⁰ A) ∈ₚ* (Δₚ ▹p⁰ A) + both∈ₚ* zero∈ₚ* = next∈ₚ* pvzero zero∈ₚ* + both∈ₚ* (next∈ₚ* x h) = next∈ₚ* pvzero (next∈ₚ* (pvnext x) (right∈ₚ* h)) + refl∈ₚ* : Γₚ ∈ₚ* Γₚ + refl∈ₚ* {Γₚ = ◇p} = zero∈ₚ* + refl∈ₚ* {Γₚ = Γₚ ▹p⁰ x} = both∈ₚ* refl∈ₚ* + + ∈ₚ▹tp : {A : For Δₜ} → PfVar (con Δₜ Δₚ) A → PfVar (con Δₜ Δₚ ▹t) (A [ wkₜσt idₜ ]f) + ∈ₚ▹tp pvzero = pvzero + ∈ₚ▹tp (pvnext x) = pvnext (∈ₚ▹tp x) + ∈ₚ*▹tp : Γₚ ∈ₚ* Δₚ → (Γₚ ▹tp) ∈ₚ* (Δₚ ▹tp) + ∈ₚ*▹tp zero∈ₚ* = zero∈ₚ* + ∈ₚ*▹tp (next∈ₚ* x s) = next∈ₚ* (∈ₚ▹tp x) (∈ₚ*▹tp s) + + mon∈ₚ∈ₚ* : {A : For Δₜ} → PfVar (con Δₜ Δₚ') A → Δₚ' ∈ₚ* Δₚ → PfVar (con Δₜ Δₚ) A + mon∈ₚ∈ₚ* pvzero (next∈ₚ* x x₁) = x + mon∈ₚ∈ₚ* (pvnext s) (next∈ₚ* x x₁) = mon∈ₚ∈ₚ* s x₁ + + ∈ₚ*→Sub : Δₚ ∈ₚ* Δₚ' → Subp {Δₜ} Δₚ' Δₚ + ∈ₚ*→Sub zero∈ₚ* = εₚ + ∈ₚ*→Sub (next∈ₚ* x s) = ∈ₚ*→Sub s ,ₚ var x + + + wkₚp : {A : For Δₜ} → Δₚ ∈ₚ* Δₚ' → Pf (con Δₜ Δₚ) A → Pf (con Δₜ Δₚ') A + wkₚp s (var pv) = var (mon∈ₚ∈ₚ* pv s) + wkₚp s (app pf pf₁) = app (wkₚp s pf) (wkₚp s pf₁) + wkₚp s (lam {A = A} pf) = lam (wkₚp (both∈ₚ* s) pf) + wkₚp s (p∀∀e pf) = p∀∀e (wkₚp s pf) + wkₚp s (p∀∀i pf) = p∀∀i (wkₚp (∈ₚ*▹tp s) pf) + lliftₚ : {Γₚ : Conp Δₜ} → Δₚ ∈ₚ* Δₚ' → Subp {Δₜ} Δₚ Γₚ → Subp {Δₜ} Δₚ' Γₚ + lliftₚ s εₚ = εₚ + lliftₚ s (σₚ ,ₚ pf) = lliftₚ s σₚ ,ₚ wkₚp s pf + + wkₚσt : {Δₜ : Cont} {Δₚ Γₚ : Conp Δₜ}{A : For Δₜ} → Subp {Δₜ} Δₚ Γₚ → Subp {Δₜ} (Δₚ ▹p⁰ A) Γₚ + wkₚσt εₚ = εₚ + wkₚσt (σₚ ,ₚ pf) = (wkₚσt σₚ) ,ₚ wkₚp (right∈ₚ* refl∈ₚ*) pf + --wkₜσt-wkₜt : {tv : TmVar Γₜ} → {σ : Subt Δₜ Γₜ} → wkₜt (var tv [ σ ]t) ≡ var tv [ wkₜσt σ ]t + --wkₜσt-wkₜt {tv = tvzero} {σ = σ ,ₜ x} = refl + --wkₜσt-wkₜt {tv = tvnext tv} {σ = σ ,ₜ x} = wkₜσt-wkₜt {tv = tv} {σ = σ} + + -- From a substitution into n variables, we construct a substitution from n+1 variables to n+1 variables which maps it to itself + -- i.e. 0 -> 0 and for all i ->(old) σ(i) we get i+1 -> σ(i)+1 + liftₚσ : {Δₜ : Cont}{Δₚ Γₚ : Conp Δₜ}{A : For Δₜ} → Subp {Δₜ} Δₚ Γₚ → Subp {Δₜ} (Δₚ ▹p⁰ A) (Γₚ ▹p⁰ A) + liftₚσ σ = (wkₚσt σ) ,ₚ (var pvzero) + + idₚ : Subp {Δₜ} Δₚ Δₚ + idₚ {Δₚ = ◇p} = εₚ + idₚ {Δₚ = Δₚ ▹p⁰ x} = liftₚσ (idₚ {Δₚ = Δₚ}) + + + + + + + + + + lem7 : {σ : Subt Δₜ Γₜ} → ((Δₚ ▹tp) [ liftₜσ σ ]c) ≡ ((Δₚ [ σ ]c) ▹tp) + lem7 {Δₚ = ◇p} = refl + lem7 {Δₚ = Δₚ ▹p⁰ A} = cong₂ _▹p⁰_ lem7 (≡tran² (≡sym []f-∘) (cong (λ σ → A [ σ ]f) (≡tran² (≡sym wkₜσt-∘) (cong wkₜσt (≡tran σ-idl (≡sym σ-idr))) (≡sym lem3))) []f-∘) + lem8 : {σ : Subt Δₜ Γₜ} {t : Tm Γₜ} → ((wkₜσt σ ∘ₜ (idₜ ,ₜ (t [ σ ]t))) ,ₜ (t [ σ ]t)) ≡ ((idₜ ∘ₜ σ) ,ₜ (t [ σ ]t)) + lem8 = cong₂ _,ₜ_ (≡tran² wk∘, σ-idr (≡sym σ-idl)) refl + + _[_]pvₜ : {A : For Δₜ} → PfVar (con Δₜ Δₚ) A → (σ : Subt Γₜ Δₜ) → PfVar (con Γₜ (Δₚ [ σ ]c)) (A [ σ ]f) + _[_]pₜ : {A : For Δₜ} → Pf (con Δₜ Δₚ) A → (σ : Subt Γₜ Δₜ) → Pf (con Γₜ (Δₚ [ σ ]c)) (A [ σ ]f) + pvzero [ σ ]pvₜ = pvzero + pvnext pv [ σ ]pvₜ = pvnext (pv [ σ ]pvₜ) + var pv [ σ ]pₜ = var (pv [ σ ]pvₜ) + app pf pf' [ σ ]pₜ = app (pf [ σ ]pₜ) (pf' [ σ ]pₜ) + lam pf [ σ ]pₜ = lam (pf [ σ ]pₜ) + _[_]pₜ {Δₚ = Δₚ} {Γₜ = Γₜ} (p∀∀e {A = A} {t = t} pf) σ = substP (λ F → Pf (con Γₜ (Δₚ [ σ ]c)) F) (≡tran² (≡sym []f-∘) (cong (λ σ → A [ σ ]f) (lem8 {t = t})) ([]f-∘)) (p∀∀e {t = t [ σ ]t} (pf [ σ ]pₜ)) + _[_]pₜ {Γₜ = Γₜ} (p∀∀i pf) σ = p∀∀i (substP (λ Ξₚ → Pf (con (Γₜ ▹t⁰) (Ξₚ)) _) lem7 (pf [ liftₜσ σ ]pₜ)) + + _[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c) + εₚ [ σₜ ]σₚ = εₚ + (σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ) + + lem9 : (Δₚ [ wkₜσt idₜ ]c) ≡ (Δₚ ▹tp) + lem9 {Δₚ = ◇p} = refl + lem9 {Δₚ = Δₚ ▹p⁰ x} = cong₂ _▹p⁰_ lem9 refl + wkₜσₚ : Subp {Δₜ} Δₚ' Δₚ → Subp {Δₜ ▹t⁰} (Δₚ' ▹tp) (Δₚ ▹tp) + wkₜσₚ εₚ = εₚ + wkₜσₚ {Δₜ = Δₜ} (_,ₚ_ {A = A} σₚ pf) = (wkₜσₚ σₚ) ,ₚ substP (λ Ξₚ → Pf (con (Δₜ ▹t⁰) Ξₚ) (A [ wkₜσt idₜ ]f)) lem9 (_[_]pₜ {Γₜ = Δₜ ▹t⁰} pf (wkₜσt idₜ)) + + _[_]p : {A : For Δₜ} → Pf (con Δₜ Δₚ) A → (σ : Subp {Δₜ} Δₚ' Δₚ) → Pf (con Δₜ Δₚ') A + var pvzero [ σ ,ₚ pf ]p = pf + var (pvnext pv) [ σ ,ₚ pf ]p = var pv [ σ ]p + app pf pf₁ [ σ ]p = app (pf [ σ ]p) (pf₁ [ σ ]p) + lam pf [ σ ]p = lam (pf [ lliftₚ (right∈ₚ* refl∈ₚ*) σ ,ₚ var pvzero ]p) + p∀∀e pf [ σ ]p = p∀∀e (pf [ σ ]p) + p∀∀i pf [ σ ]p = p∀∀i (pf [ wkₜσₚ σ ]p) + + + _∘ₚ_ : {Γₚ Δₚ Ξₚ : Conp Δₜ} → Subp {Δₜ} Δₚ Ξₚ → Subp {Δₜ} Γₚ Δₚ → Subp {Δₜ} Γₚ Ξₚ + εₚ ∘ₚ β = εₚ + (α ,ₚ pf) ∘ₚ β = (α ∘ₚ β) ,ₚ (pf [ β ]p) + ε-u : {Γₚ : Conp Γₜ} → {σ : Subp Γₚ ◇p} → σ ≡ εₚ {Δₚ = Γₚ} + ε-u {σ = εₚ} = refl + lemJ : {Δₜ : Cont}{Δₚ : Conp Δₜ}{A : For Δₜ} → Pf (con Δₜ Δₚ) A → (Pf (con Δₜ (Δₚ [ idₜ ]c)) (A [ idₜ ]f)) + lemJ {Δₜ}{Δₚ}{A} pf = substP (Pf (con Δₜ (Δₚ [ idₜ ]c))) (≡sym []f-id) (substP (λ Ξₚ → Pf (con Δₜ Ξₚ) A) (≡sym []c-id) pf) + []σₚ-id : {σₚ : Subp {Δₜ} Δₚ Δₚ'} → coe (cong₂ Subp []c-id []c-id) (σₚ [ idₜ ]σₚ) ≡ σₚ + []σₚ-id {σₚ = εₚ} = ε-u + []σₚ-id {Δₜ}{Δₚ}{Δₚ' ▹p⁰ A} {σₚ = σₚ ,ₚ x} = substP (λ ξ → coe (cong₂ Subp []c-id []c-id) (ξ ,ₚ (x [ idₜ ]pₜ)) ≡ (σₚ ,ₚ x)) (≡sym (coeshift ([]σₚ-id))) + (≡sym (coeshift {eq = cong₂ Subp (≡sym []c-id) (≡sym []c-id)} + (substfpoly'' {A = (Conp Δₜ) × (Conp Δₜ)}{P = λ W F → Subp (proj×₁ W) ((proj×₂ W) ▹p⁰ F)}{R = λ W → Subp (proj×₁ W) (proj×₂ W)}{Q = λ W F → Pf (con Δₜ (proj×₁ W)) F}{α = Δₚ ,× Δₚ'}{ε = A}{eq = ×≡ (≡sym []c-id) (≡sym []c-id)}{eq'' = ≡sym []f-id}{f = λ {W} {F} ξ pf → _,ₚ_ ξ pf}{x = σₚ}{y = x}))) + []σₚ-∘ : {Ξₚ Ξₚ' : Conp Ξₜ}{α : Subt Δₜ Ξₜ} {β : Subt Γₜ Δₜ} {σₚ : Subp {Ξₜ} Ξₚ Ξₚ'} + --{eq₅ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)} + → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((σₚ [ α ]σₚ) [ β ]σₚ) ≡ σₚ [ α ∘ₜ β ]σₚ + []σₚ-∘ {σₚ = εₚ} = ε-u + []σₚ-∘ {Ξₜ}{Δₜ}{Γₜ}{Ξₚ}{Δₚ' ▹p⁰ A}{α}{β}{σₚ = σₚ ,ₚ pf} = + substP (λ ξ → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) (ξ ,ₚ ((pf [ α ]pₜ) [ β ]pₜ)) ≡ ((σₚ [ α ∘ₜ β ]σₚ) ,ₚ (pf [ α ∘ₜ β ]pₜ))) (≡sym (coeshift []σₚ-∘)) + (≡sym (coeshift {eq = cong₂ Subp []c-∘ []c-∘} + (substfpoly'' + {A = (Conp Γₜ) × (Conp Γₜ)} + {P = λ W F → Subp (proj×₁ W) ((proj×₂ W) ▹p⁰ F)} + {R = λ W → Subp (proj×₁ W) (proj×₂ W)} + {Q = λ W F → Pf (con Γₜ (proj×₁ W)) F} + {eq = cong₂ _,×_ []c-∘ []c-∘} + {eq'' = []f-∘ {α = β} {β = α} {F = A}} + {f = λ {W} {F} ξ pf → _,ₚ_ ξ pf}{x = σₚ [ α ∘ₜ β ]σₚ}{y = pf [ α ∘ₜ β ]pₜ}) + )) + wkₚ∘, : {Δₜ : Cont}{Γₚ Δₚ Ξₚ : Conp Δₜ}{α : Subp {Δₜ} Γₚ Δₚ}{β : Subp {Δₜ} Ξₚ Γₚ}{A : For Δₜ}{pf : Pf (con Δₜ Ξₚ) A} → (wkₚσt α) ∘ₚ (β ,ₚ pf) ≡ (α ∘ₚ β) + wkₚ∘, {α = εₚ} = refl + wkₚ∘, {α = α ,ₚ pf} {β = β} {pf = pf'} = cong (λ ξ → ξ ,ₚ (pf [ β ]p)) wkₚ∘, + idlₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → (idₚ {Δₚ = Δₚ}) ∘ₚ σₚ ≡ σₚ + idlₚ {Δₚ = ◇p} {εₚ} = refl + idlₚ {Δₚ = Δₚ ▹p⁰ pf} {σₚ ,ₚ pf'} = cong (λ ξ → ξ ,ₚ pf') (≡tran wkₚ∘, (idlₚ {σₚ = σₚ})) + idrₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → σₚ ∘ₚ (idₚ {Δₚ = Γₚ}) ≡ σₚ + idrₚ {σₚ = εₚ} = refl + idrₚ {σₚ = σₚ ,ₚ prf} = cong (λ X → X ,ₚ prf) (idrₚ {σₚ = σₚ}) + wkₚ[] : {σₜ : Subt Γₜ Δₜ} {σₚ : Subp Δₚ Δₚ'} {A : For Δₜ} → (wkₚσt {A = A} σₚ) [ σₜ ]σₚ ≡ wkₚσt (σₚ [ σₜ ]σₚ) + wkₚ[] {σₚ = εₚ} = refl + wkₚ[] {σₚ = σₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ _) (wkₚ[] {σₚ = σₚ}) + idₚ[] : {σₜ : Subt Γₜ Δₜ} → ((idₚ {Δₜ} {Δₚ}) [ σₜ ]σₚ) ≡ idₚ {Γₜ} {Δₚ [ σₜ ]c} + idₚ[] {Δₚ = ◇p} = refl + idₚ[] {Δₚ = Δₚ ▹p⁰ A} = cong (λ ξ → ξ ,ₚ var pvzero) (≡tran wkₚ[] (cong wkₚσt idₚ[])) + + + id : Sub Γ Γ + id {Γ} = sub idₜ (subst (Subp _) (≡sym []c-id) idₚ) + _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (subst (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ) + idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ + idl {Δ = Δ} {σ = sub σₜ σₚ} = cong₂' sub σ-idl (≡tran (substfpoly {α = ((Con.p Δ) [ idₜ ∘ₜ σₜ ]c)} {β = ((Con.p Δ) [ σₜ ]c)} {eq = cong (λ ξ → Con.p Δ [ ξ ]c) σ-idl} {f = λ {Ξₚ} ξ → _∘ₚ_ {Ξₚ = Ξₚ} ξ σₚ}) (≡tran (cong₂ _∘ₚ_ (≡tran³ coecoe-coe (substfpoly {eq = []c-id} {f = λ {Ξₚ} ξ → _[_]σₚ {Δₚ = Con.p Δ} {Δₚ' = Ξₚ} ξ σₜ}) (cong (λ ξ → ξ [ σₜ ]σₚ) coeaba) idₚ[]) refl) idlₚ)) + lemK : {Γ Δ : Con}{σₜ : Subt (Con.t Γ) (Con.t Δ)}{σₚ : Subp (Con.p Γ [ idₜ ]c) ((Con.p Δ [ σₜ ]c)[ idₜ ]c)} + {eq1 : Subp (Con.p Γ) ((Con.p Δ [ σₜ ]c) [ idₜ ]c) ≡ Subp (Con.p Γ) (Con.p Δ [ σₜ ]c)} + {eq2 : Subp (Con.p Γ) (Con.p Γ) ≡ Subp (Con.p Γ) (Con.p Γ [ idₜ ]c)} + {eq3 : Subp (Con.p Γ [ idₜ ]c) ((Con.p Δ [ σₜ ]c)[ idₜ ]c) ≡ Subp (Con.p Γ) (Con.p Δ [ σₜ ]c)} + → coe eq1 (σₚ ∘ₚ coe eq2 idₚ) + ≡ (coe eq3 σₚ ∘ₚ idₚ) + lemK {Γ}{Δ}{σₚ = σₚ}{eq1}{eq2}{eq3} = substP (λ X → coe eq1 (X ∘ₚ coe eq2 idₚ) ≡ (coe eq3 σₚ ∘ₚ idₚ)) (coeaba {eq1 = eq3}{eq2 = ≡sym eq3}) (coep∘ {p = λ {Γₚ}{Δₚ}{Ξₚ} x y → _∘ₚ_ {Δₚ = Γₚ} x y} {eq1 = refl}{eq2 = ≡sym []c-id}{eq3 = ≡sym []c-id}) + idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ + idr {Γ} {Δ} {σ = sub σₜ σₚ} = cong₂' sub σ-idr (≡tran⁴ (cong (coe _) (≡sym (substfpoly {eq = ≡sym ([]c-∘ {α = σₜ} {β = idₜ}{Ξₚ = Con.p Δ})} {f = λ {Ξₚ} ξ → _∘ₚ_ {Ξₚ = Ξₚ} ξ (coe (cong (Subp (Con.p Γ)) (≡sym []c-id)) idₚ)} {x = σₚ [ idₜ ]σₚ}))) coecoe-coe lemK idrₚ []σₚ-id) + ∘ₚ-ass : {Γₚ Δₚ Ξₚ Ψₚ : Conp Γₜ}{αₚ : Subp Γₚ Δₚ}{βₚ : Subp Δₚ Ξₚ}{γₚ : Subp Ξₚ Ψₚ} → (γₚ ∘ₚ βₚ) ∘ₚ αₚ ≡ γₚ ∘ₚ (βₚ ∘ₚ αₚ) + ∘ₚ-ass {γₚ = εₚ} = refl + ∘ₚ-ass {αₚ = αₚ} {βₚ} {γₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ (x [ βₚ ∘ₚ αₚ ]p)) ∘ₚ-ass + + lemG' : + {Γₜ Δₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Δₜ}{Ψₚ : Conp Δₜ} + {αₜ : Subt Γₜ Δₜ}{γₚ : Subp Ξₚ Ψₚ}{βₚ : Subp Δₚ Ξₚ}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)} + → ((γₚ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ ≡ (γₚ [ αₜ ]σₚ) ∘ₚ ((βₚ [ αₜ ]σₚ) ∘ₚ αₚ) + lemG' {γₚ = εₚ} = refl + lemG' {αₜ = αₜ}{γₚ ,ₚ x}{βₚ}{αₚ} = cong (λ ξ → ξ ,ₚ (((x [ βₚ ]p) [ αₜ ]pₜ) [ αₚ ]p)) (lemG' {γₚ = γₚ}) + lemG : + {Γₜ Δₜ Ξₜ Ψₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{Ψₚ : Conp Ψₜ} + {αₜ : Subt Γₜ Δₜ}{βₜ : Subt Δₜ Ξₜ}{γₜ : Subt Ξₜ Ψₜ}{γₚ : Subp Ξₚ (Ψₚ [ γₜ ]c)}{βₚ : Subp Δₚ (Ξₚ [ βₜ ]c)}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)} + {eq₁ : Subp Γₚ (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c) ≡ Subp Γₚ (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)} + {eq₂ : Subp (Δₚ [ αₜ ]c) ((Ψₚ [ γₜ ∘ₜ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c)} + {eq₃ : Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ∘ₜ αₜ ]c) ≡ Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)} + {eq₄ : Subp (Δₚ [ αₜ ]c) ((Ξₚ [ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ξₚ [ βₜ ∘ₜ αₜ ]c)} + {eq₅ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)} + → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ (γₚ [ βₜ ∘ₜ αₜ ]σₚ)) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ) + lemG {Γₜ}{Δₜ}{Ξₜ}{Ψₜ}{Γₚ}{Δₚ}{Ξₚ}{Ψₚ}{αₜ = αₜ}{βₜ}{γₜ}{γₚ}{βₚ}{αₚ}{eq₁}{eq₂}{eq₃}{eq₄}{eq₅} = + substP (λ X → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ X) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ)) []σₚ-∘ ( + ≡tran⁵ + (cong (coe eq₁) (≡tran ( + ≡sym (substfpoly + {R = λ X → Subp (Δₚ [ αₜ ]c) X} + {eq = ≡sym []c-∘} + {f = λ ξ → ξ ∘ₚ αₚ} + {x = ((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ})) + (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘))) + (≡sym (substfpoly + {R = λ X → Subp (Ξₚ [ βₜ ]c) X} + {eq = ≡sym []c-∘} + {f = λ ξ → ((ξ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ} + {x = γₚ [ βₜ ]σₚ} + ))) + )) + (≡tran coecoe-coe coecoe-coe) + (cong (coe (≡tran (cong (λ z → Subp Γₚ (z [ αₜ ]c)) (≡sym []c-∘)) (≡tran (cong (λ z → Subp Γₚ z) (≡sym []c-∘)) eq₁))) lemG') + (≡sym coecoe-coe) + (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘))) (substppoly + {A = (Conp Γₜ) × (Conp Γₜ)} + {R = λ W → Subp (proj×₁ W) (proj×₂ W)} + {Q = λ W → Subp (Δₚ [ αₜ ]c) (proj×₁ W)} + {eq = ×≡ (≡sym []c-∘) (≡sym []c-∘)} + {f = λ x y → x ∘ₚ (y ∘ₚ αₚ)} + {x = (γₚ [ βₜ ]σₚ) [ αₜ ]σₚ} + {y = βₚ [ αₜ ]σₚ} + ))(substfpoly + {R = λ X → Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) X} + {eq = ≡sym []c-∘} + {f = λ {τ} ξ → (ξ ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ))} + {x = (coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((γₚ [ βₜ ]σₚ) [ αₜ ]σₚ))} + )) + ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) + ∘-ass {Γ}{Δ}{Ξ}{Ψ}{α = sub αₜ αₚ} {β = sub βₜ βₚ} {γ = sub γₜ γₚ} = cong₂' sub ∘ₜ-ass lemG + + -- SUB-ization + + lemA : {σₜ : Subt Γₜ Δₜ}{t : Tm Γₜ} → (Γₚ ▹tp) [ σₜ ,ₜ t ]c ≡ Γₚ [ σₜ ]c + lemA {Γₚ = ◇p} = refl + lemA {Γₚ = Γₚ ▹p⁰ t} = cong₂ _▹p⁰_ lemA (≡tran (≡sym []f-∘) (cong (λ σ → t [ σ ]f) (≡tran wk∘, σ-idl))) + πₜ¹* : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Sub Δ Γ + πₜ¹* (sub (σₜ ,ₜ t) σₚ) = sub σₜ (subst (Subp _) lemA σₚ) + πₜ²* : {Γ Δ : Con} → Sub Δ (Γ ▹t) → Tm (Con.t Δ) + πₜ²* (sub (σₜ ,ₜ t) σₚ) = t + _,ₜ*_ : {Γ Δ : Con} → Sub Δ Γ → Tm (Con.t Δ) → Sub Δ (Γ ▹t) + (sub σₜ σₚ) ,ₜ* t = sub (σₜ ,ₜ t) (subst (Subp _) (≡sym lemA) σₚ) + πₜ²∘,ₜ* : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm (Con.t Δ)} → πₜ²* (σ ,ₜ* t) ≡ t + πₜ²∘,ₜ* = refl + πₜ¹∘,ₜ* : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm (Con.t Δ)} → πₜ¹* (σ ,ₜ* t) ≡ σ + πₜ¹∘,ₜ* {Γ}{Δ}{σ}{t} = cong (sub (Sub.t σ)) coeaba + ,ₜ∘πₜ* : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹t)} → (πₜ¹* σ) ,ₜ* (πₜ²* σ) ≡ σ + ,ₜ∘πₜ* {Γ} {Δ} {sub (σₜ ,ₜ t) σₚ} = cong (sub (σₜ ,ₜ t)) coeaba + ,ₜ∘* : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm (Con.t Γ)} → (σ ,ₜ* t) ∘ δ ≡ (σ ∘ δ) ,ₜ* (t [ Sub.t δ ]t) + lemE : {σₜ : Subt Γₜ Ξₜ}{σₚ : Subp Γₚ (Ξₚ [ σₜ ]c)} {δₜ : Subt Δₜ Γₜ} → (coe _ σₚ [ δₜ ]σₚ) ≡ coe _ (σₚ [ δₜ ]σₚ) + lemE {δₜ = δₜ} = coecong {eq = refl} {eq' = refl} (λ ξₚ → ξₚ [ δₜ ]σₚ) + lemF : {Γα Γβ : Conp Δₜ}{δₜ : Subt Δₜ Γₜ}{δₚ : Subp Δₚ (Γₚ [ δₜ ]c)} → (eq : Γβ ≡ Γα) → (ξ : Subp (Γₚ [ δₜ ]c) Γβ) → coe (cong (Subp Δₚ) eq) (ξ ∘ₚ δₚ) ≡ coe (cong (Subp _) eq) ξ ∘ₚ δₚ + lemF refl ξ = ≡tran coerefl (cong₂ _∘ₚ_ (≡sym coerefl) refl) + --lemG : {Γα Γβ : Conp Δₜ}{σₜ : Subt Γₜ Ξₜ}{δₜ : Subt Δₜ Γₜ} → (eq : Γβ ≡ Γα) → (ξ : Subp Γₚ (Ξₚ [ σₜ ]c)) → coe refl (ξ [ δₜ ]σₚ) ≡ (coe refl ξ) [ δₜ ]σₚ + --lemG eq ε= {!!} + substf : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{Q : A → Set ℓ'}{a b c d : A}{eqa : a ≡ a}{eqb : b ≡ b}{eqcd : c ≡ d}{eqdc : d ≡ c}{f : P a → P b}{g : P b → Q c}{x : P a} → g (subst P eqb (f (subst P eqa x))) ≡ subst Q eqdc (subst Q eqcd (g (f x))) + substf {P = P} {Q = Q} {eqcd = refl} {f = f} {g = g} = ≡tran² (cong g (≡tran (substrefl {P = P} {e = refl}) (cong f (substrefl {P = P} {e = refl})))) (≡sym (substrefl {P = Q} {e = refl})) (≡sym (substrefl {P = Q} {e = refl})) + + ,ₜ∘* {Γ} {Δ} {Ξ} {sub σₜ σₚ} {sub δₜ δₚ} {t} = cong (sub ((σₜ ∘ₜ δₜ) ,ₜ (t [ δₜ ]t))) + (substfgpoly + {P = Subp {Con.t Δ} (Con.p Δ)} + {Q = Subp {Con.t Δ} ((Con.p Γ) [ δₜ ]c)} + {R = Subp {Con.t Γ} (Con.p Γ)} + {F = λ X → X [ δₜ ]c} + {eq₁ = ≡sym lemA} + {eq₂ = ≡sym []c-∘} + {eq₃ = ≡sym []c-∘} + {eq₄ = ≡sym lemA} + {g = λ σₚ → σₚ ∘ₚ δₚ} + {f = λ σₚ → σₚ [ δₜ ]σₚ} + {x = σₚ}) + + πₚ¹* : {Γ Δ : Con} {A : For (Con.t Γ)} → Sub Δ (Γ ▹p A) → Sub Δ Γ + πₚ¹* (sub σₜ (σₚ ,ₚ pf)) = sub σₜ σₚ + πₚ² : {Γ Δ : Con} {F : For (Con.t Γ)} (σ : Sub Δ (Γ ▹p F)) → Pf Δ (F [ Sub.t (πₚ¹* σ) ]f) + πₚ² (sub σₜ (σₚ ,ₚ pf)) = pf + _,ₚ*_ : {Γ Δ : Con} {F : For (Con.t Γ)} (σ : Sub Δ Γ) → Pf Δ (F [ Sub.t σ ]f) → Sub Δ (Γ ▹p F) + sub σₜ σₚ ,ₚ* pf = sub σₜ (σₚ ,ₚ pf) + + ,ₚ∘πₚ : {Γ Δ : Con} → {F : For (Con.t Γ)} → {σ : Sub Δ (Γ ▹p F)} → (πₚ¹* σ) ,ₚ* (πₚ² σ) ≡ σ + ,ₚ∘πₚ {σ = sub σₜ (σₚ ,ₚ p)} = refl + ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For (Con.t Ξ)}{prf : Pf Γ (F [ Sub.t σ ]f)} + → (σ ,ₚ* prf) ∘ δ ≡ (σ ∘ δ) ,ₚ* (substP (λ F → Pf Δ F) (≡sym []f-∘) ((prf [ Sub.t δ ]pₜ) [ Sub.p δ ]p)) + ,ₚ∘ {Γ}{Δ}{Ξ}{σ = sub σₜ σₚ} {sub δₜ δₚ} {F = A} {prf} = cong (sub (σₜ ∘ₜ δₜ)) (cong (λ ξ → ξ ∘ₚ δₚ) + (substfpoly⁴ {P = λ W → Subp (Con.p Γ [ δₜ ]c) ((proj×₁ W) ▹p⁰ (proj×₂ W))}{R = λ W → Subp (Con.p Γ [ δₜ ]c) (proj×₁ W)}{Q = λ W → Pf (con (Con.t Δ) (Con.p Γ [ δₜ ]c)) (proj×₂ W)}{α = ((Con.p Ξ [ σₜ ]c) [ δₜ ]c) ,× ((A [ σₜ ]f) [ δₜ ]f)}{eq = cong₂ _,×_ (≡sym []c-∘) (≡sym []f-∘)}{f = λ ξ p → ξ ,ₚ p} {x = σₚ [ δₜ ]σₚ}{y = prf [ δₜ ]pₜ})) -- + + --_,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹t) + --πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t + --πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ + --,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ + --,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) + +-- lemB : ∀{ℓ}{A : Set ℓ}{ℓ'}{P : A → Set ℓ'}{a a' : A}{e : a ≡ a'}{p : P a}{p' : P a'} → p' ≡ p → subst P e p' ≡ p + + lemC : {σₜ : Subt Δₜ Γₜ}{t : Tm Δₜ} → (Γₚ ▹tp) [ σₜ ,ₜ t ]c ≡ Γₚ [ σₜ ]c + lemC {Γₚ = ◇p} = refl + lemC {Γₚ = Γₚ ▹p⁰ x} = cong₂ _▹p⁰_ lemC (≡tran (≡sym []f-∘) (cong (λ σ → x [ σ ]f) (≡tran wk∘, σ-idl))) + + lemD : {A : For (Con.t Γ)}{σ : Sub Δ (Γ ▹p A)} → Sub.t (πₚ¹* σ) ≡ Sub.t σ + lemD {σ = sub σₜ (σₚ ,ₚ pf)} = refl + + + imod : FFOL {lsuc lzero} {lsuc lzero} {lsuc lzero} {lsuc lzero} + imod = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; ∘-ass = ∘-ass + ; id = id + ; idl = idl + ; idr = idr + ; ◇ = ◇ + ; ε = sub εₜ εₚ + ; ε-u = cong₂' sub εₜ-u ε-u + ; Tm = λ Γ → Tm (Con.t Γ) + ; _[_]t = λ t σ → t [ Sub.t σ ]t + ; []t-id = []t-id + ; []t-∘ = λ {Γ}{Δ}{Ξ}{α}{β}{t} → []t-∘ {α = Sub.t α} {β = Sub.t β} {t = t} + ; _▹ₜ = _▹t + ; πₜ¹ = πₜ¹* + ; πₜ² = πₜ²* + ; _,ₜ_ = _,ₜ*_ + ; πₜ²∘,ₜ = refl + ; πₜ¹∘,ₜ = πₜ¹∘,ₜ* + ; ,ₜ∘πₜ = ,ₜ∘πₜ* + ; ,ₜ∘ = ,ₜ∘* + ; For = λ Γ → For (Con.t Γ) + ; _[_]f = λ A σ → A [ Sub.t σ ]f + ; []f-id = []f-id + ; []f-∘ = []f-∘ + ; R = r + ; R[] = refl + ; _⊢_ = Pf + ; _[_]p = λ pf σ → (pf [ Sub.t σ ]pₜ) [ Sub.p σ ]p + ; _▹ₚ_ = _▹p_ + ; πₚ¹ = πₚ¹* + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ*_ + ; ,ₚ∘πₚ = ,ₚ∘πₚ + ; πₚ¹∘,ₚ = refl + ; ,ₚ∘ = λ {Γ}{Δ}{Ξ}{σ}{δ}{F}{prf} → ,ₚ∘ {prf = prf} + ; _⇒_ = _⇒_ + ; []f-⇒ = refl + ; ∀∀ = ∀∀ + ; []f-∀∀ = []f-∀∀ + ; lam = λ {Γ}{F}{G} pf → substP (λ H → Pf Γ (F ⇒ H)) (≡tran (cong (_[_]f G) (lemD {σ = id})) []f-id) (lam pf) + ; app = app + ; ∀i = p∀∀i + ; ∀e = λ {Γ} {F} pf {t} → p∀∀e pf + } + diff --git a/FinitaryFirstOrderLogic.agda b/FinitaryFirstOrderLogic.agda new file mode 100644 index 0000000..245a615 --- /dev/null +++ b/FinitaryFirstOrderLogic.agda @@ -0,0 +1,319 @@ +{-# OPTIONS --prop --rewriting #-} + +open import PropUtil + +module FinitaryFirstOrderLogic where + + open import Agda.Primitive + open import ListUtil + + variable + ℓ¹ ℓ² ℓ³ ℓ⁴ ℓ⁵ : Level + + record FFOL : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ⁵)) where + infixr 10 _∘_ + infixr 5 _⊢_ + field + Con : Set ℓ¹ + Sub : Con → Con → Set ℓ⁵ -- It makes a category + _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) + id : {Γ : Con} → Sub Γ Γ + idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ + idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ + ◇ : Con -- The initial object of the category + ε : {Γ : Con} → Sub Γ ◇ -- The morphism from the initial to any object + ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ} + + -- Functor Con → Set called Tm + Tm : Con → Set ℓ² + _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms + []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x + []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t + + -- Tm : Set+ + _▹ₜ : Con → Con + πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ + πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ + _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ) + πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t + πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ + ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ + ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) + + -- Functor Con → Set called For + For : Con → Set ℓ³ + _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- The functor's action on morphisms + []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F + []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f + + -- Formulas with relation on terms + R : {Γ : Con} → (t u : Tm Γ) → For Γ + R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t) + + -- Proofs + _⊢_ : (Γ : Con) → For Γ → Prop ℓ⁴ + _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) -- The functor's action on morphisms + -- Equalities below are useless because Γ ⊢ F is in prop + -- []p-id : {Γ : Con} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ id {Γ} ]p ≡ prf + -- []p-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → {prf : Γ ⊢ F} → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p + + -- → Prop⁺ + _▹ₚ_ : (Γ : Con) → For Γ → Con + πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) + _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + -- Equalities below are useless because Γ ⊢ F is in Prop + ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ + πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ (σ ,ₚ prf) ≡ σ + -- πₚ²∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ² (σ ,ₚ prf) ≡ prf + ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym []f-∘) (prf [ δ ]p)) + + + -- Implication + _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ + []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) + + -- Forall + ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ + []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f)) + + -- Lam & App + lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) + app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G + -- Again, we don't write the _[_]p equalities as everything is in Prop + + -- ∀i and ∀e + ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) + ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) + + + -- Examples + -- Proof utils + forall-in : {Γ Δ : Con} {σ : Sub Γ Δ} {A : For (Δ ▹ₜ)} → Γ ⊢ ∀∀ (A [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f) → Γ ⊢ (∀∀ A [ σ ]f) + forall-in {Γ = Γ} f = substP (λ F → Γ ⊢ F) (≡sym ([]f-∀∀)) f + wkₜ : {Γ : Con} → Sub (Γ ▹ₜ) Γ + wkₜ = πₜ¹ id + 0ₜ : {Γ : Con} → Tm (Γ ▹ₜ) + 0ₜ = πₜ² id + 1ₜ : {Γ : Con} → Tm (Γ ▹ₜ ▹ₜ) + 1ₜ = πₜ² (πₜ¹ id) + wkₚ : {Γ : Con} {A : For Γ} → Sub (Γ ▹ₚ A) Γ + wkₚ = πₚ¹ id + 0ₚ : {Γ : Con} {A : For Γ} → Γ ▹ₚ A ⊢ A [ πₚ¹ id ]f + 0ₚ = πₚ² id + + -- Examples + ex0 : {A : For ◇} → ◇ ⊢ (A ⇒ A) + ex0 {A = A} = lam 0ₚ + {- + ex1 : {A : For (◇ ▹ₜ)} → ◇ ⊢ ((∀∀ A) ⇒ (∀∀ A)) + -- πₚ¹ id is adding an unused variable (syntax's llift) + ex1 {A = A} = lam (forall-in (∀i (substP (λ σ → ((◇ ▹ₚ ∀∀ A) ▹ₜ) ⊢ (A [ σ ]f)) {!!} {!!}))) + -- (∀ x ∀ y . A(y,x)) ⇒ ∀ x ∀ y . A(x,y) + -- translation is (∀ ∀ A(0,1)) => (∀ ∀ A(1,0)) + ex1' : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ ∀∀ (∀∀ ( A [ (ε ,ₜ 0ₜ) ,ₜ 1ₜ ]f))) + ex1' = {!!} + -- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x) + ex2 : {A : For ◇} → {B : For (◇ ▹ₜ)} → ◇ ⊢ ((A ⇒ (∀∀ B)) ⇒ (∀∀ ((A [ wkₜ ]f) ⇒ B))) + ex2 = {!!} + -- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x) + -- For simplicity, I swiched positions of parameters of A (somehow...) + ex3 : {A : For (◇ ▹ₜ ▹ₜ)} → ◇ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (A [ id ,ₜ 0ₜ ]f))) + ex3 = {!!} + -- ∀ x . A (x) ⇒ ∀ x y . A(x) + ex4 : {A : For (◇ ▹ₜ)} → ◇ ⊢ ((∀∀ A) ⇒ (∀∀ (∀∀ (A [ ε ,ₜ 1ₜ ]f)))) + ex4 = {!!} + -- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B) + ex5 : {A : For (◇ ▹ₜ)} → {B : For ◇} → ◇ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ wkₜ ]f)) ⇒ (B [ wkₜ ]f)))) + ex5 = {!!} + -} + + record Tarski : Set₁ where + field + TM : Set + REL : TM → TM → Prop + infixr 10 _∘_ + Con = Set + Sub : Con → Con → Set + Sub Γ Δ = (Γ → Δ) -- It makes a posetal category + _∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ + f ∘ g = λ x → f (g x) + id : {Γ : Con} → Sub Γ Γ + id = λ x → x + ε : {Γ : Con} → Sub Γ ⊤ₛ -- The morphism from the initial to any object + ε Γ = ttₛ + ε-u : {Γ : Con} → {σ : Sub Γ ⊤ₛ} → σ ≡ ε {Γ} + ε-u = refl + + -- Functor Con → Set called Tm + Tm : Con → Set + Tm Γ = Γ → TM + _[_]t : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ -- The functor's action on morphisms + t [ σ ]t = λ γ → t (σ γ) + []t-id : {Γ : Con} → {x : Tm Γ} → x [ id {Γ} ]t ≡ x + []t-id = refl + []t-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {t : Tm Γ} → t [ β ∘ α ]t ≡ (t [ β ]t) [ α ]t + []t-∘ {α = α} {β} {t} = refl {_} {_} {λ z → t (β (α z))} + + _[_]tz : {Γ Δ : Con} → {n : Nat} → Array (Tm Γ) n → Sub Δ Γ → Array (Tm Δ) n + tz [ σ ]tz = map (λ s → s [ σ ]t) tz + []tz-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {n : Nat} → {tz : Array (Tm Γ) n} → tz [ β ∘ α ]tz ≡ tz [ β ]tz [ α ]tz + []tz-∘ {tz = zero} = refl + []tz-∘ {α = α} {β = β} {tz = next x tz} = substP (λ tz' → (next ((x [ β ]t) [ α ]t) tz') ≡ (((next x tz) [ β ]tz) [ α ]tz)) (≡sym ([]tz-∘ {α = α} {β = β} {tz = tz})) refl + []tz-id : {Γ : Con} → {n : Nat} → {tz : Array (Tm Γ) n} → tz [ id ]tz ≡ tz + []tz-id {tz = zero} = refl + []tz-id {tz = next x tz} = substP (λ tz' → next x tz' ≡ next x tz) (≡sym ([]tz-id {tz = tz})) refl + thm : {Γ Δ : Con} → {n : Nat} → {tz : Array (Tm Γ) n} → {σ : Sub Δ Γ} → {δ : Δ} → map (λ t → t δ) (tz [ σ ]tz) ≡ map (λ t → t (σ δ)) tz + thm {tz = zero} = refl + thm {tz = next x tz} {σ} {δ} = substP (λ tz' → (next (x (σ δ)) (map (λ t → t δ) (map (λ s γ → s (σ γ)) tz))) ≡ (next (x (σ δ)) tz')) (thm {tz = tz}) refl + + -- Tm⁺ + _▹ₜ : Con → Con + Γ ▹ₜ = Γ × TM + πₜ¹ : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Sub Δ Γ + πₜ¹ σ = λ x → proj×₁ (σ x) + πₜ² : {Γ Δ : Con} → Sub Δ (Γ ▹ₜ) → Tm Δ + πₜ² σ = λ x → proj×₂ (σ x) + _,ₜ_ : {Γ Δ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹ₜ) + σ ,ₜ t = λ x → (σ x) ,× (t x) + πₜ²∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ² (σ ,ₜ t) ≡ t + πₜ²∘,ₜ {σ = σ} {t} = refl {a = t} + πₜ¹∘,ₜ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t : Tm Δ} → πₜ¹ (σ ,ₜ t) ≡ σ + πₜ¹∘,ₜ = refl + ,ₜ∘πₜ : {Γ Δ : Con} → {σ : Sub Δ (Γ ▹ₜ)} → (πₜ¹ σ) ,ₜ (πₜ² σ) ≡ σ + ,ₜ∘πₜ = refl + ,ₜ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{t : Tm Γ} → (σ ,ₜ t) ∘ δ ≡ (σ ∘ δ) ,ₜ (t [ δ ]t) + ,ₜ∘ = refl + + -- Functor Con → Set called For + For : Con → Set₁ + For Γ = Γ → Prop + _[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ + F [ σ ]f = λ x → F (σ x) + []f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F + []f-id = refl + []f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ} → F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f + []f-∘ = refl + + R : {Γ : Con} → Tm Γ → Tm Γ → For Γ + R t u = λ γ → REL (t γ) (u γ) + R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : Tm Γ} → (R t u) [ σ ]f ≡ R (t [ σ ]t) (u [ σ ]t) + R[] {σ = σ} = cong₂ R refl refl + + -- Proofs + _⊢_ : (Γ : Con) → For Γ → Prop + Γ ⊢ F = ∀ (γ : Γ) → F γ + _[_]p : {Γ Δ : Con} → {F : For Γ} → Γ ⊢ F → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) + prf [ σ ]p = λ γ → prf (σ γ) + -- Two rules are irrelevent beccause Γ ⊢ F is in Prop + + -- → Prop⁺ + _▹ₚ_ : (Γ : Con) → For Γ → Con + Γ ▹ₚ F = Γ ×'' F + πₚ¹ : {Γ Δ : Con} → {F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ + πₚ¹ σ δ = proj×''₁ (σ δ) + πₚ² : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Δ ⊢ (F [ πₚ¹ σ ]f) + πₚ² σ δ = proj×''₂ (σ δ) + _,ₚ_ : {Γ Δ : Con} → {F : For Γ} → (σ : Sub Δ Γ) → Δ ⊢ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F) + _,ₚ_ {F = F} σ pf δ = (σ δ) ,×'' pf δ + ,ₚ∘πₚ : {Γ Δ : Con} → {F : For Γ} → {σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ + ,ₚ∘πₚ = refl + πₚ¹∘,ₚ : {Γ Δ : Con} → {σ : Sub Δ Γ} → {F : For Γ} → {prf : Δ ⊢ (F [ σ ]f)} → πₚ¹ {Γ} {Δ} {F} (σ ,ₚ prf) ≡ σ + πₚ¹∘,ₚ = refl + ,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Γ ⊢ (F [ σ ]f)} → + (_,ₚ_ {F = F} σ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (λ F → Δ ⊢ F) (≡sym ([]f-∘ {α = δ} {β = σ} {F = F})) (prf [ δ ]p)) + ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} = refl + + -- Implication + _⇒_ : {Γ : Con} → For Γ → For Γ → For Γ + F ⇒ G = λ γ → (F γ) → (G γ) + []f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ} → (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f) + []f-⇒ = refl + + -- Forall + ∀∀ : {Γ : Con} → For (Γ ▹ₜ) → For Γ + ∀∀ {Γ} F = λ (γ : Γ) → (∀ (t : TM) → F (γ ,× t)) + []f-∀∀ : {Γ Δ : Con} → {F : For (Γ ▹ₜ)} → {σ : Sub Δ Γ} → (∀∀ F) [ σ ]f ≡ (∀∀ (F [ (σ ∘ πₜ¹ id) ,ₜ πₜ² id ]f)) + []f-∀∀ {Γ} {Δ} {F} {σ} = refl + + -- Lam & App + lam : {Γ : Con} → {F : For Γ} → {G : For Γ} → (Γ ▹ₚ F) ⊢ (G [ πₚ¹ id ]f) → Γ ⊢ (F ⇒ G) + lam pf = λ γ x → pf (γ ,×'' x) + app : {Γ : Con} → {F G : For Γ} → Γ ⊢ (F ⇒ G) → Γ ⊢ F → Γ ⊢ G + app pf pf' = λ γ → pf γ (pf' γ) + -- Again, we don't write the _[_]p equalities as everything is in Prop + + -- ∀i and ∀e + ∀i : {Γ : Con} → {F : For (Γ ▹ₜ)} → (Γ ▹ₜ) ⊢ F → Γ ⊢ (∀∀ F) + ∀i p γ = λ t → p (γ ,× t) + ∀e : {Γ : Con} → {F : For (Γ ▹ₜ)} → Γ ⊢ (∀∀ F) → {t : Tm Γ} → Γ ⊢ ( F [(id {Γ}) ,ₜ t ]f) + ∀e p {t} γ = p γ (t γ) + + tod : FFOL + tod = record + { Con = Con + ; Sub = Sub + ; _∘_ = _∘_ + ; ∘-ass = refl + ; id = id + ; idl = refl + ; idr = refl + ; ◇ = ⊤ₛ + ; ε = ε + ; ε-u = refl + ; Tm = Tm + ; _[_]t = _[_]t + ; []t-id = []t-id + ; []t-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {t} → []t-∘ {Γ} {Δ} {Ξ} {α} {β} {t} + ; _▹ₜ = _▹ₜ + ; πₜ¹ = πₜ¹ + ; πₜ² = πₜ² + ; _,ₜ_ = _,ₜ_ + ; πₜ²∘,ₜ = λ {Γ} {Δ} {σ} → πₜ²∘,ₜ {Γ} {Δ} {σ} + ; πₜ¹∘,ₜ = λ {Γ} {Δ} {σ} {t} → πₜ¹∘,ₜ {Γ} {Δ} {σ} {t} + ; ,ₜ∘πₜ = ,ₜ∘πₜ + ; ,ₜ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {t} → ,ₜ∘ {Γ} {Δ} {Ξ} {σ} {δ} {t} + ; For = For + ; _[_]f = _[_]f + ; []f-id = []f-id + ; []f-∘ = λ {Γ} {Δ} {Ξ} {α} {β} {F} → []f-∘ {Γ} {Δ} {Ξ} {α} {β} {F} + ; _⊢_ = _⊢_ + ; _[_]p = _[_]p + ; _▹ₚ_ = _▹ₚ_ + ; πₚ¹ = πₚ¹ + ; πₚ² = πₚ² + ; _,ₚ_ = _,ₚ_ + ; ,ₚ∘πₚ = ,ₚ∘πₚ + ; πₚ¹∘,ₚ = λ {Γ} {Δ} {F} {σ} {p} → πₚ¹∘,ₚ {Γ} {Δ} {F} {σ} {p} + ; ,ₚ∘ = λ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} → ,ₚ∘ {Γ} {Δ} {Ξ} {σ} {δ} {F} {prf} + ; _⇒_ = _⇒_ + ; []f-⇒ = λ {Γ} {F} {G} {σ} → []f-⇒ {Γ} {F} {G} {σ} + ; ∀∀ = ∀∀ + ; []f-∀∀ = λ {Γ} {Δ} {F} {σ} → []f-∀∀ {Γ} {Δ} {F} {σ} + ; lam = lam + ; app = app + ; ∀i = ∀i + ; ∀e = ∀e + ; R = R + ; R[] = λ {Γ} {Δ} {σ} {t} {u} → R[] {Γ} {Δ} {σ} {t} {u} + } + + + -- (∀ x ∀ y . A(x,y)) ⇒ ∀ y ∀ x . A(y,x) + -- both sides are ∀ ∀ A (0,1) + ex1 : {A : For (⊤ₛ ▹ₜ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (∀∀ A))) + ex1 _ hyp = hyp + -- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x) + ex2 : {A : For ⊤ₛ} → {B : For (⊤ₛ ▹ₜ)} → ⊤ₛ ⊢ ((A ⇒ (∀∀ B)) ⇒ (∀∀ ((A [ πₜ¹ id ]f) ⇒ B))) + ex2 _ h t h' = h h' t + -- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x) + -- For simplicity, I swiched positions of parameters of A (somehow...) + ex3 : {A : For (⊤ₛ ▹ₜ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ (∀∀ A)) ⇒ (∀∀ (A [ id ,ₜ (πₜ² id) ]f))) + ex3 _ h t = h t t + -- ∀ x . A (x) ⇒ ∀ x y . A(x) + ex4 : {A : For (⊤ₛ ▹ₜ)} → ⊤ₛ ⊢ ((∀∀ A) ⇒ (∀∀ (∀∀ (A [ ε ,ₜ (πₜ² (πₜ¹ id)) ]f)))) + ex4 {A} ◇◇ x t t' = x t + -- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B) + ex5 : {A : For (⊤ₛ ▹ₜ)} → {B : For ⊤ₛ} → ⊤ₛ ⊢ ((((∀∀ A) ⇒ B) ⇒ B) ⇒ (∀∀ ((A ⇒ (B [ πₜ¹ id ]f)) ⇒ (B [ πₜ¹ id ]f)))) + ex5 ◇◇ h t h' = h (λ h'' → h' (h'' t)) diff --git a/ListUtil.agda b/ListUtil.agda index 1a7bcd9..b857d4e 100644 --- a/ListUtil.agda +++ b/ListUtil.agda @@ -1,8 +1,14 @@ -{-# OPTIONS --prop #-} +{-# OPTIONS --prop --rewriting #-} module ListUtil where - open import Data.List using (List; _∷_; []) public + + infixr 5 _∷_ + data List : (T : Set₀) → Set where + [] : {T : Set₀} → List T + _∷_ : {T : Set₀} → T → List T → List T + + {-# BUILTIN LIST List #-} private variable @@ -138,4 +144,17 @@ module ListUtil where ⊆→∈* : L ⊆ L' → L ∈* L' ⊆→∈* h = ⊂⁺→∈* (⊂→⊂⁺ (⊆→⊂ h)) + + open import PropUtil using (Nat; zero; succ) + open import Agda.Primitive + variable + ℓ : Level + data Array (T : Set ℓ) : Nat → Set ℓ where + zero : Array T zero + next : {n : Nat} → T → Array T n → Array T (succ n) + + map : {T U : Set ℓ} → (T → U) → {n : Nat} → Array T n → Array U n + map f zero = zero + map f (next t a) = next (f t) (map f a) + diff --git a/PropUtil.agda b/PropUtil.agda index 99b77d2..1fbbaaa 100644 --- a/PropUtil.agda +++ b/PropUtil.agda @@ -1,7 +1,15 @@ -{-# OPTIONS --prop #-} +{-# OPTIONS --prop --rewriting #-} module PropUtil where + open import Agda.Primitive + variable ℓ ℓ' : Level + + data ⊥ₛ : Set where + record ⊤ₛ : Set ℓ where + constructor ttₛ + + -- ⊥ is a data with no constructor -- ⊤ is a record with one always-available constructor data ⊥ : Prop where @@ -50,3 +58,239 @@ module PropUtil where infixr 200 _$_ _$_ : {T U : Prop} → (T → U) → T → U h $ t = h t + + + + + + + postulate _≈_ : ∀{ℓ}{A : Set ℓ}(a : A) → A → Set ℓ + infix 3 _≡_ + data _≡_ {ℓ}{A : Set ℓ}(a : A) : A → Prop ℓ where + refl : a ≡ a + {-# BUILTIN REWRITE _≡_ #-} + + ≡sym : {ℓ : Level} → {A : Set ℓ}→ {a a' : A} → a ≡ a' → a' ≡ a + ≡sym refl = refl + + + ≡tran : {ℓ : Level} {A : Set ℓ} → {a a' a'' : A} → a ≡ a' → a' ≡ a'' → a ≡ a'' + ≡tran² : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₀ ≡ a₃ + ≡tran³ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₀ ≡ a₄ + ≡tran⁴ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₀ ≡ a₅ + ≡tran⁵ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₀ ≡ a₆ + ≡tran⁶ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₆ ≡ a₇ → a₀ ≡ a₇ + ≡tran⁷ : {ℓ : Level} {A : Set ℓ} → {a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : A} → a₀ ≡ a₁ → a₁ ≡ a₂ → a₂ ≡ a₃ → a₃ ≡ a₄ → a₄ ≡ a₅ → a₅ ≡ a₆ → a₆ ≡ a₇ → a₇ ≡ a₈ → a₀ ≡ a₈ + ≡tran refl refl = refl + ≡tran² refl refl refl = refl + ≡tran³ refl refl refl refl = refl + ≡tran⁴ refl refl refl refl refl = refl + ≡tran⁵ refl refl refl refl refl refl = refl + ≡tran⁶ refl refl refl refl refl refl refl = refl + ≡tran⁷ refl refl refl refl refl refl refl refl = refl + + cong : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (f : A → B) → {a a' : A} → a ≡ a' → f a ≡ f a' + cong f refl = refl + cong₂ : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''} → (f : A → B → C) → {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → f a b ≡ f a' b' + cong₂ f refl refl = refl + cong₃ : {ℓ ℓ' ℓ'' ℓ''' : Level}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{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' + cong₃ f refl refl refl = refl + + -- We can make a proof-irrelevant substitution + substP : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Prop ℓ'){a a' : A} → a ≡ a' → P a → P a' + substP P refl h = h + substPP : ∀{ℓ}{A B : Set ℓ}{Q : A → Prop ℓ}{ℓ'}(P : {k : A} → Q k → Prop ℓ'){a a' : A}{x : Q a} + → (eq : a ≡ a') → P x → P (substP Q eq x) + substPP P refl h = h + substP² : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}(P : A → B → Prop ℓ''){a a' : A}{b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b' + substP² P refl refl p = p + + + postulate coe : ∀{ℓ}{A B : Set ℓ} → A ≡ B → A → B + postulate coerefl : ∀{ℓ}{A : Set ℓ}{eq : A ≡ A}{a : A} → coe eq a ≡ a + + postulate ≡fun : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : Set ℓ'} → {f g : A → B} → ((x : A) → (f x ≡ g x)) → f ≡ g + postulate ≡fun' : {ℓ ℓ' : Level} → {A : Set ℓ} → {B : A → Set ℓ'} → {f g : (a : A) → B a} → ((x : A) → (f x ≡ g x)) → f ≡ g + + coeaba : {ℓ : Level}{A B : Set ℓ}{eq1 : A ≡ B}{eq2 : B ≡ A}{a : A} → coe eq2 (coe eq1 a) ≡ a + coeaba {eq1 = refl} = ≡tran coerefl coerefl + + coefgcong : {ℓ : Level}{A B C D : Set ℓ}{aa : A ≡ A}{dd : D ≡ D}{cb : C ≡ B}{f : B → A}{g : D → C}{x : D} → f (coe cb (g (coe dd x))) ≡ coe aa (f (coe cb (g x))) + coefgcong {cb = refl} {f} {g} = ≡tran (cong f (cong (coe _) (cong g coerefl))) (≡sym coerefl) + + coecong : {ℓ : Level}{A B : Set ℓ}{eq : B ≡ B}{eq' : A ≡ A}(f : A → B){x : A} → (f (coe eq' x)) ≡ (coe eq (f x)) + + coecong f = ≡tran (cong f coerefl) (≡sym coerefl) + + coecoe-coe : {ℓ : Level}{A B C : Set ℓ}{eq1 : B ≡ A}{eq2 : C ≡ B}{x : C} → coe eq1 (coe eq2 x) ≡ coe (≡tran eq2 eq1) x + coecoe-coe {eq1 = refl} {refl} = coerefl + + coe-f : {ℓ : Level}{A B C D : Set ℓ} → (A → B) → A ≡ C → B ≡ D → C → D + coe-f f ac bd x = coe bd (f (coe (≡sym ac) x)) + coewtf : {ℓ : Level}{A B C D E F G H : Set ℓ}{ab : A ≡ B}{cd : C ≡ D}{ef : E ≡ F}{gh : G ≡ H}{f : F → B}{g : H → E}{x : G} → + {fd : F ≡ D} → f (coe ef (g (coe gh x))) ≡ coe ab ((coe-f f fd (≡sym ab)) (coe cd ((coe-f g (≡sym gh) (≡tran² ef fd (≡sym cd))) x))) + coewtf {ab = refl} {refl} {refl} {refl} {f} {g} {fd = refl} = ≡tran (cong f (cong (coe _) (≡sym coeaba))) (≡sym coeaba) + + coeshift : {ℓ : Level}{A B : Set ℓ}{x : A} {y : B} {eq : A ≡ B} → coe eq x ≡ y → x ≡ coe (≡sym eq) y + coeshift {eq=refl} refl = ≡sym coeaba + + subst : ∀{ℓ}{A : Set ℓ}{ℓ'}(P : A → Set ℓ'){a a' : A} → a ≡ a' → P a → P a' + subst P eq p = coe (cong P eq) p + subst² : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Set ℓ'}(P : A → B → Set ℓ''){a a' : A}{b b' : B} → a ≡ a' → b ≡ b' → P a b → P a' b' + subst² P eq eq' p = coe (cong₂ P eq eq') p + subst¹P : ∀{ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : Prop ℓ'}(P : A → B → Set ℓ''){a a' : A}{b : B} → a ≡ a' → P a b → P a' b + subst¹P P {b = b} eq p = coe (cong (λ x → P x b) eq) p + + --{-# REWRITE transprefl #-} + + coereflrefl : {ℓ : Level}{A : Set ℓ}{eq eq' : A ≡ A}{a : A} → coe eq (coe eq' a) ≡ a + coereflrefl = ≡tran coerefl coerefl + + substrefl : ∀{ℓ}{A : Set ℓ}{ℓ'}{P : A → Set ℓ'}{a : A}{e : a ≡ a}{p : P a} → subst P e p ≡ p + substrefl = coerefl + --{-# REWRITE substrefl #-} + substreflrefl : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{a : A}{e : a ≡ a}{p : P a} → subst P e (subst P e p) ≡ p + substreflrefl {P = P} {a} {e} {p} = ≡tran (substrefl {P = P} {a = a} {e = e} {p = subst P e p}) (substrefl {P = P} {a = a} {e = e} {p = p}) + + cong₂' : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{B : A → Set ℓ'}{C : Set ℓ''} → (f : (a : A) → B a → C) → {a a' : A} {b : B a} {b' : B a'} → (eq : a ≡ a') → subst B eq b ≡ b' → f a b ≡ f a' b' + cong₂' f {a} refl refl = cong (f a) (≡sym coerefl) + + congsubst : {ℓ ℓ' : Level}{A : Set ℓ}{P : A → Set ℓ'}{a a' : A}{e : a ≡ a}{p : P a}{p' : P a} → p ≡ p' → subst P e p ≡ subst P e p' + congsubst {P = P} {e = refl} h = cong (subst P refl) h + + substfpoly : {ℓ ℓ' : Level}{A : Set ℓ}{P R : A → Set ℓ'}{α β : A} + {eq : α ≡ β} {f : {ξ : A} → R ξ → P ξ} {x : R α} + → coe (cong P eq) (f {α} x) ≡ f (coe (cong R eq) x) + substfpoly {eq = refl} {f} = ≡tran coerefl (cong f (≡sym coerefl)) + + substppoly : {ℓ ℓ' ℓ'' ℓ''' : Level}{A : Set ℓ}{P : A → Set ℓ'}{R : A → Set ℓ''}{Q : A → Set ℓ'''}{α β : A} + {eq : α ≡ β}{f : {ξ : A} → R ξ → Q ξ → P ξ} {x : R α} {y : Q α} + → coe (cong P eq) (f {α} x y) ≡ f {β} (coe (cong R eq) x) (coe (cong Q eq) y) + substppoly {eq = refl} {f}{x}{y} = ≡tran coerefl (cong₂ f (≡sym coerefl) (≡sym coerefl)) + + substfpoly' : {ℓ ℓ' ℓ'' : Level}{A B : Set ℓ}{P R : A → Set ℓ'}{Q : B → Prop ℓ''}{α β : A}{γ δ : B} + {eq : α ≡ β}{eq' : γ ≡ δ} {f : {ξ : A}{ι : B} → R ξ → Q ι → P ξ} {x : R α} {y : Q γ} + → coe (cong P eq) (f {α} {γ} x y) ≡ f {β} {δ} (coe (cong R eq) x) (substP Q eq' y) + substfpoly' {eq = refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl + substfpoly⁴ : {ℓ ℓ' ℓ'' : Level}{A : Set ℓ}{P R : A → Set ℓ'}{Q : A → Prop ℓ''}{α β : A} + {eq : α ≡ β} {f : {ξ : A} → R ξ → Q ξ → P ξ} {x : R α} {y : Q α} + → coe (cong P eq) (f {α} x y) ≡ f {β} (coe (cong R eq) x) (substP Q eq y) + substfpoly⁴ {eq = refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl + substfpoly³ : {ℓ ℓ' ℓ'' ℓ''' : Level}{A B C : Set ℓ}{R : A → Set ℓ'}{Q : B → Prop ℓ''}{P : C → Set ℓ'''}{α β : A}{γ δ : B}{ε φ : C} + {eq : α ≡ β}{eq' : γ ≡ δ}{eq'' : ε ≡ φ} {f : {ξ : A}{ι : B}{τ : C} → R ξ → Q ι → P τ} {x : R α} {y : Q γ} + → coe (cong P eq'') (f {α} {γ} {ε} x y) ≡ f {β} {δ} {φ} (coe (cong R eq) x) (substP Q eq' y) + substfpoly³ {eq = refl} {refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl + substfpoly'' : {ℓ ℓ' ℓ'' : Level}{A C : Set ℓ}{P : A → C → Set ℓ'}{R : A → Set ℓ'}{Q : A → C → Prop ℓ''}{α β : A}{ε φ : C} + {eq : α ≡ β}{eq'' : ε ≡ φ} {f : {ξ : A}{κ : C} → R ξ → Q ξ κ → P ξ κ} {x : R α} {y : Q α ε} + → coe (cong₂ P eq eq'') (f {α} {ε} x y) ≡ f {β} {φ} (coe (cong R eq) x) (substP (λ X → Q X φ) eq (substP (Q α) eq'' y)) + substfpoly'' {eq = refl} {refl} {f}{x}{y} = ≡tran² coerefl (cong (λ x → f x y) (≡sym coerefl)) refl + + substfgpoly : {ℓ ℓ' : Level}{A B : Set ℓ} {P Q : A → Set ℓ'} {R : B → Set ℓ'} {F : B → A} {α β : A} {ε φ : B} + {eq₁ : α ≡ β} {eq₂ : F ε ≡ α} {eq₃ : F φ ≡ β} {eq₄ : ε ≡ φ} + {g : {a : A} → Q a → P a} {f : {b : B} → R b → Q (F b)} {x : R ε} + → g {β} (subst Q eq₃ (f {φ} (subst R eq₄ x))) ≡ subst P eq₁ (g {α} (subst Q eq₂ (f {ε} x))) + substfgpoly {P = P} {Q} {R} {eq₁ = refl} {refl} {refl} {refl} {g} {f} = ≡tran³ (cong g (substrefl {P = Q} {e = refl})) (cong g (cong f (substrefl {P = R} {e = refl}))) (cong g (≡sym (substrefl {P = Q} {e = refl}))) (≡sym (substrefl {P = P} {e = refl})) + + {-# BUILTIN EQUALITY _≡_ #-} + + coep² : {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set ℓ₁} {R : A → Set ℓ₂}{T : A → Set ℓ₃}{S : A → Set ℓ₄}{α β : A} + {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R α}{y : T α}{eq : α ≡ β} + → subst S (≡sym eq) (p {β} (subst R eq x) (subst T eq y)) ≡ p {α} x y + coep² {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong₂ p (substrefl {a = x} {e = refl}) (substrefl {a = y} {e = refl})) + coep²'' : {ℓ ℓ' : Level} {A : Set ℓ} {R S : A → Set ℓ'}{T : A → Prop ℓ'}{α β : A} + {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R α}{y : T α}{eq : α ≡ β} + → subst S (≡sym eq) (p {β} (subst R eq x) (substP T eq y)) ≡ p {α} x y + coep²'' {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong (λ X → p X y) (substrefl {a = x} {e = refl})) + coep²' : {ℓ ℓ' : Level} {A : Set ℓ} {R T S : A → Set ℓ'}{α β : A} + {p : {ξ : A} → R ξ → T ξ → S ξ}{x : R β}{y : T α}{eq : α ≡ β} + → subst S (≡sym eq) (p {β} x (subst T eq y)) ≡ p {α} (subst R (≡sym eq) x) y + coep²' {S = S}{p = p}{x}{y}{refl} = ≡tran (substrefl {P = S} {e = refl}) (cong₂ p (≡sym (substrefl {a = x} {e = refl})) (substrefl {a = y} {e = refl})) + + coep∘ : {ℓ ℓ' : Level}{A : Set ℓ} {R : A → A → Set ℓ'} {α β γ δ ε φ : A} + {p : {x y z : A} → R x y → R z x → R z y}{x : R β γ}{y : R α β} + {eq1 : α ≡ δ} {eq2 : β ≡ ε} {eq3 : γ ≡ φ} → + coe (cong₂ R (≡sym eq1) (≡sym eq3)) (p (coe (cong₂ R eq2 eq3) x) (coe (cong₂ R eq1 eq2) y)) ≡ p x y + coep∘ {p = p}{eq1 = refl}{refl}{refl} = ≡tran coerefl (cong₂ p coerefl coerefl) + coep∘-helper = λ {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'} + {b₁ b₂ : B} {α γ : A b₁} {δ φ : A b₂} + {eq0 : b₁ ≡ b₂}{eqa : subst A eq0 α ≡ δ}{eqb : subst A eq0 γ ≡ φ} + → (≡tran² (cong (R b₂ δ) (≡sym eqb)) (cong (λ X → R b₂ X (subst A eq0 γ)) (≡sym eqa)) (≡tran (≡sym (substrefl {P = λ X → Set ℓ'}{a = R b₂ (subst A eq0 α) (subst A eq0 γ)}{e = refl})) (coep² {p = λ {t} x y → R t x y}{eq = eq0}))) + coep∘-helper-coe : {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'} + {b₁ b₂ : B} {α γ : A b₁} {δ φ : A b₂} + {eq0 : b₁ ≡ b₂}{eqa : subst A eq0 α ≡ δ}{eqb : subst A eq0 γ ≡ φ} → {a : R b₂ δ φ}{a' : R b₁ α γ} → coe (coep∘-helper {eq0 = eq0} {eqa = eqa} {eqb = eqb}) a ≡ a + coep∘-helper-coe {eq0 = refl}{refl}{refl} = coerefl + {-coep∘' : {ℓ ℓ' ℓ'' : Level}{B : Set ℓ}{A : B → Set ℓ''} {R : (b : B) → A b → A b → Set ℓ'} + {b₁ b₂ : B} {α β γ : A b₁} {δ ε φ : A b₂} + {p : {b : B}{x y z : A b} → R b x y → R b z x → R b z y}{x : R b₁ β γ}{y : R b₁ α β} + {eq0 : b₁ ≡ b₂}{eq1 : subst A eq0 α ≡ δ} {eq2 : subst A eq0 β ≡ ε} {eq3 : subst A eq0 γ ≡ φ} + {eq4 : R b₂ δ φ ≡ R b₁ α γ}{eq5 : R b₂ ε φ ≡ R b₁ β γ}{eq6 : R b₂ δ ε ≡ R b₁ α β} + → coe eq4 + (p {b₂} {ε} {φ} {δ} (coe (≡sym (eq5)) x) (coe (≡sym ( + eq6 + )) y)) ≡ p {b₁} {β} {γ} {α} x y + --coep∘' {p = p} {x} {y} {eq0 = refl} {refl} {refl} {refl} {eq4} = {!!} + -} + + + + + + + + data Nat : Set where + zero : Nat + succ : Nat → Nat + + {-# BUILTIN NATURAL Nat #-} + + record _×_ (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where + constructor _,×_ + field + a : A + b : B + + record _×'_ (A : Set ℓ) (B : Prop ℓ') : Set (ℓ ⊔ ℓ') where + constructor _,×'_ + field + a : A + b : B + + record _×''_ (A : Set ℓ) (B : A → Prop ℓ') : Set (ℓ ⊔ ℓ') where + constructor _,×''_ + field + a : A + b : B a + + record _×ᵈ_ (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where + constructor _,×ᵈ_ + field + a : A + b : B a + + + proj×₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → A + proj×₁ p = _×_.a p + proj×₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Set ℓ'} → (A × B) → B + proj×₂ p = _×_.b p + + proj×'₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Prop ℓ'} → (A ×' B) → A + proj×'₁ p = _×'_.a p + proj×'₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : Prop ℓ'} → (A ×' B) → B + proj×'₂ p = _×'_.b p + + proj×''₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (A ×'' B) → A + proj×''₁ p = _×''_.a p + proj×''₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Prop ℓ'} → (p : A ×'' B) → B (proj×''₁ p) + proj×''₂ p = _×''_.b p + + proj×ᵈ₁ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Set ℓ'} → (A ×ᵈ B) → A + proj×ᵈ₁ p = _×ᵈ_.a p + proj×ᵈ₂ : {ℓ ℓ' : Level}{A : Set ℓ}{B : A → Set ℓ'} → (p : A ×ᵈ B) → (B (proj×ᵈ₁ p)) + proj×ᵈ₂ p = _×ᵈ_.b p + + + ×≡ : {A : Set ℓ}{B : Set ℓ'}{a a' : A}{b b' : B} → a ≡ a' → b ≡ b' → a ,× b ≡ a' ,× b' + ×≡ refl refl = refl + + ×ᵈ≡ : {A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'} → (eq : a ≡ a') → subst B eq b ≡ b' → a ,×ᵈ b ≡ a' ,×ᵈ b' + ×ᵈ≡ {B = B} {a = a}{b = b} refl refl = cong₂' _,×ᵈ_ refl refl