Built with Alectryon, running Coq+SerAPI v8.17.0+0.17.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.

Renamings

As explained in the abstract theory, renamings are a particular kind of assignements, where variables are mapped to variables.

In this file we define renamings for a given abstract context structure and provide all their properties that we will use throughout the development.

Definition

Context inclusion, or renaming is defined as an assignment of variables in Ξ“ to variables in Ξ”.

  Notation "Ξ“ βŠ† Ξ”" := (@assignment T C CC c_var Ξ“%ctx Ξ”%ctx).

The identity inclusion, whose renaming is the identity.

  Definition r_id {Ξ“} : Ξ“ βŠ† Ξ“ := fun _ i => i .
  #[global] Arguments r_id _ _ /.

Renaming assignments on the left by precomposition

  Definition a_ren_l {F Ξ“1 Ξ“2 Ξ“3} : Ξ“1 βŠ† Ξ“2 -> Ξ“2 =[F]> Ξ“3 -> Ξ“1 =[F]> Ξ“3 := a_map.
  #[global] Arguments a_ren_l _ _ _ _ _ _ _ /.
  Notation "r α΅£βŠ› u" := (a_ren_l r u) : asgn_scope.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3: C
Proper
  (asgn_eq Ξ“1 Ξ“2 ==> asgn_eq Ξ“2 Ξ“3 ==> asgn_eq Ξ“1 Ξ“3)
  a_ren_l

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3: C
Proper
  (asgn_eq Ξ“1 Ξ“2 ==> asgn_eq Ξ“2 Ξ“3 ==> asgn_eq Ξ“1 Ξ“3)
  a_ren_l
 intros ?? H1 ?? H2 ??; cbn; now rewrite H1, H2. Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2: C
a: Ξ“1 =[ F ]> Ξ“2
r_id α΅£βŠ› a ≑ₐ a

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2: C
a: Ξ“1 =[ F ]> Ξ“2
r_id α΅£βŠ› a ≑ₐ a
 reflexivity. Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ“4: C
u: Ξ“1 βŠ† Ξ“2
v: Ξ“2 βŠ† Ξ“3
w: Ξ“3 =[ F ]> Ξ“4
(u α΅£βŠ› v) α΅£βŠ› w ≑ₐ u α΅£βŠ› (v α΅£βŠ› w)

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ“4: C
u: Ξ“1 βŠ† Ξ“2
v: Ξ“2 βŠ† Ξ“3
w: Ξ“3 =[ F ]> Ξ“4
(u α΅£βŠ› v) α΅£βŠ› w ≑ₐ u α΅£βŠ› (v α΅£βŠ› w)
 reflexivity. Qed.

The fiber of the inclusion c_var (Ξ“ +β–Ά Ξ”) β†ͺ c_var Ξ“ + c_var Ξ” is a subsingleton.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“1 +β–Ά Ξ“2 βˆ‹ x
a, b: c_cat_view Ξ“1 Ξ“2 x i
a = b

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“1 +β–Ά Ξ“2 βˆ‹ x
a, b: c_cat_view Ξ“1 Ξ“2 x i
a = b

    
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
i, i0: Ξ“1 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_l i0)
x1: r_cat_l i = r_cat_l i0
x: Vcat_l i ~= b0
Vcat_l i0 = b0
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
j: Ξ“2 βˆ‹ x0
i0: Ξ“1 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_l i0)
x1: r_cat_r j = r_cat_l i0
x: Vcat_r j ~= b0
Vcat_l i0 = b0
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
i: Ξ“1 βˆ‹ x0
j: Ξ“2 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_r j)
x1: r_cat_l i = r_cat_r j
x: Vcat_l i ~= b0
Vcat_r j = b0
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
j0, j: Ξ“2 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_r j)
x1: r_cat_r j0 = r_cat_r j
x: Vcat_r j0 ~= b0
Vcat_r j = b0

    
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
i, i0: Ξ“1 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_l i0)
x1: r_cat_l i = r_cat_l i0
x: Vcat_l i ~= b0
Vcat_l i0 = b0
 
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
i, i0: Ξ“1 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_l i0)
x1: i = i0
x: Vcat_l i ~= b0
Vcat_l i0 = b0

      now rewrite x1 in x |-; rewrite x.
    
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
j: Ξ“2 βˆ‹ x0
i0: Ξ“1 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_l i0)
x1: r_cat_r j = r_cat_l i0
x: Vcat_r j ~= b0
Vcat_l i0 = b0
 symmetry in x1; destruct (r_cat_disj _ _ x1).
    
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
i: Ξ“1 βˆ‹ x0
j: Ξ“2 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_r j)
x1: r_cat_l i = r_cat_r j
x: Vcat_l i ~= b0
Vcat_r j = b0
 destruct (r_cat_disj _ _ x1).
    
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
j0, j: Ξ“2 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_r j)
x1: r_cat_r j0 = r_cat_r j
x: Vcat_r j0 ~= b0
Vcat_r j = b0
 
T, C: Type
CC: context T C
Ξ“1, Ξ“2: C
x0: T
CL: context_laws T C
j0, j: Ξ“2 βˆ‹ x0
b0: c_cat_view Ξ“1 Ξ“2 x0 (r_cat_r j)
x1: j0 = j
x: Vcat_r j0 ~= b0
Vcat_r j = b0

      now rewrite x1 in x |-; rewrite x.
  Qed.

Simplifications of the embedding.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“1 βˆ‹ x
c_view_cat (r_cat_l i) =
(Vcat_l i : c_cat_view Ξ“1 Ξ“2 x (r_cat_l i))

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“1 βˆ‹ x
c_view_cat (r_cat_l i) =
(Vcat_l i : c_cat_view Ξ“1 Ξ“2 x (r_cat_l i))
 apply view_cat_irr. Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“2 βˆ‹ x
c_view_cat (r_cat_r i) =
(Vcat_r i : c_cat_view Ξ“1 Ξ“2 x (r_cat_r i))

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
x: T
i: Ξ“2 βˆ‹ x
c_view_cat (r_cat_r i) =
(Vcat_r i : c_cat_view Ξ“1 Ξ“2 x (r_cat_r i))
 apply view_cat_irr. Qed.

Simplifying copairing.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
r_cat_l α΅£βŠ› [u, v] ≑ₐ u

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
r_cat_l α΅£βŠ› [u, v] ≑ₐ u
 intros ? i; cbn; now rewrite c_view_cat_simpl_l. Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
r_cat_r α΅£βŠ› [u, v] ≑ₐ v

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
r_cat_r α΅£βŠ› [u, v] ≑ₐ v
 intros ? i; cbv; now rewrite c_view_cat_simpl_r. Qed.

Universal property of copairing.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: (Ξ“1 +β–Ά Ξ“2) =[ F ]> Ξ”
H1: u ≑ₐ r_cat_l α΅£βŠ› w
H2: v ≑ₐ r_cat_r α΅£βŠ› w
[u, v] ≑ₐ w

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: (Ξ“1 +β–Ά Ξ“2) =[ F ]> Ξ”
H1: u ≑ₐ r_cat_l α΅£βŠ› w
H2: v ≑ₐ r_cat_r α΅£βŠ› w
[u, v] ≑ₐ w

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: (Ξ“1 +β–Ά Ξ“2) =[ F ]> Ξ”
H1: u ≑ₐ r_cat_l α΅£βŠ› w
H2: v ≑ₐ r_cat_r α΅£βŠ› w
a: T
i: Ξ“1 +β–Ά Ξ“2 βˆ‹ a
match c_view_cat i with
| Vcat_l i => u a i
| Vcat_r j => v a j
end = w a i

    destruct (c_view_cat i); [ exact (H1 _ i) | exact (H2 _ j) ].
  Qed.

Identity copairing.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
[r_cat_l, r_cat_r] ≑ₐ r_id

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2: C
[r_cat_l, r_cat_r] ≑ₐ r_id
 now apply a_cat_uniq. Qed.

Action of concatenation on maps.

  Definition r_catβ‚‚ {Ξ“1 Ξ“2 Ξ”1 Ξ”2} (r1 : Ξ“1 βŠ† Ξ”1) (r2 : Ξ“2 βŠ† Ξ”2)
    : (Ξ“1 +β–Ά Ξ“2) βŠ† (Ξ”1 +β–Ά Ξ”2)
    := [ r1 α΅£βŠ› r_cat_l , r2 α΅£βŠ› r_cat_r ] .
  #[global] Arguments r_catβ‚‚ _ _ _ _ _ _ _ _ /.

Shifting renamings on the right.

  Definition r_shift {Ξ“ Ξ”} R (r : Ξ“ βŠ† Ξ”) : (Ξ“ +β–Ά R) βŠ† (Ξ” +β–Ά R)
    := [ r α΅£βŠ› r_cat_l , r_cat_r ] .
  #[global] Arguments r_shift _ _ _ _ _ _ /.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“, R: C
r_shift R r_id ≑ₐ r_id

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“, R: C
r_shift R r_id ≑ₐ r_id
 now apply a_cat_uniq. Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
r_shift R (r1 α΅£βŠ› r2) ≑ₐ r_shift R r1 α΅£βŠ› r_shift R r2

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
r_shift R (r1 α΅£βŠ› r2) ≑ₐ r_shift R r1 α΅£βŠ› r_shift R r2

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
a: T
i: Ξ“1 βˆ‹ a
r_cat_l (r2 a (r1 a i)) =
match c_view_cat (r_cat_l (r1 a i)) with
| Vcat_l i => r_cat_l (r2 a i)
| Vcat_r j => r_cat_r j
end
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
a: T
j: R βˆ‹ a
r_cat_r j =
match c_view_cat (r_cat_r j) with
| Vcat_l i => r_cat_l (r2 a i)
| Vcat_r j => r_cat_r j
end

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
a: T
i: Ξ“1 βˆ‹ a
r_cat_l (r2 a (r1 a i)) =
match c_view_cat (r_cat_l (r1 a i)) with
| Vcat_l i => r_cat_l (r2 a i)
| Vcat_r j => r_cat_r j
end
 remember (r1 _ i) as j; now rewrite c_view_cat_simpl_l.
    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3, R: C
r1: Ξ“1 βŠ† Ξ“2
r2: Ξ“2 βŠ† Ξ“3
a: T
j: R βˆ‹ a
r_cat_r j =
match c_view_cat (r_cat_r j) with
| Vcat_l i => r_cat_l (r2 a i)
| Vcat_r j => r_cat_r j
end
 now rewrite c_view_cat_simpl_r.
  Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“, Ξ”, R: C
Proper
  (asgn_eq Ξ“ Ξ” ==> asgn_eq (Ξ“ +β–Ά R)%ctx (Ξ” +β–Ά R)%ctx)
  (r_shift R)

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“, Ξ”, R: C
Proper
  (asgn_eq Ξ“ Ξ” ==> asgn_eq (Ξ“ +β–Ά R)%ctx (Ξ” +β–Ά R)%ctx)
  (r_shift R)

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“, Ξ”, R: C
x, y: Ξ“ βŠ† Ξ”
H: x ≑ₐ y
a: T
i: Ξ“ βˆ‹ a
r_cat_l (x a i) = r_cat_l (y a i)

    now rewrite H.
  Qed.

A bunch of shorthands for useful renamings.

  Definition r_cat_rr {Ξ“1 Ξ“2 Ξ“3} : Ξ“3 βŠ† (Ξ“1 +β–Ά (Ξ“2 +β–Ά Ξ“3)) :=
    r_cat_r α΅£βŠ› r_cat_r .

  Definition r_cat3_1 {Ξ“1 Ξ“2 Ξ“3} : (Ξ“1 +β–Ά Ξ“2) βŠ† (Ξ“1 +β–Ά (Ξ“2 +β–Ά Ξ“3)) :=
    [ r_cat_l , r_cat_l α΅£βŠ› r_cat_r ].

  Definition r_cat3_2 {Ξ“1 Ξ“2 Ξ“3} : (Ξ“1 +β–Ά Ξ“3) βŠ† (Ξ“1 +β–Ά (Ξ“2 +β–Ά Ξ“3)) :=
    [ r_cat_l , r_cat_r α΅£βŠ› r_cat_r ].

  Definition r_cat3_3 {Ξ“1 Ξ“2 Ξ“3} : (Ξ“2 +β–Ά Ξ“3) βŠ† ((Ξ“1 +β–Ά Ξ“2) +β–Ά Ξ“3) :=
    [ r_cat_r α΅£βŠ› r_cat_l , r_cat_r ].

  Definition r_assoc_r {Ξ“1 Ξ“2 Ξ“3} : ((Ξ“1 +β–Ά Ξ“2) +β–Ά Ξ“3) βŠ† (Ξ“1 +β–Ά (Ξ“2 +β–Ά Ξ“3))
    := [ r_cat3_1 , r_cat_r α΅£βŠ› r_cat_r ].

  Definition r_assoc_l {Ξ“1 Ξ“2 Ξ“3} : (Ξ“1 +β–Ά (Ξ“2 +β–Ά Ξ“3)) βŠ† ((Ξ“1 +β–Ά Ξ“2) +β–Ά Ξ“3)
    := [ r_cat_l α΅£βŠ› r_cat_l , r_cat3_3 ] .

Misc. laws.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_1 α΅£βŠ› [u, [v, w]] ≑ₐ [u, v]

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_1 α΅£βŠ› [u, [v, w]] ≑ₐ [u, v]

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = u a i
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_l j)) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = v a j

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = u a i
 now rewrite c_view_cat_simpl_l.
    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_l j)) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = v a j
 now rewrite c_view_cat_simpl_r, c_view_cat_simpl_l.
  Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_2 α΅£βŠ› [u, [v, w]] ≑ₐ [u, w]

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_2 α΅£βŠ› [u, [v, w]] ≑ₐ [u, w]

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = u a i
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_r j)) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = w a j

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = u a i
 now rewrite c_view_cat_simpl_l.
    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_r j)) with
| Vcat_l i => u a i
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => v a i
    | Vcat_r j0 => w a j0
    end
end = w a j
 now rewrite 2 c_view_cat_simpl_r.
  Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_3 α΅£βŠ› [[u, v], w] ≑ₐ [v, w]

  
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
r_cat3_3 α΅£βŠ› [[u, v], w] ≑ₐ [v, w]

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_r i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => u a i0
    | Vcat_r j => v a j
    end
| Vcat_r j => w a j
end = v a i
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r j) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => u a i0
    | Vcat_r j => v a j
    end
| Vcat_r j => w a j
end = w a j

    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
i: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_r i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => u a i0
    | Vcat_r j => v a j
    end
| Vcat_r j => w a j
end = v a i
 now rewrite c_view_cat_simpl_l, c_view_cat_simpl_r.
    
T, C: Type
CC: context T C
CL: context_laws T C
F: Fam₁ T C
Ξ“1, Ξ“2, Ξ“3, Ξ”: C
u: Ξ“1 =[ F ]> Ξ”
v: Ξ“2 =[ F ]> Ξ”
w: Ξ“3 =[ F ]> Ξ”
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r j) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => u a i0
    | Vcat_r j => v a j
    end
| Vcat_r j => w a j
end = w a j
 now rewrite c_view_cat_simpl_r.
  Qed.

These last two are pretty interesting, they are the proofs witnessing the associativity isomorphism Γ₁ +β–Ά (Ξ“β‚‚ +β–Ά Γ₃) β‰ˆ (Γ₁ +β–Ά Ξ“β‚‚) +β–Ά Γ₃. Here isomorphism means isomorphism of the set of variables.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
r_assoc_l α΅£βŠ› r_assoc_r ≑ₐ r_id

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
r_assoc_l α΅£βŠ› r_assoc_r ≑ₐ r_id

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_l i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_l i
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“2 +β–Ά Ξ“3 βˆ‹ a
match
  c_view_cat
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j => r_cat_r j
    end
with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r j

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_l i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_l i
 now rewrite 2 c_view_cat_simpl_l.
    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“2 +β–Ά Ξ“3 βˆ‹ a
match
  c_view_cat
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j => r_cat_r j
    end
with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r j
 
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_r i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r (r_cat_l i)
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r j) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r (r_cat_r j)

      
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_l (r_cat_r i)) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r (r_cat_l i)
 now rewrite c_view_cat_simpl_l, c_view_cat_simpl_r.
      
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r j) with
| Vcat_l i =>
    match c_view_cat i with
    | Vcat_l i0 => r_cat_l i0
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
| Vcat_r j => r_cat_r (r_cat_r j)
end = r_cat_r (r_cat_r j)
 now rewrite c_view_cat_simpl_r.
  Qed.

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
r_assoc_r α΅£βŠ› r_assoc_l ≑ₐ r_id

  
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
r_assoc_r α΅£βŠ› r_assoc_l ≑ₐ r_id

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 +β–Ά Ξ“2 βˆ‹ a
match
  c_view_cat
    match c_view_cat i with
    | Vcat_l i => r_cat_l i
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l i
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_r j)) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_r j

    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 +β–Ά Ξ“2 βˆ‹ a
match
  c_view_cat
    match c_view_cat i with
    | Vcat_l i => r_cat_l i
    | Vcat_r j => r_cat_r (r_cat_l j)
    end
with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l i
 
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l (r_cat_l i)
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_l j)) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l (r_cat_r j)

      
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
i: Ξ“1 βˆ‹ a
match c_view_cat (r_cat_l i) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l (r_cat_l i)
 now rewrite c_view_cat_simpl_l.
      
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“2 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_l j)) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_l (r_cat_r j)
 now rewrite c_view_cat_simpl_r, c_view_cat_simpl_l.
    
T, C: Type
CC: context T C
CL: context_laws T C
Ξ“1, Ξ“2, Ξ“3: C
a: T
j: Ξ“3 βˆ‹ a
match c_view_cat (r_cat_r (r_cat_r j)) with
| Vcat_l i => r_cat_l (r_cat_l i)
| Vcat_r j =>
    match c_view_cat j with
    | Vcat_l i => r_cat_l (r_cat_r i)
    | Vcat_r j0 => r_cat_r j0
    end
end = r_cat_r j
 now rewrite 2 c_view_cat_simpl_r.
  Qed.
End with_param.

Misc.

Ltac asgn_unfold :=
  repeat unfold a_empty, a_cat, a_map, r_id, a_ren_l, a_cat, r_catβ‚‚, r_shift, r_cat3_1,
    r_cat3_2, r_cat3_3, r_assoc_r, r_assoc_l.

#[global] Notation "Ξ“ βŠ† Ξ”" := (assignment c_var Ξ“%ctx Ξ”%ctx).
#[global] Notation "r α΅£βŠ› u" := (a_ren_l r u) : asgn_scope.