https://bitbucket.org/akaposi/prop
Tip revision: 342f0758427932316130a5a5facbeb6844c55c17 authored by Ambrus Kaposi on 02 June 2022, 14:03:40 UTC
add supplementary link and remove negative spaces
add supplementary link and remove negative spaces
Tip revision: 342f075
todo.txt
- add the category of graphs to the applications section of the paper
- is pfprop closed under sums with eta?
- do we have coinductive types?
- try Palmgren's version of family of setoids with definitional
equalities instead of propositional for coeT, coeR, irr
- to extend TyP in the model construction with inductive types, we need definitional truncation (TyP Γ = (A : Ty Γ) × (q_A[p] = q_A)):
Tr : Ty Γ → Ty Γ
Tr[] : (Tr A)[σ] = Tr(A[σ])
irr : (u v : Tm Γ (Tr A)) → u = v
mkTr : Tm Γ A → Tm Γ (Tr A)
unTr : {B : Ty(Γ▹Tr A)}→{q[p]=q : Tm(Γ▹Tr A▹B▹B[p])(B[p²])}(u : Tm (Γ▹A)(B[p,mkTr q]))(t : Tm Γ (Tr A))→Tm Γ(B[id,t])
derivable : unTr u (mkTr t) = u[id,t]
(mkTr t)[σ] = mkTr (t[σ])
(unTr u t)[σ] = unTr (u[σ∘p,q]) (t[σ])
- can't we have an isomorphism instead? η shouldn't be a problem
because everything is in TyP. it seems we can't. the only
candidate is Tm Γ (Tr A) ≅ Tm Γ A, but we don't want this
- then we have finitary inductive types in TyP. e.g. Nat can be derived from Tr:
Nat : Ty Γ
zero : Tm Γ Nat
suc : Tm Γ Nat → Tm Γ Nat
ind : (P:Ty(Γ▹Nat))→Tm Γ(P[id,zero])→Tm(Γ▹Nat▹P)(P[p²,suc q[p]])→(t:Tm Γ Nat)→Tm Γ(P[id,t])
Natβ₁ : ind P u v zero = u
Natβ₂ : ind P u v (suc t) = v[id,t,ind P u v t]
Nat[]
zero[]
suc[]
ind[] : (ind P u v t)[σ] = ind(P[σ∘p,q])(u[σ])(v[σ∘p²,q[p],q])(t[σ])
------------------------------------------------------------------------
Nat' := Tr Nat : TyP Γ
zero' := mkTr zero : TmP Γ Nat'
suc' t := unTr {Tr Nat}(mkTr(suc q)) t : TmP Γ Nat'
t:Tm Γ (Tr Nat)
ind' P u v t := unTr {P} (ind {Γ▹Nat} (P[p²,mkTr q]) (u[p]) (v[p²,mkTr q[p],q][p]) q) t
^: Tm (Γ▹Nat)(P[p,mkTr q])
P : TyP(Γ▹Tr Nat)
u : TmP Γ(P[id,mkTr zero])
v : TmP (Γ▹Tr Nat▹P) (P[id,unTr {Tr Nat}(mkTr(suc q))(q[p])])
t : TmP Γ (Tr Nat)
ind {Γ}(P[p,mkTr q]) u (v[p²,mkTr q[p],q]) ?
^:Tm Γ (P[p,mkTr q][id,zero]) = Tm Γ (P[id,mkTr zero])
^:Tm (Γ▹Nat▹P[p,mkTr q]) (P[p,mkTr q][id,suc q[p]]) = Tm (Γ▹Nat▹P[p,mkTr q]) (P[p²,mkTr(suc q[p])])
(p²,mkTr q[p],q) : Sub (Γ▹Nat▹P[p,mkTr q]) (Γ▹Tr Nat▹P)
v[p²,mkTr q[p],q] : Tm (Γ▹Nat▹P[p,mkTr q]) (P[id,unTr(mkTr(suc q))(q[p])][p²,mkTr q[p],q])
^=P[p²,unTr(mkTr(suc q))(mkTr q[p])] = P[p²,mkTr(suc q)[id,q[p]]] = P[p²,mkTr(suc q[p])]
^:Tm Γ Nat
Nat'[] : Nat'[σ] = (Tr Nat)[σ] = Tr(Nat[σ]) = Tr Nat = Nat'
formalisation in Agda: [[file:~/git/fp_notes/inductiveTypesProp.agda]]. infinitary
ones don't seem to work