observe, fixed an error in _≅e_

Core.agda

@@ -207,7 +207,7 @@ var i₁    , x₁      ≅s var i₂    , x₂      = x₁ ≅ x₂
 _                   ≅s _                   = bot
 
 var i₁    , q₁      ≅e var i₂    , q₂      = i₁ ≅ i₂
-π A₁ D₁   , x₁ , e₁ ≅e π A₂ D₂   , x₂ , e₂ = D₁ x₁ , e₁ ≅e D₂ x₂ , e₂
+π A₁ D₁   , x₁ , e₁ ≅e π A₂ D₂   , x₂ , e₂ = x₁ ≅ x₂ & D₁ x₁ , e₁ ≅e D₂ x₂ , e₂
 (D₁ ⊛ E₁) , s₁ , e₁ ≅e (D₂ ⊛ E₂) , s₂ , e₂ = D₁ , s₁ ≅s D₂ , s₂ & E₁ , e₁ ≅e E₂ , e₂
 _                   ≅e _                   = bot
 

Data/Maybe.agda

@@ -1,6 +1,6 @@
 module OTT.Data.Maybe where
 
-open import OTT.Main
+open import OTT.Main hiding (Maybe; nothing; just)
 
 maybe : ∀ {a} {α : Level a} -> Univ α -> Type₋₁ α
 maybe {α = α} A = cmu₋₁ α

Main.agda

@@ -1,6 +1,6 @@
 module OTT.Main where
 
-open import OTT.Core          hiding (Maybe; nothing; just) public
+open import OTT.Core          public
 open import OTT.Coerce        public
 open import OTT.Data.List     public
 open import OTT.Function.Pi   public

Prelude.agda

@@ -3,8 +3,8 @@ module OTT.Prelude where
 open import Level
   renaming (Level to MetaLevel; zero to lzeroₘ; suc to lsucₘ; _⊔_ to _⊔ₘ_) using () public
 open import Function public
-open import Relation.Binary.PropositionalEquality
-  as P renaming (refl to prefl; trans to ptrans; cong to pcong; cong₂ to pcong₂) using (_≡_) public
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+  renaming (refl to prefl; trans to ptrans; subst to psubst; cong to pcong; cong₂ to pcong₂) public
 open import Data.Empty public
 open import Data.Nat.Base hiding (_⊔_; _≟_; erase) public
 open import Data.Maybe.Base using (Maybe; nothing; just) public
@@ -36,6 +36,10 @@ instance
 pright : ∀ {α} {A : Set α} {x y z : A} -> x ≡ y -> x ≡ z -> y ≡ z
 pright prefl prefl = prefl
 
+hpcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
+        -> (f : ∀ x -> B x -> C) -> (q : x₁ ≡ x₂) -> psubst B q y₁ ≡ y₂ -> f x₁ y₁ ≡ f x₂ y₂
+hpcong₂ f prefl prefl = prefl
+
 record Apply {α β} {A : Set α} (B : A -> Set β) x : Set β where
   constructor tag
   field detag : B x

Property/Eq.agda

@@ -14,8 +14,6 @@ module _ where
   contr : {A : Prop} {x y : ⟦ A ⟧} -> x ≡ y
   contr = trustMe
 
--- We could compare functions with a finite domain for equality,
--- but then equality can't be `_≡_`.
 SemEq : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} -> Desc I α -> Set
 SemEq (var i) = ⊤
 SemEq (π A D) = ⊥
@@ -71,6 +69,59 @@ mutual
   _≟_ {A = desc I α} {{()}}
   _≟_ {A = imu D j }                d₁        d₂       = decMu d₁ d₂
 
+coerceFamEnum : ∀ {n} {e f : Apply Enum n} -> (A : Apply Enum n -> Set) -> ⟦ e ≅ f ⟧ -> A e -> A f
+coerceFamEnum {0}           {tag ()      } {tag ()      } A q  x
+coerceFamEnum {1}           {tag tt      } {tag tt      } A q  x = x
+coerceFamEnum {suc (suc n)} {tag nothing } {tag nothing } A q  x = x
+coerceFamEnum {suc (suc n)} {tag (just _)} {tag (just _)} A q  x =
+  coerceFamEnum (A ∘ tag ∘ just ∘ detag) q x
+coerceFamEnum {suc (suc n)} {tag nothing } {tag (just _)} A () x
+coerceFamEnum {suc (suc n)} {tag (just _)} {tag nothing } A () x
+
+mutual
+  observeSem : ∀ {i a} {ι : Level i} {α : Level a}
+                 {I : Type ι} {E : Desc I α} {{eqE : ExtendEq E}}
+             -> (D : Desc I α) {{edD : SemEq D}}
+             -> (d₁ d₂ : ⟦ D ⟧ᵈ (μ E)) -> ⟦ D , d₁ ≅s D , d₂ ⟧ -> d₁ ≡ d₂
+  observeSem (var i)                d₁        d₂        q        = observe q
+  observeSem (π A D) {{()}}         d₁        d₂        q
+  observeSem (D ⊛ E) {{eqD , eqE}} (d₁ , e₁) (d₂ , e₂) (qd , qe) =
+    pcong₂ _,_ (observeSem D {{eqD}} d₁ d₂ qd) (observeSem E {{eqE}} e₁ e₂ qe)
+
+  observeExtend : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι}
+                    {E : Desc I α} {j} {{edE : ExtendEq E}}
+                -> (D : Desc I α) {{edD : ExtendEq D}}
+                -> (e₁ e₂ : Extend D (μ E) j) -> ⟦ D , e₁ ≅e D , e₂ ⟧ -> e₁ ≡ e₂
+  observeExtend (var i)                q₁        q₂        q        = contr
+  observeExtend (π A D) {{eqA , eqD}} (x₁ , e₁) (x₂ , e₂) (qx , qe)
+    rewrite observe {x = x₁} {x₂} {{eqA}} qx =
+      pcong (_,_ _) (observeExtend (D x₂) {{apply eqD x₂}} e₁ e₂ qe)
+  observeExtend (D ⊛ E) {{eqD , eqE}} (d₁ , e₁) (d₂ , e₂) (qd , qe) =
+    pcong₂ _,_ (observeSem D {{eqD}} d₁ d₂ qd) (observeExtend E {{eqE}} e₁ e₂ qe)
+
+  observeMu : ∀ {i a} {ι : Level i} {α : Level a} {I : Type ι} {j}
+                {D : Desc I α} {d e : μ D j} {{eqD : ExtendEq D}}
+            -> ⟦ d ≅ e ⟧ -> d ≡ e
+  observeMu {D = D} {node e₁} {node e₂} q = pcong node (observeExtend D e₁ e₂ q)
+
+  observe : ∀ {a} {α : Level a} {A : Univ α} {x y : ⟦ A ⟧} {{eqA : Eq A}} -> ⟦ x ≅ y ⟧ -> x ≡ y
+  observe {A = bot     } {()}      {()}
+  observe {A = top     }                                    q        = prefl
+  observe {A = nat     }                                    q        = coerceFamℕ    (_ ≡_) q prefl
+  observe {A = enum n  } {e₁}      {e₂}                     q        = coerceFamEnum (_ ≡_) q prefl
+  observe {A = univ α  }                     {{()}}
+  observe {A = σ A B   } {x₁ , y₁} {x₂ , y₂} {{eqA , eqB}} (qx , qy)
+    rewrite observe {x = x₁} {x₂} {{eqA}} qx = pcong (_,_ _) (observe {{apply eqB x₂}} qy)
+  observe {A = π A B   }                     {{()}}
+  observe {A = desc I α}                     {{()}}
+  observe {A = imu D j } {node e₁} {node e₂}                q        = observeMu q
+
+module _ where
+  open import Relation.Binary.PropositionalEquality.TrustMe
+
+  eobserve : ∀ {a} {α : Level a} {A : Univ α} {x y : ⟦ A ⟧} {{eqA : Eq A}} -> ⟦ x ≅ y ⟧ -> x ≡ y
+  eobserve = erase ∘ observe
+
 private
   module Test where
     open import OTT.Data.Fin