Definition of assignments

We distinguish assignments, mapping variables in a context to terms, from substitutions, applying an assignment to a term. Assignments are intrinsically typed, mapping variables of a context Γ to open terms with variables in Δ.

  Definition assignment (F : Fam₁ T C) (Γ Δ : C) := forall x, Γ ∋ x -> F Δ x.

  Notation "Γ =[ F ]> Δ" := (assignment F Γ%ctx Δ%ctx).

Pointwise equality of assignments.

  Definition asgn_eq {F : Fam₁ T C} Γ Δ : relation (Γ =[F]> Δ) := ∀ₕ _, ∀ₕ _, eq.
  Notation "u ≡ₐ v" := (asgn_eq _ _ u%asgn v%asgn).

  #[global] Instance asgn_equiv {F Γ Δ} : Equivalence (@asgn_eq F Γ Δ).
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Equivalence (asgn_eq Γ Δ)
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Equivalence (asgn_eq Γ Δ)
    econstructor.
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Reflexive (asgn_eq Γ Δ)
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Symmetric (asgn_eq Γ Δ)
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Transitive (asgn_eq Γ Δ)
    -
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Reflexive (asgn_eq Γ Δ) now intros u ? i.
    -
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Symmetric (asgn_eq Γ Δ) intros u h ? ? i; symmetry; now apply (H _ i).
    -
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ, Δ: C
Transitive (asgn_eq Γ Δ) intros u v w h1 h2 ? i; transitivity (v _ i); [ now apply h1 | now apply h2 ].
  Qed.

Internal hom functors. The monoidal product for substitution is a bit cumbersome as it is expressed as a coend, that is, a quotient. Following the formalization by Dima Szamozvancev, we instead prefer to express everything in terms of its adjoint, the internal hom.

For example the monoidal multiplication map will not be typed X ⊗ X ⇒ X but X ⇒ ⟦ X , X ⟧.

It is an end, that is, a subset, which are far more easy to work with as they can simply be encoded as a record pairing an element and a proof. The proof part is not written here but encoded later on.

The real one is ⟦-,-⟧₁, but in fact we can define an analogue to this bifunctor for any functor category ctx → C, which we do here for Fam₀ and Fam₂ (unsorted and bisorted, scoped families). This will be helpful to define what it means to substitute other kinds of syntactic objects.

See Ctx/Abstract.v for more details on the theory.

  Definition internal_hom₀ : Fam₁ T C -> Fam₀ T C -> Fam₀ T C
    := fun F G Γ => forall Δ, Γ =[F]> Δ -> G Δ.
  Definition internal_hom₁ : Fam₁ T C -> Fam₁ T C -> Fam₁ T C
    := fun F G Γ x => forall Δ, Γ =[F]> Δ -> G Δ x.
  Definition internal_hom₂ : Fam₁ T C -> Fam₂ T C -> Fam₂ T C
    := fun F G Γ x y => forall Δ, Γ =[F]> Δ -> G Δ x y.

  Notation "⟦ F , G ⟧₀" := (internal_hom₀ F G).
  Notation "⟦ F , G ⟧₁" := (internal_hom₁ F G).
  Notation "⟦ F , G ⟧₂" := (internal_hom₂ F G).

Experimental. The left action on maps of the internal hom bifunctor.

  Definition hom_precomp₀ {F1 F2 : Fam₁ T C} {G} (m : F1 ⇒₁ F2)
    : ⟦ F2 , G ⟧₀ ⇒₀ ⟦ F1 , G ⟧₀
    := fun _ f _ a => f _ (fun _ i => m _ _ (a _ i)).
  Definition hom_precomp₁ {F1 F2 : Fam₁ T C} {G} (m : F1 ⇒₁ F2)
    : ⟦ F2 , G ⟧₁ ⇒₁ ⟦ F1 , G ⟧₁
    := fun _ _ f _ a => f _ (fun _ i => m _ _ (a _ i)).
  Definition hom_precomp₂ {F1 F2 : Fam₁ T C} {G} (m : F1 ⇒₁ F2)
    : ⟦ F2 , G ⟧₂ ⇒₂ ⟦ F1 , G ⟧₂
    := fun _ _ _ f _ a => f _ (fun _ i => m _ _ (a _ i)).

Constructing a sorted family of operations from O with arguments taken from the family F.

  Record filled_op (O : Oper T C) (F : Fam₁ T C) (Γ : C) (t : T) :=
    OFill { fill_op : O t ; fill_args : o_dom fill_op =[F]> Γ }.
  Notation "S # F" := (filled_op S F).

We can forget the arguments and get back a bare operation.

  Definition forget_args {O : Oper T C} {F} : (O # F) ⇒₁ ⦉ O ⦊
    := fun _ _ => fill_op.

The empty assignment.

  Definition a_empty {F Γ} : ∅ =[F]> Γ
    := fun _ i => match c_view_emp i with end.

The copairing of assignments.

  Definition a_cat {F Γ1 Γ2 Δ} (u : Γ1 =[F]> Δ) (v : Γ2 =[F]> Δ) : (Γ1 +▶ Γ2) =[F]> Δ
    := fun t i => match c_view_cat i with
               | Vcat_l i => u _ i
               | Vcat_r j => v _ j
               end.

A kind relaxed of pointwise mapping.

  Definition a_map {F G : Fam₁ T C} {Γ Δ1 Δ2} (u : Γ =[F]> Δ1) (f : forall x, F Δ1 x -> G Δ2 x)
    : Γ =[G]> Δ2
    := fun _ i => f _ (u _ i) .

Copairing respects pointwise equality.

  #[global] Instance a_cat_eq {F Γ1 Γ2 Δ}
    : Proper (asgn_eq _ _ ==> asgn_eq _ _ ==> asgn_eq _ _) (@a_cat F Γ1 Γ2 Δ).
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ1, Γ2, Δ: C
Proper
  (asgn_eq Γ1 Δ ==>
   asgn_eq Γ2 Δ ==> asgn_eq (Γ1 +▶ Γ2)%ctx Δ) a_cat
  Proof.
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ1, Γ2, Δ: C
Proper
  (asgn_eq Γ1 Δ ==>
   asgn_eq Γ2 Δ ==> asgn_eq (Γ1 +▶ Γ2)%ctx Δ) a_cat
    intros ?? Hu ?? Hv ??; cbn.
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Γ1, Γ2, Δ: C
x, y: Γ1 =[ F ]> Δ
Hu: x ≡ₐ y
x0, y0: Γ2 =[ F ]> Δ
Hv: x0 ≡ₐ y0
a: T
a0: Γ1 +▶ Γ2 ∋ a
match c_view_cat a0 with
| Vcat_l i => x a i
| Vcat_r j => x0 a j
end =
match c_view_cat a0 with
| Vcat_l i => y a i
| Vcat_r j => y0 a j
end
    destruct (c_view_cat a0); [ now apply Hu | now apply Hv ].
  Qed.
End with_param.

Registering all the notations...

#[global] Notation "Γ =[ F ]> Δ" := (assignment F Γ%ctx Δ%ctx).
#[global] Bind Scope asgn_scope with assignment.

#[global] Notation "u ≡ₐ v" := (asgn_eq _ _ u%asgn v%asgn).
#[global] Notation "⟦ F , G ⟧₀" := (internal_hom₀ F G).
#[global] Notation "⟦ F , G ⟧₁" := (internal_hom₁ F G).
#[global] Notation "⟦ F , G ⟧₂" := (internal_hom₂ F G).

#[global] Notation "S # F" := (filled_op S F).
#[global] Notation "o ⦇ u ⦈" := (OFill o u%asgn).

#[global] Notation "!" := (a_empty) : asgn_scope.
#[global] Notation "[ u , v ]" := (a_cat u v) : asgn_scope.