From c7503815ef1543a22eb6336c28c7a5eda29667ba Mon Sep 17 00:00:00 2001
From: 1337777 <OOO1337777@outlook.com>
Date: Tue, 26 Nov 2024 18:35:41 +0400
Subject: [PATCH 1/2] Preliminary: alternative context-extension for
 dependent-types

This file will compare a usual traditional context-extension
  (categories with families, etc) versus a more general and clearer
  direct computational (strictified via Lambdapi rewrite rules) implementation
  as required for a proof assistant for categories/sheaves/schemes
---
 Context.lp | 159 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 159 insertions(+)
 create mode 100644 Context.lp

diff --git a/Context.lp b/Context.lp
new file mode 100644
index 0000000..fdb743b
--- /dev/null
+++ b/Context.lp
@@ -0,0 +1,159 @@
+/* Preliminary: alternative context-extension for dependent-types.
+  This file will compare a usual traditional context-extension 
+  (categories with families, etc) versus a more general and clearer 
+  direct computational (strictified via Lambdapi rewrite rules) implementation 
+  as required for a proof assistant for categories/sheaves/schemes
+*/
+
+/*  PRELIM: USUAL FORMULATION FOR TYPE THEORY
+
+data Con : Set
+
+postulate
+  Ty : Con → ℕ → Set
+
+infixl 2 _▹_
+data Con where
+  ◇ : Con
+  _▹_ : (Γ : Con) → Ty Γ i → Con
+
+postulate
+  Sub : Con → Con → Set
+
+postulate
+  _∘_ : Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
+  assoc : γ ∘ (δ ∘ θ) ≡ (γ ∘ δ) ∘ θ
+
+  id : Sub Γ Γ
+  idr : γ ∘ id ≡ γ
+  idl : id ∘ γ ≡ γ
+
+postulate
+  _[_]ᵀ : Ty Γ i → Sub Δ Γ → Ty Δ i
+  []ᵀ-∘ : A [ γ ∘ δ ]ᵀ ≡ A [ γ ]ᵀ [ δ ]ᵀ
+  []ᵀ-id : A [ id ]ᵀ ≡ A
+
+postulate
+  Tm : (Γ : Con) → Ty Γ i → Set
+
+
+postulate
+  _[_]ᵗ : Tm Γ A → (γ : Sub Δ Γ) → Tm Δ (A [ γ ]ᵀ)
+  []ᵗ-∘ : a [ γ ∘ δ ]ᵗ ≡[ ap-Tm []ᵀ-∘ ] a [ γ ]ᵗ [ δ ]ᵗ
+  []ᵗ-id : a [ id ]ᵗ ≡[ ap-Tm []ᵀ-id ] a
+
+postulate
+  ε : Sub Δ ◇
+  ε-∘ : ε ∘ γ ≡ ε
+  ◇-η : id ≡ ε
+
+  p : Sub (Γ ▹ A) Γ
+  q : Tm (Γ ▹ A) (A [ p ]ᵀ)
+
+  _,_ : (γ : Sub Δ Γ) → Tm Δ (A [ γ ]ᵀ) → Sub Δ (Γ ▹ A)
+  ,-∘ : (γ , a) ∘ δ ≡ (γ ∘ δ , coe (ap-Tm (sym []ᵀ-∘)) (a [ δ ]ᵗ))
+
+  ▹-β₁ : p ∘ (γ , a) ≡ γ
+  ▹-β₂ : q [ γ , a ]ᵗ ≡[ ap-Tm (sym []ᵀ-∘ ∙ ap-[]ᵀᵣ ▹-β₁) ] a
+  ▹-η : id ≡ (p , q) ∈ Sub (Γ ▹ A) (Γ ▹ A)
+
+  */
+
+// MORE GENERAL AND CLEARED FORMULATION FOR CATEGORIES
+
+constant symbol cat : TYPE ;
+
+constant symbol func : Π (A B : cat), TYPE ;
+
+constant symbol Id_func : Π [A : cat], func A A;
+symbol ∘> : Π [A B C: cat], func A B → func B C → func A C;
+notation ∘> infix left 90;
+
+rule $X ∘> ($G ∘> $H) ↪ ($X ∘> $G) ∘> $H
+with $F ∘> Id_func ↪ $F
+with Id_func ∘> $F ↪ $F;
+
+constant symbol Terminal_cat : cat;
+injective symbol Terminal_func :  Π (A : cat), func A Terminal_cat;
+
+rule (@∘> $A $B $C $F (Terminal_func $B)) ↪ (Terminal_func $A) ; 
+
+rule (Terminal_func (Terminal_cat)) ↪ Id_func;
+
+constant symbol catd: Π (X : cat), TYPE ; 
+
+constant symbol Terminal_catd : Π (A : cat), catd A;
+
+constant symbol funcd : Π [X Y : cat] (A : catd X) (F : func X Y) (B : catd Y), TYPE ;
+
+constant symbol  Id_funcd : Π [X : cat] [A : catd X], funcd A Id_func A;
+symbol ∘>d: Π [X Y Z : cat] [A : catd X] [B : catd Y] [C : catd Z] [F : func X Y]
+[G : func Y Z], funcd A F B → funcd B G C → funcd A (F ∘> G) C;
+notation ∘>d infix left 90;
+
+rule $X ∘>d ($G ∘>d $H) ↪ ($X ∘>d $G) ∘>d $H
+with $F ∘>d Id_funcd ↪ $F
+with Id_funcd ∘>d $F ↪ $F; 
+
+injective symbol Terminal_funcd :  Π [X Y: cat] (A : catd X) (xy : func X Y), funcd A xy (Terminal_catd Y);
+
+rule ($FF ∘>d (Terminal_funcd $B $xy)) ↪ (Terminal_funcd _ _) ;
+rule (Terminal_funcd (Terminal_catd _) Id_func) ↪ Id_funcd;
+
+symbol Fibre_catd : Π [X I : cat] (A : catd X) (x : func I X), catd I;
+
+rule Fibre_catd $A Id_func ↪ $A
+with Fibre_catd $A ($x ∘> $y)  ↪ Fibre_catd (Fibre_catd $A $y) $x
+with Fibre_catd (Terminal_catd _) _ ↪ (Terminal_catd _);
+
+symbol Fibre_intro_funcd : Π [X I I' : cat] (A : catd X) (x : func I X) [J : catd I'] (i : func I' I) ,
+ funcd J (i ∘> x) A  → funcd J i (Fibre_catd A x);
+
+symbol Fibre_elim_funcd : Π [X I : cat] (A : catd X) (x : func I X), funcd (Fibre_catd A x) x A;
+
+rule (Fibre_intro_funcd $A $x _ $FF) ∘>d (Fibre_elim_funcd $A $x) ↪ $FF ;
+rule $HH ∘>d (Fibre_intro_funcd $A $x _ $FF) ↪ (Fibre_intro_funcd $A $x _ ($HH ∘>d $FF)) ;
+
+rule Fibre_elim_funcd $A Id_func ↪ Id_funcd
+with (Fibre_elim_funcd /* (Fibre_catd $A $y) */ _ $x) ∘>d Fibre_elim_funcd $A $y  ↪ Fibre_elim_funcd $A ($x ∘> $y);
+
+rule Fibre_elim_funcd (Terminal_catd _) $xy ↪  (Terminal_funcd (Terminal_catd _) $xy) ;
+
+rule Fibre_intro_funcd $A Id_func $i $FF ↪ $FF
+// reverse direction?
+with (Fibre_intro_funcd /* (Fibre_catd $A $y) */ _ $x $i (Fibre_intro_funcd $A $y /* ($i ∘> $x) */ _ $FF)) 
+↪  (Fibre_intro_funcd $A ($x ∘> $y) $i $FF) 
+// with (Fibre_intro_funcd $A ($x ∘> $y) $i $FF) 
+// ↪ (Fibre_intro_funcd (Fibre_catd $A $y) $x $i (Fibre_intro_funcd $A $y ($i ∘> $x) $FF))
+;
+
+/* constant */ injective symbol Context_cat : Π [X : cat], catd X → cat;
+/* constant */ injective symbol Context_proj_func : Π [X : cat] (A : catd X), func (Context_cat A) X;
+injective symbol Context_proj2_funcd : Π [X : cat] (A : catd X), funcd (Terminal_catd _) (Context_proj_func A) A;
+/* constant */ injective symbol Context_intro_func : Π [Y : cat] [B : catd Y] [X] (xy : func X Y),
+funcd (Terminal_catd X) xy B → func X (Context_cat B);
+/* constant */ injective symbol Context_func : Π [X Y : cat] [A : catd X] [B : catd Y] [xy : func X Y],
+funcd A xy B → func (Context_cat A) (Context_cat B); 
+
+rule @Context_intro_func _ $A _ $xy $FF ∘> Context_proj_func $A ↪ $xy;
+
+rule (@Context_func _ _ $A $B $F $FF) ∘> (Context_proj_func $B) 
+↪ (Context_proj_func $A) ∘> $F;
+
+rule @Context_intro_func _ $A _ $xy $GG ∘> (@Context_func _ _ $A $B $F $FF) 
+↪ Context_intro_func _ ($GG ∘>d $FF);
+
+rule (Terminal_funcd (Terminal_catd _) (@Context_intro_func _ $A _ $xy $GG)) ∘>d (Context_proj2_funcd $B) 
+↪ $GG;
+
+rule (@Context_func $X $Y $A $B $F $FF) ∘> (@Context_func $Y $Z $B $C $G $GG)
+ ↪  Context_func ($FF ∘>d $GG);
+
+rule Context_cat (Terminal_catd $A) ↪ $A;
+
+rule Context_proj_func (Terminal_catd $A) ↪ Id_func;
+
+rule Context_intro_func $xy (Terminal_funcd _ _) ↪ $xy;
+
+rule Context_func (Id_funcd)  ↪ Id_func;
+

From 9a6756d176d803f5db848d880a7ae4025e6a28e3 Mon Sep 17 00:00:00 2001
From: 1337777 <admin@anthroplogic.onmicrosoft.com>
Date: Tue, 10 Dec 2024 18:26:40 +0400
Subject: [PATCH 2/2] Update Context.lp

---
 Context.lp | 274 ++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 177 insertions(+), 97 deletions(-)

diff --git a/Context.lp b/Context.lp
index fdb743b..03c8c7a 100644
--- a/Context.lp
+++ b/Context.lp
@@ -5,155 +5,235 @@
   as required for a proof assistant for categories/sheaves/schemes
 */
 
-/*  PRELIM: USUAL FORMULATION FOR TYPE THEORY
+/*****************************************
+* # PRELIMINARIES REMINDERS ABOUT DEPENDENT TYPES
+* AND IMPLEMENTING CONTEXT-EXTENSION 
+* (CATEGORIES WITH FAMILIES) WHICH COMPUTES
+******************************************/
 
-data Con : Set
+constant symbol 
+  Con : TYPE;
 
-postulate
-  Ty : Con → ℕ → Set
+constant symbol
+  Ty : Con → TYPE;
 
-infixl 2 _▹_
-data Con where
-  ◇ : Con
-  _▹_ : (Γ : Con) → Ty Γ i → Con
+constant symbol
+  ◇ : Con;
 
-postulate
-  Sub : Con → Con → Set
+injective symbol
+  ▹ : Π (Γ : Con), Ty Γ → Con;
 
-postulate
-  _∘_ : Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
-  assoc : γ ∘ (δ ∘ θ) ≡ (γ ∘ δ) ∘ θ
+notation ▹ infix right 90;
 
-  id : Sub Γ Γ
-  idr : γ ∘ id ≡ γ
-  idl : id ∘ γ ≡ γ
+constant symbol
+  Sub : Con → Con → TYPE;
 
-postulate
-  _[_]ᵀ : Ty Γ i → Sub Δ Γ → Ty Δ i
-  []ᵀ-∘ : A [ γ ∘ δ ]ᵀ ≡ A [ γ ]ᵀ [ δ ]ᵀ
-  []ᵀ-id : A [ id ]ᵀ ≡ A
+symbol
+  ∘ : Π [Δ Γ Θ], Sub Δ Γ → Sub Θ Δ → Sub Θ Γ;
 
-postulate
-  Tm : (Γ : Con) → Ty Γ i → Set
+notation ∘ infix right 80;
 
+rule /* assoc */ 
+  $γ ∘ ($δ ∘ $θ) ↪ ($γ ∘ $δ) ∘ $θ;
 
-postulate
-  _[_]ᵗ : Tm Γ A → (γ : Sub Δ Γ) → Tm Δ (A [ γ ]ᵀ)
-  []ᵗ-∘ : a [ γ ∘ δ ]ᵗ ≡[ ap-Tm []ᵀ-∘ ] a [ γ ]ᵗ [ δ ]ᵗ
-  []ᵗ-id : a [ id ]ᵗ ≡[ ap-Tm []ᵀ-id ] a
+constant symbol
+  id : Π [Γ], Sub Γ Γ;
 
-postulate
-  ε : Sub Δ ◇
-  ε-∘ : ε ∘ γ ≡ ε
-  ◇-η : id ≡ ε
+rule /* idr */ 
+  $γ ∘ id ↪ $γ
+with /* idl */ 
+  id ∘ $γ ↪ $γ;
 
-  p : Sub (Γ ▹ A) Γ
-  q : Tm (Γ ▹ A) (A [ p ]ᵀ)
+symbol
+  'ᵀ_ : Π [Γ Δ], Ty Γ → Sub Δ Γ → Ty Δ;
 
-  _,_ : (γ : Sub Δ Γ) → Tm Δ (A [ γ ]ᵀ) → Sub Δ (Γ ▹ A)
-  ,-∘ : (γ , a) ∘ δ ≡ (γ ∘ δ , coe (ap-Tm (sym []ᵀ-∘)) (a [ δ ]ᵗ))
+notation 'ᵀ_ infix left 70;
 
-  ▹-β₁ : p ∘ (γ , a) ≡ γ
-  ▹-β₂ : q [ γ , a ]ᵗ ≡[ ap-Tm (sym []ᵀ-∘ ∙ ap-[]ᵀᵣ ▹-β₁) ] a
-  ▹-η : id ≡ (p , q) ∈ Sub (Γ ▹ A) (Γ ▹ A)
+rule /* 'ᵀ_-∘ */ 
+  $A 'ᵀ_ $γ 'ᵀ_ $δ ↪ $A 'ᵀ_( $γ ∘ $δ )
+with /* 'ᵀ_-id */
+  $A 'ᵀ_ id ↪ $A;
 
-  */
+constant symbol
+  Tm : Π (Γ : Con), Ty Γ → TYPE;
 
-// MORE GENERAL AND CLEARED FORMULATION FOR CATEGORIES
+symbol
+  'ᵗ_ : Π [Γ A Δ], Tm Γ A → Π (γ : Sub Δ Γ), Tm Δ (A 'ᵀ_ γ);
 
-constant symbol cat : TYPE ;
+notation 'ᵗ_ infix left 70;
 
-constant symbol func : Π (A B : cat), TYPE ;
+rule /*  'ᵗ_-∘ */ 
+  $a 'ᵗ_ $γ 'ᵗ_ $δ ↪ $a 'ᵗ_( $γ ∘ $δ )
+with /* 'ᵗ_-id */ 
+  $a 'ᵗ_ id ↪ $a;
+
+injective symbol
+  ε : Π [Δ], Sub Δ ◇;
+
+rule /* ε-∘ */
+  ε ∘ $γ ↪ ε
+with /* ◇-η */
+  @ε ◇ ↪ id;
+
+injective symbol 
+  pₓ : Π [Γ A], Sub (Γ ▹ A) Γ;
+
+injective symbol 
+  qₓ : Π [Γ A], Tm (Γ ▹ A) (A 'ᵀ_ pₓ);
+
+injective symbol 
+  &ₓ : Π [Γ Δ A], Π (γ : Sub Δ Γ), Tm Δ (A 'ᵀ_ γ) → Sub Δ (Γ ▹ A);
+
+notation &ₓ infix left 70;
+
+rule /*  &ₓ-∘ */
+  ($γ &ₓ $a) ∘ $δ ↪ ($γ ∘ $δ &ₓ ($a 'ᵗ_ $δ));
+
+rule /*  ▹-β₁ */ 
+  pₓ ∘ ($γ &ₓ $a) ↪ $γ;
+
+rule /* ▹-β₂ */ 
+  qₓ 'ᵗ_ ($γ &ₓ $a) ↪ $a;
+
+rule /* ▹-η */
+  (@&ₓ _ _ $A (@pₓ _ $A) qₓ) ↪ id;
+
+
+/*****************************************
+* # CATEGORIES, FUNCTORS, ISOFIBRATIONS OF CATEGORIES
+******************************************/
+
+constant symbol cat : TYPE;
+
+constant symbol func : Π (A B : cat), TYPE;
+
+constant symbol catd: Π (X : cat), TYPE;
+
+constant symbol funcd : Π [X Y : cat] (A : catd X) (F : func X Y) (B : catd Y), TYPE;
+
+/* -----
+* ## categories and functors (objects) */
+
+constant symbol Terminal_cat : cat;
 
 constant symbol Id_func : Π [A : cat], func A A;
+
 symbol ∘> : Π [A B C: cat], func A B → func B C → func A C;
-notation ∘> infix left 90;
+notation ∘> infix left 90; // compo_func
 
 rule $X ∘> ($G ∘> $H) ↪ ($X ∘> $G) ∘> $H
 with $F ∘> Id_func ↪ $F
 with Id_func ∘> $F ↪ $F;
 
-constant symbol Terminal_cat : cat;
 injective symbol Terminal_func :  Π (A : cat), func A Terminal_cat;
 
-rule (@∘> $A $B $C $F (Terminal_func $B)) ↪ (Terminal_func $A) ; 
-
-rule (Terminal_func (Terminal_cat)) ↪ Id_func;
+rule (@∘> $A $B $C $F (Terminal_func $B)) ↪ (Terminal_func $A)
+with (Terminal_func (Terminal_cat)) ↪ Id_func;
 
-constant symbol catd: Π (X : cat), TYPE ; 
+/* -----
+* ## fibred (dependent) categories */
 
 constant symbol Terminal_catd : Π (A : cat), catd A;
 
-constant symbol funcd : Π [X Y : cat] (A : catd X) (F : func X Y) (B : catd Y), TYPE ;
+symbol Fibre_catd : Π [X I : cat] (A : catd X) (x : func I X), catd I;
+
+rule Fibre_catd $A Id_func ↪ $A
+with Fibre_catd $A ($x ∘> $y) ↪ Fibre_catd (Fibre_catd $A $y) $x;
+rule Fibre_catd (Terminal_catd _) _ ↪ (Terminal_catd _);
+
+/* -----
+* ## fibred (dependent) functors */
+
+constant symbol Id_funcd : Π [X : cat] [A : catd X], funcd A Id_func A;
 
-constant symbol  Id_funcd : Π [X : cat] [A : catd X], funcd A Id_func A;
 symbol ∘>d: Π [X Y Z : cat] [A : catd X] [B : catd Y] [C : catd Z] [F : func X Y]
 [G : func Y Z], funcd A F B → funcd B G C → funcd A (F ∘> G) C;
-notation ∘>d infix left 90;
+notation ∘>d infix left 90; // compo_funcd
 
 rule $X ∘>d ($G ∘>d $H) ↪ ($X ∘>d $G) ∘>d $H
 with $F ∘>d Id_funcd ↪ $F
-with Id_funcd ∘>d $F ↪ $F; 
+with Id_funcd ∘>d $F ↪ $F;
 
 injective symbol Terminal_funcd :  Π [X Y: cat] (A : catd X) (xy : func X Y), funcd A xy (Terminal_catd Y);
 
-rule ($FF ∘>d (Terminal_funcd $B $xy)) ↪ (Terminal_funcd _ _) ;
-rule (Terminal_funcd (Terminal_catd _) Id_func) ↪ Id_funcd;
+injective symbol Fibre_intro_funcd : Π [X I I' : cat] (A : catd X) (x : func I X) [J : catd I'] (i : func I' I) ,
+ funcd J (i ∘> x) A → funcd J i (Fibre_catd A x);
 
-symbol Fibre_catd : Π [X I : cat] (A : catd X) (x : func I X), catd I;
+injective symbol Fibre_elim_funcd : Π [X I : cat] (A : catd X) (x : func I X), funcd (Fibre_catd A x) x A;
 
-rule Fibre_catd $A Id_func ↪ $A
-with Fibre_catd $A ($x ∘> $y)  ↪ Fibre_catd (Fibre_catd $A $y) $x
-with Fibre_catd (Terminal_catd _) _ ↪ (Terminal_catd _);
+// naturality
+rule $HH ∘>d (Fibre_intro_funcd $A $x _ $FF) ↪ (Fibre_intro_funcd $A $x _ ($HH ∘>d $FF))
+with (Fibre_elim_funcd /*DON'T SPECIFY, ALLOW CONVERSION: (Fibre_catd $A $y) */ _ $x) ∘>d Fibre_elim_funcd $A $y
+ ↪ Fibre_elim_funcd $A ($x ∘> $y);
 
-symbol Fibre_intro_funcd : Π [X I I' : cat] (A : catd X) (x : func I X) [J : catd I'] (i : func I' I) ,
- funcd J (i ∘> x) A  → funcd J i (Fibre_catd A x);
-
-symbol Fibre_elim_funcd : Π [X I : cat] (A : catd X) (x : func I X), funcd (Fibre_catd A x) x A;
-
-rule (Fibre_intro_funcd $A $x _ $FF) ∘>d (Fibre_elim_funcd $A $x) ↪ $FF ;
-rule $HH ∘>d (Fibre_intro_funcd $A $x _ $FF) ↪ (Fibre_intro_funcd $A $x _ ($HH ∘>d $FF)) ;
+// beta, eta
+rule (Fibre_intro_funcd $A $x _ $FF) ∘>d (Fibre_elim_funcd $A $x) ↪ $FF
+with (Fibre_intro_funcd $A $x Id_func (Fibre_elim_funcd $A $x)) ↪ Id_funcd;
 
 rule Fibre_elim_funcd $A Id_func ↪ Id_funcd
-with (Fibre_elim_funcd /* (Fibre_catd $A $y) */ _ $x) ∘>d Fibre_elim_funcd $A $y  ↪ Fibre_elim_funcd $A ($x ∘> $y);
-
-rule Fibre_elim_funcd (Terminal_catd _) $xy ↪  (Terminal_funcd (Terminal_catd _) $xy) ;
-
-rule Fibre_intro_funcd $A Id_func $i $FF ↪ $FF
-// reverse direction?
+with Fibre_intro_funcd $A Id_func $i $FF ↪ $FF
 with (Fibre_intro_funcd /* (Fibre_catd $A $y) */ _ $x $i (Fibre_intro_funcd $A $y /* ($i ∘> $x) */ _ $FF)) 
-↪  (Fibre_intro_funcd $A ($x ∘> $y) $i $FF) 
-// with (Fibre_intro_funcd $A ($x ∘> $y) $i $FF) 
-// ↪ (Fibre_intro_funcd (Fibre_catd $A $y) $x $i (Fibre_intro_funcd $A $y ($i ∘> $x) $FF))
-;
+↪ (Fibre_intro_funcd $A ($x ∘> $y) $i $FF);
 
-/* constant */ injective symbol Context_cat : Π [X : cat], catd X → cat;
-/* constant */ injective symbol Context_proj_func : Π [X : cat] (A : catd X), func (Context_cat A) X;
-injective symbol Context_proj2_funcd : Π [X : cat] (A : catd X), funcd (Terminal_catd _) (Context_proj_func A) A;
-/* constant */ injective symbol Context_intro_func : Π [Y : cat] [B : catd Y] [X] (xy : func X Y),
-funcd (Terminal_catd X) xy B → func X (Context_cat B);
-/* constant */ injective symbol Context_func : Π [X Y : cat] [A : catd X] [B : catd Y] [xy : func X Y],
-funcd A xy B → func (Context_cat A) (Context_cat B); 
+rule (Terminal_funcd (Terminal_catd _) $xy) ↪ Fibre_elim_funcd (Terminal_catd _) $xy;
+rule ($FF ∘>d (Terminal_funcd $B $xy)) ↪ (Terminal_funcd _ _);
+rule (Terminal_funcd (Terminal_catd _) Id_func) ↪ Id_funcd; // confluent...
 
-rule @Context_intro_func _ $A _ $xy $FF ∘> Context_proj_func $A ↪ $xy;
 
-rule (@Context_func _ _ $A $B $F $FF) ∘> (Context_proj_func $B) 
-↪ (Context_proj_func $A) ∘> $F;
+/*****************************************
+* # CONTEXT EXTENSION FOR CATEGORIES
+******************************************/
 
-rule @Context_intro_func _ $A _ $xy $GG ∘> (@Context_func _ _ $A $B $F $FF) 
-↪ Context_intro_func _ ($GG ∘>d $FF);
+injective symbol Context_cat : Π [X : cat], catd X → cat;
 
-rule (Terminal_funcd (Terminal_catd _) (@Context_intro_func _ $A _ $xy $GG)) ∘>d (Context_proj2_funcd $B) 
-↪ $GG;
+injective symbol Context_elimCat_func : Π [X : cat] (A : catd X), func (Context_cat A) X;
 
-rule (@Context_func $X $Y $A $B $F $FF) ∘> (@Context_func $Y $Z $B $C $G $GG)
- ↪  Context_func ($FF ∘>d $GG);
+injective symbol Context_elimCatd_funcd : Π [X : cat] (A : catd X), funcd (Terminal_catd _) (Context_elimCat_func A) A;
 
-rule Context_cat (Terminal_catd $A) ↪ $A;
-
-rule Context_proj_func (Terminal_catd $A) ↪ Id_func;
-
-rule Context_intro_func $xy (Terminal_funcd _ _) ↪ $xy;
-
-rule Context_func (Id_funcd)  ↪ Id_func;
+injective symbol Context_intro_func : Π [X Y : cat] [A : catd X] [B : catd Y] [xy : func X Y],
+funcd A xy B → func (Context_cat A) (Context_cat B);
 
+rule Context_cat (Terminal_catd $A) ↪ $A;
+rule Context_elimCat_func (Terminal_catd $A) ↪ Id_func;
+rule Context_elimCatd_funcd (Terminal_catd $A) ↪ Id_funcd;
+rule Context_intro_func (Id_funcd) ↪ Id_func
+with Context_intro_func (Terminal_funcd $A $xy) ↪ Context_elimCat_func $A ∘> $xy;
+
+// definable symbols
+injective symbol Context_intro_single_func [Y : cat] [B : catd Y] [X] (xy : func X Y)
+(FF : funcd (Terminal_catd X) xy B) : func X (Context_cat B);
+rule Context_intro_single_func _ $FF ↪ @Context_intro_func _ _ (Terminal_catd _) _ _ $FF;
+
+injective symbol Context_intro_congr_func [Y : cat] [B : catd Y] [X] (xy : func X Y) 
+: func (Context_cat (Fibre_catd B xy)) (Context_cat B);
+rule Context_intro_congr_func $xy ↪ Context_intro_func (Fibre_elim_funcd _ $xy);
+
+// beta rules
+rule (@Context_intro_func _ _ $A $B $F $FF) ∘> (Context_elimCat_func $B) 
+↪ (Context_elimCat_func $A) ∘> $F;
+rule (Fibre_elim_funcd (Terminal_catd $X) (@Context_intro_func _ _ (Terminal_catd $X) $B $xy $FF)) ∘>d (Context_elimCatd_funcd $B) 
+↪ $FF;
+
+// LAMBDAPI BUG? this unification rule doesnt work... so finding an alternative
+// unif_rule Context_cat $B ≡ (Context_cat (Terminal_catd (Context_cat $X))) ↪ [ $B ≡ $X];
+symbol rule_Context_cat_Terminal_catd_func [X: cat] (A: catd X) 
+: func (Context_cat (Terminal_catd (Context_cat A))) (Context_cat A)
+≔ begin assume X A; simplify; refine Id_func; end;
+
+// eta rules
+rule Context_intro_func (Context_elimCatd_funcd $A) 
+ ↪ rule_Context_cat_Terminal_catd_func $A;
+rule @Context_intro_func _ _ _ _ $xy (Fibre_elim_funcd (Terminal_catd _) _) ↪ $xy;
+
+// naturality rules
+// confluent ... and both rules required despite in meta the latter conversion is derivable from the former rules
+rule (@Context_intro_func $X $Y $A $B $F $FF) ∘> (@Context_intro_func $Y $Z $B $C $G $GG)
+ ↪ Context_intro_func ($FF ∘>d $GG)
+with $z ∘> @Context_intro_func _ _ (Terminal_catd _) _ _ $FF
+↪ Context_intro_func ( (Fibre_elim_funcd (Terminal_catd _) $z)  ∘>d $FF );
+
+assert [X Y : cat] [B : catd Y] [xy : func X Y] (FF : funcd (Terminal_catd X) xy B) [Z] [z : func Z X] ⊢  
+(@Context_intro_func _ _ _ _ z (Terminal_funcd (Terminal_catd Z) z)) ∘> Context_intro_func FF
+ ≡ Context_intro_func ( (Terminal_funcd (Terminal_catd Z) z)  ∘>d FF );
+
+/* voila */