Renamed 'EqView' to 'ShapeView'

Definition/LogicalRelation/Application.agda

@@ -13,7 +13,7 @@ import Definition.Typed.Weakening as T
 open import Definition.Typed.Properties
 open import Definition.Typed.RedSteps
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties
 

Definition/LogicalRelation/Irrelevance.agda

@@ -11,7 +11,7 @@ open import Definition.Typed
 open import Definition.Typed.Properties
 open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 
 open import Tools.Product
 import Tools.PropositionalEquality as PE
@@ -63,9 +63,9 @@ mutual
                       → Γ ∙ C ⊩⟨ l ⟩ A ≡ B / p → Γ ∙ C′ ⊩⟨ l′ ⟩ A′ ≡ B′ / q
   irrelevanceEqLift″ PE.refl PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B
 
-  -- Helper for irrelevance of type equality using equality view
+  -- Helper for irrelevance of type equality using shape view
   irrelevanceEqT : ∀ {Γ A B l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
-                       → EqView Γ l l′ A A p q
+                       → ShapeView Γ l l′ A A p q
                        → Γ ⊩⟨ l ⟩ A ≡ B / p → Γ ⊩⟨ l′ ⟩ A ≡ B / q
   irrelevanceEqT (ℕ D D′) A≡B = A≡B
   irrelevanceEqT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
@@ -119,9 +119,9 @@ mutual
                      → Γ′ ⊩⟨ l′ ⟩ t′ ∷ A′ / [A′]
   irrelevanceTermΓ″ PE.refl PE.refl PE.refl [A] [A′] [t] = irrelevanceTerm [A] [A′] [t]
 
-  -- Helper for irrelevance of terms using equality view
+  -- Helper for irrelevance of terms using shape view
   irrelevanceTermT : ∀ {Γ A t l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
-                         → EqView Γ l l′ A A p q
+                         → ShapeView Γ l l′ A A p q
                          → Γ ⊩⟨ l ⟩ t ∷ A / p → Γ ⊩⟨ l′ ⟩ t ∷ A / q
   irrelevanceTermT (ℕ D D′) t = t
   irrelevanceTermT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ k d nf)
@@ -174,9 +174,9 @@ mutual
                       → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t′ ≡ u′ ∷ A′ / q
   irrelevanceEqTerm″ PE.refl PE.refl PE.refl p q t≡u = irrelevanceEqTerm p q t≡u
 
-  -- Helper for irrelevance of term equality using equality view
+  -- Helper for irrelevance of term equality using shape view
   irrelevanceEqTermT : ∀ {Γ A t u} {l l′} {p : Γ ⊩⟨ l ⟩ A} {q : Γ ⊩⟨ l′ ⟩ A}
-                           → EqView Γ l l′ A A p q
+                           → ShapeView Γ l l′ A A p q
                            → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A / q
   irrelevanceEqTermT (ℕ D D′) t≡u = t≡u
   irrelevanceEqTermT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ₌ k m d d′ nf)

Definition/LogicalRelation/Properties/Conversion.agda

@@ -11,7 +11,7 @@ open import Definition.Typed.RedSteps
 open import Definition.Typed.Properties
 open import Definition.Typed.Weakening
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties.Escape
 
@@ -26,7 +26,7 @@ convRed:*: [ ⊢t , ⊢u , d ] A≡B = [ conv ⊢t  A≡B , conv ⊢u  A≡B , c
 mutual
   -- Helper function for conversion of terms converting from left to right.
   convTermT₁ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
-             → EqView Γ l l′ A B [A] [B]
+             → ShapeView Γ l l′ A B [A] [B]
              → Γ ⊩⟨ l ⟩  A ≡ B / [A]
              → Γ ⊩⟨ l ⟩  t ∷ A / [A]
              → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
@@ -74,7 +74,7 @@ mutual
 
   -- Helper function for conversion of terms converting from right to left.
   convTermT₂ : ∀ {l l′ Γ A B t} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
-           → EqView Γ l l′ A B [A] [B]
+           → ShapeView Γ l l′ A B [A] [B]
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B / [B]
            → Γ ⊩⟨ l ⟩  t ∷ A / [A]
@@ -147,7 +147,7 @@ mutual
 
   -- Helper function for conversion of term equality converting from left to right.
   convEqTermT₁ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
-               → EqView Γ l l′ A B [A] [B]
+               → ShapeView Γ l l′ A B [A] [B]
                → Γ ⊩⟨ l ⟩  A ≡ B / [A]
                → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]
                → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
@@ -190,7 +190,7 @@ mutual
 
   -- Helper function for conversion of term equality converting from right to left.
   convEqTermT₂ : ∀ {l l′ Γ A B t u} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
-             → EqView Γ l l′ A B [A] [B]
+             → ShapeView Γ l l′ A B [A] [B]
              → Γ ⊩⟨ l ⟩  A ≡ B / [A]
              → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B / [B]
              → Γ ⊩⟨ l ⟩  t ≡ u ∷ A / [A]

Definition/LogicalRelation/Properties/Neutral.agda

@@ -10,7 +10,7 @@ open import Definition.Typed
 open import Definition.Typed.Properties
 open import Definition.Typed.Weakening
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties.Reflexivity
 open import Definition.LogicalRelation.Properties.Escape

Definition/LogicalRelation/Properties/Reduction.agda

@@ -11,7 +11,7 @@ open import Definition.Typed.Weakening
 open import Definition.Typed.Properties
 open import Definition.Typed.RedSteps
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Properties.Reflexivity
 open import Definition.LogicalRelation.Properties.Symmetry
 open import Definition.LogicalRelation.Properties.Transitivity

Definition/LogicalRelation/Properties/Successor.agda

@@ -10,7 +10,7 @@ open import Definition.Typed
 open import Definition.Typed.Properties
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 
 open import Tools.Product
 

Definition/LogicalRelation/Properties/Symmetry.agda

@@ -10,7 +10,7 @@ open import Definition.Typed
 open import Definition.Typed.Properties
 open import Definition.Typed.Weakening
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties.Conversion
 
@@ -19,9 +19,9 @@ import Tools.PropositionalEquality as PE
 
 
 mutual
-  -- Helper function for symmetry of type equality using equality views.
+  -- Helper function for symmetry of type equality using shape views.
   symEqT : ∀ {Γ A B l l′} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
-         → EqView Γ l l′ A B [A] [B]
+         → ShapeView Γ l l′ A B [A] [B]
          → Γ ⊩⟨ l  ⟩ A ≡ B / [A]
          → Γ ⊩⟨ l′ ⟩ B ≡ A / [B]
   symEqT (ℕ D D′) A≡B = red D

Definition/LogicalRelation/Properties/Transitivity.agda

@@ -10,7 +10,7 @@ open import Definition.Typed
 open import Definition.Typed.Properties
 open import Definition.Typed.Weakening
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties.Conversion
 
@@ -19,10 +19,10 @@ import Tools.PropositionalEquality as PE
 
 
 mutual
-  -- Helper function for transitivity of type equality using equality views.
+  -- Helper function for transitivity of type equality using shape views.
   transEqT : ∀ {Γ A B C l l′ l″}
              {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B} {[C] : Γ ⊩⟨ l″ ⟩ C}
-           → EqView₃ Γ l l′ l″ A B C [A] [B] [C]
+           → ShapeView₃ Γ l l′ l″ A B C [A] [B] [C]
            → Γ ⊩⟨ l ⟩  A ≡ B / [A]
            → Γ ⊩⟨ l′ ⟩ B ≡ C / [B]
            → Γ ⊩⟨ l ⟩  A ≡ C / [A]

Definition/LogicalRelation/Properties/Universe.agda

@@ -9,7 +9,7 @@ open import Definition.Untyped
 open import Definition.Typed
 open import Definition.Typed.Properties as T
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 
 open import Tools.Product

Definition/LogicalRelation/EqView.agda → Definition/LogicalRelation/ShapeView.agda

@@ -2,7 +2,7 @@
 
 open import Definition.Typed.EqualityRelation
 
-module Definition.LogicalRelation.EqView {{eqrel : EqRelSet}} where
+module Definition.LogicalRelation.ShapeView {{eqrel : EqRelSet}} where
 open EqRelSet {{...}}
 
 open import Definition.Untyped
@@ -112,23 +112,23 @@ extractMaybeEmb (noemb x) = _ , x
 extractMaybeEmb (emb 0<1 x) = extractMaybeEmb x
 
 -- A view for constructor equality of types where embeddings are ignored
-data EqView Γ : ∀ l l′ A B (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ B) → Set where
-  U : ∀ {l l′} UA UB → EqView Γ l l′ U U (U UA) (U UB)
-  ℕ : ∀ {A B l l′} ℕA ℕB → EqView Γ l l′ A B (ℕ ℕA) (ℕ ℕB)
+data ShapeView Γ : ∀ l l′ A B (p : Γ ⊩⟨ l ⟩ A) (q : Γ ⊩⟨ l′ ⟩ B) → Set where
+  U : ∀ {l l′} UA UB → ShapeView Γ l l′ U U (U UA) (U UB)
+  ℕ : ∀ {A B l l′} ℕA ℕB → ShapeView Γ l l′ A B (ℕ ℕA) (ℕ ℕB)
   ne  : ∀ {A B l l′} neA neB
-      → EqView Γ l l′ A B (ne neA) (ne neB)
+      → ShapeView Γ l l′ A B (ne neA) (ne neB)
   Π : ∀ {A B l l′} ΠA ΠB
-    → EqView Γ l l′ A B (Π ΠA) (Π ΠB)
+    → ShapeView Γ l l′ A B (Π ΠA) (Π ΠB)
   emb⁰¹ : ∀ {A B l p q}
-        → EqView Γ ⁰ l A B p q
-        → EqView Γ ¹ l A B (emb 0<1 p) q
+        → ShapeView Γ ⁰ l A B p q
+        → ShapeView Γ ¹ l A B (emb 0<1 p) q
   emb¹⁰ : ∀ {A B l p q}
-        → EqView Γ l ⁰ A B p q
-        → EqView Γ l ¹ A B p (emb 0<1 q)
+        → ShapeView Γ l ⁰ A B p q
+        → ShapeView Γ l ¹ A B p (emb 0<1 q)
 
--- Construct an equality view from an equality
+-- Construct an shape view from an equality
 goodCases : ∀ {l l′ Γ A B} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
-          → Γ ⊩⟨ l ⟩ A ≡ B / [A] → EqView Γ l l′ A B [A] [B]
+          → Γ ⊩⟨ l ⟩ A ≡ B / [A] → ShapeView Γ l l′ A B [A] [B]
 goodCases (U UA) (U UB) A≡B = U UA UB
 goodCases (U′ _ _ ⊢Γ) (ℕ D) PE.refl = ⊥-elim (U≢ℕ (whnfRed* (red D) U))
 goodCases (U′ _ _ ⊢Γ) (ne′ K D neK K≡K) PE.refl = ⊥-elim (U≢ne neK (whnfRed* (red D) U))
@@ -162,39 +162,39 @@ goodCases {l} [A] (emb 0<1 x) A≡B =
 goodCases {l′ = l} (emb 0<1 x) [B] A≡B =
   emb⁰¹ (goodCases {⁰} {l} x [B] A≡B)
 
--- Construct an equality view between two derivations of the same type
+-- Construct an shape view between two derivations of the same type
 goodCasesRefl : ∀ {l l′ Γ A} ([A] : Γ ⊩⟨ l ⟩ A) ([A′] : Γ ⊩⟨ l′ ⟩ A)
-              → EqView Γ l l′ A A [A] [A′]
+              → ShapeView Γ l l′ A A [A] [A′]
 goodCasesRefl [A] [A′] = goodCases [A] [A′] (reflEq [A])
 
 
 -- A view for constructor equality between three types
-data EqView₃ Γ : ∀ l l′ l″ A B C
+data ShapeView₃ Γ : ∀ l l′ l″ A B C
                  (p : Γ ⊩⟨ l   ⟩ A)
                  (q : Γ ⊩⟨ l′  ⟩ B)
                  (r : Γ ⊩⟨ l″ ⟩ C) → Set where
-  U : ∀ {l l′ l″} UA UB UC → EqView₃ Γ l l′ l″ U U U (U UA) (U UB) (U UC)
+  U : ∀ {l l′ l″} UA UB UC → ShapeView₃ Γ l l′ l″ U U U (U UA) (U UB) (U UC)
   ℕ : ∀ {A B C l l′ l″} ℕA ℕB ℕC
-    → EqView₃ Γ l l′ l″ A B C (ℕ ℕA) (ℕ ℕB) (ℕ ℕC)
+    → ShapeView₃ Γ l l′ l″ A B C (ℕ ℕA) (ℕ ℕB) (ℕ ℕC)
   ne  : ∀ {A B C l l′ l″} neA neB neC
-      → EqView₃ Γ l l′ l″ A B C (ne neA) (ne neB) (ne neC)
+      → ShapeView₃ Γ l l′ l″ A B C (ne neA) (ne neB) (ne neC)
   Π : ∀ {A B C l l′ l″} ΠA ΠB ΠC
-    → EqView₃ Γ l l′ l″ A B C (Π ΠA) (Π ΠB) (Π ΠC)
+    → ShapeView₃ Γ l l′ l″ A B C (Π ΠA) (Π ΠB) (Π ΠC)
   emb⁰¹¹ : ∀ {A B C l l′ p q r}
-         → EqView₃ Γ ⁰ l l′ A B C p q r
-         → EqView₃ Γ ¹ l l′ A B C (emb 0<1 p) q r
+         → ShapeView₃ Γ ⁰ l l′ A B C p q r
+         → ShapeView₃ Γ ¹ l l′ A B C (emb 0<1 p) q r
   emb¹⁰¹ : ∀ {A B C l l′ p q r}
-         → EqView₃ Γ l ⁰ l′ A B C p q r
-         → EqView₃ Γ l ¹ l′ A B C p (emb 0<1 q) r
+         → ShapeView₃ Γ l ⁰ l′ A B C p q r
+         → ShapeView₃ Γ l ¹ l′ A B C p (emb 0<1 q) r
   emb¹¹⁰ : ∀ {A B C l l′ p q r}
-         → EqView₃ Γ l l′ ⁰ A B C p q r
-         → EqView₃ Γ l l′ ¹ A B C p q (emb 0<1 r)
+         → ShapeView₃ Γ l l′ ⁰ A B C p q r
+         → ShapeView₃ Γ l l′ ¹ A B C p q (emb 0<1 r)
 
 -- Combines two two-way views into a three-way view
 combine : ∀ {Γ l l′ l″ l‴ A B C [A] [B] [B]′ [C]}
-        → EqView Γ l l′ A B [A] [B]
-        → EqView Γ l″ l‴ B C [B]′ [C]
-        → EqView₃ Γ l l′ l‴ A B C [A] [B] [C]
+        → ShapeView Γ l l′ A B [A] [B]
+        → ShapeView Γ l″ l‴ B C [B]′ [C]
+        → ShapeView₃ Γ l l′ l‴ A B C [A] [B] [C]
 combine (U UA₁ UB₁) (U UA UB) = U UA₁ UB₁ UB
 combine (U UA UB) (ℕ ℕA ℕB) = ⊥-elim (U≢ℕ (whnfRed* (red ℕA) U))
 combine (U UA UB) (ne (ne K D neK K≡K) neB) =

Definition/LogicalRelation/Substitution/Introductions/Lambda.agda

@@ -12,7 +12,7 @@ open import Definition.Typed.Properties
 open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
 open import Definition.Typed.RedSteps
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Weakening
 open import Definition.LogicalRelation.Properties

Definition/LogicalRelation/Substitution/Introductions/Natrec.agda

@@ -12,7 +12,7 @@ import Definition.Typed.Weakening as T
 open import Definition.Typed.Properties
 open import Definition.Typed.RedSteps
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties
 open import Definition.LogicalRelation.Application

Definition/LogicalRelation/Substitution/Introductions/Pi.agda

@@ -11,7 +11,7 @@ open import Definition.Typed
 open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
 open import Definition.Typed.Properties
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Weakening
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties

Definition/LogicalRelation/Substitution/Introductions/SingleSubst.agda

@@ -12,7 +12,7 @@ import Definition.Typed.Weakening as T
 open import Definition.Typed.Properties
 open import Definition.Typed.RedSteps
 open import Definition.LogicalRelation
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Irrelevance
 open import Definition.LogicalRelation.Properties
 open import Definition.LogicalRelation.Substitution

Definition/LogicalRelation/Substitution/Introductions/Universe.agda

@@ -8,7 +8,7 @@ open EqRelSet {{...}}
 open import Definition.Untyped
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Properties
 open import Definition.LogicalRelation.Substitution
 

Definition/LogicalRelation/Weakening.agda

@@ -13,7 +13,7 @@ open import Definition.Typed.Weakening as T hiding (wk; wkEq; wkTerm; wkEqTerm)
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Properties.Reflexivity
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 
 open import Tools.Product
 open import Tools.Unit

Definition/Typed/Consequences/Canonicity.agda

@@ -15,7 +15,7 @@ open import Definition.Typed.EqRelInstance
 
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Properties
 open import Definition.LogicalRelation.Substitution
 open import Definition.LogicalRelation.Substitution.Properties

Definition/Typed/Consequences/Consistency.agda

@@ -13,7 +13,7 @@ open import Definition.Typed.Properties
 open import Definition.Typed.EqRelInstance
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Substitution
 open import Definition.LogicalRelation.Fundamental.Reducibility
 

Definition/Typed/Consequences/Equality.agda

@@ -9,7 +9,7 @@ open import Definition.Typed.Properties
 open import Definition.Typed.EqRelInstance
 open import Definition.LogicalRelation
 open import Definition.LogicalRelation.Irrelevance
-open import Definition.LogicalRelation.EqView
+open import Definition.LogicalRelation.ShapeView
 open import Definition.LogicalRelation.Substitution
 open import Definition.LogicalRelation.Substitution.Properties
 open import Definition.LogicalRelation.Fundamental.Reducibility