text:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Transitivity {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening renaming (wk to TWwk)
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Conversion

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

import Data.Nat as Nat

mutual
  -- Helper function for transitivity of type equality using shape views.
  transEqT : ∀ {Γ A B C r l l′ l″}
             {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r} {[C] : Γ ⊩⟨ l″ ⟩ C ^ r}
           → ShapeView₃ Γ l l′ l″ A B C r r r [A] [B] [C]
           → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
           → Γ ⊩⟨ l′ ⟩ B ≡ C ^ r / [B]
           → Γ ⊩⟨ l ⟩  A ≡ C ^ r / [A]
  transEqT (Uᵥ UA UB UC) A≡B B≡C =
    let
      U≡U : Univ (LogRel._⊩¹U_^_.r UA) (LogRel._⊩¹U_^_.l′ UA) PE.≡ Univ (LogRel._⊩¹U_^_.r UB) (LogRel._⊩¹U_^_.l′ UB)
      U≡U = whrDet* (A≡B , Uₙ) ((_⊢_:⇒*:_^_.D (LogRel._⊩¹U_^_.d UB)) , Uₙ)
      r≡r , l≡l = Univ-PE-injectivity U≡U
    in
    PE.subst₂ (λ X Y → _ ⊢ _ ⇒* Univ X Y ^ [ ! , _ ]) (PE.sym r≡r) (PE.sym l≡l) B≡C
  transEqT (ℕᵥ D D′ D″) A≡B B≡C = B≡C
  transEqT (Emptyᵥ D D′ D″) A≡B B≡C = B≡C
  transEqT (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K) (ne K₁ D₁ neK₁ _)
               (ne K₂ D₂ neK₂ _))
           (ne₌ M D′ neM K≡M) (ne₌ M₁ D″ neM₁ K≡M₁)
           rewrite whrDet* (red D₁ , ne neK₁) (red D′ , ne neM)
                 | whrDet* (red D₂ , ne neK₂) (red D″ , ne neM₁) =
    ne₌ M₁ D″ neM₁
        (~-trans K≡M K≡M₁)
  transEqT {Γ}  {r = [ r , ι lΠ ]} {l = l} {l′ = l′} {l″ = l″}
           (Πᵥ (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (Πᵣ rF₁ lF₁ lG₁ _ _ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁)
               (Πᵣ rF₂ lF₂ lG₂ _ _ F₂ G₂ D₂ ⊢F₂ ⊢G₂ A≡A₂ [F]₂ [G]₂ G-ext₂))
           (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
           (Π₌ F″ G″ D″ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
    let ΠF₁G₁≡ΠF′G′    = whrDet* (red D₁ , Πₙ) (D′  , Πₙ)
        F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , _ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        F₂≡F″ , rF₂≡rF′ , lF₂≡lF′ , G₂≡G″ , lG₂≡lG″  , _ = Π-PE-injectivity (whrDet* (red D₂ , Πₙ) (D″ , Πₙ))
        substLift {Δ} {l} {a} {r} ρ x = Δ ⊩⟨ l ⟩ wk (lift ρ) x [ a ] ^ r
        [F′] : ∀ {ρ Δ} [ρ] ⊢Δ → Δ ⊩⟨ l′ ⟩ wk ρ F′ ^ [ rF₁ , ι lF₁ ]
        [F′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk ρ x ^ _) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
        [F″] : ∀ {ρ} {Δ} [ρ] ⊢Δ → Δ ⊩⟨ l″ ⟩ wk ρ F″ ^ [ rF₂ , ι lF₂ ]
        [F″] {ρ} [ρ] ⊢Δ = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk ρ x ^ _) F₂≡F″ ([F]₂ [ρ] ⊢Δ)
        [F′≡F″] : ∀ {ρ} {Δ} [ρ] ⊢Δ → Δ ⊩⟨ l′ ⟩ wk ρ F′ ≡ wk ρ F″ ^ [ rF₁ , ι lF₁ ] / [F′] [ρ] ⊢Δ
        [F′≡F″] {ρ} [ρ] ⊢Δ = irrelevanceEq′ (PE.cong (wk ρ) F₁≡F′) PE.refl PE.refl
                                      ([F]₁ [ρ] ⊢Δ) ([F′] [ρ] ⊢Δ) ([F≡F′]₁ [ρ] ⊢Δ)
        [G′] : ∀ {ρ Δ a} [ρ] ⊢Δ
             → Δ ⊩⟨ l′ ⟩ a ∷ wk ρ F′ ^ [ rF₁ , ι lF₁ ] / [F′] [ρ] ⊢Δ
             → Δ ⊩⟨ l′ ⟩ wk (lift ρ) G′ [ a ] ^ [ r , ι lG₁ ]
        [G′] {ρ} [ρ] ⊢Δ [a] =
             let [a′] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₁≡F′)) PE.refl PE.refl
                                      ([F′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [a]
             in  PE.subst (substLift ρ) G₁≡G′ ([G]₁ [ρ] ⊢Δ [a′])
        [G″] : ∀ {ρ Δ a} [ρ] ⊢Δ
             → Δ ⊩⟨ l″ ⟩ a ∷ wk ρ F″ ^ [ rF₂ , ι lF₂ ] / [F″] [ρ] ⊢Δ
             → Δ ⊩⟨ l″ ⟩ wk (lift ρ) G″ [ a ] ^ [ r , ι lG₂ ]
        [G″] {ρ} [ρ] ⊢Δ [a] =
          let [a″] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₂≡F″)) PE.refl PE.refl
                                      ([F″] [ρ] ⊢Δ) ([F]₂ [ρ] ⊢Δ) [a]
          in  PE.subst (substLift ρ) G₂≡G″ ([G]₂ [ρ] ⊢Δ [a″])
        [G′≡G″] : ∀ {ρ Δ a} [ρ] ⊢Δ
                  ([a] : Δ ⊩⟨ l′ ⟩ a ∷ wk ρ F′ ^ [ rF₁ , ι lF₁ ] / [F′] [ρ] ⊢Δ)
                → Δ ⊩⟨ l′ ⟩ wk (lift ρ) G′  [ a ]
                          ≡ wk (lift ρ) G″ [ a ] ^ [ r , ι lG₁ ] / [G′] [ρ] ⊢Δ [a]
        [G′≡G″] {ρ} [ρ] ⊢Δ [a′] =
          let [a]₁ = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₁≡F′)) PE.refl PE.refl
                                      ([F′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [a′]
          in  irrelevanceEq′ (PE.cong (λ x → wk (lift ρ) x [ _ ]) G₁≡G′) PE.refl PE.refl
                             ([G]₁ [ρ] ⊢Δ [a]₁) ([G′] [ρ] ⊢Δ [a′])
                             ([G≡G′]₁ [ρ] ⊢Δ [a]₁)
                             -- Γ ⊢ .C ⇒* Π F″ ^ rF ▹ G″ ^ r
    in  Π₌ F″ G″ (PE.subst₃ _ rF₁≡rF′ lF₁≡lF′ lG₁≡lG′ D″) (PE.subst₃ _ rF₁≡rF′ lF₁≡lF′ lG₁≡lG′ (≅-trans A≡B (PE.subst (λ x → Γ ⊢ x ≅ Π F″ ^ rF₁ ° lF₁ ▹ G″ ° lG₁ ° lΠ ^ [ r , ι lΠ ]) ΠF₁G₁≡ΠF′G′ A≡B₁)))
           (λ ρ ⊢Δ → transEq′ PE.refl PE.refl (PE.sym rF₁≡rF′) (PE.sym rF₂≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) (PE.cong ι (PE.sym lF₂≡lF′))
           ([F] ρ ⊢Δ) ([F′] ρ ⊢Δ) ([F″] ρ ⊢Δ)
           ([F≡F′] ρ ⊢Δ) ([F′≡F″] ρ ⊢Δ))
           (λ ρ ⊢Δ [a] →
              let [a′] = convTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] ρ ⊢Δ) ([F′] ρ ⊢Δ) ([F≡F′] ρ ⊢Δ) [a]
                  [a″] = convTerm₁′ (PE.sym rF₂≡rF′) (PE.cong ι (PE.sym lF₂≡lF′)) ([F′] ρ ⊢Δ) ([F″] ρ ⊢Δ) ([F′≡F″] ρ ⊢Δ) [a′]
              in transEq′ PE.refl PE.refl PE.refl PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) (PE.cong ι (PE.sym lG₂≡lG″))
                          ([G] ρ ⊢Δ [a]) ([G′] ρ ⊢Δ [a′]) ([G″] ρ ⊢Δ [a″])
                          ([G≡G′] ρ ⊢Δ [a]) ([G′≡G″] ρ ⊢Δ [a′]))
  transEqT {Γ}  {r = r} {l = l} {l′ = l′} {l″ = l″}
           (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (∃ᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁)
               (∃ᵣ F₂ G₂ D₂ ⊢F₂ ⊢G₂ A≡A₂ [F]₂ [G]₂ G-ext₂))
           (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′])
           (∃₌ F″ G″ D″ A≡B₁ [F≡F′]₁ [G≡G′]₁) =
    let ∃F₁G₁≡∃F′G′    = whrDet* (red D₁ , ∃ₙ) (D′  , ∃ₙ)
        F₁≡F′ ,  G₁≡G′ = ∃-PE-injectivity ∃F₁G₁≡∃F′G′
        F₂≡F″ ,  G₂≡G″  = ∃-PE-injectivity (whrDet* (red D₂ , ∃ₙ) (D″ , ∃ₙ))
        substLift {Δ} {l} {a} {r} ρ x = Δ ⊩⟨ l ⟩ wk (lift ρ) x [ a ] ^ r
        lr = TypeInfo.l r
        [F′] : ∀ {ρ Δ} [ρ] ⊢Δ → Δ ⊩⟨ l′ ⟩ wk ρ F′ ^ [ % , lr ]
        [F′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk ρ x ^ _) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
        [F″] : ∀ {ρ} {Δ} [ρ] ⊢Δ → Δ ⊩⟨ l″ ⟩ wk ρ F″ ^ [ % , lr ]
        [F″] {ρ} [ρ] ⊢Δ = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk ρ x ^ _) F₂≡F″ ([F]₂ [ρ] ⊢Δ)
        [F′≡F″] : ∀ {ρ} {Δ} [ρ] ⊢Δ → Δ ⊩⟨ l′ ⟩ wk ρ F′ ≡ wk ρ F″ ^ [ % , lr ] / [F′] [ρ] ⊢Δ
        [F′≡F″] {ρ} [ρ] ⊢Δ = irrelevanceEq′ (PE.cong (wk ρ) F₁≡F′) PE.refl PE.refl
                                      ([F]₁ [ρ] ⊢Δ) ([F′] [ρ] ⊢Δ) ([F≡F′]₁ [ρ] ⊢Δ)
        [G′] : ∀ {ρ Δ a} [ρ] ⊢Δ
             → Δ ⊩⟨ l′ ⟩ a ∷ wk ρ F′ ^ [ % , lr ] / [F′] [ρ] ⊢Δ
             → Δ ⊩⟨ l′ ⟩ wk (lift ρ) G′ [ a ] ^ r
        [G′] {ρ} [ρ] ⊢Δ [a] =
          let [a′] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₁≡F′)) PE.refl PE.refl
                                      ([F′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [a]
          in  PE.subst (substLift ρ) G₁≡G′ ([G]₁ [ρ] ⊢Δ [a′])
        [G″] : ∀ {ρ Δ a} [ρ] ⊢Δ
             → Δ ⊩⟨ l″ ⟩ a ∷ wk ρ F″ ^ [ % , lr ] / [F″] [ρ] ⊢Δ
             → Δ ⊩⟨ l″ ⟩ wk (lift ρ) G″ [ a ] ^ r
        [G″] {ρ} [ρ] ⊢Δ [a] =
          let [a″] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₂≡F″)) PE.refl PE.refl
                                      ([F″] [ρ] ⊢Δ) ([F]₂ [ρ] ⊢Δ) [a]
          in  PE.subst (substLift ρ) G₂≡G″ ([G]₂ [ρ] ⊢Δ [a″])
        [G′≡G″] : ∀ {ρ Δ a} [ρ] ⊢Δ
                  ([a] : Δ ⊩⟨ l′ ⟩ a ∷ wk ρ F′ ^ [ % , lr ] / [F′] [ρ] ⊢Δ)
                → Δ ⊩⟨ l′ ⟩ wk (lift ρ) G′  [ a ]
                          ≡ wk (lift ρ) G″ [ a ] ^ r / [G′] [ρ] ⊢Δ [a]
        [G′≡G″] {ρ} [ρ] ⊢Δ [a′] =
          let [a]₁ = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F₁≡F′)) PE.refl PE.refl
                                      ([F′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [a′]
          in  irrelevanceEq′ (PE.cong (λ x → wk (lift ρ) x [ _ ]) G₁≡G′) PE.refl PE.refl
                             ([G]₁ [ρ] ⊢Δ [a]₁) ([G′] [ρ] ⊢Δ [a′])
                             ([G≡G′]₁ [ρ] ⊢Δ [a]₁)
                             -- Γ ⊢ .C ⇒* ∃ F″ ^ rF ▹ G″ ^ r
    in  ∃₌ F″ G″ D″ (≅-trans A≡B (PE.subst (λ x → Γ ⊢ x ≅ ∃ F″ ▹ G″ ^ [ % , lr ]) ∃F₁G₁≡∃F′G′ A≡B₁))
           (λ ρ ⊢Δ → transEq′ PE.refl PE.refl PE.refl PE.refl PE.refl PE.refl
           ([F] ρ ⊢Δ) ([F′] ρ ⊢Δ) ([F″] ρ ⊢Δ)
           ([F≡F′] ρ ⊢Δ) ([F′≡F″] ρ ⊢Δ))
           (λ ρ ⊢Δ [a] →
              let [a′] = convTerm₁′ PE.refl PE.refl ([F] ρ ⊢Δ) ([F′] ρ ⊢Δ) ([F≡F′] ρ ⊢Δ) [a]
                  [a″] = convTerm₁′ PE.refl PE.refl ([F′] ρ ⊢Δ) ([F″] ρ ⊢Δ) ([F′≡F″] ρ ⊢Δ) [a′]
              in  transEq ([G] ρ ⊢Δ [a]) ([G′] ρ ⊢Δ [a′]) ([G″] ρ ⊢Δ [a″])
                          ([G≡G′] ρ ⊢Δ [a]) ([G′≡G″] ρ ⊢Δ [a′]))
  transEqT (emb⁰¹¹ S) A≡B B≡C = transEqT S A≡B B≡C
  transEqT (emb¹⁰¹ S) A≡B B≡C = transEqT S A≡B B≡C
  transEqT (emb¹¹⁰ S) A≡B B≡C = transEqT S A≡B B≡C
  transEqT (emb¹∞∞ S) A≡B B≡C = transEqT S A≡B B≡C
  transEqT (emb∞¹∞ S) A≡B B≡C = transEqT S A≡B B≡C
  transEqT (emb∞∞¹ S) A≡B B≡C = transEqT S A≡B B≡C

  -- Transitivty of type equality.
  transEq : ∀ {Γ A B C r l l′ l″}
            ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([B] : Γ ⊩⟨ l′ ⟩ B ^ r) ([C] : Γ ⊩⟨ l″ ⟩ C ^ r)
          → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
          → Γ ⊩⟨ l′ ⟩ B ≡ C ^ r / [B]
          → Γ ⊩⟨ l ⟩  A ≡ C ^ r / [A]
  transEq [A] [B] [C] A≡B B≡C =
    transEqT (combine (goodCases [A] [B] A≡B) (goodCases [B] [C] B≡C)) A≡B B≡C

  -- Transitivity of type equality with some propositonally equal types.
  transEq′ : ∀ {Γ A B B′ C C′ r r' r'' ll ll' ll'' l l′ l″} → B PE.≡ B′ → C PE.≡ C′ → r PE.≡ r' → r' PE.≡ r'' → ll PE.≡ ll' → ll' PE.≡ ll''
           → ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ]) ([C] : Γ ⊩⟨ l″ ⟩ C ^ [ r'' , ll'' ])
           → Γ ⊩⟨ l ⟩  A ≡ B′ ^ [ r , ll ] / [A]
           → Γ ⊩⟨ l′ ⟩ B ≡ C′ ^ [ r' , ll' ] / [B]
           → Γ ⊩⟨ l ⟩  A ≡ C  ^ [ r , ll ] / [A]
  transEq′ PE.refl PE.refl PE.refl PE.refl PE.refl PE.refl [A] [B] [C] A≡B B≡C = transEq [A] [B] [C] A≡B B≡C

transEqTermNe : ∀ {Γ n n′ n″ A r}
              → Γ ⊩neNf n  ≡ n′  ∷ A ^ r
              → Γ ⊩neNf n′ ≡ n″ ∷ A ^ r
              → Γ ⊩neNf n  ≡ n″ ∷ A ^ r
transEqTermNe (neNfₜ₌ neK neM k≡m) (neNfₜ₌ neK₁ neM₁ k≡m₁) =
  neNfₜ₌ neK neM₁ (~-trans k≡m k≡m₁)

mutual
  transEqTermℕ : ∀ {Γ n n′ n″}
               → Γ ⊩ℕ n  ≡ n′  ∷ℕ
               → Γ ⊩ℕ n′ ≡ n″ ∷ℕ
               → Γ ⊩ℕ n  ≡ n″ ∷ℕ
  transEqTermℕ (ℕₜ₌ k k′ d d′ t≡u prop)
               (ℕₜ₌ k₁ k″ d₁ d″ t≡u₁ prop₁) =
    let k₁Whnf = naturalWhnf (proj₁ (split prop₁))
        k′Whnf = naturalWhnf (proj₂ (split prop))
        k₁≡k′ = whrDet*Term (redₜ d₁ , k₁Whnf) (redₜ d′ , k′Whnf)
        prop′ = PE.subst (λ x → [Natural]-prop _ x _) k₁≡k′ prop₁
    in  ℕₜ₌ k k″ d d″ (≅ₜ-trans t≡u (PE.subst (λ x → _ ⊢ x ≅ _ ∷ _ ^ _) k₁≡k′ t≡u₁))
            (transNatural-prop prop prop′)

  transNatural-prop : ∀ {Γ k k′ k″}
                    → [Natural]-prop Γ k k′
                    → [Natural]-prop Γ k′ k″
                    → [Natural]-prop Γ k k″
  transNatural-prop (sucᵣ x) (sucᵣ x₁) = sucᵣ (transEqTermℕ x x₁)
  transNatural-prop (sucᵣ x) (ne (neNfₜ₌ () neM k≡m))
  transNatural-prop zeroᵣ prop₁ = prop₁
  transNatural-prop prop zeroᵣ = prop
  transNatural-prop (ne (neNfₜ₌ neK () k≡m)) (sucᵣ x₃)
  transNatural-prop (ne [k≡k′]) (ne [k′≡k″]) =
    ne (transEqTermNe [k≡k′] [k′≡k″])

-- Empty
transEmpty-prop : ∀ {Γ k k′ k″ l}
  → [Empty]-prop Γ k k′ l
  → [Empty]-prop Γ k′ k″ l
  → [Empty]-prop Γ k k″ l
transEmpty-prop (ne a b) (ne c d) = ne a d

transEqTermEmpty : ∀ {Γ n n′ n″ l}
  → Γ ⊩Empty n  ≡ n′ ∷Empty^ l
  → Γ ⊩Empty n′ ≡ n″ ∷Empty^ l
  → Γ ⊩Empty n  ≡ n″ ∷Empty^ l
transEqTermEmpty (Emptyₜ₌ (ne a b)) (Emptyₜ₌ (ne c d)) = Emptyₜ₌ (ne a d)

-- Transitivity of term equality.
transEqTerm⁰ : ∀ {Γ A t u v r}
               ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ r)
             → Γ ⊩⟨ ι ⁰ ⟩ t ≡ u ∷ A ^ r / [A]
             → Γ ⊩⟨ ι ⁰ ⟩ u ≡ v ∷ A ^ r / [A]
             → Γ ⊩⟨ ι ⁰ ⟩ t ≡ v ∷ A ^ r / [A]
transEqTerm⁰ (ℕᵣ D) [t≡u] [u≡v] = transEqTermℕ [t≡u] [u≡v]
transEqTerm⁰ (Emptyᵣ D) [t≡u] [u≡v] = transEqTermEmpty [t≡u] [u≡v]
transEqTerm⁰ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ (neNfₜ₌ neK₁ neM k≡m))
                              (neₜ₌ k₁ m₁ d₁ d″ (neNfₜ₌ neK₂ neM₁ k≡m₁)) =
  let k₁≡m = whrDet*Term (redₜ d₁ , ne neK₂) (redₜ d′ , ne neM)
  in  neₜ₌ k m₁ d d″
           (neNfₜ₌ neK₁ neM₁
                   (~-trans k≡m (PE.subst (λ x → _ ⊢ x ~ _ ∷ _ ^ _) k₁≡m k≡m₁)))
transEqTerm⁰ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ₌ d d′)
                              (neₜ₌ d₁ d″) = neₜ₌ d d″
transEqTerm⁰ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g])
            (Πₜ₌ f₁ g₁ d₁ d₁′ funcF₁ funcG₁ f≡g₁ [f]₁ [g]₁ [f≡g]₁)
            rewrite whrDet*Term (redₜ d′ , functionWhnf funcG)
                            (redₜ d₁ , functionWhnf funcF₁) =
  Πₜ₌ f g₁ d d₁′ funcF funcG₁ (≅ₜ-trans f≡g f≡g₁) [f] [g]₁
      (λ ρ ⊢Δ [a] → transEqTerm⁰ ([G] ρ ⊢Δ [a])
                                ([f≡g] ρ ⊢Δ [a])
                                ([f≡g]₁ ρ ⊢Δ [a]))
transEqTerm⁰ {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′
transEqTerm⁰ {r = [ % , l ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′

transEqTerm¹ : ∀ {Γ A t u v r}
               ([A] : Γ ⊩⟨ ι ¹ ⟩ A ^ r)
             → Γ ⊩⟨ ι ¹ ⟩ t ≡ u ∷ A ^ r / [A]
             → Γ ⊩⟨ ι ¹ ⟩ u ≡ v ∷ A ^ r / [A]
             → Γ ⊩⟨ ι ¹ ⟩ t ≡ v ∷ A ^ r / [A]
transEqTerm¹ {Γ} {A} {t} {u} {v} {r} (Uᵣ (Uᵣ rU ⁰ l< eq d)) (Uₜ₌ [t] [u] A≡B [t≡u])
  (Uₜ₌ [u]′ [v] B′≡C [u≡v]) =
  let
    ti = LogRel._⊩¹U_∷_^_/_.[t]
    ⊢Γ = wf (_⊢_:⇒*:_^_.⊢A d)
    B≡B′ = whrDet*Term (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]))
      (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]′) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]′))
    A≡C = ≅ₜ-trans (PE.subst (λ X → EqRelSet._⊢_≅_∷_^_ eqrel Γ (LogRel._⊩¹U_∷_^_/_.K [t]) X (Univ rU ⁰) ([ ! , ι ¹ ])) B≡B′ A≡B) B′≡C
    [t≡v] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      transEq (ti [t] [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) (ti [v] [ρ] ⊢Δ) ([t≡u] [ρ] ⊢Δ)
        (irrelevanceEq (ti [u]′ [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) ([u≡v] [ρ] ⊢Δ))
  in
  Uₜ₌ [t] [v] A≡C [t≡v]
transEqTerm¹ (ℕᵣ D) [t≡u] [u≡v] = transEqTermℕ [t≡u] [u≡v]
transEqTerm¹ (Emptyᵣ D) [t≡u] [u≡v] = transEqTermEmpty [t≡u] [u≡v]
transEqTerm¹ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ (neNfₜ₌ neK₁ neM k≡m))
                              (neₜ₌ k₁ m₁ d₁ d″ (neNfₜ₌ neK₂ neM₁ k≡m₁)) =
  let k₁≡m = whrDet*Term (redₜ d₁ , ne neK₂) (redₜ d′ , ne neM)
  in  neₜ₌ k m₁ d d″
           (neNfₜ₌ neK₁ neM₁
                   (~-trans k≡m (PE.subst (λ x → _ ⊢ x ~ _ ∷ _ ^ _) k₁≡m k≡m₁)))
transEqTerm¹ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ₌ d d′)
                              (neₜ₌ d₁ d″) = neₜ₌ d d″
transEqTerm¹ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g])
            (Πₜ₌ f₁ g₁ d₁ d₁′ funcF₁ funcG₁ f≡g₁ [f]₁ [g]₁ [f≡g]₁)
            rewrite whrDet*Term (redₜ d′ , functionWhnf funcG)
                            (redₜ d₁ , functionWhnf funcF₁) =
  Πₜ₌ f g₁ d d₁′ funcF funcG₁ (≅ₜ-trans f≡g f≡g₁) [f] [g]₁
      (λ ρ ⊢Δ [a] → transEqTerm¹ ([G] ρ ⊢Δ [a])
                                ([f≡g] ρ ⊢Δ [a])
                                ([f≡g]₁ ρ ⊢Δ [a]))
transEqTerm¹ {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′
transEqTerm¹ {r = [ % , l ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′
transEqTerm¹ (emb l< [A]) [t≡u] [u≡v] = transEqTerm⁰ [A] [t≡u] [u≡v]

transEqTerm∞ : ∀ {Γ A t u v r}
               ([A] : Γ ⊩⟨ ∞ ⟩ A ^ r)
             → Γ ⊩⟨ ∞ ⟩ t ≡ u ∷ A ^ r / [A]
             → Γ ⊩⟨ ∞ ⟩ u ≡ v ∷ A ^ r / [A]
             → Γ ⊩⟨ ∞ ⟩ t ≡ v ∷ A ^ r / [A]
transEqTerm∞ {Γ} {A} {t} {u} {v} {r} (Uᵣ (Uᵣ rU ⁰ l< eq d)) (Uₜ₌ [t] [u] A≡B [t≡u])
  (Uₜ₌ [u]′ [v] B′≡C [u≡v]) =
  let
    ti = LogRel._⊩¹U_∷_^_/_.[t]
    ⊢Γ = wf (_⊢_:⇒*:_^_.⊢A d)
    B≡B′ = whrDet*Term (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]))
      (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]′) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]′))
    A≡C = ≅ₜ-trans (PE.subst (λ X → EqRelSet._⊢_≅_∷_^_ eqrel Γ (LogRel._⊩¹U_∷_^_/_.K [t]) X (Univ rU ⁰) ([ ! , ι ¹ ])) B≡B′ A≡B) B′≡C
    [t≡v] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      transEq (ti [t] [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) (ti [v] [ρ] ⊢Δ) ([t≡u] [ρ] ⊢Δ)
        (irrelevanceEq (ti [u]′ [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) ([u≡v] [ρ] ⊢Δ))
  in
  Uₜ₌ [t] [v] A≡C [t≡v]
transEqTerm∞ {Γ} {A} {t} {u} {v} {r} (Uᵣ (Uᵣ rU ¹ l< eq d)) (Uₜ₌ [t] [u] A≡B [t≡u])
  (Uₜ₌ [u]′ [v] B′≡C [u≡v]) =
  let
    ti = LogRel._⊩¹U_∷_^_/_.[t]
    ⊢Γ = wf (_⊢_:⇒*:_^_.⊢A d)
    B≡B′ = whrDet*Term (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]))
      (_⊢_:⇒*:_∷_^_.d (LogRel._⊩¹U_∷_^_/_.d [u]′) , typeWhnf (LogRel._⊩¹U_∷_^_/_.typeK [u]′))
    A≡C = ≅ₜ-trans (PE.subst (λ X → EqRelSet._⊢_≅_∷_^_ eqrel Γ (LogRel._⊩¹U_∷_^_/_.K [t]) X (Univ rU ¹) ([ ! , ∞ ])) B≡B′ A≡B) B′≡C
    [t≡v] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      transEq (ti [t] [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) (ti [v] [ρ] ⊢Δ) ([t≡u] [ρ] ⊢Δ)
        (irrelevanceEq (ti [u]′ [ρ] ⊢Δ) (ti [u] [ρ] ⊢Δ) ([u≡v] [ρ] ⊢Δ))
  in
  Uₜ₌ [t] [v] A≡C [t≡v]
transEqTerm∞ (ℕᵣ D) [t≡u] [u≡v] = transEqTermℕ [t≡u] [u≡v]
transEqTerm∞ (Emptyᵣ D) [t≡u] [u≡v] = transEqTermEmpty [t≡u] [u≡v]
transEqTerm∞ {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ (neNfₜ₌ neK₁ neM k≡m))
                              (neₜ₌ k₁ m₁ d₁ d″ (neNfₜ₌ neK₂ neM₁ k≡m₁)) =
  let k₁≡m = whrDet*Term (redₜ d₁ , ne neK₂) (redₜ d′ , ne neM)
  in  neₜ₌ k m₁ d d″
           (neNfₜ₌ neK₁ neM₁
                   (~-trans k≡m (PE.subst (λ x → _ ⊢ x ~ _ ∷ _ ^ _) k₁≡m k≡m₁)))
transEqTerm∞ {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ₌ d d′)
                              (neₜ₌ d₁ d″) = neₜ₌ d d″
transEqTerm∞ {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g])
            (Πₜ₌ f₁ g₁ d₁ d₁′ funcF₁ funcG₁ f≡g₁ [f]₁ [g]₁ [f≡g]₁)
            rewrite whrDet*Term (redₜ d′ , functionWhnf funcG)
                            (redₜ d₁ , functionWhnf funcF₁) =
  Πₜ₌ f g₁ d d₁′ funcF funcG₁ (≅ₜ-trans f≡g f≡g₁) [f] [g]₁
      (λ ρ ⊢Δ [a] → transEqTerm∞ ([G] ρ ⊢Δ [a])
                                ([f≡g] ρ ⊢Δ [a])
                                ([f≡g]₁ ρ ⊢Δ [a]))
transEqTerm∞ {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′
transEqTerm∞ {r = [ % , l ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
            (d , d′)
            (d₁ , d₁′) = d , d₁′
transEqTerm∞ (emb {l′ = ι ¹} l< [A]) [t≡u] [u≡v] = transEqTerm¹ [A] [t≡u] [u≡v]

transEqTerm : ∀ {l Γ A t u v r}
              ([A] : Γ ⊩⟨ l ⟩ A ^ r)
            → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / [A]
            → Γ ⊩⟨ l ⟩ u ≡ v ∷ A ^ r / [A]
            → Γ ⊩⟨ l ⟩ t ≡ v ∷ A ^ r / [A]
transEqTerm {l = ι ⁰} = transEqTerm⁰
transEqTerm {l = ι ¹} = transEqTerm¹
transEqTerm {l = ∞} = transEqTerm∞

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.core where

open import level using (_⊔_)
open import equality.core
open import equality.groupoid
open import equality.reasoning
open import function.core
open import function.overloading
open import sum
open import function.extensionality.core
open import overloading.core

-- isomorphisms
record _≅_ {i j}(X : Set i)(Y : Set j) : Set (i ⊔ j) where
  constructor iso
  field
    to : X → Y
    from : Y → X
    iso₁ : (x : X) → from (to x) ≡ x
    iso₂ : (y : Y) → to (from y) ≡ y
infix 5 _≅_

≅-struct-iso : ∀ {i j}{X : Set i}{Y : Set j}
             → (X ≅ Y)
             ≅ ( Σ (X → Y) λ f
               → Σ (Y → X) λ g
               → ((x : X) → g (f x) ≡ x)
               × ((y : Y) → f (g y) ≡ y) )
≅-struct-iso = record
  { to = λ { (iso f g α β) → f , g , α , β }
  ; from = λ { (f , g , α , β) → iso f g α β }
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl  }

refl≅ : ∀ {i}{X : Set i} → X ≅ X
refl≅ = iso id id (λ _ → refl) (λ _ → refl)

≡⇒≅ : ∀ {i}{X Y : Set i} → X ≡ Y → X ≅ Y
≡⇒≅ refl = refl≅

sym≅ : ∀ {i j}{X : Set i}{Y : Set j} → X ≅ Y → Y ≅ X
sym≅ (iso f g H K) = iso g f K H

trans≅ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
       → X ≅ Y → Y ≅ Z → X ≅ Z
trans≅ {X = X}{Z = Z} (iso f g H K) (iso f' g' H' K') = record
  { to = f' ∘ f
  ; from = g ∘ g'
  ; iso₁ = iso₁
  ; iso₂ = iso₂ }
  where
    abstract
      iso₁ : (x : X) → g (g' (f' (f x))) ≡ x
      iso₁ x = ap g (H' (f x)) · H x

      iso₂ : (z : Z) → f' (f (g (g' z))) ≡ z
      iso₂ y = ap f' (K (g' y)) · K' y

_·≅_ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
     → X ≅ Y → Y ≅ Z → X ≅ Z
_·≅_ = trans≅
infixl 9 _·≅_

module ≅-Reasoning where
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≅⟨_⟩_
  infixr 2 _≡⟨_⟩_
  infix  1 begin_

  data _IsRelatedTo_ {i j}(x : Set i)(y : Set j) : Set (i ⊔ j) where
    relTo : x ≅ y → x IsRelatedTo y

  begin_ : ∀ {i j}{X : Set i}{Y : Set j} → X IsRelatedTo Y → X ≅ Y
  begin relTo p = p

  _≅⟨_⟩_ : ∀ {i j k} (X : Set i) {Y : Set j}{Z : Set k}
         → X ≅ Y → Y IsRelatedTo Z → X IsRelatedTo Z
  _ ≅⟨ p ⟩ relTo q = relTo (trans≅ p q)

  _≡⟨_⟩_ : ∀ {i j} (X : Set i) {Y : Set i} {Z : Set j}
         → X ≡ Y → Y IsRelatedTo Z → X IsRelatedTo Z
  _ ≡⟨ p ⟩ relTo q = relTo (trans≅ (≡⇒≅ p) q)

  _∎ : ∀ {i} (X : Set i) → X IsRelatedTo X
  _∎ _ = relTo refl≅

injective : ∀ {i j}{X : Set i}{Y : Set j}
          → (f : X → Y) → Set _
injective f = ∀ {x x'} → f x ≡ f x' → x ≡ x'

retraction : ∀ {i j}{X : Set i}{Y : Set j}
           → (f : X → Y) → Set _
retraction {X = X}{Y = Y} f = (y : Y) → Σ X λ x → f x ≡ y

_↣_ : ∀ {i j} → Set i → Set j → Set _
A ↣ B = Σ (A → B) injective

-- composition of injections:
_∘i_ : ∀ {i j k}{A : Set i}{B : Set j}{C : Set k}
     → (B ↣ C) → (A ↣ B) → (A ↣ C)
(g , p) ∘i (f , q) = g ∘ f , q ∘ p

_↠_ : ∀ {i j} → Set i → Set j → Set _
A ↠ B = Σ (A → B) retraction

private
  module properties {i j}{X : Set i}{Y : Set j} where
    apply≅ : (X ≅ Y) → X → Y
    apply≅ = _≅_.to

    invert≅ : (X ≅ Y) → Y → X
    invert≅ = _≅_.from

    instance
      iso-is-fun : Coercion (X ≅ Y) (X → Y)
      iso-is-fun = record
        { coerce = _≅_.to }

      iso-is-iso : Coercion (X ≅ Y) (X ≅ Y)
      iso-is-iso = coerce-self _

      inj-is-fun : Coercion (X ↣ Y) (X → Y)
      inj-is-fun = record
        { coerce = proj₁ }

      srj-is-fun : Coercion (X ↠ Y) (X → Y)
      srj-is-fun = record
        { coerce = proj₁ }

    private
      module iso-methods {k}{Source : Set k}
                         ⦃ c : Coercion Source (X ≅ Y) ⦄ where
        private
          module with-source (source : Source) where
            private target = coerce c source
            open _≅_ target public using ()
              renaming (from to invert)
        open with-source public
    open iso-methods public

    iso⇒inj : (iso : X ≅ Y) → injective (apply iso)
    iso⇒inj f {x}{x'} q = (iso₁ x) ⁻¹ · ap from q · iso₁ x'
      where
        open _≅_ f

    iso⇒retr : (iso : X ≅ Y) → retraction (apply iso)
    iso⇒retr f y = from y , iso₂ y
      where
        open _≅_ f

    inj+retr⇒iso : (f : X → Y) → injective f → retraction f → X ≅ Y
    inj+retr⇒iso f inj-f retr-f = iso f g H K
      where
        g : Y → X
        g y = proj₁ (retr-f y)

        H : (x : X) → g (f x) ≡ x
        H x = inj-f (proj₂ (retr-f (f x)))

        K : (y : Y) → f (g y) ≡ y
        K y = proj₂ (retr-f y)

open properties public

ext: agda

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
{-# OPTIONS --without-K --safe #-}

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Morphism.Bundles
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Algebra.FunctionProperties as FP
open import Relation.Binary using (Rel; Setoid)
open import Level

import Algebra.Linear.Structures.Bundles as VS

open import Algebra.Linear.Morphism.VectorSpace K

open import Function.Equality as FunEq using (_⟶_; _⟨$⟩_; setoid)

module _
  {a₁ ℓ₁} (From : VS.VectorSpace K a₁ ℓ₁)
  {a₂ ℓ₂} (To   : VS.VectorSpace K a₂ ℓ₂)
  where

  private
    module F = VS.VectorSpace From
    module T = VS.VectorSpace To

    K' : Set k
    K' = Field.Carrier K

    open F using ()
      renaming
        ( Carrier to A
        ; _≈_     to _≈₁_
        ; refl    to ≈₁-refl
        ; sym     to ≈₁-sym
        ; setoid  to A-setoid
        ; _+_     to +₁
        ; _∙_     to ∙₁
        )

    open T using ()
      renaming
        ( Carrier to B
        ; _≈_     to _≈₂_
        ; refl    to ≈₂-refl
        ; sym     to ≈₂-sym
        ; trans   to ≈₂-trans
        ; setoid  to B-setoid
        ; _+_     to +₂
        ; _∙_     to ∙₂
        )

    hom-setoid : ∀ {Carrier} -> (Carrier -> (A-setoid ⟶ B-setoid))
                     -> Setoid (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) (a₁ ⊔ ℓ₁ ⊔ ℓ₂)
    hom-setoid {Carrier} app = record
      { Carrier       = Carrier
      ; _≈_           = λ f g → ∀ {x y} (r : x ≈₁ y) -> (app f ⟨$⟩ x) ≈₂ (app g ⟨$⟩ y)
      ; isEquivalence = record
        { refl  = λ {f} -> FunEq.cong (app f)
        ; sym   = λ r rₓ → ≈₂-sym (r (≈₁-sym rₓ))
        ; trans = λ r₁ r₂ rₓ → ≈₂-trans (r₁ ≈₁-refl) (r₂ rₓ)
        }
      }

  open LinearDefinitions A B _≈₂_

  record LinearMap : Set (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) where
    field
      ⟦_⟧         : Morphism
      isLinearMap : IsLinearMap From To ⟦_⟧

    infixr 25 _⟪$⟫_
    _⟪$⟫_ : A -> B
    _⟪$⟫_ = ⟦_⟧

    open IsLinearMap isLinearMap public

  linearMap-setoid : Setoid (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) (a₁ ⊔ ℓ₁ ⊔ ℓ₂)
  linearMap-setoid = hom-setoid {LinearMap} λ f → record
    { _⟨$⟩_ = λ x → f LinearMap.⟪$⟫ x
    ; cong = LinearMap.⟦⟧-cong f
    }

  record LinearIsomorphism : Set (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) where
    field
      ⟦_⟧                 : Morphism
      isLinearIsomorphism : IsLinearIsomorphism From To ⟦_⟧

    open IsLinearIsomorphism isLinearIsomorphism public

    linearMap : LinearMap
    linearMap = record { ⟦_⟧ = ⟦_⟧ ; isLinearMap = isLinearMap }

    open LinearMap linearMap public
      using (_⟪$⟫_)

  linearIsomorphism-setoid : Setoid (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) (a₁ ⊔ ℓ₁ ⊔ ℓ₂)
  linearIsomorphism-setoid = hom-setoid {LinearIsomorphism} λ f → record
    { _⟨$⟩_ = λ x -> f LinearIsomorphism.⟪$⟫ x
    ; cong = LinearIsomorphism.⟦⟧-cong f
    }

module _ {a ℓ} (V : VS.VectorSpace K a ℓ) where
  LinearEndomorphism : Set (suc (k ⊔ a ⊔ ℓ))
  LinearEndomorphism = LinearMap V V

  LinearAutomorphism : Set (suc (k ⊔ a ⊔ ℓ))
  LinearAutomorphism = LinearIsomorphism V V

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Reflection
open import Agda.Builtin.Sigma

macro
  @0 trivial : Term → TC ⊤
  trivial = unify (con (quote refl) [])

test : 42 ≡ 42
test = trivial

@0 m : Name → TC ⊤
m F = defineFun F
  (clause
     (( "A"
      , arg (arg-info visible (modality relevant quantity-0))
          (agda-sort (lit 0))) ∷
      [])
     (arg (arg-info visible (modality relevant quantity-0)) (var 0) ∷
      [])
     (var 0 []) ∷
   [])

F : Set → Set
unquoteDef F = m F


text:
open import Level using () renaming (_⊔_ to _⊔ˡ_)

open import Data.Product using (_,_; proj₁)
open import Data.Sum using (_⊎_; inj₁; inj₂)

open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Reflexive; Symmetric; Transitive; Setoid; Tri)
open Tri
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_) renaming (refl to ≡-refl; sym to ≡-sym)
open import Algebra.Bundles using (RawRing)
open import AKS.Algebra.Bundles using (DecField)

module AKS.Polynomial.Base {c ℓ} (F : DecField c ℓ)  where

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)
open import AKS.Nat using (ℕ; _∸_; _≤_; _<_; lte; pred) renaming (_+_ to _+ℕ_; _⊔_ to _⊔ℕ_)
open ℕ
open import AKS.Nat using (≢⇒¬≟; <-cmp; ≤-totalOrder; m<n⇒n∸m≢0)
open import AKS.Nat using (ℕ⁺; ⟅_⇓⟆; ⟅_⇑⟆)
open import AKS.Nat.WellFounded using (Acc; acc; <-well-founded)

open DecField F
  using (0#; 1#; _+_; _*_; -_; _-_; _⁻¹; _/_; C/0)
  renaming (Carrier to C)
open DecField F using (_≈_; _≈?_; setoid)
open Setoid setoid using (refl; sym; trans)
open DecField F
  using (*-commutativeMonoid; 1#-nonzero; -1#-nonzero; _*-nonzero_; _/-nonzero_)
open import AKS.Exponentiation *-commutativeMonoid using (_^_; _^⁺_)

data Spine : Set (c ⊔ˡ ℓ) where
  K : C/0 → Spine
  _+x^_∙_ : C/0 → ℕ⁺ → Spine → Spine

data Polynomial : Set (c ⊔ˡ ℓ) where
  0ᵖ : Polynomial
  x^_∙_ : ℕ → Spine → Polynomial

⟦_⟧ˢ : Spine → C → C
⟦ K c ⟧ˢ x = proj₁ c
⟦ c +x^ n ∙ p ⟧ˢ x = proj₁ c + x ^⁺ n * ⟦ p ⟧ˢ x

⟦_⟧ : Polynomial → C → C
⟦ 0ᵖ ⟧ x = 0#
⟦ x^ n ∙ p ⟧ x = x ^ n * ⟦ p ⟧ˢ x

1ᵖ : Polynomial
1ᵖ = x^ 0 ∙ K 1#-nonzero

_+?_ : ∀ (k₁ k₂ : C/0) → (proj₁ k₁ + proj₁ k₂ ≈ 0#) ⊎ C/0
k₁ +? k₂ with proj₁ k₁ + proj₁ k₂ ≈? 0#
... | yes k₁+k₂≈0 = inj₁ k₁+k₂≈0
... | no  k₁+k₂≉0 = inj₂ (proj₁ k₁ + proj₁ k₂ , k₁+k₂≉0)

+ᵖ-spine-≡-K : ℕ → C/0 → Spine → Polynomial
+ᵖ-spine-≡-K n c₁ (K c₂) with c₁ +? c₂
... | inj₁ _ = 0ᵖ
... | inj₂ c₁+c₂ = x^ n ∙ K c₁+c₂
+ᵖ-spine-≡-K n c₁ (c₂ +x^ i₂ ∙ q) with c₁ +? c₂
... | inj₁ _ = x^ (n +ℕ ⟅ i₂ ⇓⟆) ∙ q
... | inj₂ c₁+c₂ = x^ n ∙ (c₁+c₂ +x^ i₂ ∙ q)

+ᵖ-spine-≡ : ℕ → Spine → Spine → Polynomial
+ᵖ-spine-< : (n : ℕ) → Spine → (m : ℕ) → Spine → n < m → Polynomial
+ᵖ-spine : ℕ → Spine → ℕ → Spine → Polynomial

+ᵖ-spine-≡ n (K c₁) q = +ᵖ-spine-≡-K n c₁ q
+ᵖ-spine-≡ n (c₁ +x^ i₁ ∙ p) (K c₂) = +ᵖ-spine-≡-K n c₂ (c₁ +x^ i₁ ∙ p)
+ᵖ-spine-≡ n (c₁ +x^ i₁ ∙ p) (c₂ +x^ i₂ ∙ q) with c₁ +? c₂
... | inj₁ _ = +ᵖ-spine (n +ℕ ⟅ i₁ ⇓⟆) p (n +ℕ ⟅ i₂ ⇓⟆) q
... | inj₂ c₁+c₂ with +ᵖ-spine ⟅ i₁ ⇓⟆ p ⟅ i₂ ⇓⟆ q
...   | 0ᵖ = x^ n ∙ K c₁+c₂
...   | x^ zero ∙ r = +ᵖ-spine-≡-K n c₁+c₂ r
...   | x^ suc n₃ ∙ r = x^ n ∙ (c₁+c₂ +x^ ⟅ suc n₃ ⇑⟆ ∙ r)

+ᵖ-spine-< n₁ (K c₁) n₂ q n₁<n₂ = x^ n₁ ∙ (c₁ +x^ ⟅ n₂ ∸ n₁ ⇑⟆ {≢⇒¬≟ (m<n⇒n∸m≢0 n₁<n₂)} ∙ q)
+ᵖ-spine-< n₁ (c₁ +x^ i₁ ∙ p) n₂ q n₁<n₂ with +ᵖ-spine ⟅ i₁ ⇓⟆ p (n₂ ∸ n₁) q
... | 0ᵖ = x^ n₁ ∙ K c₁
... | x^ zero ∙ r = +ᵖ-spine-≡-K n₁ c₁ r
... | x^ suc n₃ ∙ r = x^ n₁ ∙ (c₁ +x^ ⟅ suc n₃ ⇑⟆ ∙ r)

+ᵖ-spine n₁ p n₂ q with <-cmp n₁ n₂
... | tri< n₁<n₂ _ _ = +ᵖ-spine-< n₁ p n₂ q n₁<n₂
... | tri≈ _ n₁≡n₂ _ = +ᵖ-spine-≡ n₁ p q
... | tri> _ _ n₁>n₂ = +ᵖ-spine-< n₂ q n₁ p n₁>n₂

infixl 6 _+ᵖ_
_+ᵖ_ : Polynomial → Polynomial → Polynomial
0ᵖ +ᵖ q = q
(x^ n₁ ∙ p) +ᵖ 0ᵖ = x^ n₁ ∙ p
(x^ n₁ ∙ p) +ᵖ (x^ n₂ ∙ q) = +ᵖ-spine n₁ p n₂ q

_∙𝑋^_ : C/0 → ℕ → Polynomial
c ∙𝑋^ n = x^ n ∙ K c

𝑋^_ : ℕ → Polynomial
𝑋^ n = 1#-nonzero ∙𝑋^ n

𝑋 : Polynomial
𝑋 = 𝑋^ 1

𝐾 : C → Polynomial
𝐾 c with c ≈? 0#
... | yes _  = 0ᵖ
... | no c≉0 = (c , c≉0) ∙𝑋^ 0

∙ᵖ-spine : C/0 → Spine → Spine
∙ᵖ-spine c₁ (K c₂) = K (c₁ *-nonzero c₂)
∙ᵖ-spine c₁ (c₂ +x^ n ∙ p) = (c₁ *-nonzero c₂) +x^ n ∙ (∙ᵖ-spine c₁ p)

infixl 7 _∙ᵖ_
_∙ᵖ_ : C/0 → Polynomial → Polynomial
c ∙ᵖ 0ᵖ = 0ᵖ
c ∙ᵖ (x^ n ∙ p) = x^ n ∙ (∙ᵖ-spine c p)

*ᵖ-spine : ℕ → Spine → ℕ → Spine → Polynomial
*ᵖ-spine o₁ (K c₁) o₂ q = x^ (o₁ +ℕ o₂) ∙ (∙ᵖ-spine c₁ q)
*ᵖ-spine o₁ (c₁ +x^ n₁ ∙ p) o₂ (K c₂) = x^ (o₁ +ℕ o₂) ∙ (∙ᵖ-spine c₂ (c₁ +x^ n₁ ∙ p))
*ᵖ-spine o₁ (c₁ +x^ n₁ ∙ p) o₂ (c₂ +x^ n₂ ∙ q) =
  x^ (o₁ +ℕ o₂) ∙ K (c₁ *-nonzero c₂) +ᵖ
  c₁ ∙ᵖ x^ (o₁ +ℕ o₂ +ℕ ⟅ n₂ ⇓⟆) ∙ q +ᵖ
  c₂ ∙ᵖ (x^ (o₁ +ℕ o₂ +ℕ ⟅ n₁ ⇓⟆) ∙ p) +ᵖ
  *ᵖ-spine (o₁ +ℕ ⟅ n₁ ⇓⟆) p (o₂ +ℕ ⟅ n₂ ⇓⟆) q
-- (c₁ + x ^ n₁ * p[x]) * (c₂ + x ^ n₂ * q[x]) = (c₁ * c₂) + (c₁ * x ^ n₂ * q[x]) + (x ^ n₁ * p[x] * c₂) + (x ^ n₁ * p[x] * x ^ n₂ * q[x])

infixl 7 _*ᵖ_
_*ᵖ_ : Polynomial → Polynomial → Polynomial
0ᵖ *ᵖ q = 0ᵖ
(x^ n₁ ∙ p) *ᵖ 0ᵖ = 0ᵖ
(x^ n₁ ∙ p) *ᵖ (x^ n₂ ∙ q) = *ᵖ-spine n₁ p n₂ q

infix 6 -ᵖ_
-ᵖ_ : Polynomial → Polynomial
-ᵖ p = -1#-nonzero ∙ᵖ p

infixl 6 _-ᵖ_
_-ᵖ_ : Polynomial → Polynomial → Polynomial
p -ᵖ q = p +ᵖ (-ᵖ q)

data Polynomialⁱ : Set c where
  0ⁱ    : Polynomialⁱ
  _+x∙_ : C → Polynomialⁱ → Polynomialⁱ

1ⁱ : Polynomialⁱ
1ⁱ = 1# +x∙ 0ⁱ

infixl 6 _+ⁱ_
_+ⁱ_ : Polynomialⁱ → Polynomialⁱ → Polynomialⁱ
0ⁱ +ⁱ q = q
(c₁ +x∙ p) +ⁱ 0ⁱ = c₁ +x∙ p
(c₁ +x∙ p) +ⁱ (c₂ +x∙ q) = (c₁ + c₂) +x∙ (p +ⁱ q)

infixl 7 _∙ⁱ_
_∙ⁱ_ : C → Polynomialⁱ → Polynomialⁱ
a ∙ⁱ 0ⁱ = 0ⁱ
a ∙ⁱ (c +x∙ p) = (a * c) +x∙ (a ∙ⁱ p)

infix 8 x∙_
x∙_ : Polynomialⁱ → Polynomialⁱ
x∙ p = 0# +x∙ p

infixl 7 _*ⁱ_
_*ⁱ_ : Polynomialⁱ → Polynomialⁱ → Polynomialⁱ
0ⁱ *ⁱ q = 0ⁱ
(c₁ +x∙ p) *ⁱ 0ⁱ = 0ⁱ
(c₁ +x∙ p) *ⁱ (c₂ +x∙ q) = (c₁ * c₂) +x∙ (c₁ ∙ⁱ q +ⁱ c₂ ∙ⁱ p +ⁱ x∙ (p *ⁱ q))

-ⁱ_ : Polynomialⁱ → Polynomialⁱ
-ⁱ p = (- 1#) ∙ⁱ p

infixl 6 _-ⁱ_
_-ⁱ_ : Polynomialⁱ → Polynomialⁱ → Polynomialⁱ
p -ⁱ q = p +ⁱ (-ⁱ q)

expandˢ : ℕ → Spine → Polynomialⁱ
expandˢ zero (K c) = proj₁ c +x∙ 0ⁱ
expandˢ zero (c +x^ n ∙ s) = proj₁ c +x∙ expandˢ (pred ⟅ n ⇓⟆) s
expandˢ (suc n) s = 0# +x∙ expandˢ n s

expand : Polynomial → Polynomialⁱ
expand 0ᵖ = 0ⁱ
expand (x^ n ∙ p) = expandˢ n p

constant : C → Polynomial
constant c with c ≈? 0#
... | yes _   = 0ᵖ
... | no  c≉0 = (c , c≉0) ∙𝑋^ 0

simplify : Polynomialⁱ → Polynomial
simplify 0ⁱ = 0ᵖ
simplify (c₁ +x∙ p) with c₁ ≈? 0# | simplify p
... | yes _   | 0ᵖ       = 0ᵖ
... | yes _   | x^ n ∙ q = x^ suc n ∙ q
... | no c₁≉0 | 0ᵖ       = x^ 0 ∙ (K (c₁ , c₁≉0))
... | no c₁≉0 | x^ n ∙ q = x^ 0 ∙ ((c₁ , c₁≉0) +x^ ⟅ suc n ⇑⟆ ∙ q)

data _≈ˢ_ : Spine → Spine → Set (c ⊔ˡ ℓ) where
  K≈ : ∀ {c₁ c₂} → proj₁ c₁ ≈ proj₁ c₂ → K c₁ ≈ˢ K c₂
  +≈ : ∀ {c₁ c₂} {n₁ n₂} {p q} → proj₁ c₁ ≈ proj₁ c₂ → n₁ ≡ n₂ → p ≈ˢ q → (c₁ +x^ n₁ ∙ p) ≈ˢ (c₂ +x^ n₂ ∙ q)

infix 4 _≈ᵖ_
data _≈ᵖ_ : Polynomial → Polynomial → Set (c ⊔ˡ ℓ) where
  0ᵖ≈ : 0ᵖ ≈ᵖ 0ᵖ
  0ᵖ≉ : ∀ {o₁ o₂} {p q} → o₁ ≡ o₂ → p ≈ˢ q → x^ o₁ ∙ p ≈ᵖ x^ o₂ ∙ q

infix 4 _≉ᵖ_
_≉ᵖ_ : Polynomial → Polynomial → Set (c ⊔ˡ ℓ)
p ≉ᵖ q = ¬ (p ≈ᵖ q)

≈ᵖ-refl : Reflexive _≈ᵖ_
≈ᵖ-refl {0ᵖ} = 0ᵖ≈
≈ᵖ-refl {x^ n ∙ p} = 0ᵖ≉ ≡-refl ≈ˢ-refl
  where
  ≈ˢ-refl : Reflexive _≈ˢ_
  ≈ˢ-refl {K c} = K≈ refl
  ≈ˢ-refl {c +x^ n ∙ p} = +≈ refl ≡-refl ≈ˢ-refl

≈ᵖ-sym : Symmetric _≈ᵖ_
≈ᵖ-sym {0ᵖ} {0ᵖ} 0ᵖ≈ = 0ᵖ≈
≈ᵖ-sym {x^ n ∙ p} {x^ n ∙ q} (0ᵖ≉ ≡-refl p≈ˢq) = 0ᵖ≉ ≡-refl (≈ˢ-sym p≈ˢq)
  where
  ≈ˢ-sym : Symmetric _≈ˢ_
  ≈ˢ-sym {K c₁} {K c₂} (K≈ c₁≈c₂) = K≈ (sym c₁≈c₂)
  ≈ˢ-sym {c₁ +x^ n ∙ p} {c₂ +x^ n ∙ q} (+≈ c₁≈c₂ ≡-refl p≈ˢq) = +≈ (sym c₁≈c₂) ≡-refl (≈ˢ-sym p≈ˢq)

≈ᵖ-trans : Transitive _≈ᵖ_
≈ᵖ-trans {0ᵖ} {0ᵖ} {0ᵖ} 0ᵖ≈ 0ᵖ≈ = 0ᵖ≈
≈ᵖ-trans {_}  {_}  {_} (0ᵖ≉ ≡-refl p≈ˢq) (0ᵖ≉ ≡-refl q≈ˢr) = 0ᵖ≉ ≡-refl (≈ˢ-trans p≈ˢq q≈ˢr)
  where
  ≈ˢ-trans : Transitive _≈ˢ_
  ≈ˢ-trans (K≈ c₁≈c₂) (K≈ c₂≈c₃) = K≈ (trans c₁≈c₂ c₂≈c₃)
  ≈ˢ-trans (+≈ c₁≈c₂ ≡-refl p≈ˢq) (+≈ c₂≈c₃ ≡-refl q≈ˢr) = +≈ (trans c₁≈c₂ c₂≈c₃) ≡-refl (≈ˢ-trans p≈ˢq q≈ˢr)

infix 4 _≈ⁱ_
data _≈ⁱ_ : Polynomialⁱ → Polynomialⁱ → Set (c ⊔ˡ ℓ) where
  0≈0 : 0ⁱ ≈ⁱ 0ⁱ
  0≈+ : ∀ {c} {p} → c ≈ 0# → 0ⁱ ≈ⁱ p → 0ⁱ ≈ⁱ c +x∙ p
  +≈0 : ∀ {c} {p} → c ≈ 0# → 0ⁱ ≈ⁱ p → c +x∙ p ≈ⁱ 0ⁱ
  +≈+ : ∀ {c₁ c₂} {p q} → c₁ ≈ c₂ → p ≈ⁱ q → c₁ +x∙ p ≈ⁱ c₂ +x∙ q

infix 4 _≉ⁱ_
_≉ⁱ_ : Polynomialⁱ → Polynomialⁱ → Set (c ⊔ˡ ℓ)
p ≉ⁱ q = ¬ (p ≈ⁱ q)

≈ⁱ-refl : Reflexive _≈ⁱ_
≈ⁱ-refl {0ⁱ} = 0≈0
≈ⁱ-refl {c +x∙ p} = +≈+ refl ≈ⁱ-refl

≈ⁱ-sym : Symmetric _≈ⁱ_
≈ⁱ-sym 0≈0 = 0≈0
≈ⁱ-sym (0≈+ c≈0 0≈p) = +≈0 c≈0 0≈p
≈ⁱ-sym (+≈0 c≈0 0≈p) = 0≈+ c≈0 0≈p
≈ⁱ-sym (+≈+ c₁≈c₂ p≈q) = +≈+ (sym c₁≈c₂) (≈ⁱ-sym p≈q)

≈ⁱ-trans : Transitive _≈ⁱ_
≈ⁱ-trans 0≈0 q = q
≈ⁱ-trans (0≈+ c₁≈0 0≈p) (+≈0 c₂≈0 0≈q) = 0≈0
≈ⁱ-trans (0≈+ c₁≈0 0≈p) (+≈+ c₁≈c₂ p≈q) = 0≈+ (trans (sym c₁≈c₂) c₁≈0) (≈ⁱ-trans 0≈p p≈q)
≈ⁱ-trans (+≈0 c₁≈0 0≈p) 0≈0 = +≈0 c₁≈0 0≈p
≈ⁱ-trans (+≈0 c₁≈0 0≈p) (0≈+ c₂≈0 0≈q) = +≈+ (trans c₁≈0 (sym c₂≈0)) (≈ⁱ-trans (≈ⁱ-sym 0≈p) 0≈q)
≈ⁱ-trans (+≈+ c₁≈c₂ p≈q) (+≈0 c₂≈0 0≈q) = +≈0 (trans c₁≈c₂ c₂≈0) (≈ⁱ-trans 0≈q (≈ⁱ-sym p≈q))
≈ⁱ-trans (+≈+ c₁≈c₂ p≈q) (+≈+ c₂≈c₃ q≈r) = +≈+ (trans c₁≈c₂ c₂≈c₃) (≈ⁱ-trans p≈q q≈r)

+ᵖ-*ᵖ-rawRing : RawRing (c ⊔ˡ ℓ) (c ⊔ˡ ℓ)
+ᵖ-*ᵖ-rawRing = record
  { Carrier = Polynomial
  ; _≈_ = _≈ᵖ_
  ; _+_ = _+ᵖ_
  ; _*_ = _*ᵖ_
  ; -_ = -ᵖ_
  ; 0# = 0ᵖ
  ; 1# = 1ᵖ
  }

+ⁱ-*ⁱ-rawRing : RawRing c (c ⊔ˡ ℓ)
+ⁱ-*ⁱ-rawRing = record
  { Carrier = Polynomialⁱ
  ; _≈_ = _≈ⁱ_
  ; _+_ = _+ⁱ_
  ; _*_ = _*ⁱ_
  ; -_ = -ⁱ_
  ; 0# = 0ⁱ
  ; 1# = 1ⁱ
  }

open import AKS.Extended ≤-totalOrder
  using (module ≤ᵉ-Reasoning)
  renaming
  ( Extended to Degree
  ; _≤ᵉ_ to _≤ᵈ_
  ; ≤ᵉ-refl to ≤ᵈ-refl
  ; ≤ᵉ-trans to ≤ᵈ-trans
  )
  public
open Degree public
open _≤ᵈ_ public

module ≤ᵈ-Reasoning where
  open ≤ᵉ-Reasoning renaming (_∼⟨_⟩_ to _≤ᵈ⟨_⟩_; _∎ to _∎ᵈ; _≡⟨_⟩_ to _≡ᵈ⟨_⟩_) public

instance
  Degree-number : Number Degree
  Degree-number = record
    { Constraint = λ _ → ⊤
    ; fromNat = λ n → ⟨ n ⟩
    }

infixl 5 _⊔ᵈ_
_⊔ᵈ_ : Degree → Degree → Degree
-∞ ⊔ᵈ d₂ = d₂
⟨ d₁ ⟩ ⊔ᵈ -∞ = ⟨ d₁ ⟩
⟨ d₁ ⟩ ⊔ᵈ ⟨ d₂ ⟩ = ⟨ d₁ ⊔ℕ d₂ ⟩

infixl 5 _+ᵈ_
_+ᵈ_ : Degree → Degree → Degree
-∞ +ᵈ d₂ = -∞
⟨ d₁ ⟩ +ᵈ -∞ = -∞
⟨ d₁ ⟩ +ᵈ ⟨ d₂ ⟩ = ⟨ d₁ +ℕ d₂ ⟩

degreeˢ : Spine → ℕ
degreeˢ (K c) = 0
degreeˢ (c +x^ n ∙ p) = ⟅ n ⇓⟆ +ℕ degreeˢ p

degree : Polynomial → Degree
degree 0ᵖ = -∞
degree (x^ n ∙ p) = ⟨ n +ℕ degreeˢ p ⟩

deg : ∀ p {p≉0 : p ≉ᵖ 0ᵖ} → ℕ
deg 0ᵖ {p≉0} = contradiction ≈ᵖ-refl p≉0
deg (x^ n ∙ p) {p≉0} = n +ℕ degreeˢ p

degreeⁱ : Polynomialⁱ → Degree
degreeⁱ 0ⁱ = -∞
degreeⁱ (c +x∙ p) with degreeⁱ p
... | ⟨ n ⟩ = ⟨ suc n ⟩
... | -∞ with c ≈? 0#
...   | yes _ = -∞
...   | no  _ = 0

open import Data.String using (String; _++_)
open import Data.Nat.Show using () renaming (show to show-ℕ)

show-Polynomial : (C → String) → Polynomial → String
show-Polynomial show-c 0ᵖ = "0"
show-Polynomial show-c (x^ n ∙ p) = loop n p
  where
  loop : ℕ → Spine → String
  loop zero (K c) = show-c (proj₁ c)
  loop zero (c +x^ n ∙ p) = show-c (proj₁ c) ++ " + " ++ loop ⟅ n ⇓⟆ p
  loop (suc n) (K c) = show-c (proj₁ c) ++ " * X^" ++ show-ℕ (suc n)
  loop (suc n) (c +x^ m ∙ p) = show-c (proj₁ c) ++ " * X^" ++ show-ℕ (suc n) ++ " + " ++ loop (suc n +ℕ ⟅ m ⇓⟆) p

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
{-# OPTIONS --erased-cubical #-}

module SMain where

open import Data.List using (map)
open import Data.Nat  using (_*_)
open import Data.Unit using (⊤)

open import Midi      using (IO; exportTracks; track→htrack)

open import Soundness using (soundTracks)
open import Motif     using (multiplier)

main : IO ⊤
main =
  let ticksPerBeat = 4 * multiplier -- (1 = quarter notes; 4 = 16th notes)
      file         = "/Users/leo/Music/MusicTools/test.mid"
      song         = soundTracks
  in exportTracks file ticksPerBeat (map track→htrack song)

max_stars_repo_name: halfaya/Music

max_issues_repo_name: halfaya/Music

max_forks_repo_name: halfaya/Music


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Connecting Parametric.Change.Term and Parametric.Change.Value.
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value
import Parametric.Denotation.Evaluation as Evaluation
import Parametric.Change.Type as ChangeType
import Parametric.Change.Term as ChangeTerm
import Parametric.Change.Value as ChangeValue

module Parametric.Change.Evaluation
    {Base : Type.Structure}
    {Const : Term.Structure Base}
    (⟦_⟧Base : Value.Structure Base)
    (⟦_⟧Const : Evaluation.Structure Const ⟦_⟧Base)
    (ΔBase : ChangeType.Structure Base)
    (apply-base : ChangeTerm.ApplyStructure Const ΔBase)
    (diff-base : ChangeTerm.DiffStructure Const ΔBase)
    (nil-base : ChangeTerm.NilStructure Const ΔBase)
    (⟦apply-base⟧ : ChangeValue.ApplyStructure Const ⟦_⟧Base ΔBase)
    (⟦diff-base⟧ : ChangeValue.DiffStructure Const ⟦_⟧Base ΔBase)
    (⟦nil-base⟧ : ChangeValue.NilStructure Const ⟦_⟧Base ΔBase)
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base
open Evaluation.Structure Const ⟦_⟧Base ⟦_⟧Const
open ChangeType.Structure Base ΔBase
open ChangeTerm.Structure Const ΔBase apply-base diff-base nil-base
open ChangeValue.Structure Const ⟦_⟧Base ΔBase ⟦apply-base⟧ ⟦diff-base⟧ ⟦nil-base⟧

open import Relation.Binary.PropositionalEquality
open import Base.Denotation.Notation
open import Postulate.Extensionality

-- Extension point 1: Relating ⊕ and its value on base types
ApplyStructure : Set
ApplyStructure = ∀ ι {Γ} →
  {t : Term Γ (base ι)} {Δt : Term Γ (ΔType (base ι))} {ρ : ⟦ Γ ⟧} →
  ⟦ t ⟧ ρ ⟦⊕₍ base ι ₎⟧ ⟦ Δt ⟧ ρ ≡ ⟦ t ⊕₍ base ι ₎ Δt ⟧ ρ

-- Extension point 2: Relating ⊝ and its value on base types
DiffStructure : Set
DiffStructure = ∀ ι {Γ} →
  {s : Term Γ (base ι)} {t : Term Γ (base ι)} {ρ : ⟦ Γ ⟧} →
  ⟦ s ⟧ ρ ⟦⊝₍ base ι ₎⟧ ⟦ t ⟧ ρ ≡ ⟦ s ⊝₍ base ι ₎ t ⟧ ρ

-- Extension point 3: Relating nil-term and its value on base types
NilStructure : Set
NilStructure = ∀ ι {Γ} →
  {t : Term Γ (base ι)} {ρ : ⟦ Γ ⟧} →
  ⟦nil₍ base ι ₎⟧ (⟦ t ⟧ ρ) ≡ ⟦ onil₍ base ι ₎ t ⟧ ρ

module Structure
    (meaning-⊕-base    : ApplyStructure)
    (meaning-⊝-base    : DiffStructure)
    (meaning-onil-base : NilStructure)
  where

  -- unique names with unambiguous types
  -- to help type inference figure things out
  private
    module Disambiguation where
      infixr 9 _⋆_
      _⋆_ : Type → Context → Context
      _⋆_ = _•_

  -- We provide: Relating ⊕ and ⊝ and their values on arbitrary types.
  meaning-⊕ : ∀ {τ Γ}
    {t : Term Γ τ} {Δt : Term Γ (ΔType τ)} {ρ : ⟦ Γ ⟧} →
    ⟦ t ⟧ ρ ⟦⊕₍ τ ₎⟧ ⟦ Δt ⟧ ρ ≡ ⟦ t ⊕₍ τ ₎ Δt ⟧ ρ

  meaning-⊝ : ∀ {τ Γ}
    {s : Term Γ τ} {t : Term Γ τ} {ρ : ⟦ Γ ⟧} →
    ⟦ s ⟧ ρ ⟦⊝₍ τ ₎⟧ ⟦ t ⟧ ρ ≡ ⟦ s ⊝₍ τ ₎ t ⟧ ρ

  meaning-onil : ∀ {τ Γ}
    {t : Term Γ τ} {ρ : ⟦ Γ ⟧} →
    ⟦nil₍ τ ₎⟧ (⟦ t ⟧ ρ) ≡ ⟦ onil₍ τ ₎ t ⟧ ρ

  meaning-⊕ {base ι} {Γ} {τ} {Δt} {ρ} = meaning-⊕-base ι {Γ} {τ} {Δt} {ρ}
  meaning-⊕ {σ ⇒ τ} {Γ} {t} {Δt} {ρ} = ext (λ v →
    let
      Γ′ = σ ⋆ (σ ⇒ τ) ⋆ ΔType (σ ⇒ τ) ⋆ Γ
      ρ′ : ⟦ Γ′ ⟧
      ρ′ = v • (⟦ t ⟧ ρ) • (⟦ Δt ⟧ ρ) • ρ
      x  : Term Γ′ σ
      x  = var this
      f  : Term Γ′ (σ ⇒ τ)
      f  = var (that this)
      Δf : Term Γ′ (ΔType (σ ⇒ τ))
      Δf = var (that (that this))
      y  = app f x
      Δy = app (app Δf x) (onil x)
    in
      begin
        ⟦ t ⟧ ρ v ⟦⊕₍ τ ₎⟧ ⟦ Δt ⟧ ρ v (⟦nil₍ σ ₎⟧ v)
      ≡⟨ cong (λ hole → ⟦ t ⟧ ρ v ⟦⊕₍ τ ₎⟧ ⟦ Δt ⟧ ρ v hole)
           (meaning-onil {t = x} {ρ′}) ⟩
        ⟦ t ⟧ ρ v ⟦⊕₍ τ ₎⟧ ⟦ Δt ⟧ ρ v (⟦ onil x ⟧ ρ′)
      ≡⟨ meaning-⊕ {t = y} {Δt = Δy} {ρ′} ⟩
        ⟦ y ⊕₍ τ ₎ Δy ⟧ ρ′
      ∎)
    where
      open ≡-Reasoning
      open Disambiguation

  meaning-⊝ {base ι} {Γ} {s} {t} {ρ} = meaning-⊝-base ι {Γ} {s} {t} {ρ}
  meaning-⊝ {σ ⇒ τ} {Γ} {s} {t} {ρ} =
    ext (λ v → ext (λ Δv →
    let
      Γ′ = ΔType σ ⋆ σ ⋆ (σ ⇒ τ) ⋆ (σ ⇒ τ) ⋆ Γ
      ρ′ : ⟦ Γ′ ⟧Context
      ρ′ = Δv • v • ⟦ t ⟧Term ρ • ⟦ s ⟧Term ρ • ρ
      Δx : Term Γ′ (ΔType σ)
      Δx = var this
      x  : Term Γ′ σ
      x  = var (that this)
      f  : Term Γ′ (σ ⇒ τ)
      f  = var (that (that this))
      g  : Term Γ′ (σ ⇒ τ)
      g  = var (that (that (that this)))
      y  = app f x
      y′ = app g (x ⊕₍ σ ₎ Δx)
    in
      begin
        ⟦ s ⟧ ρ (v ⟦⊕₍ σ ₎⟧ Δv) ⟦⊝₍ τ ₎⟧ ⟦ t ⟧ ρ v
      ≡⟨ cong (λ hole → ⟦ s ⟧ ρ hole ⟦⊝₍ τ ₎⟧ ⟦ t ⟧ ρ v)
           (meaning-⊕ {t = x} {Δt = Δx} {ρ′}) ⟩
        ⟦ s ⟧ ρ (⟦ x ⊕₍ σ ₎ Δx ⟧ ρ′) ⟦⊝₍ τ ₎⟧ ⟦ t ⟧ ρ v
      ≡⟨ meaning-⊝ {s = y′} {y} {ρ′} ⟩
        ⟦ y′ ⊝ y ⟧ ρ′
      ∎))
    where
      open ≡-Reasoning
      open Disambiguation

  meaning-onil {base ι} {Γ} {t} {ρ} = meaning-onil-base ι {Γ} {t} {ρ}
  meaning-onil {σ ⇒ τ} {Γ} {t} {ρ} = meaning-⊝ {σ ⇒ τ} {Γ} {t} {t} {ρ}
  -- Ideally, this proof should simply be:
  -- meaning-⊝ {σ ⇒ τ} {Γ} {t} {t} {ρ}
  --
  -- However, the types of the results don't match because using onil constructs
  -- different environments.

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module TelescopingLet1 where

f : (let ★ = Set) (A : ★) → A → A
f A x = x

data X : ★ where
-- should fail, since ★ is not in global scope

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-09-03, issue #2729.
-- Expect non-indexed or -primed variables when splitting.

-- {-# OPTIONS -v interaction.case:100 #-}
-- {-# OPTIONS -v tc.cover:40 #-}

data Size : Set where
  ↑ : Size → Size

data Nat : Size → Set where
  zero : ∀ i → Nat (↑ i)
  suc  : ∀ i → Nat i → Nat (↑ i)

pred : ∀ i → Nat i → Nat i
pred i x = {!x!}  -- C-c C-c

-- WRONG (agda-2.5.3):
-- pred .(↑ i₁) (zero i₁) = ?
-- pred .(↑ i₁) (suc i₁ x) = ?

-- EXPECTED (correct in agda-2.5.1.1):
-- pred .(↑ i) (zero i) = ?
-- pred .(↑ i) (suc i x) = ?


text:
-- Andreas, 2017-07-29, issue #2644 reported by Christian Sattler
--
-- Silly mistake in expandRecordVar:
-- Substitution applied to ListTel instead of Telescope.
-- (Messed up the de Bruijn indices, garbage.)

-- This file should pass with lots of yellow.

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.meta.assign.proj:45 #-}

-- OLD:
-- {-# OPTIONS -v tc.cc:20 #-}
-- {-# OPTIONS -v tc.lhs:10 #-}
-- {-# OPTIONS -v tc.decl:10 #-}
-- {-# OPTIONS -v tc.ip:20 #-}
-- {-# OPTIONS -v tc.check.internal:20 #-}
-- {-# OPTIONS -v tc.meta.check:30 #-}
-- {-# OPTIONS -v tc:20 #-}
-- {-# OPTIONS -v tc.meta:50 #-}
-- {-# OPTIONS -v tc:45 #-}
-- {-# OPTIONS -v tc.term.exlam:100 -v tc:90 #-}

record Σ (A¹ : Set) (B¹ : A¹ → Set) : Set where
  constructor pair
  field
    fst : A¹
    snd : B¹ fst
open Σ

postulate
  Path : (A² : Set) → A² → A² → Set
  path : (A³ : Set) → Path _ _ _

record S : Set₁ where
  constructor mkS
  field
    Aₛ : Set
    Bₛ : (aₛ¹ : Aₛ) → Set
    zₛ : (aₛ² : Aₛ) → Bₛ aₛ²

record T : Set₁ where
  constructor mkT
  field
    A : Set
    B : (a¹ : A) → Set
    z : (a² : A) → B a²
    s : (a³ : A) → B a³ → B a³
    p : (a⁴ : A) (f : B a⁴) → Path _ f (s _ (z _))

-- passes without the matching
f₀ : S → T
f₀ X = record { A = Σ _ _
             ; B =  λ b → Σ _ _ -- λ { (b₁ , b₂) → Σ _ _ }
             ; z =  λ z₁ → pair (S.zₛ X _) _
             ; s =  λ s₁ s₂ → _
             ; p =  λ p₁ p₂ → path _
             }

-- This was my final variant

module Final where
 mutual
  TA : S → Set
  TA Z = Σ _ _
  aux : (Y : S) → TA Y → Set
  aux Y (pair b¹ b²) = Σ _ _  -- fails
  fₐ : S → T
  fₐ X = record { A = TA X
                ; B =  aux X
                ; z =  λ (z¹ : TA X) → pair (S.zₛ X _) _
                ; s =  λ (s¹ : TA X) (s² : aux X s¹) → _
                ; p =  λ (p¹ : TA X) (p² : aux X p¹) → path _
                }

-- Intermediate

fₐᵤ : S → T
fₐᵤ X = record { A = TA
              ; B =  aux
              ; z =  λ (z₁ : TA) → pair (S.zₛ X _) _
              ; s =  λ (s₁ : TA) (s₂ : aux s₁) → _
              ; p =  λ (p₁ : TA) (p₂ : aux p₁) → path _
              }
  where
  TA = Σ _ _
  aux : TA → Set
  -- (passes without the matching)
  -- aux b = let b₁ = fst b; b₂ = snd b in {! Σ _ _ !}  -- worked
  aux (pair b₁ b₂) = Σ _ _  -- failed

-- Close to original

f : S → T
f X = record { A = Σ _ _
             ; B =  λ { (pair b₁ b₂) → Σ _ _ }
             ; z =  λ z₁ → pair (S.zₛ X _) _
             ; s =  λ s₁ s₂ → _
             ; p =  λ p₁ p₂ → path _
             }

{- Hunted down the crash cause:

context before projection expansion
  (X : S) (p¹ : TA X) (p² : aux X p¹)
meta args:  [X, p¹, pair (S.zₛ X (_aₛ²_34 X p¹)) (?1 X p¹)]
trying to expand projected variable X
eta-expanding var  X  in terms  ([X, p¹,
                                  pair (S.zₛ X (_aₛ²_34 X p¹)) (?1 X p¹)],_8 (?2 X p¹ p²))
meta args:  [mkS Aₛ(X) Bₛ(X) zₛ(X), p¹,
             pair (zₛ(X) (_aₛ²_34 (mkS Aₛ(X) Bₛ(X) zₛ(X)) p¹))
             (?1 (mkS Aₛ(X) Bₛ(X) zₛ(X)) p¹)]
context before projection expansion
  (X : S)           S
  (p¹ : TA X)       TA 0
  (p² : aux X p¹)   aux 1 0
context after projection expansion
  (Aₛ(X) : Set)
  (Bₛ(X) : Aₛ(X) → Set)
  (zₛ(X) : (aₛ² : Aₛ(X)) → Bₛ(X) aₛ²)
  (p¹ : TA (mkS Aₛ(X) Bₛ(X) zₛ(X)))      -- This type is fine
  (p² : aux Aₛ(X) (mkS Bₛ(X) zₛ(X) p¹))  -- This type is messed up!

-}

-- -}
-- -}
-- -}
-- -}
-- -}


text:
-- Kapitel 1, Abschnitt D (Die Eigenschaften der Gleichheit)
module CombinatoryLogic.Equality where

open import Algebra.Definitions using (Congruent₂; LeftCongruent; RightCongruent)
open import Data.Vec using (Vec; []; _∷_; foldr₁; lookup)
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence; Setoid)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import CombinatoryLogic.Semantics
open import CombinatoryLogic.Syntax

private
  -- A lemma used in the proofs of Propositions 1 and 2.
  lemma-CQXX : ∀ {X} → ⊢ C ∙ Q ∙ X ∙ X
  lemma-CQXX {X} =
    let s₁ = ⊢ Π ∙ (W ∙ (C ∙ Q))                        [ ax Q ]
        s₂ = ⊢ W ∙ (C ∙ Q) ∙ X                          [ Π s₁ ]
        s₃ = ⊢ Q ∙ (W ∙ (C ∙ Q) ∙ X) ∙ (C ∙ Q ∙ X ∙ X)  [ W ]
        s₄ = ⊢ C ∙ Q ∙ X ∙ X                            [ Q₁ s₂ s₃ ]
    in s₄

-- Satz 1
prop₁ : ∀ {X} → ⊢ Q ∙ X ∙ X
prop₁ {X} = s₆ where
  s₄ = ⊢ C ∙ Q ∙ X ∙ X                            [ lemma-CQXX ]
  s₅ = ⊢ Q ∙ (C ∙ Q ∙ X ∙ X) ∙ (Q ∙ X ∙ X)        [ C ]
  s₆ = ⊢ Q ∙ X ∙ X                                [ Q₁ s₄ s₅ ]

-- Satz 2
prop₂ : ∀ {X Y} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ Y ∙ X
prop₂ {X} {Y} ⊢QXY = s₅ where
  s₁ = ⊢ Q ∙ X ∙ Y                             [ ⊢QXY ]
  -- NOTE: Curry's proof contains a mistake: CQXX should be CQXY.
  s₂ = ⊢ Q ∙ (C ∙ Q ∙ X ∙ X) ∙ (C ∙ Q ∙ X ∙ Y) [ Q₂ {Z = C ∙ Q ∙ X} s₁ ]
  s₃ = ⊢ C ∙ Q ∙ X ∙ X                         [ lemma-CQXX ]
  -- NOTE: Curry's proof uses rule Q, but there is no such rule.
  s₄ = ⊢ C ∙ Q ∙ X ∙ Y                         [ Q₁ s₃ s₂ ]
  s₅ = ⊢ Q ∙ Y ∙ X                             [ Q₁ s₄ C ]

-- Satz 3
prop₃ : ∀ {X Y Z} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ Y ∙ Z → ⊢ Q ∙ X ∙ Z
prop₃ {X} {Y} {Z} ⊢QXY ⊢QYZ = s₃ where
  s₁ = ⊢ Q ∙ Y ∙ Z                     [ ⊢QYZ ]
  s₂ = ⊢ Q ∙ (Q ∙ X ∙ Y) ∙ (Q ∙ X ∙ Z) [ Q₂ {Z = Q ∙ X} s₁ ]
  s₃ = ⊢ Q ∙ X ∙ Z                     [ Q₁ ⊢QXY s₂ ]

-- Satz 4
prop₄ : ∀ {X Y Z} → ⊢ Q ∙ X ∙ Y → ⊢ Q ∙ (X ∙ Z) ∙ (Y ∙ Z)
prop₄ {X} {Y} {Z} Hp = s₅ where
  p₁ = λ {X} → ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (B ∙ (W ∙ K) ∙ X ∙ Z)  [ C ]
  p₂ = λ {X} → ⊢ Q ∙ (B ∙ (W ∙ K) ∙ X ∙ Z) ∙ (W ∙ K ∙ (X ∙ Z))            [ B ]
  p₃ = λ {X} → ⊢ Q ∙ (W ∙ K ∙ (X ∙ Z)) ∙ (K ∙ (X ∙ Z) ∙ (X ∙ Z))          [ W ]
  p₄ = λ {X} → ⊢ Q ∙ (K ∙ (X ∙ Z) ∙ (X ∙ Z)) ∙ (X ∙ Z)                    [ K ]
  p₅ = λ {X} → ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (X ∙ Z)                [ prop₃ p₁ $ prop₃ p₂ $ prop₃ p₃ p₄ ]
  s₁ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ Y)  [ Q₂ Hp ]
  s₂ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X) ∙ (X ∙ Z)                      [ p₅ ]
  s₃ = ⊢ Q ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ Y) ∙ (Y ∙ Z)                      [ p₅ ]
  s₄ = ⊢ Q ∙ (X ∙ Z) ∙ (C ∙ (B ∙ (W ∙ K)) ∙ Z ∙ X)                      [ prop₂ s₂ ]
  s₅ = ⊢ Q ∙ (X ∙ Z) ∙ (Y ∙ Z)                                          [ prop₃ s₄ $ prop₃ s₁ s₃ ]

-- Satz 5
prop₅ : ∀ {X Y} → X ≡ Y → ⊢ Q ∙ X ∙ Y
prop₅ {X} {Y} refl = prop₁

-- Satz 6 (first part)
isEquivalence : IsEquivalence _≈_
isEquivalence = record
  { refl = prop₁
  ; sym = prop₂
  ; trans = prop₃
  }

setoid : Setoid _ _
setoid = record
  { Carrier = Combinator
  ; _≈_ = _≈_
  ; isEquivalence = isEquivalence
  }

module Reasoning where
  module ≈ = IsEquivalence isEquivalence
  import Relation.Binary.Reasoning.Base.Single _≈_ ≈.refl ≈.trans as Base
  open Base using (begin_; _∎) public

  infixr 2 _≈⟨⟩_ step-≈ step-≈˘

  _≈⟨⟩_ : ∀ x {y} → x Base.IsRelatedTo y → x Base.IsRelatedTo y
  _ ≈⟨⟩ x≈y = x≈y

  step-≈ = Base.step-∼
  syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z

  step-≈˘ : ∀ x {y z} → y Base.IsRelatedTo z → y ≈ x → x Base.IsRelatedTo z
  step-≈˘ x y∼z y≈x = x ≈⟨ ≈.sym y≈x ⟩ y∼z
  syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z

-- Satz 6 (second part)
cong : Congruent₂ _≈_ _∙_
cong {X} {X′} {Y} {Y′} ⊢X==X′ ⊢Y==Y′ = s₃ where
  s₁ = ⊢ X ∙ Y == X ∙ Y′    [ Q₂ ⊢Y==Y′ ]
  s₂ = ⊢ X ∙ Y′ == X′ ∙ Y′  [ prop₄ ⊢X==X′ ]
  s₃ = ⊢ X ∙ Y == X′ ∙ Y′   [ prop₃ s₁ s₂ ]

-- congˡ and congʳ follow from cong, but are also just different names for
-- Q₂ and prop₄, respectively.
congˡ : LeftCongruent _≈_ _∙_
congˡ = Q₂

congʳ : RightCongruent _≈_ _∙_
congʳ = prop₄

-- TODO: Satz 7, 8

prop₉ : ∀ {X} → ⊢ I ∙ X == X
prop₉ {X} = begin
  I ∙ X      ≈⟨⟩
  W ∙ K ∙ X  ≈⟨ W ⟩
  K ∙ X ∙ X  ≈⟨ K ⟩
  X          ∎
  where open Reasoning

-- Note after the proof of Satz 9.
S : Combinator
S = B ∙ (B ∙ W) ∙ (B ∙ B ∙ C)

prop-S : ∀ {X} {Y} {Z} → ⊢ S ∙ X ∙ Y ∙ Z == X ∙ Z ∙ (Y ∙ Z)
prop-S {X} {Y} {Z} = begin
  S ∙ X ∙ Y ∙ Z                          ≈⟨⟩
  B ∙ (B ∙ W) ∙ (B ∙ B ∙ C) ∙ X ∙ Y ∙ Z  ≈⟨ congʳ $ congʳ B ⟩
  B ∙ W ∙ (B ∙ B ∙ C ∙ X) ∙ Y ∙ Z        ≈⟨ congʳ B ⟩
  W ∙ (B ∙ B ∙ C ∙ X ∙ Y) ∙ Z            ≈⟨ W ⟩
  B ∙ B ∙ C ∙ X ∙ Y ∙ Z ∙ Z              ≈⟨ congʳ $ congʳ $ congʳ B ⟩
  B ∙ (C ∙ X) ∙ Y ∙ Z ∙ Z                ≈⟨ congʳ B ⟩
  C ∙ X ∙ (Y ∙ Z) ∙ Z                    ≈⟨ C ⟩
  X ∙ Z ∙ (Y ∙ Z)                        ∎
  where open Reasoning

-- TODO: ⊢ B == S(KS)K, ⊢ C == S(BBS)(KK), ⊢ W == SS(SK), ⊢ I == SKK

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
{-# OPTIONS --guardedness #-}

module Cubical.README where

------------------------------------------------------------------------
-- An experimental library for Cubical Agda
-----------------------------------------------------------------------

-- The library comes with a .agda-lib file, for use with the library
-- management system.

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- The core library for Cubical Agda.
-- It contains basic primitives, equivalences, glue types.
import Cubical.Core.Everything

-- The foundations for Cubical Agda.
-- The Prelude module is self-explanatory.
import Cubical.Foundations.Prelude
import Cubical.Foundations.Everything

-- Kinds and properties of functions
import Cubical.Functions.Everything

-- Data types and properties
import Cubical.Data.Everything

-- Higher-inductive types
import Cubical.HITs.Everything

-- Coinductive data types and properties
import Cubical.Codata.Everything

-- Papers
import Cubical.Papers.Everything

-- Properties and proofs about relations
import Cubical.Relation.Everything

-- Category theory
import Cubical.Categories.Everything

-- Homotopy theory
import Cubical.Homotopy.Everything

-- Properties and kinds of Modalities
import Cubical.Modalities.Everything

-- Various experiments using Cubical Agda
import Cubical.Experiments.Everything

-- Other modules (TODO: add descriptions)
import Cubical.Induction.Everything
import Cubical.Structures.Everything

-- general definition of cohomology
import Cubical.Cohomology.Everything

-- cohomology with constant Integer coefficients
import Cubical.ZCohomology.Everything

-- Algebra library (in development)
import Cubical.Algebra.Everything

-- Various talks
import Cubical.Talks.Everything

-- Reflection
import Cubical.Reflection.Everything

-- Displayed univalent graphs
import Cubical.Displayed.Everything

-- Syntax typeclasses
import Cubical.Syntax.Everything

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Andreas, 2017-04-26, issue #2554
-- Allow mutual sized types in successor style.

-- {-# OPTIONS -v tc.pos.args:100 #-}
-- {-# OPTIONS -v tc.pos:100 #-}
-- {-# OPTIONS -v tc.polarity:20 #-}

open import Agda.Builtin.Size

mutual

  data C : Size → Set where
    c : ∀{i} → D i → C (↑ i)

  data D : Size → Set where
    d : ∀{i} → C i → D (↑ i)

-- Test subtyping

test : ∀{i} {j : Size< i} → C j → C i
test x = x

-- Define a size-preserving function

mutual

  f : ∀{i} → C i → C i
  f (c y) = c (g y)

  g : ∀{i} → D i → D i
  g (d x) = d (f x)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.TopLevel(x : X) where
  import OutsideIn.Expressions as E
  open E(x)
  open X(x)

  data Program (ev : Set)(tv : Set) : Set where
    end : Program ev tv
    bind₁_,_ : ∀ {s} → Expression ev tv s → Program (Ⓢ ev) tv → Program ev tv
    bind₂_·_∷_⇒_,_ : ∀ {s} → (n : ℕ) → Expression ev (tv ⨁ n) s
                   → QConstraint (tv ⨁ n) → Type (tv ⨁ n)
                   → Program (Ⓢ ev) tv → Program ev tv

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
module Fail.NonCopatternInstance where

record HasId (a : Set) : Set where
  field id : a → a

open HasId ⦃ ... ⦄

{-# COMPILE AGDA2HS HasId class #-}

data Unit : Set where
  MkUnit : Unit

{-# COMPILE AGDA2HS Unit #-}

instance
  UnitHasId : HasId Unit
  UnitHasId = record { id = λ x → x }   -- NOT CORRECT
  -- UnitHasId .id x = x                -- CORRECT

{-# COMPILE AGDA2HS UnitHasId #-}


text:
-- Andreas, 2020-02-15, issue #4447
--
-- Positivity checker needs to see the constructor types
-- in the same way as the type checker has seen them.
--
-- Thus, we need to reduce types of constructors even
-- with definitions that have not yet been subjected to termination
-- checking, e.g. because they live in a mutual block with the data type.

-- {-# OPTIONS -v term:10 #-}
-- {-# OPTIONS -v tc.pos:10 #-}
-- {-# OPTIONS -v tc.data:10 #-}

data ⊥ : Set where

-- Mutual block:

data D : Set
D' = (D → ⊥) → D
data D where
  abs : D'

-- Positivity checker needs to unfold D', otherwise it does not see
-- the correct occurrences of D.

-- From here, the road to absurdity is paved:

app : D → D → ⊥
app (abs f) = f

delta : D → ⊥
delta x = app x x

Omega : ⊥
Omega = delta (abs delta)

max_forks_repo_name: shlevy/agda


text:
module Acme.Data.Fin where

open import Acme.Type
open import Acme.Data.Nat as ℕ using (ℕ)

Fin : Elt ℕ → Type
Fin = ℕ.induction (λ _ → Type) base (λ _ → step)

  where

  base : Type
  base _ = false

  step : Type → Type
  step ih [] = false
  step ih (c ∷ cs) = c == 'Z' && isNil cs
                  || c == 'S' && ih cs

zero : ∀ {n} → Elt (Fin (ℕ.suc n))
zero {n} = Fin (ℕ.suc n) ∋ "Z"

suc : ∀ {n} → Elt (Fin n) → Elt (Fin (ℕ.suc n))
suc [ k ] = [ 'S' ∷ k ]

sub : ∀ n str → str ∈ Fin n → str ∈ ℕ
sub = ℕ.induction
        (λ n → ∀ str → str ∈ Fin n → str ∈ ℕ)
        (λ _ ())
         step

  where

  step : ∀ n → (∀ str → str ∈ Fin n → str ∈ ℕ) →
               (∀ str → str ∈ Fin (ℕ.suc n) → str ∈ ℕ)
  step n ih (c ∷ cs) isFin = checkZ (c ≟ 'Z') cs {{isFin}} where

    checkS : ∀ {b} → Reflects c 'S' b → ∀ cs →
             {{IsTrue (b && Fin n cs)}} →
             (c ∷ cs) ∈ ℕ
    checkS true cs {{isFin}} = ih cs isFin

    checkZ : ∀ {b} → Reflects c 'Z' b → ∀ cs →
             {{IsTrue (b && isNil cs || c == 'S' && Fin n cs)}} →
             (c ∷ cs) ∈ ℕ
    checkZ true  [] = _
    checkZ false cs = checkS (c ≟ 'S') cs

cast : ∀ {n} → Elt (Fin n) → Elt ℕ
cast {n} p .value = p .value
cast {n} p .check = sub n (p .value) (p .check)

max_stars_repo_name: gallais/STRINaGda

max_issues_repo_name: gallais/STRINaGda

max_forks_repo_name: gallais/STRINaGda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.PointedSets where

-- Category of Pointed Sets

open import Level
open import Relation.Binary
open import Function using (_∘′_; _$_) renaming (id to idf)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
open import Data.Product

open import Categories.Category
open import Categories.Category.Instance.Sets
open import Categories.Functor using (Functor)

PointedSets : ∀ o → Category (suc o) o o
PointedSets o = record
  { Obj       = Σ (Set o) idf
  ; _⇒_       = λ c d → Σ (proj₁ c → proj₁ d) (λ f → f (proj₂ c) ≡ proj₂ d)
  ; _≈_       = λ f g → ∀ x → proj₁ f x ≡ proj₁ g x
  ; id        = idf , refl
  ; _∘_       = λ { (f , f-pres-pt) (g , g-pres-pt) → f ∘′ g , ≡.trans (≡.cong f g-pres-pt) f-pres-pt}
  ; assoc     = λ _ → refl
  ; sym-assoc = λ _ → refl
  ; identityˡ = λ _ → refl
  ; identityʳ = λ _ → refl
  ; identity² = λ _ → refl
  ; equiv     = record { refl = λ _ → refl ; sym = λ pf x → ≡.sym $ pf x ; trans = λ i≡j j≡k x → ≡.trans (i≡j x) (j≡k x) }
  ; ∘-resp-≈  = λ {_} {_} {_} {_} {h} {g} f≡h g≡i x → ≡.trans (f≡h (proj₁ g x)) (≡.cong (proj₁ h) $ g≡i x)
  }

Underlying : {o : Level} → Functor (PointedSets o) (Sets o)
Underlying = record
  { F₀           = proj₁
  ; F₁           = proj₁
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ f≈g {x} → f≈g x
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K --rewriting --termination-depth=2 #-}

open import HoTT
open import cw.CW
open import cw.examples.Sphere

module cw.examples.Torus where

⊤-has-dec-eq : has-dec-eq ⊤
⊤-has-dec-eq unit unit = inl idp

⊤-is-set : is-set ⊤
⊤-is-set = dec-eq-is-set ⊤-has-dec-eq

cw-torus-skel : Skeleton {lzero} (S (S 0))

CWTorus : Type₀
CWTorus = ⟦ cw-torus-skel ⟧

α₁ : Bool → S⁰ → ⊤
α₁ _ _ = unit

X₁ = attached-skeleton (⊤ , ⊤-is-set) (Bool , Bool-is-set) α₁

α₂ : ⊤ → S¹ → (Attached α₁)
α₂ unit = Pushout-rec ψ ψ (cst idp)
    where
    ψ : ⊤ → Attached α₁
    ψ unit = PushoutGeneric.from-cc (inl unit)

X₂ = attached-skeleton X₁ (⊤ , ⊤-is-set) α₂

cw-torus-skel = X₂

max_stars_repo_name: maxdore/hott-morse

max_issues_repo_name: maxdore/hott-morse

max_forks_repo_name: maxdore/hott-morse


text:
{-# OPTIONS --without-K #-}
module equality.reasoning where

open import equality.core

module ≡-Reasoning {i} {X : Set i} where
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≡⟨_⟩_
  infix  1 begin_

  -- This seemingly unnecessary type is used to make it possible to
  -- infer arguments even if the underlying equality evaluates.

  data _IsRelatedTo_ (x y : X) : Set i where
    relTo : x ≡ y → x IsRelatedTo y

  begin_ : ∀ {x y} → x IsRelatedTo y → x ≡ y
  begin relTo p = p

  _≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≡⟨ p ⟩ relTo q = relTo (p · q)

  _∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo refl


text:
{-# OPTIONS --allow-unsolved-metas #-}

{-
  The moral of the story is best told by comparing RegularVsConstructedMoreSimpler and RegularVsConstructed-EnhancedReg:
  * aliased type constructors can lose information about their dependencies, leading to some inconvenience when using a function which takes those dependencies implicitly
  * expressing those constructors as records (instead of as aliases) averts the above inconvenience
  * the loss of information happens when the resultant type is made from projections on the dependencies, where only a proper subset of all the possible projections are used
  TODO: what if instead of projections, we use a function? (try one that's abstract, and one that case splits on arguments)
    - see ProjectedMorality ... so far it looks like it doesn't matter --- not sure why
  TODO: what if the argument type (the one that's losing information) were data instead of record?
    - see DataMorality ... weirdness!
-}

module AgdaFeaturePitfallInstanceResolution where

record Symmetry {B : Set₁} (_∼_ : B → B → Set) : Set₁ where
  field symmetry : ∀ {x y} → x ∼ y → y ∼ x

Property : Set → Set₁
Property A = A → Set

Extension : {A : Set} → Property A → Set
Extension P = ∀ f → P f

postulate PropertyEquivalence : ∀ {P : Set} → Property P → Property P → Set

record Regular : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : 𝔓 π₀

  open Σ public

  ExtensionProperty : ∀ (𝔒 : Set) → Set₁
  ExtensionProperty 𝔒 = Σ (Property 𝔒) Extension

  _≈_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  record Instance : Set where
    no-eta-equality

    postulate instance _ : ∀ {𝔒 : Set} → Symmetry (_≈_ {𝔒 = 𝔒})
    open Symmetry ⦃ … ⦄

    module Test {𝔒 : Set} where

      test1-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-fails P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-fails {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

  record Function : Set where
    no-eta-equality

    postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
    -- normalises to   : {𝔒 : Set} {x y : Σ (𝔒 → Set) (λ P → (f : 𝔒) → P f)} → PropertyEquivalence (π₀ x) (π₀ y) → PropertyEquivalence (π₀ y) (π₀ x)

    module Test {𝔒 : Set} where

      test1-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-fails P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-fails {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

record Revamped : Set where
  no-eta-equality

  record ExtensionProperty (𝔒 : Set) : Set₁ where
    constructor _,_
    field
      π₀ : Property 𝔒
      π₁ : Extension π₀

  open ExtensionProperty

  _≈_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  record Instance : Set where
    no-eta-equality

    postulate instance _ : ∀ {𝔒 : Set} → Symmetry (_≈_ {𝔒 = 𝔒})
    open Symmetry ⦃ … ⦄

    module Test {𝔒 : Set} where

      test1-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-fails P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-fails {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

  record Function : Set where
    no-eta-equality

    postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
    -- normalises to   : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → PropertyEquivalence (π₀ x) (π₀ y) → PropertyEquivalence (π₀ y) (π₀ x)

    module Test {𝔒 : Set} where

      test1-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-fails P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-fails : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-fails {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

record PostulatedExtensionProperty : Set where
  no-eta-equality

  postulate
    ExtensionProperty : Set → Set₁
    π₀ : {𝔒 : Set} → ExtensionProperty 𝔒 → Property 𝔒
    π₁ : {𝔒 : Set} → (P : ExtensionProperty 𝔒) → Extension (π₀ P)
    _,_ : {𝔒 : Set} → (π₀ : Property 𝔒) → Extension π₀ → ExtensionProperty 𝔒

  _≈_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  record Instance : Set where
    no-eta-equality

    postulate instance _ : ∀ {𝔒 : Set} → Symmetry (_≈_ {𝔒 = 𝔒})
    open Symmetry ⦃ … ⦄

    module Test {𝔒 : Set} where

      test1-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-works P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-inexpressible : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-inexpressible {P} {Q} P≈Q = {!!} -- symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-inexpressible : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-inexpressible {P} {Q} P≈Q = {!!} -- symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

  record Function : Set where
    no-eta-equality

    postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
    -- normalises to   : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → PropertyEquivalence (π₀ x) (π₀ y) → PropertyEquivalence (π₀ y) (π₀ x)

    module Test {𝔒 : Set} where

      test1-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-works P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-inexpressible : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-inexpressible {P} {Q} P≈Q = {!!} -- symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-inexpressible : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-inexpressible {P} {Q} P≈Q = {!!} -- symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

record Constructed : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : 𝔓 π₀

  open Σ public

  ExtensionProperty : Set → Set₁
  ExtensionProperty 𝔒 = Σ (Property 𝔒) Extension

  record _≈_ {𝔒 : Set} (P Q : ExtensionProperty 𝔒) : Set where
    constructor ∁
    field
      π₀ : PropertyEquivalence (π₀ P) (π₀ Q)

  record Instance : Set where
    no-eta-equality

    postulate instance _ : {𝔒 : Set} → Symmetry (_≈_ {𝔒 = 𝔒})
    open Symmetry ⦃ … ⦄

    module Test {𝔒 : Set} where

      test1-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-works P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-works {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

  record Function : Set where
    no-eta-equality

    postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
    -- normalises to   : {𝔒 : Set} {x y : Σ (𝔒 → Set) (λ P → (f : 𝔒) → P f)} → x ≈ y → y ≈ x

    module Test {𝔒 : Set} where

      test1-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test1-works P≈Q = symmetry P≈Q

      test2-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test2-works {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test3-works {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-works : {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
      test4-works {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

record RegularVsConstructed : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : 𝔓 π₀

  open Σ public

  ExtensionProperty : Set → Set₁
  ExtensionProperty 𝔒 = Σ (Property 𝔒) Extension

  record _≈R_ {𝔒 : Set} (P Q : ExtensionProperty 𝔒) : Set where
    constructor ∁
    field
      π₀ : PropertyEquivalence (π₀ P) (π₀ Q)

  _≈F_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈F_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  record Instance : Set where
    no-eta-equality

    postulate instance _ : {𝔒 : Set} → Symmetry (_≈R_ {𝔒 = 𝔒})
    postulate instance _ : {𝔒 : Set} → Symmetry (_≈F_ {𝔒 = 𝔒})
    open Symmetry ⦃ … ⦄

    module Test {𝔒 : Set} where

      test1-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test1-worksR P≈Q = symmetry P≈Q

      test2-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test2-worksR {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test3-worksR {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test4-worksR {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

      test1-failsF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test1-failsF P≈Q = symmetry P≈Q

      test2-worksF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test2-worksF {P} {Q} P≈Q = symmetry {x = P} {y = Q} P≈Q

      test3-failsF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test3-failsF {P} {Q} P≈Q = symmetry {x = _ , _} {y = _ , _} P≈Q

      test4-worksF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test4-worksF {P} {Q} P≈Q = symmetry {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

  record Function : Set where
    no-eta-equality

    postulate symmetryR : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈R y → y ≈R x
    postulate symmetryF : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈F y → y ≈F x

    module Test {𝔒 : Set} where

      test1-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test1-worksR P≈Q = symmetryR P≈Q

      test2-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test2-worksR {P} {Q} P≈Q = symmetryR {x = P} {y = Q} P≈Q

      test3-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test3-worksR {P} {Q} P≈Q = symmetryR {x = _ , _} {y = _ , _} P≈Q

      test4-worksR : {P Q : ExtensionProperty 𝔒} → P ≈R Q → Q ≈R P
      test4-worksR {P} {Q} P≈Q = symmetryR {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

      test1-failsF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test1-failsF P≈Q = symmetryF P≈Q

      test2-worksF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test2-worksF {P} {Q} P≈Q = symmetryF {x = P} {y = Q} P≈Q

      test3-failsF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test3-failsF {P} {Q} P≈Q = symmetryF {x = _ , _} {y = _ , _} P≈Q

      test4-worksF : {P Q : ExtensionProperty 𝔒} → P ≈F Q → Q ≈F P
      test4-worksF {P} {Q} P≈Q = symmetryF {x = _ , π₁ P} {y = _ , π₁ Q} P≈Q

record RegularVsConstructedSimpler : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : 𝔓 π₀

  open Σ public

  postulate Prop : Set₁
  postulate Ext : Prop → Set
  postulate PropEq : Prop → Set

  ExtProp : Set₁
  ExtProp = Σ Prop Ext

  record ≈C_ (P : ExtProp) : Set where
    constructor ∁
    field
      π₀ : PropEq (π₀ P)

  ≈R_ : ExtProp → Set
  ≈R_ P = PropEq (π₀ P)

  record Instance : Set where
    no-eta-equality

    record Class {B : Set₁} (∼_ : B → Set) : Set₁ where
      field foo : ∀ {x} → ∼ x → Set
    open Class ⦃ … ⦄

    postulate instance _ : Class ≈C_
    postulate instance _ : Class ≈R_

    module Test where

      test1-worksC : {P : ExtProp} → ≈C P → Set
      test1-worksC P≈Q = foo P≈Q

      test2-worksC : {P : ExtProp} → ≈C P → Set
      test2-worksC {P} P≈Q = foo {x = P} P≈Q

      test3-worksC : {P : ExtProp} → ≈C P → Set
      test3-worksC {P} P≈Q = foo {x = _ , _} P≈Q

      test4-worksC : {P : ExtProp} → ≈C P → Set
      test4-worksC {P} P≈Q = foo {x = _ , π₁ P} P≈Q

      test1-failsR : {P : ExtProp} → ≈R P → Set
      test1-failsR P≈Q = foo P≈Q

      test2-worksR : {P : ExtProp} → ≈R P → Set
      test2-worksR {P} P≈Q = foo {x = P} P≈Q

      test3-failsR : {P : ExtProp} → ≈R P → Set
      test3-failsR {P} P≈Q = foo {x = _ , _} P≈Q

      test4-worksR : {P : ExtProp} → ≈R P → Set
      test4-worksR {P} P≈Q = foo {x = _ , π₁ P} P≈Q

  record Function : Set where
    no-eta-equality

    postulate fooC : {x : ExtProp} → ≈C x → Set
    postulate fooR : {x : ExtProp} → ≈R x → Set

    module Test where

      test1-worksC : {P : ExtProp} → ≈C P → Set
      test1-worksC P≈Q = fooC P≈Q

      test2-worksC : {P : ExtProp} → ≈C P → Set
      test2-worksC {P} P≈Q = fooC {x = P} P≈Q

      test3-worksC : {P : ExtProp} → ≈C P → Set
      test3-worksC {P} P≈Q = fooC {x = _ , _} P≈Q

      test4-worksC : {P : ExtProp} → ≈C P → Set
      test4-worksC {P} P≈Q = fooC {x = _ , π₁ P} P≈Q

      test1-failsR : {P : ExtProp} → ≈R P → Set
      test1-failsR P≈Q = fooR P≈Q

      test2-worksR : {P : ExtProp} → ≈R P → Set
      test2-worksR {P} P≈Q = fooR {x = P} P≈Q

      test3-failsR : {P : ExtProp} → ≈R P → Set
      test3-failsR {P} P≈Q = fooR {x = _ , _} P≈Q

      test4-worksR : {P : ExtProp} → ≈R P → Set
      test4-worksR {P} P≈Q = fooR {x = _ , π₁ P} P≈Q

record RegularVsConstructedMoreSimpler : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : Set

  open Σ

  postulate Prop : Set₁
  postulate Ext : Prop → Set
  postulate PropEq : Prop → Set

  ExtProp : Set₁
  ExtProp = Σ Prop Ext

  Reg : ExtProp → Set
  Reg P = PropEq (π₀ P)

  record Con (P : ExtProp) : Set where
    constructor ∁
    field
      π₀ : Reg P

  module Instance where

    record Class {B : Set₁} (F : B → Set) : Set₁ where
      field foo : ∀ {x} → F x → Set
    open Class ⦃ … ⦄

    postulate instance _ : Class Reg
    postulate instance _ : Class Con
    postulate instance _ : Class Ext
    postulate instance _ : Class PropEq

    test1-failsR : {P : ExtProp} → Reg P → Set
    test1-failsR P≈Q = foo P≈Q

    test2-worksR : {P : ExtProp} → Reg P → Set
    test2-worksR {P} P≈Q = foo {x = P} P≈Q

    test3-failsR : {P : ExtProp} → Reg P → Set
    test3-failsR {P} P≈Q = foo {x = _ , _} P≈Q

    test4-worksR : {P : ExtProp} → Reg P → Set
    test4-worksR {P} P≈Q = foo {x = _ , π₁ P} P≈Q

    test1-worksC : {P : ExtProp} → Con P → Set
    test1-worksC P≈Q = foo P≈Q

    test2-worksC : {P : ExtProp} → Con P → Set
    test2-worksC {P} P≈Q = foo {x = P} P≈Q

    test3-worksC : {P : ExtProp} → Con P → Set
    test3-worksC {P} P≈Q = foo {x = _ , _} P≈Q

    test4-worksC : {P : ExtProp} → Con P → Set
    test4-worksC {P} P≈Q = foo {x = _ , π₁ P} P≈Q

  module Function where

    postulate fooR : {x : ExtProp} → Reg x → Set
    postulate fooC : {x : ExtProp} → Con x → Set

    test1-failsR : {P : ExtProp} → Reg P → Set
    test1-failsR P≈Q = fooR P≈Q

    test2-worksR : {P : ExtProp} → Reg P → Set
    test2-worksR {P} P≈Q = fooR {x = P} P≈Q

    test3-failsR : {P : ExtProp} → Reg P → Set
    test3-failsR {P} P≈Q = fooR {x = _ , _} P≈Q

    test4-worksR : {P : ExtProp} → Reg P → Set
    test4-worksR {P} P≈Q = fooR {x = _ , π₁ P} P≈Q

    test1-worksC : {P : ExtProp} → Con P → Set
    test1-worksC P≈Q = fooC P≈Q

    test2-worksC : {P : ExtProp} → Con P → Set
    test2-worksC {P} P≈Q = fooC {x = P} P≈Q

    test3-worksC : {P : ExtProp} → Con P → Set
    test3-worksC {P} P≈Q = fooC {x = _ , _} P≈Q

    test4-worksC : {P : ExtProp} → Con P → Set
    test4-worksC {P} P≈Q = fooC {x = _ , π₁ P} P≈Q

module RegularVsConstructed-EnhancedReg where

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : Set

  open Σ

  postulate Prop : Set₁
  postulate Ext : Prop → Set
  postulate PropEq : Prop → Set → Set

  ExtProp : Set₁
  ExtProp = Σ Prop Ext

  Reg : ExtProp → Set
  Reg P = PropEq (π₀ P) (π₁ P)

  record Con (P : ExtProp) : Set where
    constructor ∁
    field
      π₀ : Reg P

  module Instance where

    record Class {B : Set₁} (F : B → Set) : Set₁ where
      field foo : ∀ {x} → F x → Set
    open Class ⦃ … ⦄

    postulate instance _ : Class Reg
    postulate instance _ : Class Con
    postulate instance _ : Class Ext

    test1-failsR : {P : ExtProp} → Reg P → Set
    test1-failsR P≈Q = foo P≈Q

    test2-worksR : {P : ExtProp} → Reg P → Set
    test2-worksR {P} P≈Q = foo {x = P} P≈Q

    test3-failsR : {P : ExtProp} → Reg P → Set
    test3-failsR {P} P≈Q = foo {x = _ , _} P≈Q

    test4-worksR : {P : ExtProp} → Reg P → Set
    test4-worksR {P} P≈Q = foo {x = _ , π₁ P} P≈Q

    test1-worksC : {P : ExtProp} → Con P → Set
    test1-worksC P≈Q = foo P≈Q

    test2-worksC : {P : ExtProp} → Con P → Set
    test2-worksC {P} P≈Q = foo {x = P} P≈Q

    test3-worksC : {P : ExtProp} → Con P → Set
    test3-worksC {P} P≈Q = foo {x = _ , _} P≈Q

    test4-worksC : {P : ExtProp} → Con P → Set
    test4-worksC {P} P≈Q = foo {x = _ , π₁ P} P≈Q

  module Function where

    postulate fooR : {x : ExtProp} → Reg x → Set
    postulate fooC : {x : ExtProp} → Con x → Set

    test1-failsR : {P : ExtProp} → Reg P → Set
    test1-failsR P≈Q = fooR P≈Q

    test2-worksR : {P : ExtProp} → Reg P → Set
    test2-worksR {P} P≈Q = fooR {x = P} P≈Q

    test3-failsR : {P : ExtProp} → Reg P → Set
    test3-failsR {P} P≈Q = fooR {x = _ , _} P≈Q

    test4-worksR : {P : ExtProp} → Reg P → Set
    test4-worksR {P} P≈Q = fooR {x = _ , π₁ P} P≈Q

    test1-worksC : {P : ExtProp} → Con P → Set
    test1-worksC P≈Q = fooC P≈Q

    test2-worksC : {P : ExtProp} → Con P → Set
    test2-worksC {P} P≈Q = fooC {x = P} P≈Q

    test3-worksC : {P : ExtProp} → Con P → Set
    test3-worksC {P} P≈Q = fooC {x = _ , _} P≈Q

    test4-worksC : {P : ExtProp} → Con P → Set
    test4-worksC {P} P≈Q = fooC {x = _ , π₁ P} P≈Q

record ProjectedMorality : Set where
  no-eta-equality

  infixr 5 _,_
  record Σ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) : Set₁ where
    constructor _,_
    field
      π₀ : 𝔒
      π₁ : Set

  open Σ

  postulate Prop : Set₁
  postulate Ext : Prop → Set
  postulate PropEq : Prop → Set

  Reg : Σ Prop Ext → Set
  Reg P = PropEq (π₀ P)

  postulate bar : ∀ {𝔒 : Set₁} → 𝔒 → 𝔒
  postulate qux : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → Σ 𝔒 𝔓
  postulate fake-π₀ : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → 𝔒

  abstract

    abstracted-π₀ : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → 𝔒
    abstracted-π₀ x = π₀ x

  Reg-using-abstracted-projection : Σ Prop Ext → Set
  Reg-using-abstracted-projection (P0 , P1) = PropEq (abstracted-π₀ {𝔒 = Prop} {𝔓 = Ext} (P0 , P1))

  Reg-using-q : Σ Prop Ext → Set
  Reg-using-q x = PropEq (π₀ (qux x))

  Reg-using-fake-π₀ : Σ Prop Ext → Set
  Reg-using-fake-π₀ x = PropEq (fake-π₀ x)

  record Con (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg P

  record Con-using-abstracted-projection (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-abstracted-projection P

  record Con-using-q (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-q P

  record Con-using-fake-π₀ (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-fake-π₀ P

  record Class {B : Set₁} (F : B → Set) : Set₁ where
    field foo : ∀ {x} → F x → Set
  open Class ⦃ … ⦄

  postulate instance _ : Class Reg
  postulate instance _ : Class Reg-using-abstracted-projection
  postulate instance _ : Class Reg-using-q
  postulate instance _ : Class Reg-using-fake-π₀
  postulate instance _ : Class Con
  postulate instance _ : Class Con-using-abstracted-projection
  postulate instance _ : Class Con-using-q
  postulate instance _ : Class Con-using-fake-π₀

  test1-failsR : ∀ {P} → Reg P → Set
  test1-failsR = foo

  test1-failsRap : ∀ {P} → Reg-using-abstracted-projection P → Set
  test1-failsRap = foo

  test1-failsRq : ∀ {P} → Reg-using-q P → Set
  test1-failsRq = foo

  test1-failsRf : ∀ {P} → Reg-using-fake-π₀ P → Set
  test1-failsRf = foo

  test1-worksC : ∀ {P} → Con P → Set
  test1-worksC = foo

  test1-worksCap : ∀ {P} → Con-using-abstracted-projection P → Set
  test1-worksCap = foo

  test1-worksCq : ∀ {P} → Con-using-q P → Set
  test1-worksCq = foo

  test1-worksCf : ∀ {P} → Con-using-fake-π₀ P → Set
  test1-worksCf = foo

record DataMorality : Set where
  no-eta-equality

  module _ (𝔒 : Set₁) (𝔓 : 𝔒 → Set) where

    data Σ : Set₁ where
      _,_ : 𝔒 → Set → Σ

  module _ {𝔒 : Set₁} {𝔓 : 𝔒 → Set} where

    dπ₀ : Σ _ 𝔓 → 𝔒
    dπ₀ (x , _) = x

    dπ₁ : Σ _ 𝔓 → Set
    dπ₁ (_ , y) = y

  postulate Prop : Set₁
  postulate Ext : Prop → Set
  postulate PropEq : Prop → Set

  Reg : Σ Prop Ext → Set
  Reg P = PropEq (dπ₀ P)

  postulate bar : ∀ {𝔒 : Set₁} → 𝔒 → 𝔒
  postulate qux : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → Σ 𝔒 𝔓
  postulate fake-π₀ : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → 𝔒

  abstract

    abstracted-π₀ : ∀ {𝔒} {𝔓 : 𝔒 → Set} → Σ 𝔒 𝔓 → 𝔒
    abstracted-π₀ x = dπ₀ x

  Reg-using-abstracted-projection : Σ Prop Ext → Set
  Reg-using-abstracted-projection (P0 , P1) = PropEq (abstracted-π₀ {𝔒 = Prop} {𝔓 = Ext} (P0 , P1))

  Reg-using-q : Σ Prop Ext → Set
  Reg-using-q x = PropEq (dπ₀ (qux x))

  Reg-using-fake-π₀ : Σ Prop Ext → Set
  Reg-using-fake-π₀ x = PropEq (fake-π₀ x)

  record Con (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg P

  record Con-using-abstracted-projection (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-abstracted-projection P

  record Con-using-q (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-q P

  record Con-using-fake-π₀ (P : Σ Prop Ext) : Set where
    constructor ∁
    field
      π₀ : Reg-using-fake-π₀ P

  record Class {B : Set₁} (F : B → Set) : Set₁ where
    field foo : ∀ {x} → F x → Set
  open Class ⦃ … ⦄

  postulate instance _ : Class Reg
  postulate instance _ : Class Reg-using-abstracted-projection
  postulate instance _ : Class Reg-using-q
  postulate instance _ : Class Reg-using-fake-π₀
  postulate instance _ : Class Con
  postulate instance _ : Class Con-using-abstracted-projection
  postulate instance _ : Class Con-using-q
  postulate instance _ : Class Con-using-fake-π₀

  test1-failsR : ∀ {P} → Reg P → Set
  test1-failsR = foo

  test1-failsRap : ∀ {P} → Reg-using-abstracted-projection P → Set
  test1-failsRap = foo -- woah, it actually works. why?

  test1-failsRq : ∀ {P} → Reg-using-q P → Set
  test1-failsRq = foo -- NB this doesn't fail if instance of Class Reg is excluded

  test1-failsRf : ∀ {P} → Reg-using-fake-π₀ P → Set
  test1-failsRf = foo -- NB this doesn't fail if instance of Class Reg is excluded

  test1-worksC : ∀ {P} → Con P → Set
  test1-worksC = foo

  test1-worksCap : ∀ {P} → Con-using-abstracted-projection P → Set
  test1-worksCap = foo

  test1-worksCq : ∀ {P} → Con-using-q P → Set
  test1-worksCq = foo

  test1-worksCf : ∀ {P} → Con-using-fake-π₀ P → Set
  test1-worksCf = foo

module RevampedSimpleFailure where

  record ExtensionProperty (𝔒 : Set) : Set₁ where
    field
      π₀ : Property 𝔒
      π₁ : Extension π₀

  open ExtensionProperty

  _≈_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
  -- normalises to   : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → PropertyEquivalence (π₀ x) (π₀ y) → PropertyEquivalence (π₀ y) (π₀ x)

  test-fails : {𝔒 : Set} {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
  test-fails P≈Q = symmetry P≈Q

module PostulatedExtensionPropertySimpleSuccess where

  postulate
    ExtensionProperty : Set → Set₁
    π₀ : {𝔒 : Set} → ExtensionProperty 𝔒 → Property 𝔒

  _≈_ : {𝔒 : Set} → ExtensionProperty 𝔒 → ExtensionProperty 𝔒 → Set
  _≈_ P Q = PropertyEquivalence (π₀ P) (π₀ Q)

  postulate symmetry : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → x ≈ y → y ≈ x
  -- normalises to   : ∀ {𝔒} {x y : ExtensionProperty 𝔒} → PropertyEquivalence (π₀ {𝔒} x) (π₀ {𝔒} y) → PropertyEquivalence (π₀ {𝔒} y) (π₀ {𝔒} x)

  test-works : {𝔒 : Set} {P Q : ExtensionProperty 𝔒} → P ≈ Q → Q ≈ P
  test-works P≈Q = symmetry P≈Q

module RevampedVerySimpleFailure where

  -- was PropertyEquivalence : ∀ {P : Set} → Property P → Property P → Set
  postulate _∼_ : Set → Set → Set

  record ExtensionProperty : Set₁ where
    field
      π₀ : Set -- was Property 𝔒
      π₁ : Set -- was Extension π₀

  open ExtensionProperty

  postulate symmetry : ∀ {x y : ExtensionProperty} → π₀ x ∼ π₀ y → π₀ y ∼ π₀ x

  postulate x y : ExtensionProperty

  test-fails : π₀ x ∼ π₀ y → π₀ y ∼ π₀ x
  test-fails = symmetry

module PostulatedExtensionPropertyVerySimpleSuccess where

  postulate _∼_ : Set → Set → Set

  postulate
    ExtensionProperty : Set₁
    π₀ : ExtensionProperty → Set

  postulate symmetry : ∀ {x y : ExtensionProperty} → π₀ x ∼ π₀ y → π₀ y ∼ π₀ x

  postulate x y : ExtensionProperty

  test-works : π₀ x ∼ π₀ y → π₀ y ∼ π₀ x
  test-works P≈Q = symmetry P≈Q

module RevampedEvenSimplerFailure where

  -- was _∼_, which was PropertyEquivalence
  postulate F : Set → Set

  record ExtensionProperty : Set₁ where
    field
      π₀ : Set
      π₁ : Set

  open ExtensionProperty

  postulate symmetry : ∀ {x : ExtensionProperty} → F (π₀ x) → Set

  postulate x : ExtensionProperty
  postulate Fpx : F (π₀ x)

  test-fails1 : Set
  test-fails1 = symmetry Fpx

  test-fails2 : Set
  test-fails2 = symmetry {x = record { π₀ = π₀ x ; π₁ = _}} Fpx

  test-works-arbitrarily : Set
  test-works-arbitrarily = symmetry {x = record { π₀ = π₀ x ; π₁ = F (F (π₁ x)) }} Fpx

module PostulatedExtensionPropertyEvenSimplerSuccess where

  postulate F : Set → Set

  postulate
    ExtensionProperty : Set₁
    π₀ : ExtensionProperty → Set

  postulate symmetry : ∀ {x : ExtensionProperty} → F (π₀ x) → Set

  postulate x : ExtensionProperty
  postulate Fpx : F (π₀ x)

  test-works1 : Set
  test-works1 = symmetry Fpx

  test-works2 : Set
  test-works2 = symmetry {x = x} Fpx

module RevampedEvenSimplerFailureClassified where

  postulate F : Set → Set

  record ExtensionProperty : Set₁ where
    field
      π₀ : Set
      π₁ : Set

  open ExtensionProperty

  record Symmetry' (R : Set → Set) : Set₁ where
    field symmetry : ∀ {x : ExtensionProperty} → R (π₀ x) → Set
  open Symmetry' ⦃ … ⦄

  postulate instance _ : Symmetry' F

  postulate x : ExtensionProperty
  postulate Fpx : F (π₀ x)

  test-fails1 : Set
  test-fails1 = symmetry Fpx

  test-fails2 : Set
  test-fails2 = symmetry {x = record { π₀ = π₀ x ; π₁ = _}} Fpx

  test-works-arbitrarily : Set
  test-works-arbitrarily = symmetry {x = record { π₀ = π₀ x ; π₁ = F (F (π₁ x)) }} Fpx

module PostulatedExtensionPropertyEvenSimplerSuccessClassified where

  postulate F : Set → Set

  postulate
    ExtensionProperty : Set₁
    π₀ : ExtensionProperty → Set

  record Symmetry' (R : Set → Set) : Set₁ where
    field symmetry : ∀ {x : ExtensionProperty} → R (π₀ x) → Set
  open Symmetry' ⦃ … ⦄

  postulate instance _ : Symmetry' F

  postulate x : ExtensionProperty
  postulate Fpx : F (π₀ x)

  test-works1 : Set
  test-works1 = symmetry Fpx

  test-works2 : Set
  test-works2 = symmetry {x = x} Fpx

module RevampedVsPostulated where

  record R : Set₁ where
    field
      f1 : Set
      f2 : Set

  open R

  postulate fooR : ∀ {x : R} → f1 x → Set

  postulate r : R
  postulate f1r : f1 r

  test-fails1 : Set
  test-fails1 = fooR f1r

  postulate
    S : Set₁
    g1 : S → Set

  postulate fooS : ∀ {x : S} → g1 x → Set

  postulate s : S
  postulate g1s : g1 s

  test-works1 : Set
  test-works1 = fooS g1s