src/Thinning/Triangle.agda

@@ -14,7 +14,7 @@ private
     A : Set a
     x : A
     xs ys zs : List A
-    θ φ ψ : Thinning A xs ys
+    θ φ φ′ ψ : Thinning A xs ys
 
 -- Thinning triangles
 ------------------------------------------------------------------------
@@ -46,3 +46,10 @@ untriangle end = refl
 untriangle (include ▴) = cong include (untriangle ▴)
 untriangle (occlude ▴) = cong exclude (untriangle ▴)
 untriangle (exclude ▴) = cong exclude (untriangle ▴)
+
+-- If we have two triangles with common edges, the third edge must also be equal
+triangleUnique : Triangle A θ φ ψ → Triangle A θ φ′ ψ → φ ≡ φ′
+triangleUnique end end = refl
+triangleUnique (include ▴) (include ▵) = cong include (triangleUnique ▴ ▵)
+triangleUnique (occlude ▴) (occlude ▵) = triangleUnique ▴ ▵
+triangleUnique (exclude ▴) (exclude ▵) = cong exclude (triangleUnique ▴ ▵)