cooltt
cooltt copied to clipboard
RedPRL
Problem with patching and names
Not sure what is going on here, but consider the following example:
def category : type :=
sig
def ob : type
def hom : sig [s : ob, t : ob] → type
def idn : (x : ob) → hom # [s := x, t := x]
def seq : (f : hom) → (g : hom # [s := f.t]) → hom # [s := f.s, t := g.t]
def seqL :
(f : hom) → path {hom # [s := f.s, t := f.t]} {seq {idn {f.s}} f} f
def seqR :
(f : hom) → path {hom # [s := f.s, t := f.t]} {seq f {idn {f.t}}} f
def seqA :
(f : hom) (g : hom # [s := f.t]) (h : hom # [s := g.t])
→ path {hom # [s := f.s, t := h.t]} {seq f {seq g h}} {seq {seq f g} h}
end
def functor : type :=
sig
def s : category
def t : category
def ob : {s.ob} → {t.ob}
def hom : (f : s.hom) → {t.hom # [s := ob {f.s}, t := ob {f.t}]}
def idn : (x : s.ob) → path {t.hom # [s := ob x, t := ob x]} {hom {s.idn x}} {t.idn {ob x}}
def seq : (f : s.hom) (g : s.hom # [s := f.t]) → path {t.hom # [s := ob {f.s}, t := ob {g.t}]} {hom {s.seq f g}} {t.seq {hom f} {hom g}}
end
def nat-trans : type :=
sig
def src : functor
def trg : functor # [s := src.s, t := src.t]
def fam : (i : src.s.ob) → {src.t.hom # [s := src.ob i, t := trg.ob i]}
def natural
: (f : src.s.hom)
→ path {src.t.hom # [s := src.ob {f.s}, t := trg.ob {f.t}]}
{src.t.seq {fam {f.s}} {trg.hom f}}
{src.t.seq {src.hom f} {fam {f.t}}}
end
In nat-trans, if I rename src,trg to s,t as I would like to, then the following happens:
[stdin]:34.38-34.41 [Error]:
Expected (s₁ : sig
(ob : type)
(hom : (_x₁ : sig def s : ob def t : ob end) → type)
(idn : (x : ob) →
sig
def s : ext ob ⊤ {_x₁ => x}
def t : ext ob ⊤ {_x₁ => x}
def fib : hom {struct def s := x def t := x end}
end)
(seq : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
(g : sig
def s : ext ob ⊤ {_x₁ => f.t}
def t : ob
def fib : hom {struct def s := f.t def t := t end}
end) →
sig
def s : ext ob ⊤ {_x₁ => f.s}
def t : ext ob ⊤ {_x₁ => g.t}
def fib : hom {struct def s := f.s def t := g.t end}
end)
(seqL : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
ext
{i =>
sig
def s : ext ob ⊤ {_x₁ => f.s}
def t : ext ob ⊤ {_x₁ => f.t}
def fib : hom {struct def s := f.s def t := f.t end}
end}
{i => i = 0 ∨ i = 1}
{i _x₁ =>
[ i = 0 =>
struct
def s := f.s
def t := f.t
def fib :=
seq {struct
def s := idn {f.s}.s def t := idn {f.s}.t def fib := idn {f.s}.fib
end} {struct def s := f.s def t := f.t def fib := f.fib end}.fib
end
| i = 1 => struct def s := f.s def t := f.t def fib := f.fib end
]})
(seqR : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
ext
{i =>
sig
def s : ext ob ⊤ {_x₁ => f.s}
def t : ext ob ⊤ {_x₁ => f.t}
def fib : hom {struct def s := f.s def t := f.t end}
end}
{i => i = 0 ∨ i = 1}
{i _x₁ =>
[ i = 0 =>
struct
def s := f.s
def t := f.t
def fib :=
seq {struct def s := f.s def t := f.t def fib := f.fib end} {
struct
def s := idn {f.t}.s def t := idn {f.t}.t def fib := idn {f.t}.fib
end}.fib
end
| i = 1 => struct def s := f.s def t := f.t def fib := f.fib end
]})def seqA :
(f : sig
def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end}
end) →
(g : sig
def s : ext ob ⊤ {_x₁ => f.t}
def t : ob
def fib : hom {struct def s := f.t def t := t end}
end) →
(h : sig
def s : ext ob ⊤ {_x₁ => g.t}
def t : ob
def fib : hom {struct def s := g.t def t := t end}
end) →
ext
{i =>
sig
def s : ext ob ⊤ {_x₁ => f.s}
def t : ext ob ⊤ {_x₁ => h.t}
def fib : hom {struct def s := f.s def t := h.t end}
end}
{i => i = 0 ∨ i = 1}
{i _x₁ =>
[ i = 0 =>
struct
def s := f.s
def t := h.t
def fib :=
seq {struct def s := f.s def t := f.t def fib := f.fib end} {
struct
def s :=
seq {struct def s := g.s def t := g.t def fib := g.fib end} {
struct
def s := h.s def t := h.t def fib := h.fib
end}.s
def t :=
seq {struct def s := g.s def t := g.t def fib := g.fib end} {
struct
def s := h.s def t := h.t def fib := h.fib
end}.t
def fib :=
seq {struct def s := g.s def t := g.t def fib := g.fib end} {
struct
def s := h.s def t := h.t def fib := h.fib
end}.fib
end}.fib
end
| i = 1 =>
struct
def s := f.s
def t := h.t
def fib :=
seq {struct
def s :=
seq {struct
def s := f.s def t := f.t def fib := f.fib
end} {struct
def s := g.s
def t := g.t
def fib := g.fib
end}.s
def t :=
seq {struct
def s := f.s def t := f.t def fib := f.fib
end} {struct
def s := g.s
def t := g.t
def fib := g.fib
end}.t
def fib :=
seq {struct
def s := f.s def t := f.t def fib := f.fib
end} {struct
def s := g.s
def t := g.t
def fib := g.fib
end}.fib
end} {struct
def s := h.s def t := h.t def fib := h.fib
end}.fib
end
]}) to have field t
cooltt: encountered one or more errors
I wonder if the scoping of patches is a bit different than I had expected?
Each patch has all the previous patches in scope. So sig [A : type, B : type] # [A := nat, B := A] is valid in the empty context. I don't know if this is strictly needed though.
Actually with the recent record PR, each patch has all the fields of the record that precede it in scope. so sig [A : type, B : type] # [B := A] is also valid.
I feel having the previous patches in scope is unexpected behavior from a user's point of view...