https://bitbucket.org/akaposi/prop
Raw File
Tip revision: 342f0758427932316130a5a5facbeb6844c55c17 authored by Ambrus Kaposi on 02 June 2022, 14:03:40 UTC
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
back to top