Added IFOL algebra and initial and morphism and initiality proof
This commit is contained in:
parent
370daed594
commit
b93ce31ab3
GPG Key ID:
7054D5D6A90F084F
107
IFOL2.lagda
Normal file
107
IFOL2.lagda
Normal file
@ -0,0 +1,107 @@
|
||||
\begin{code}
|
||||
{-# OPTIONS --prop --rewriting #-}
|
||||
|
||||
open import PropUtil
|
||||
|
||||
module IFOL2 where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import ListUtil
|
||||
|
||||
variable
|
||||
ℓ¹ ℓ² ℓ³ ℓ⁴ ℓ⁵ : Level
|
||||
|
||||
record IFOL (TM : Set) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where
|
||||
infixr 10 _∘_
|
||||
field
|
||||
|
||||
-- We first make the base category with its terminal object
|
||||
Con : Set ℓ¹
|
||||
Sub : Con → Con → Prop ℓ² -- It makes a category
|
||||
_∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
|
||||
id : {Γ : Con} → Sub Γ Γ
|
||||
◇ : Con -- The terminal object of the category
|
||||
ε : {Γ : Con} → Sub Γ ◇ -- The morphism from any object to the terminal
|
||||
|
||||
-- Functor Con → Set called For
|
||||
For : Con → Set ℓ³
|
||||
_[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms
|
||||
[]f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F
|
||||
[]f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ}
|
||||
→ F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
|
||||
|
||||
-- Functor Con × For → Prop called Pf or ⊢
|
||||
Pf : (Γ : Con) → For Γ → Prop ℓ⁴
|
||||
-- Action on morphisms
|
||||
_[_]p : {Γ Δ : Con} → {F : For Γ} → Pf Γ F → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f)
|
||||
-- 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)) → Pf Δ (F [ πₚ¹ σ ]f)
|
||||
_,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
|
||||
-- Equality below is useless because Pf Γ F is in Prop
|
||||
-- πₚ²∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Pf Δ (F [ σ ]f)}
|
||||
-- → πₚ² (σ ,ₚ prf) ≡ prf
|
||||
|
||||
|
||||
{-- FORMULAE CONSTRUCTORS --}
|
||||
-- Formulas with relation on terms
|
||||
R : {Γ : Con} → (t u : TM) → For Γ
|
||||
R[] : {Γ Δ : Con} → {σ : Sub Δ Γ} → {t u : TM}
|
||||
→ (R t u) [ σ ]f ≡ R t u
|
||||
|
||||
-- Implication
|
||||
_⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
|
||||
[]f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ}
|
||||
→ (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
|
||||
|
||||
-- Forall
|
||||
∀∀ : {Γ : Con} → (TM → For Γ) → For Γ
|
||||
[]f-∀∀ : {Γ Δ : Con} → {F : TM → For Γ} → {σ : Sub Δ Γ}
|
||||
→ (∀∀ F) [ σ ]f ≡ (∀∀ (λ t → (F t) [ σ ]f))
|
||||
|
||||
{-- PROOFS CONSTRUCTORS --}
|
||||
-- Again, we don't have to write the _[_]p equalities as Proofs are in Prop
|
||||
|
||||
-- Lam & App
|
||||
lam : {Γ : Con}{F G : For Γ} → Pf (Γ ▹ₚ F) (G [ πₚ¹ id ]f) → Pf Γ (F ⇒ G)
|
||||
app : {Γ : Con}{F G : For Γ} → Pf Γ (F ⇒ G) → Pf Γ F → Pf Γ G
|
||||
|
||||
-- ∀i and ∀e
|
||||
∀i : {Γ : Con}{A : TM → For Γ} → ((t : TM) → Pf Γ (A t)) → Pf Γ (∀∀ A)
|
||||
∀e : {Γ : Con}{A : TM → For Γ} → Pf Γ (∀∀ A) → (t : TM) → Pf Γ (A t)
|
||||
|
||||
record Mapping (TM : Set) (S : IFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} TM) (D : IFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} TM) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where
|
||||
field
|
||||
|
||||
-- We first make the base category with its final object
|
||||
mCon : (IFOL.Con S) → (IFOL.Con D)
|
||||
mSub : {Δ : (IFOL.Con S)}{Γ : (IFOL.Con S)} → (IFOL.Sub S Δ Γ) → (IFOL.Sub D (mCon Δ) (mCon Γ))
|
||||
mFor : {Γ : (IFOL.Con S)} → (IFOL.For S Γ) → (IFOL.For D (mCon Γ))
|
||||
mPf : {Γ : (IFOL.Con S)} {A : IFOL.For S Γ} → IFOL.Pf S Γ A → IFOL.Pf D (mCon Γ) (mFor A)
|
||||
|
||||
|
||||
record Morphism (TM : Set)(S : IFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} TM) (D : IFOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴} TM) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where
|
||||
field m : Mapping TM S D
|
||||
mCon = Mapping.mCon m
|
||||
mSub = Mapping.mSub m
|
||||
mFor = Mapping.mFor m
|
||||
mPf = Mapping.mPf m
|
||||
field
|
||||
e◇ : mCon (IFOL.◇ S) ≡ IFOL.◇ D
|
||||
e[]f : {Γ Δ : IFOL.Con S}{A : IFOL.For S Γ}{σ : IFOL.Sub S Δ Γ} → mFor (IFOL._[_]f S A σ) ≡ IFOL._[_]f D (mFor A) (mSub σ)
|
||||
-- Proofs are in prop, so some equations are not needed
|
||||
--[]p : {Γ Δ : IFOL.Con S}{A : IFOL.For S Γ}{pf : IFOL._⊢_ S Γ A}{σ : IFOL.Sub S Δ Γ} → mPf (IFOL._[_]p S pf σ) ≡ IFOL._[_]p D (mPf pf) (mSub σ)
|
||||
e▹ₚ : {Γ : IFOL.Con S}{A : IFOL.For S Γ} → mCon (IFOL._▹ₚ_ S Γ A) ≡ IFOL._▹ₚ_ D (mCon Γ) (mFor A)
|
||||
--πₚ² : {Γ Δ : IFOL.Con S}{A : IFOL.For S Γ}{σ : IFOL.Sub S Δ (IFOL._▹ₚ_ S Γ A)} → mPf (IFOL.πₚ² S σ) ≡ IFOL.πₚ¹ D (subst (IFOL.Sub D (mCon Δ)) ▹ₚ (mSub σ))
|
||||
eR : {Γ : IFOL.Con S}{t u : TM} → mFor {Γ} (IFOL.R S t u) ≡ IFOL.R D t u
|
||||
e⇒ : {Γ : IFOL.Con S}{A B : IFOL.For S Γ} → mFor (IFOL._⇒_ S A B) ≡ IFOL._⇒_ D (mFor A) (mFor B)
|
||||
e∀∀ : {Γ : IFOL.Con S}{A : TM → IFOL.For S Γ} → mFor (IFOL.∀∀ S A) ≡ IFOL.∀∀ D (λ t → (mFor (A t)))
|
||||
-- No equation needed for lam, app, ∀i, ∀e as their output are in prop
|
||||
\end{code}
|
||||
196
IFOLInitial.lagda
Normal file
196
IFOLInitial.lagda
Normal file
@ -0,0 +1,196 @@
|
||||
\begin{code}
|
||||
{-# OPTIONS --prop --rewriting #-}
|
||||
|
||||
open import PropUtil
|
||||
|
||||
module IFOLInitial (TM : Set) where
|
||||
|
||||
open import IFOL2
|
||||
open import Agda.Primitive
|
||||
open import ListUtil
|
||||
|
||||
data For : Set where
|
||||
R : TM → TM → For
|
||||
_⇒_ : For → For → For
|
||||
∀∀ : (TM → For) → For
|
||||
|
||||
data Con : Set where
|
||||
◇ : Con
|
||||
_▹ₚ_ : Con → For → Con
|
||||
|
||||
variable
|
||||
Γ Δ Ξ : Con
|
||||
A B : For
|
||||
|
||||
data PfVar : Con → For → Prop where
|
||||
pvzero : PfVar (Γ ▹ₚ A) A
|
||||
pvnext : PfVar Γ A → PfVar (Γ ▹ₚ B) A
|
||||
data Pf : Con → For → Prop where
|
||||
var : PfVar Γ A → Pf Γ A
|
||||
lam : Pf (Γ ▹ₚ A) B → Pf Γ (A ⇒ B)
|
||||
app : Pf Γ (A ⇒ B) → Pf Γ A → Pf Γ B
|
||||
∀i : {A : TM → For} → ((t : TM) → Pf Γ (A t)) → Pf Γ (∀∀ A)
|
||||
∀e : {A : TM → For} → Pf Γ (∀∀ A) → (t : TM) → Pf Γ (A t)
|
||||
|
||||
|
||||
data Ren : Con → Con → Prop where
|
||||
ε : Ren Γ ◇
|
||||
_,ₚR_ : Ren Δ Γ → PfVar Δ A → Ren Δ (Γ ▹ₚ A)
|
||||
|
||||
rightR : Ren Δ Γ → Ren (Δ ▹ₚ A) Γ
|
||||
rightR ε = ε
|
||||
rightR (σ ,ₚR pv) = (rightR σ) ,ₚR (pvnext pv)
|
||||
|
||||
idR : Ren Γ Γ
|
||||
idR {◇} = ε
|
||||
idR {Γ ▹ₚ A} = (rightR (idR {Γ})) ,ₚR pvzero
|
||||
|
||||
data Sub : Con → Con → Prop where
|
||||
ε : Sub Γ ◇
|
||||
_,ₚ_ : Sub Δ Γ → Pf Δ A → Sub Δ (Γ ▹ₚ A)
|
||||
|
||||
πₚ¹ : Sub Δ (Γ ▹ₚ A) → Sub Δ Γ
|
||||
πₚ² : Sub Δ (Γ ▹ₚ A) → Pf Δ A
|
||||
πₚ¹ (σ ,ₚ pf) = σ
|
||||
πₚ² (σ ,ₚ pf) = pf
|
||||
|
||||
SubR : Ren Γ Δ → Sub Γ Δ
|
||||
SubR ε = ε
|
||||
SubR (σ ,ₚR pv) = SubR σ ,ₚ var pv
|
||||
|
||||
id : Sub Γ Γ
|
||||
id = SubR idR
|
||||
|
||||
_[_]pvr : PfVar Γ A → Ren Δ Γ → PfVar Δ A
|
||||
pvzero [ _ ,ₚR pv ]pvr = pv
|
||||
pvnext pv [ σ ,ₚR _ ]pvr = pv [ σ ]pvr
|
||||
_[_]pr : Pf Γ A → Ren Δ Γ → Pf Δ A
|
||||
var pv [ σ ]pr = var (pv [ σ ]pvr)
|
||||
lam pf [ σ ]pr = lam (pf [ (rightR σ) ,ₚR pvzero ]pr)
|
||||
app pf pf' [ σ ]pr = app (pf [ σ ]pr) (pf' [ σ ]pr)
|
||||
∀i fpf [ σ ]pr = ∀i (λ t → (fpf t) [ σ ]pr)
|
||||
∀e pf t [ σ ]pr = ∀e (pf [ σ ]pr) t
|
||||
|
||||
wkSub : Sub Δ Γ → Sub (Δ ▹ₚ A) Γ
|
||||
wkSub ε = ε
|
||||
wkSub (σ ,ₚ pf) = (wkSub σ) ,ₚ (pf [ rightR idR ]pr)
|
||||
|
||||
_[_]p : Pf Γ A → Sub Δ Γ → Pf Δ A
|
||||
var pvzero [ _ ,ₚ pf ]p = pf
|
||||
var (pvnext pv) [ σ ,ₚ _ ]p = var pv [ σ ]p
|
||||
lam pf [ σ ]p = lam (pf [ wkSub σ ,ₚ var pvzero ]p)
|
||||
app pf pf' [ σ ]p = app (pf [ σ ]p) (pf' [ σ ]p)
|
||||
∀i fpf [ σ ]p = ∀i (λ t → (fpf t) [ σ ]p)
|
||||
∀e pf t [ σ ]p = ∀e (pf [ σ ]p) t
|
||||
|
||||
_∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
|
||||
ε ∘ β = ε
|
||||
(α ,ₚ pf) ∘ β = (α ∘ β) ,ₚ (pf [ β ]p)
|
||||
|
||||
|
||||
ifol : IFOL TM
|
||||
ifol = record
|
||||
{ Con = Con
|
||||
; Sub = Sub
|
||||
; _∘_ = _∘_
|
||||
; id = id
|
||||
; ◇ = ◇
|
||||
; ε = ε
|
||||
; For = λ Γ → For
|
||||
; _[_]f = λ A σ → A
|
||||
; []f-id = refl
|
||||
; []f-∘ = refl
|
||||
; Pf = Pf
|
||||
; _[_]p = _[_]p
|
||||
; _▹ₚ_ = _▹ₚ_
|
||||
; πₚ¹ = πₚ¹
|
||||
; πₚ² = πₚ²
|
||||
; _,ₚ_ = _,ₚ_
|
||||
; R = R
|
||||
; _⇒_ = _⇒_
|
||||
; ∀∀ = ∀∀
|
||||
; R[] = refl
|
||||
; []f-⇒ = refl
|
||||
; []f-∀∀ = refl
|
||||
; lam = lam
|
||||
; app = app
|
||||
; ∀i = ∀i
|
||||
; ∀e = ∀e
|
||||
}
|
||||
|
||||
module InitialMorphism (M : IFOL {lzero} {lzero} {lzero} {lzero} TM) where
|
||||
|
||||
mCon : Con → (IFOL.Con M)
|
||||
mFor : {Γ : Con} → For → (IFOL.For M (mCon Γ))
|
||||
|
||||
mCon ◇ = IFOL.◇ M
|
||||
mCon (Γ ▹ₚ A) = IFOL._▹ₚ_ M (mCon Γ) (mFor {Γ} A)
|
||||
mFor {Γ} (R t u) = IFOL.R M t u
|
||||
mFor {Γ} (A ⇒ B) = IFOL._⇒_ M (mFor {Γ} A) (mFor {Γ} B)
|
||||
mFor {Γ} (∀∀ A) = IFOL.∀∀ M (λ t → mFor {Γ} (A t))
|
||||
|
||||
|
||||
mSub : {Δ : Con}{Γ : Con} → Sub Δ Γ → (IFOL.Sub M (mCon Δ) (mCon Γ))
|
||||
mPf : {Γ : Con} {A : For} → Pf Γ A → IFOL.Pf M (mCon Γ) (mFor {Γ} A)
|
||||
|
||||
e[]f⁰ : {Γ : Con}{A B : For} → mFor {Γ ▹ₚ B} A ≡ IFOL._[_]f M (mFor {Γ} A) (IFOL.πₚ¹ M (IFOL.id M))
|
||||
e[]f⁰ {A = R t u} = ≡sym (IFOL.R[] M)
|
||||
e[]f⁰ {A = A ⇒ B} = ≡sym (≡tran ( IFOL.[]f-⇒ M) (cong₂ (IFOL._⇒_ M) (≡sym (e[]f⁰ {A = A})) (≡sym (e[]f⁰ {A = B}))))
|
||||
e[]f⁰ {Γ}{A = ∀∀ A} = ≡sym (≡tran (IFOL.[]f-∀∀ M {F = λ t → mFor {Γ} (A t)}) (cong (IFOL.∀∀ M) (≡fun (λ t → ≡sym (e[]f⁰ {Γ} {A = A t})))))
|
||||
|
||||
e[]f : {Γ Δ : Con}{A : For}{σ : Sub Δ Γ} → mFor {Δ} A ≡ IFOL._[_]f M (mFor {Γ} A) (mSub σ)
|
||||
e[]f {A = R t u} {σ} = ≡sym (IFOL.R[] M)
|
||||
e[]f {A = A ⇒ B} {σ} = ≡sym (≡tran ( IFOL.[]f-⇒ M) (cong₂ (IFOL._⇒_ M) (≡sym (e[]f {A = A} {σ})) (≡sym (e[]f {A = B} {σ}))))
|
||||
e[]f {Γ}{A = ∀∀ A} {σ} = ≡sym (≡tran (IFOL.[]f-∀∀ M {F = λ t → mFor {Γ} (A t)}) (cong (IFOL.∀∀ M) (≡fun (λ t → ≡sym (e[]f {Γ} {A = A t} {σ})))))
|
||||
|
||||
mPf {A = A} (var (pvzero {Γ})) = substP (IFOL.Pf M _) (≡sym (e[]f⁰ {Γ} {A} {A})) (IFOL.πₚ² M (IFOL.id M))
|
||||
mPf {A = A} (var (pvnext {Γ} {B = B} pv)) = substP (IFOL.Pf M _) (≡sym (e[]f⁰ {Γ} {A} {B})) (IFOL._[_]p M (mPf (var pv)) (IFOL.πₚ¹ M (IFOL.id M)))
|
||||
mPf {Γ} (lam {A = A} {B} pf) = IFOL.lam M (substP (IFOL.Pf M _) (e[]f⁰ {Γ} {B} {A}) (mPf pf))
|
||||
mPf (app pf pf') = IFOL.app M (mPf pf) (mPf pf')
|
||||
mPf (∀i pf) = IFOL.∀i M (λ t → mPf (pf t))
|
||||
mPf (∀e pf t) = IFOL.∀e M (mPf pf) t
|
||||
|
||||
mSub ε = IFOL.ε M
|
||||
mSub (_,ₚ_ {Δ} {Γ = Γ} {A} σ pf) = IFOL._,ₚ_ M (mSub σ) (substP (IFOL.Pf M _) (e[]f {Γ} {Δ} {A} {σ}) (mPf pf))
|
||||
|
||||
mor : Morphism TM ifol M
|
||||
mor = record {
|
||||
m = record {
|
||||
mCon = mCon
|
||||
; mSub = mSub
|
||||
; mFor = λ {Γ} A → mFor {Γ} A
|
||||
; mPf = mPf
|
||||
}
|
||||
; e◇ = refl
|
||||
; e▹ₚ = refl
|
||||
; e[]f = λ {Γ}{Δ}{A}{σ} → e[]f {Γ}{Δ}{A}{σ}
|
||||
; eR = refl
|
||||
; e∀∀ = refl
|
||||
; e⇒ = refl
|
||||
}
|
||||
|
||||
module InitialMorphismUniqueness {M : IFOL {lzero} {lzero} {lzero} {lzero} TM} {m : Morphism TM ifol M} where
|
||||
|
||||
open InitialMorphism M
|
||||
mCon≡ : {Γ : Con} → mCon Γ ≡ (Morphism.mCon m Γ)
|
||||
mFor≡ : {Γ : Con} {A : For} → mFor {Γ} A ≡ subst (IFOL.For M) (≡sym mCon≡) (Morphism.mFor m {Γ} A)
|
||||
|
||||
mCon≡ {◇} = ≡sym (Morphism.e◇ m)
|
||||
mCon≡ {Γ ▹ₚ A} = ≡sym (≡tran (Morphism.e▹ₚ m) (cong₂' (IFOL._▹ₚ_ M) (≡sym mCon≡) (≡sym mFor≡)))
|
||||
mFor≡ {Γ} {A ⇒ B} = ≡sym (≡tran²
|
||||
(cong (subst (IFOL.For M) (≡sym mCon≡)) (Morphism.e⇒ m))
|
||||
(substppoly {eq = ≡sym (mCon≡ {Γ})} {f = λ {ξ} X Y → IFOL._⇒_ M {ξ} X Y})
|
||||
(cong₂ (IFOL._⇒_ M) (≡sym (mFor≡ {Γ} {A})) (≡sym (mFor≡ {Γ} {B}))))
|
||||
mFor≡ {Γ} {R t u} = ≡sym (≡tran (cong (subst (IFOL.For M) (≡sym mCon≡)) (Morphism.eR m)) (substpoly {f = λ {ξ} → IFOL.R M {ξ} t u} {eq = ≡sym mCon≡}))
|
||||
mFor≡ {Γ} {∀∀ A} = ≡sym (≡tran³
|
||||
(cong (subst (IFOL.For M) (≡sym mCon≡)) (Morphism.e∀∀ m))
|
||||
(substfpoly {eq = ≡sym mCon≡}{f = λ {ξ} X → IFOL.∀∀ M {ξ} X}{x = λ t → Mapping.mFor (Morphism.m m) {Γ} (A t)})
|
||||
(cong (IFOL.∀∀ M) (≡sym coefun'))
|
||||
(cong (IFOL.∀∀ M) (≡fun λ t → ≡sym (mFor≡ {Γ} {A t}))))
|
||||
|
||||
|
||||
-- Those two lines are not needed as those sorts are in Prop
|
||||
--mSub≡ : {Δ : Con}{Γ : Con}{σ : Sub Δ Γ} → mSub {Δ} {Γ} σ ≡ Morphism.mSub m {Δ} {Γ} σ
|
||||
--mPf≡ : {Γ : Con} {A : For}{p : Pf Γ A} → mPf {Γ} {A} p ≡ Morphism.mPf m {Γ} {A} p
|
||||
|
||||
\end{code}
|
||||
@ -211,17 +211,14 @@ module PropUtil where
|
||||
{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} = {!!}
|
||||
-}
|
||||
|
||||
|
||||
coefun : {ℓ : Level}{A B C : Set ℓ}{f : B → C}{eq : A ≡ B}
|
||||
→ f ≡ coe (cong (λ X → X → C) eq) (λ (x : A) → f (coe eq x))
|
||||
coefun {f = f} {eq = refl} = ≡tran (≡fun (λ x → cong f (≡sym (coerefl {eq = refl})))) (≡sym (coerefl {eq = refl}))
|
||||
coefun' : {ℓ : Level}{A B C : Set ℓ}{f : A → B}{eq : B ≡ C}
|
||||
→ (λ (x : A) → coe eq (f x)) ≡ coe (cong (λ X → A → X) eq) (λ (x : A) → f x)
|
||||
coefun' {f = f} {eq = refl} = ≡tran (≡fun (λ x → coerefl)) (≡sym coerefl)
|
||||
|
||||
|
||||
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
git s\begin{code}
|
||||
\begin{code}
|
||||
{-# OPTIONS --prop --rewriting #-}
|
||||
|
||||
open import PropUtil
|
||||
|
||||
@ -66,7 +66,7 @@
|
||||
\Pf & : & \For \rightarrow \Prop^+ \\
|
||||
\lam & : & (\Pf A \rightarrow^+ \Pf B) \rightarrow \Pf (A \implies B)\\
|
||||
\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\
|
||||
\foralli & : & (t : \operatorname{TM} \rightarrow A\;t) \rightarrow \Pf (\forall A)\\
|
||||
\foralli & : & (t : \operatorname{TM} \rightarrow \Pf A\;t) \rightarrow \Pf (\forall A)\\
|
||||
\foralle & : & \Pf (\forall A) \rightarrow (t : \operatorname{TM}) \rightarrow \Pf (A\;t)\\
|
||||
\end{array}
|
||||
\]
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user