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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.RedSteps
open import Definition.Typed.Reduction
import Definition.Typed.Weakening as W
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance

open import Tools.Product
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- Conversion of syntactic reduction closures.
convRed:*: : ∀ {t u A B Γ l} → Γ ⊢ t :⇒*: u ∷ A ^ l → Γ ⊢ A ≡ B ^ [ ! , l ] → Γ ⊢ t :⇒*: u ∷ B ^ l
convRed:*: [[ ⊢t , ⊢u , d ]] A≡B = [[ conv ⊢t  A≡B , conv ⊢u  A≡B , conv* d  A≡B ]]

-- helper functions for the universe
convTermTUniv :  ∀ {Γ A B t l l' r ll l< d r' ll' l<' el' d'}
                      (er : r PE.≡ r') (ellll' : ll PE.≡ ll') →
                      Γ ⊩⟨ l ⟩  t ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r ll l< PE.refl d) →
                      Γ ⊩⟨ l' ⟩ t ∷ B ^ [ ! , next ll ] / Uᵣ (Uᵣ r' ll' l<' el' d')
convTermTUniv {l< = l<} {l<' = l<'} {d' = d'} er ellll' (Uₜ K d typeK K≡K [t]) =
    let dd = PE.subst (λ x → _ ⊢ _ :⇒*: Univ x _ ^ _) (PE.sym er) (PE.subst (λ x → _ ⊢ _ :⇒*: Univ _ x ^ [ ! , next x ]) (PE.sym ellll') d') in
    reduction-irrelevant-Univ {l< = l<} {l<' = l<'} {el = PE.refl} {D = dd} {D' = d'} er (Uₜ K d typeK K≡K [t])

convEqTermTUniv : ∀ {Γ A B t u l r ll l< d dd} →
                    Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r ll l< PE.refl d) →
                    Γ ⊩⟨ l ⟩ t ≡ u ∷ B ^ [ ! , next ll ] / Uᵣ (Uᵣ r ll l< PE.refl dd)
convEqTermTUniv {l = ι ¹} {r = r} {⁰} (Uₜ₌ [t] [u] A≡B [t≡u]) =
                   Uₜ₌ (convTermTUniv PE.refl PE.refl [t]) (convTermTUniv PE.refl PE.refl [u]) A≡B [t≡u]
convEqTermTUniv {l = ∞} {r = r} {¹} (Uₜ₌ [t] [u] A≡B [t≡u]) =
                   Uₜ₌ (convTermTUniv PE.refl PE.refl [t]) (convTermTUniv PE.refl PE.refl [u]) A≡B [t≡u]

mutual
  -- Helper function for conversion of terms converting from left to right.

  convTermT₁ : ∀ {Γ A B r t l l′} {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r}
            → ShapeView Γ l l′ A B r r [A] [B]
            → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
            → Γ ⊩⟨ l ⟩  t ∷ A ^ r / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B ^ r / [B]

  convTermT₁ (ℕᵥ D D′) A≡B t = t
  convTermT₁ (Emptyᵥ D D′) A≡B t = t

  convTermT₁ {r = [ ! , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M) (neₜ k d (neNfₜ neK₂ ⊢k k≡k)) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in  neₜ k (convRed:*: d K≡K₁)
              (neNfₜ neK₂ (conv ⊢k K≡K₁) (~-conv k≡k K≡K₁))
  convTermT₁ {r = [ % , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
             (neₜ d) = let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x ^ _)
                                          (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                                          (≅-eq (~-to-≅ K≡M))
                       in neₜ (conv d (reduction  (red D) (red D₁) (ne neK) (ne neK₁) K≡K₁))
  convTermT₁ {Γ = Γ} {r = [ ! , ι ll ]} (Πᵥ (Πᵣ 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 d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , lΠ≡lΠ₁ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ ! , ι ll ]) (PE.sym ΠF₁G₁≡ΠF′G′)
                             (≅-eq A≡B)
    in  Πₜ f (convRed:*: d ΠFG≡ΠF₁G₁) funcF (≅-conv f≡f ΠFG≡ΠF₁G₁)
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₂′ PE.refl (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₂′ PE.refl (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₂′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a]₁)
                                           ([G≡G′] [ρ] ⊢Δ [a]₁)
              in  convEqTerm₁′ PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁]
                              ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
          (λ {ρ} [ρ] ⊢Δ [a] →
             let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                          ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                 [a]₁ = convTerm₂′ PE.refl (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                 [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                   (PE.sym G₁≡G′))
                                          ([G] [ρ] ⊢Δ [a]₁)
                                          ([G≡G′] [ρ] ⊢Δ [a]₁)
             in  convTerm₁′ PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a]) [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₁ {Γ = Γ} {r = [ % , ι ll ]} (Πᵥ (Πᵣ 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′])
             d = 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′
                     ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ % , ι ll ]) (PE.sym ΠF₁G₁≡ΠF′G′)
                                          (≅-eq A≡B)
                 in conv d ΠFG≡ΠF₁G₁
  convTermT₁ {Γ = Γ} {r = [ % , ll ]} (∃ᵥ (∃ᵣ 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′])
             d = let ∃F₁G₁≡∃F′G′   = whrDet* (red D₁ , ∃ₙ) (D′ , ∃ₙ)
                     F₁≡F′ , G₁≡G′ = ∃-PE-injectivity ∃F₁G₁≡∃F′G′
                     ∃FG≡∃F₁G₁ = PE.subst (λ x → Γ ⊢ ∃ F ▹ G ≡ x ^ [ % , ll ]) (PE.sym ∃F₁G₁≡∃F′G′)
                                          (≅-eq A≡B)
                 in conv d ∃FG≡∃F₁G₁
  convTermT₁ (Uᵥ (Uᵣ r l l< PE.refl d) (Uᵣ r' l' l<' el' d')) A≡B X =
    let U≡U   = whrDet* (A≡B , Uₙ) (red d' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity U≡U
    in convTermTUniv r≡r l≡l X
  convTermT₁ (emb⁰¹ X) A≡B t = convTermT₁ X A≡B t
  convTermT₁ (emb¹⁰ X) A≡B t = convTermT₁ X A≡B t
  convTermT₁ (emb¹∞ X) A≡B t = convTermT₁ X A≡B t
  convTermT₁ (emb∞¹ X) A≡B t = convTermT₁ X A≡B t

  -- Helper function for conversion of terms converting from right to left.
  convTermT₂ : ∀ {l l′ Γ A B r t} {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r}
           → ShapeView Γ l l′ A B r r [A] [B]
           → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
           → Γ ⊩⟨ l′ ⟩ t ∷ B ^ r / [B]
           → Γ ⊩⟨ l ⟩  t ∷ A ^ r / [A]
  convTermT₂ (ℕᵥ D D′) A≡B t = t
  convTermT₂ (Emptyᵥ D D′) A≡B t = t
  convTermT₂ {r = [ ! , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
             (neₜ k d (neNfₜ neK₂ ⊢k k≡k)) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _ ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in  neₜ k (convRed:*: d K₁≡K)
            (neNfₜ neK₂ (conv ⊢k K₁≡K) (~-conv k≡k K₁≡K))
  convTermT₂ {r = [ % , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
             (neₜ d) = let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _ ^ _)
                                           (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                                           (sym (≅-eq (~-to-≅ K≡M)))
                       in neₜ (conv d (reduction  (red D₁) (red D) (ne neK₁) (ne neK) K₁≡K))
  convTermT₂ {Γ = Γ} {r = [ ! , ι ll ]} (Πᵥ (Πᵣ 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 d funcF f≡f [f] [f]₁) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , lΠ≡lΠ₁ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ ! , ι ll ])
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ f (convRed:*: d (sym ΠFG≡ΠF₁G₁)) funcF (≅-conv f≡f (sym ΠFG≡ΠF₁G₁))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [b]₁ = convTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [b]
                  [a≡b]₁ = convEqTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a≡b]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convEqTerm₂′ PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                              [G≡G₁] ([f] [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                           ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                  [a]₁ = convTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                  [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                    (PE.sym G₁≡G′))
                                           ([G] [ρ] ⊢Δ [a])
                                           ([G≡G′] [ρ] ⊢Δ [a])
              in  convTerm₂′ PE.refl PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                            [G≡G₁] ([f]₁ [ρ] ⊢Δ [a]₁))
  convTermT₂ {Γ = Γ} {r = [ % , ι ll ]} (Πᵥ (Πᵣ 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′])
             d = 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′
                     ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ % , ι ll ])
                                          (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
                 in  conv d (sym ΠFG≡ΠF₁G₁)
  convTermT₂ {Γ = Γ} {r = [ % , ll ]} (∃ᵥ (∃ᵣ 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′])
             d = let ∃F₁G₁≡∃F′G′   = whrDet* (red D₁ , ∃ₙ) (D′ , ∃ₙ)
                     F₁≡F′ ,  G₁≡G′ = ∃-PE-injectivity ∃F₁G₁≡∃F′G′
                     ∃FG≡∃F₁G₁ = PE.subst (λ x → Γ ⊢ ∃ F ▹ G ≡ x ^ [ % , ll ])
                                          (PE.sym ∃F₁G₁≡∃F′G′) (≅-eq A≡B)
                 in  conv d (sym ∃FG≡∃F₁G₁)
  convTermT₂ (Uᵥ (Uᵣ r l l< el d) (Uᵣ r' l' l<' PE.refl d')) A≡B X =
    let U≡U   = whrDet* (A≡B , Uₙ) (red d' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity U≡U
    in convTermTUniv (PE.sym r≡r) (PE.sym l≡l) X
  convTermT₂ (emb⁰¹ X) A≡B t = convTermT₂ X A≡B t
  convTermT₂ (emb¹⁰ X) A≡B t = convTermT₂ X A≡B t
  convTermT₂ (emb¹∞ X) A≡B t = convTermT₂ X A≡B t
  convTermT₂ (emb∞¹ X) A≡B t = convTermT₂ X A≡B t

  -- Conversion of terms converting from left to right.
  convTerm₁ : ∀ {Γ A B r ll t l l′} ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r , ll ])
            → Γ ⊩⟨ l ⟩  A ≡ B ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l ⟩  t ∷ A ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B ^ [ r , ll ] / [B]
  convTerm₁ [A] [B] A≡B t = convTermT₁ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from left to right. with PE
  convTerm₁′ : ∀ {Γ A B r r' ll ll' t l l′} (eq : r PE.≡ r') (eql : ll PE.≡ ll')
                 ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ])
            → Γ ⊩⟨ l ⟩  A ≡ B ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l ⟩  t ∷ A ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l′ ⟩ t ∷ B ^ [ r' , ll' ] / [B]
  convTerm₁′ PE.refl PE.refl [A] [B] A≡B t = convTerm₁ [A] [B] A≡B t

  -- Conversion of terms converting from right to left.
  convTerm₂ : ∀ {Γ A B r t l l′} ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([B] : Γ ⊩⟨ l′ ⟩ B ^ r)
          → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B ^ r / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A ^ r / [A]
  convTerm₂ [A] [B] A≡B t = convTermT₂ (goodCases [A] [B] A≡B) A≡B t

  -- Conversion of terms converting from right to left
  -- with some propsitionally equal types.
  convTerm₂′ : ∀ {Γ A r r' ll ll' B B′ t l l′} → B PE.≡ B′ → r PE.≡ r' → ll PE.≡ ll'
          → ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ] ) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ])
          → Γ ⊩⟨ l ⟩  A ≡ B′ ^ [ r , ll ] / [A]
          → Γ ⊩⟨ l′ ⟩ t ∷ B ^ [ r' , ll' ] / [B]
          → Γ ⊩⟨ l ⟩  t ∷ A ^ [ r , ll ] / [A]
  convTerm₂′ PE.refl PE.refl PE.refl [A] [B] A≡B t = convTerm₂ [A] [B] A≡B t

  -- Helper function for conversion of term equality converting from left to right.
  convEqTermT₁ : ∀ {l l′ Γ A B r t u} {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r}
               → ShapeView Γ l l′ A B r r [A] [B]
               → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
               → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ r / [A]
               → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ r / [B]
  convEqTermT₁ (ℕᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₁ (Emptyᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₁ {r = [ ! , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m)) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in  neₜ₌ k m (convRed:*: d K≡K₁)
                 (convRed:*: d′ K≡K₁)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K≡K₁))
  convEqTermT₁ {r = [ % , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ d d′) =
    let K≡K₁ = PE.subst (λ x → _ ⊢ _ ≡ x ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (≅-eq (~-to-≅ K≡M))
    in neₜ₌ (conv d (reduction  (red D) (red D₁) (ne neK) (ne neK₁) K≡K₁))
            (conv d′ (reduction  (red D) (red D₁) (ne neK) (ne neK₁) K≡K₁))
  convEqTermT₁ {Γ = Γ} {r = [ ! , ι ll ]} (Πᵥ (Πᵣ rF lF lG lF≤ lG≤  F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                           (Πᵣ rF₁ lF₁ lG₁ 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 d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Πᵣ′ rF₁ lF₁ lG₁ lF₁≤ lG₁≤ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ ! , ι ll ])
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d ΠFG≡ΠF₁G₁) (convRed:*: d′ ΠFG≡ΠF₁G₁)
            funcF funcG (≅-conv t≡u ΠFG≡ΠF₁G₁)
            (convTerm₁ [A] [B] [A≡B] [t]) (convTerm₁ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , lΠ≡lΠ₁ = Π-PE-injectivity (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₂′ PE.refl (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a]₁)
                                            ([G≡G′] [ρ] ⊢Δ [a]₁)
               in  convEqTerm₁′ PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]₁) ([G]₁ [ρ] ⊢Δ [a])
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₁ {Γ = Γ} {r = [ % , ι ll ]} (Πᵥ (Πᵣ 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′])
               (d , d′) = let ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
                              ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ % , ι ll ])
                                                   (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
                          in conv d ΠFG≡ΠF₁G₁ , conv d′ ΠFG≡ΠF₁G₁
  convEqTermT₁ {Γ = Γ} {r = [ % , ll ]} (∃ᵥ (∃ᵣ 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′])
               (d , d′) = let ∃F₁G₁≡∃F′G′ = whrDet* (red D₁ , ∃ₙ) (D′ , ∃ₙ)
                              ∃FG≡∃F₁G₁ = PE.subst (λ x → Γ ⊢ ∃ F ▹ G ≡ x ^ [ % , ll ])
                                                   (PE.sym ∃F₁G₁≡∃F′G′) (≅-eq A≡B)
                          in (conv d ∃FG≡∃F₁G₁) , conv d′ ∃FG≡∃F₁G₁
  convEqTermT₁ (Uᵥ (Uᵣ r ll l< PE.refl d) (Uᵣ r' ll' l<' el' d')) A≡B X =
    let U≡U   = whrDet* (A≡B , Uₙ) (red d' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity U≡U
        dd = PE.subst (λ x → _ ⊢ _ :⇒*: Univ x _ ^ _) (PE.sym r≡r) (PE.subst (λ x → _ ⊢ _ :⇒*: Univ _ x ^ [ ! , next x ]) (PE.sym l≡l) d')
    in reduction-irrelevant-Univ= {l< = l<} {l<' = l<'} {el = PE.refl} {el' = el'} {D = dd} {D' = d'} r≡r (convEqTermTUniv X)
  convEqTermT₁ (emb⁰¹ X) A≡B t≡u = convEqTermT₁ X A≡B t≡u
  convEqTermT₁ (emb¹⁰ X) A≡B t≡u = convEqTermT₁ X A≡B t≡u
  convEqTermT₁ (emb¹∞ X) A≡B t≡u = convEqTermT₁ X A≡B t≡u
  convEqTermT₁ (emb∞¹ X) A≡B t≡u = convEqTermT₁ X A≡B t≡u

  -- Helper function for conversion of term equality converting from right to left.
  convEqTermT₂ : ∀ {l l′ Γ A B t u r} {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r}
             → ShapeView Γ l l′ A B r r [A] [B]
             → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
             → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ r / [B]
             → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ r / [A]
  convEqTermT₂ (ℕᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₂ (Emptyᵥ D D′) A≡B t≡u = t≡u
  convEqTermT₂ {r = [ ! , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ k m d d′ (neNfₜ₌ neK₂ neM₁ k≡m)) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _ ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in  neₜ₌ k m (convRed:*: d K₁≡K) (convRed:*: d′ K₁≡K)
                 (neNfₜ₌ neK₂ neM₁ (~-conv k≡m K₁≡K))
  convEqTermT₂ {r = [ % , ll ]} (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
               (neₜ₌ d d′) =
    let K₁≡K = PE.subst (λ x → _ ⊢ x ≡ _ ^ _)
                        (whrDet* (red D′ , ne neM) (red D₁ , ne neK₁))
                        (sym (≅-eq (~-to-≅ K≡M)))
    in neₜ₌ (conv d (reduction  (red D₁) (red D) (ne neK₁) (ne neK) K₁≡K))
            (conv d′ (reduction  (red D₁) (red D) (ne neK₁) (ne neK) K₁≡K))
  convEqTermT₂ {Γ = Γ} {r = [ ! , ι ll ]} (Πᵥ (Πᵣ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                           (Πᵣ rF₁ lF₁ lG₁ 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 d′ funcF funcG t≡u [t] [u] [t≡u]) =
    let [A] = Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [B] = Πᵣ′ rF₁ lF₁ lG₁ lF₁≤ lG₁≤ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
        [A≡B] = Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]
        ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ ! , ι ll ])
                             (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
    in  Πₜ₌ f g (convRed:*: d (sym ΠFG≡ΠF₁G₁)) (convRed:*: d′ (sym ΠFG≡ΠF₁G₁))
            funcF funcG (≅-conv t≡u (sym ΠFG≡ΠF₁G₁))
            (convTerm₂ [A] [B] [A≡B] [t]) (convTerm₂ [A] [B] [A≡B] [u])
            (λ {ρ} [ρ] ⊢Δ [a] →
               let F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , lΠ≡lΠ₁ = Π-PE-injectivity (whrDet* (red D₁ , Πₙ) (D′ , Πₙ))
                   [F≡F₁] = irrelevanceEqR′ (PE.cong (wk ρ) (PE.sym F₁≡F′))
                                            ([F] [ρ] ⊢Δ) ([F≡F′] [ρ] ⊢Δ)
                   [a]₁ = convTerm₁′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ) [F≡F₁] [a]
                   [G≡G₁] = irrelevanceEqR′ (PE.cong (λ x → wk (lift ρ) x [ _ ])
                                                     (PE.sym G₁≡G′))
                                            ([G] [ρ] ⊢Δ [a])
                                            ([G≡G′] [ρ] ⊢Δ [a])
               in  convEqTerm₂′ PE.refl (PE.cong ι (PE.sym lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                               [G≡G₁] ([t≡u] [ρ] ⊢Δ [a]₁))
  convEqTermT₂ {Γ = Γ} {r = [ % , ι ll ]} (Πᵥ (Πᵣ 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′])
               (d , d′) =
               let ΠF₁G₁≡ΠF′G′ = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
                   ΠFG≡ΠF₁G₁ = PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° ll ≡ x ^ [ % , ι ll ])
                                        (PE.sym ΠF₁G₁≡ΠF′G′) (≅-eq A≡B)
               in (conv d (sym ΠFG≡ΠF₁G₁)) , (conv d′ (sym ΠFG≡ΠF₁G₁))
  convEqTermT₂ {Γ = Γ} {r = [ % , ll ]} (∃ᵥ (∃ᵣ 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′])
               (d , d′) =
               let ∃F₁G₁≡∃F′G′ = whrDet* (red D₁ , ∃ₙ) (D′ , ∃ₙ)
                   ∃FG≡∃F₁G₁ = PE.subst (λ x → Γ ⊢ ∃ F ▹ G ≡ x ^ [ % , ll ])
                                        (PE.sym ∃F₁G₁≡∃F′G′) (≅-eq A≡B)
               in (conv d (sym ∃FG≡∃F₁G₁)) , (conv d′ (sym ∃FG≡∃F₁G₁))
  convEqTermT₂ (Uᵥ (Uᵣ r l l< el d) (Uᵣ r' l' l<' PE.refl d')) A≡B X =
    let U≡U   = whrDet* (A≡B , Uₙ) (red d' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity (PE.sym U≡U)
        dd = PE.subst (λ x → _ ⊢ _ :⇒*: Univ x _ ^ _) (PE.sym r≡r) (PE.subst (λ x → _ ⊢ _ :⇒*: Univ _ x ^ [ ! , next x ]) (PE.sym l≡l) d)
    in reduction-irrelevant-Univ= {l< = l<'} {el = PE.refl} {D = dd} {D' = d} r≡r (convEqTermTUniv X)
  convEqTermT₂ (emb⁰¹ X) A≡B t≡u = convEqTermT₂ X A≡B t≡u
  convEqTermT₂ (emb¹⁰ X) A≡B t≡u = convEqTermT₂ X A≡B t≡u
  convEqTermT₂ (emb¹∞ X) A≡B t≡u = convEqTermT₂ X A≡B t≡u
  convEqTermT₂ (emb∞¹ X) A≡B t≡u = convEqTermT₂ X A≡B t≡u

  -- Conversion of term equality converting from left to right.
  convEqTerm₁ : ∀ {l l′ Γ A B t u r} ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([B] : Γ ⊩⟨ l′ ⟩ B ^ r)
              → Γ ⊩⟨ l ⟩  A ≡ B ^ r / [A]
              → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ r / [A]
              → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ r / [B]
  convEqTerm₁ [A] [B] A≡B t≡u = convEqTermT₁ (goodCases [A] [B] A≡B) A≡B t≡u

  -- Conversion of term equality converting from left to right. with PE
  convEqTerm₁′ : ∀ {l l′ Γ A B t u r r' ll ll'} (eq : r PE.≡ r') (eql : ll PE.≡ ll')
                   ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ])
              → Γ ⊩⟨ l ⟩  A ≡ B ^ [ r , ll ] / [A]
              → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ [ r , ll ] / [A]
              → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ [ r' , ll' ] / [B]
  convEqTerm₁′ PE.refl PE.refl [A] [B] A≡B t≡u = convEqTerm₁ [A] [B] A≡B t≡u

  -- Conversion of term equality converting from right to left.
  convEqTerm₂ : ∀ {l l′ Γ A B t u r ll} ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r , ll ])
            → Γ ⊩⟨ l ⟩  A ≡ B ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ [ r , ll ] / [B]
            → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ [ r , ll ] / [A]
  convEqTerm₂ [A] [B] A≡B t≡u = convEqTermT₂ (goodCases [A] [B] A≡B) A≡B t≡u

  -- Conversion of term equality converting from right to left with PE
  convEqTerm₂′ : ∀ {l l′ Γ A B t u r r' ll ll'} (eq : r PE.≡ r') (eql : ll PE.≡ ll')
                   ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ])
            → Γ ⊩⟨ l ⟩  A ≡ B ^ [ r , ll ] / [A]
            → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ B ^ [ r' , ll' ] / [B]
            → Γ ⊩⟨ l ⟩  t ≡ u ∷ A ^ [ r , ll ] / [A]
  convEqTerm₂′ PE.refl PE.refl [A] [B] A≡B t≡u = convEqTerm₂ [A] [B] A≡B t≡u


text:
-- Useless private
module Issue476a where

A : Set₁
private
  A = Set

ext: agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2015-05-06

module Issue1484 where

data ⊥ : Set where

-- Smörgåsbord of legal absurd lambdas

-- non-hidden

abs esabs eabs eabs2 eabs3 : ⊥ → Set
abs = λ()

esabs = λ{ ()}
eabs  = λ{()}
eabs2 = λ{(())}
eabs3 = λ{((()))}

-- hidden

habs eshabs eshpabs eshpabs2 : {_ : ⊥} → Set
habs     = λ{}

eshabs   = λ{ {}}
eshpabs  = λ{ {()}}
eshpabs2 = λ{ {(())}}

-- instance

iabs esiabs esipabs esipabs2 : {{_ : ⊥}} → Set
iabs     = λ{{}}

esiabs   = λ{ {{}}}
esipabs  = λ{ {{()}}}
esipabs2 = λ{ {{(())}}}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Component functions of permutations found in `Data.Fin.Permutation`
------------------------------------------------------------------------

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

module Data.Fin.Permutation.Components where

open import Data.Bool.Base using (Bool; true; false)
open import Data.Fin.Base
open import Data.Fin.Properties
open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
import Data.Nat.Properties as ℕₚ
open import Data.Product using (proj₂)
open import Function.Base using (_∘_)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (does; _because_; yes; no)
open import Relation.Nullary.Decidable using (dec-true; dec-false)
open import Relation.Binary.PropositionalEquality
open import Algebra.Definitions using (Involutive)
open ≡-Reasoning

--------------------------------------------------------------------------------
--  Functions
--------------------------------------------------------------------------------

-- 'tranpose i j' swaps the places of 'i' and 'j'.

transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
transpose i j k with does (k ≟ i)
... | true  = j
... | false with does (k ≟ j)
...   | true  = i
...   | false = k

-- reverse i = n ∸ 1 ∸ i

reverse : ∀ {n} → Fin n → Fin n
reverse {suc n} i  = inject≤ (n ℕ- i) (ℕₚ.m∸n≤m (suc n) (toℕ i))

--------------------------------------------------------------------------------
--  Properties
--------------------------------------------------------------------------------

transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                    transpose i j (transpose j i k) ≡ k
transpose-inverse i j {k} with k ≟ j
... | true  because [k≡j] rewrite dec-true (i ≟ i) refl = sym (invert [k≡j])
... | false because [k≢j] with k ≟ i
...   | true  because [k≡i]
        rewrite dec-false (j ≟ i) (invert [k≢j] ∘ trans (invert [k≡i]) ∘ sym)
                | dec-true (j ≟ j) refl
                = sym (invert [k≡i])
...   | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
                                  | dec-false (k ≟ j) (invert [k≢j]) = refl

reverse-prop : ∀ {n} → (i : Fin n) → toℕ (reverse i) ≡ n ∸ suc (toℕ i)
reverse-prop {suc n} i = begin
  toℕ (inject≤ (n ℕ- i) _)  ≡⟨ toℕ-inject≤ _ (ℕₚ.m∸n≤m (suc n) (toℕ i)) ⟩
  toℕ (n ℕ- i)              ≡⟨ toℕ‿ℕ- n i ⟩
  n ∸ toℕ i                 ∎

reverse-involutive : ∀ {n} → Involutive _≡_ (reverse {n})
reverse-involutive {suc n} i = toℕ-injective (begin
  toℕ (reverse (reverse i)) ≡⟨ reverse-prop (reverse i) ⟩
  n ∸ (toℕ (reverse i))     ≡⟨ cong (n ∸_) (reverse-prop i) ⟩
  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (ℕₚ.≤-pred (toℕ<n i)) ⟩
  toℕ i                     ∎)

reverse-suc : ∀ {n} {i : Fin n} → toℕ (reverse (suc i)) ≡ toℕ (reverse i)
reverse-suc {n} {i} = begin
  toℕ (reverse (suc i))      ≡⟨ reverse-prop (suc i) ⟩
  suc n ∸ suc (toℕ (suc i))  ≡⟨⟩
  n ∸ toℕ (suc i)            ≡⟨⟩
  n ∸ suc (toℕ i)            ≡⟨ sym (reverse-prop i) ⟩
  toℕ (reverse i)            ∎


text:
open import Common.Prelude

instance
  tti : ⊤
  tti = record{}

NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc _) = ⊤

pred′ : (n : Nat) .{{_ : NonZero n}} → Nat
pred′ zero {{}}
pred′ (suc n) = n

test : (n : Nat) {{x y : NonZero n}} → Nat
test n = pred′ n

_<_ : Nat → Nat → Set
m < zero = ⊥
zero < suc n = ⊤
suc m < suc n = m < n

instance
  <-suc : ∀ {m n} → .(m < n) → m < suc n
  <-suc {zero} _ = tt
  <-suc {suc m} {zero} ()
  <-suc {suc m} {suc n} = <-suc {m} {n}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

test : (x : Nat) (f : {n : Nat} → Nat) → f {0} ≡ x → Nat
test x f p = {!p!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Abelian.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Rings.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.EuclideanAlgorithm
open import Numbers.Primes.PrimeNumbers

module Rings.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) where

abstract

  open Setoid S
  open Ring R
  open Group additiveGroup

  ringMinusExtracts : {x y : A} → (x * Group.inverse (Ring.additiveGroup R) y) ∼ (Group.inverse (Ring.additiveGroup R) (x * y))
  ringMinusExtracts {x = x} {y} = transferToRight' additiveGroup (transitive (symmetric *DistributesOver+) (transitive (*WellDefined reflexive invLeft) (Ring.timesZero R)))
    where
      open Equivalence eq

  ringMinusExtracts' : {x y : A} → ((inverse x) * y) ∼ inverse (x * y)
  ringMinusExtracts' {x = x} {y} = transitive *Commutative (transitive ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))
    where
      open Equivalence eq

  twoNegativesTimes : {a b : A} → (inverse a) * (inverse b) ∼ a * b
  twoNegativesTimes {a} {b} = transitive (ringMinusExtracts) (transitive (inverseWellDefined additiveGroup ringMinusExtracts') (invTwice additiveGroup (a * b)))
    where
      open Equivalence eq

  groupLemmaMove0G : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → (Setoid._∼_ S (Group.0G G) (Group.inverse G x)) → Setoid._∼_ S x (Group.0G G)
  groupLemmaMove0G {S = S} G {x} pr = transitive (symmetric (invInv G)) (transitive (symmetric p) (invIdent G))
    where
      open Equivalence (Setoid.eq S)
      p : Setoid._∼_ S (Group.inverse G (Group.0G G)) (Group.inverse G (Group.inverse G x))
      p = inverseWellDefined G pr

  groupLemmaMove0G' : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S x (Group.0G G) → (Setoid._∼_ S (Group.0G G) (Group.inverse G x))
  groupLemmaMove0G' {S = S} G {x} pr = transferToRight' G (Equivalence.transitive (Setoid.eq S) (Group.identLeft G) pr)

  oneZeroImpliesAllZero : 0R ∼ 1R → {x : A} → x ∼ 0R
  oneZeroImpliesAllZero 0=1 = Equivalence.transitive eq (Equivalence.symmetric eq identIsIdent) (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))

  lemm3 : (a b : A) → 0G ∼ (a + b) → 0G ∼ a → 0G ∼ b
  lemm3 a b pr1 pr2 with transferToRight' additiveGroup (Equivalence.symmetric eq pr1)
  ... | a=-b with Equivalence.transitive eq pr2 a=-b
  ... | 0=-b with inverseWellDefined additiveGroup 0=-b
  ... | -0=--b = Equivalence.transitive eq (Equivalence.symmetric eq (invIdent additiveGroup)) (Equivalence.transitive eq -0=--b (invTwice additiveGroup b))

  charNot2ImpliesNontrivial : ((1R + 1R) ∼ 0R → False) → (0R ∼ 1R) → False
  charNot2ImpliesNontrivial charNot2 0=1 = charNot2 (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.symmetric eq 0=1)) identRight)

abelianUnderlyingGroup : AbelianGroup additiveGroup
abelianUnderlyingGroup = record { commutative = groupIsAbelian }


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

-- Reference to check out
--
-- Simply Typed Lambda Calculus in Agda, without Shortcuts
-- https://gergo.erdi.hu/blog/2013-05-01-simply_typed_lambda_calculus_in_agda,_without_shortcuts/

module InterpreterWithConstants where

open import Data.Char hiding (_≤_)
open import Data.Bool hiding (_≤_)
open import Data.Nat hiding (_≤_)
open import Data.Unit
import Data.Nat as N
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
import Data.String as Str
open import Data.Nat.Show
import Data.List as List
open import Data.Empty

infix 3 _:::_,_
infix 2 _∈_
infix 2 _∉_

infix 1 _⊢_

data `Set : Set where
  `Bool : `Set
  _`⇨_  : `Set → `Set → `Set
  `⊤    : `Set
  _`×_  : `Set → `Set → `Set
infixr 2 _`⇨_

data Var : Set where
  x' : Var
  y' : Var
  z' : Var

-- Inequality proofs on variables
data _≠_ : Var → Var → Set where
  x≠y : x' ≠ y'
  x≠z : x' ≠ z'
  y≠x : y' ≠ x'
  y≠z : y' ≠ z'
  z≠x : z' ≠ x'
  z≠y : z' ≠ y'

instance
  xy : x' ≠ y'
  xy = x≠y

  xz : x' ≠ z'
  xz = x≠z

  yx : y' ≠ x'
  yx = y≠x

  yz : y' ≠ z'
  yz = y≠z

  zx : z' ≠ x'
  zx = z≠x

  zy : z' ≠ y'
  zy = z≠y

⟦_⟧ : `Set → Set
⟦ `Bool ⟧ = Bool
⟦ (t `⇨ s) ⟧ =  ⟦ t ⟧ → ⟦ s ⟧
⟦ `⊤ ⟧ = ⊤
⟦ (t `× s) ⟧ = ⟦ t ⟧ × ⟦ s ⟧

data Γ : Set where
  ·         : Γ
  _:::_,_   : Var → `Set → Γ → Γ

data _∈_ :  Var → Γ → Set where
  H  : ∀ {x Δ t } → x ∈ x ::: t , Δ
  TH : ∀ {x y Δ t} → ⦃ prf : x ∈ Δ ⦄ → ⦃ neprf : x ≠ y ⦄ → x ∈ y ::: t , Δ

instance
  ∈_type₁ : ∀ {x Δ t} → x ∈ x ::: t , Δ
  ∈_type₁ = H

  ∈_type₂ : ∀ {x y Δ t} → ⦃ prf : x ∈ Δ ⦄ → ⦃ x ≠ y ⦄ → x ∈ y ::: t , Δ
  ∈_type₂ = TH

data _∉_ : Var → Γ → Set where
  H : ∀ {x} → x ∉ ·
  TH : ∀ {x y Δ t} → ⦃ prf : x ∉ Δ ⦄ → ⦃ neprf : x ≠ y ⦄ → x ∉ y ::: t , Δ

instance
  ∉_type₁ : ∀ {x} → x ∉ ·
  ∉_type₁ = H

  ∉_type₂ : ∀ {x y Δ t} → ⦃ prf : x ∉ Δ ⦄ → ⦃ x ≠ y ⦄ → x ∉ y ::: t , Δ
  ∉_type₂ = TH

!Γ_[_] : ∀ {x} → (Δ : Γ) → x ∈ Δ → `Set
!Γ_[_] · ()
!Γ _ ::: t , Δ [ H ]     = t
!Γ _ ::: _ , Δ [ TH ⦃ prf = i ⦄ ]  = !Γ Δ [ i ]

infix 30 `v_
infix 30 `c_

infix 24 _`,_
infixl 22 _`₋_

data Constant : `Set → Set where
  `not           : Constant (`Bool `⇨ `Bool)
  `∧             : Constant (`Bool `× `Bool `⇨ `Bool)
  `∨             : Constant (`Bool `× `Bool `⇨ `Bool)
  `xor           : Constant (`Bool `× `Bool `⇨ `Bool)

data _⊢_ : Γ → `Set → Set where
  `false           : ∀ {Δ} → Δ ⊢ `Bool
  `true            : ∀ {Δ} → Δ ⊢ `Bool
  `v_              : ∀ {Δ} → (x : Var) → ⦃ i : x ∈ Δ ⦄ → Δ ⊢ !Γ Δ [ i ]
  `c_              : ∀ {Δ t} → Constant t → Δ ⊢ t
  _`₋_             : ∀ {Δ t s} → Δ ⊢ t `⇨ s → Δ ⊢ t → Δ ⊢ s --application
  `λ_`:_⇨_         : ∀ {Δ tr} → (x : Var) → (tx : `Set)
                        → x ::: tx , Δ ⊢ tr → Δ ⊢ tx `⇨ tr

  _`,_             : ∀ {Δ t s} → Δ ⊢ t →  Δ ⊢ s →  Δ ⊢ t `× s
  `fst             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ t
  `snd             : ∀ {Δ t s} → Δ ⊢ t `× s → Δ ⊢ s
  `tt              : ∀ {Δ} → Δ ⊢ `⊤

data ⟨_⟩ : Γ → Set₁ where
  []   : ⟨ · ⟩
  _∷_  : ∀ {x t Δ} → ⟦ t ⟧ → ⟨ Δ ⟩ → ⟨ x ::: t , Δ ⟩

!_[_] : ∀ {x Δ} → ⟨ Δ ⟩ → (i : x ∈ Δ) → ⟦ !Γ Δ [ i ] ⟧
!_[_] [] ()
!_[_] (val ∷ env) H      = val
!_[_] (val ∷ env) (TH ⦃ prf = i ⦄) = ! env [ i ]

interpretConstant : ∀ {t} → Constant t → ⟦ t ⟧
interpretConstant `not = not
interpretConstant `∧   = uncurry _∧_
interpretConstant `∨   = uncurry _∨_
interpretConstant `xor = uncurry _xor_

interpret : ∀ {t} → · ⊢ t → ⟦ t ⟧
interpret = interpret' []
  where interpret' : ∀ {Δ t} → ⟨ Δ ⟩ → Δ ⊢ t → ⟦ t ⟧
        interpret' env `true                = true
        interpret' env `false               = false
        interpret' env `tt                  = tt
        interpret' env ((`v x) ⦃ i = idx ⦄) = ! env [ idx ]
        interpret' env (f `₋ x)             = (interpret' env f) (interpret' env x)
        interpret' env (`λ _ `: tx ⇨ body)  = λ (x : ⟦ tx ⟧) → interpret' (x ∷ env) body
        interpret' env (`c f)               = interpretConstant f
        interpret' env (f `, s)             = interpret' env f ,′ interpret' env s
        interpret' env (`fst p) with interpret' env p
        interpret' env (`fst p) | f , s     = f
        interpret' env (`snd p) with interpret' env p
        interpret' env (`snd p) | f , s     = s

-----

and₁ : · ⊢ `Bool `× `Bool `⇨ `Bool
and₁ = `λ x' `: `Bool `× `Bool ⇨ `c `∧ `₋ `v x'

and₂ : · ⊢ `Bool `× `Bool `⇨ `Bool
and₂ = `c `∧

{-

I want to write a function called eta-reduce that one could prove the following:

pf : eta-reduce and₁ ≡ and₂
pf = refl

This function will eta-reduce when it can, and do nothing when it can't.
For instance the following should be true:

  eta-reduce-constant : ∀ {c} → eta-reduce (`c c) ≡ `c c

However, I get stuck even on this case. Uncomment the definition below and try to
type check this module:

-}

-- eta-reduce : ∀ {t₁ t₂} → · ⊢ t₁ `⇨ t₂ → · ⊢ t₁ `⇨ t₂
-- eta-reduce (`c c) = ?

{-

You will get the following error message:

  I'm not sure if there should be a case for the constructor `v_,
  because I get stuck when trying to solve the following unification
  problems (inferred index ≟ expected index):
    Δ ≟ ·
    !Γ Δ [ i ] ≟ t₁ `⇨ t₂
  when checking the definition of eta-reduce

I did a bit of searching on the Internet and the only source I could find
that I could understand was this one: https://doisinkidney.com/posts/2018-09-20-agda-tips.html

It seems to be suggesting that one of the indices for a type is not in constructor form but is,
rather, a function.

Looking at the definition of _⊢_ we see that the `v_` constructor is most likely at fault:

  `v_ : ∀ {Δ} → (x : Var) → ⦃ i : x ∈ Δ ⦄ → Δ ⊢ !Γ Δ [ i ]

The result type is `Δ ⊢ !Γ Δ [ i ]`. Clearly the index `!Γ Δ [ i ]` is referring to a
user-defined function.

My question is, "how can I fix this?". How would I modify the _⊢_ data structure

- I would be open to an alternative interpreter for the Simply Typed Lambda Calculus
- This interpreter is a modified form of this code base. ttps://github.com/ahmadsalim/well-typed-agda-interpreter
  It has had instance declarations added and the syntactic form of terms has changed a little. I pulled out
  the constant functions into their own data structure called `Constant` and changed their types a little to work
  on products (_×_) instead of a curried form.

-}

{-
The instance based searching for _∈_ proofs might be a problem. I'm uncomfortable
with the use of --overlapping-instances

-}

-- eta-reduce : ∀ {t₁ t₂} → · ⊢ t₁ `⇨ t₂ → · ⊢ t₁ `⇨ t₂
-- eta-reduce (`λ x `: _ ⇨ f `₋ y) = {!!}
-- eta-reduce t = t

max_stars_repo_name: sseefried/well-typed-agda-interpreter

max_issues_repo_name: sseefried/well-typed-agda-interpreter

max_forks_repo_name: sseefried/well-typed-agda-interpreter


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

open import HoTT hiding (left; right)
import homotopy.WedgeExtension as WedgeExt

module homotopy.blakersmassey.CoherenceData {i j k}
  {A : Type i} {B : Type j} (Q : A → B → Type k)
  m (f-conn : ∀ a → is-connected (S m) (Σ B (λ b → Q a b)))
  n (g-conn : ∀ b → is-connected (S n) (Σ A (λ a → Q a b)))
  where

open import homotopy.blakersmassey.Pushout Q

{- goal :
    Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r)
  ≃ Trunc (m +2+ n) (hfiber bmglue r)
-}

private
  swap-level :
      (m +2+ n) -Type (lmax i (lmax j k))
    → (n +2+ m) -Type (lmax i (lmax j k))
  swap-level (X , level) = X , new-level where
    abstract new-level = transport (λ o → has-level o X) (+2+-comm m n) level

α₁=α₁α₂⁻¹α₂ : ∀ {p₁ p₂ p₃ : BMPushout} (α₁ : p₁ == p₂) (α₂ : p₃ == p₂)
  → α₁ == α₁ ∙' ! α₂ ∙' α₂
α₁=α₁α₂⁻¹α₂ _ idp = idp

α₁=α₂α₂⁻¹α₁ : ∀ {p₁ p₂ p₃ : BMPushout} (α₁ : p₁ == p₂) (α₂ : p₁ == p₃)
  → α₁ == α₂ ∙' ! α₂ ∙' α₁
α₁=α₂α₂⁻¹α₁ idp α₂ = ! (!-inv'-r α₂)

private
  path-lemma₁ : ∀ {a₀ a₁ b} (q₀ : Q a₀ b) (q₁ : Q a₁ b)
    → bmglue q₀ == bmglue q₀ ∙' ! (bmglue q₁) ∙' bmglue q₁
  path-lemma₁ q₀ q₁ = α₁=α₁α₂⁻¹α₂ (bmglue q₀) (bmglue q₁)

  path-lemma₂ : ∀ {a b₀ b₁} (q₀ : Q a b₀) (q₁ : Q a b₁)
    → bmglue q₀ == bmglue q₁ ∙' ! (bmglue q₁) ∙' bmglue q₀
  path-lemma₂ q₀ q₁ = α₁=α₂α₂⁻¹α₁ (bmglue q₀) (bmglue q₁)

  abstract
    path-coherence : ∀ {a b} (q : Q a b)
      → path-lemma₁ q q == path-lemma₂ q q
    path-coherence q = lemma (bmglue q) where
      lemma : ∀ {p₀ p₁ : BMPushout} (path : p₀ == p₁)
        → α₁=α₁α₂⁻¹α₂ path path == α₁=α₂α₂⁻¹α₁ path path
      lemma idp = idp

module To {a₁ b₀} (q₁₀ : Q a₁ b₀) where
  U = Σ A λ a → Q a b₀
  u₀ : U
  u₀ = (a₁ , q₁₀)

  V = Σ B λ b → Q a₁ b
  v₀ : V
  v₀ = (b₀ , q₁₀)

  P : U → V → Type (lmax i (lmax j k))
  P u v = (r : bmleft (fst u) == bmright (fst v))
    → bmglue (snd u) ∙' ! (bmglue q₁₀) ∙' bmglue (snd v) == r
    → Trunc (m +2+ n) (hfiber bmglue r)

  template : ∀ (u : U) (v : V)
    → (r : bmleft (fst u) == bmright (fst v))
    → (shift : bmglue (snd u) ∙' ! (bmglue q₁₀) ∙' bmglue (snd v) == r)
    → ∀ q₀₁ → bmglue q₀₁ == bmglue (snd u) ∙' ! (bmglue q₁₀) ∙' bmglue (snd v)
    → Trunc (m +2+ n) (hfiber bmglue r)
  template u v r shift q₀₁ path = [ q₀₁ , path ∙' shift ]

  f = λ u r shift → template u v₀ r shift (snd u) (path-lemma₁ (snd u) q₁₀)
  g = λ v r shift → template u₀ v r shift (snd v) (path-lemma₂ (snd v) q₁₀)
  p' = λ r shift → ap (template u₀ v₀ r shift q₁₀) (path-coherence q₁₀)
  p = λ= λ r → λ= λ shift → p' r shift

  args : WedgeExt.args {A = U} {a₀ = u₀} {B = V} {b₀ = v₀}
  args = record {
    n = n; m = m;
    cA = g-conn b₀;
    cB = f-conn a₁;
    P = λ u v → swap-level $ P u v , Π-level λ _ → Π-level λ _ → Trunc-level;
    f = f; g = g; p = p}

  ext : ∀ u v → P u v
  ext = WedgeExt.ext args

  β-l : ∀ u r shift → ext u v₀ r shift == f u r shift
  β-l u r shift = app= (app= (WedgeExt.β-l u) r) shift

  β-r : ∀ v r shift → ext u₀ v r shift == g v r shift
  β-r v r shift = app= (app= (WedgeExt.β-r v) r) shift

  abstract
    coh : ∀ r shift → ! (β-l u₀ r shift) ∙ β-r v₀ r shift == p' r shift
    coh r shift =
      ! (β-l u₀ r shift) ∙ β-r v₀ r shift
        =⟨ ap (_∙ β-r v₀ r shift) (!-ap (_$ shift) (app= (WedgeExt.β-l u₀) r))
         ∙ ∙-ap (_$ shift)
             (! (app= (WedgeExt.β-l {r = args} u₀) r))
             (app= (WedgeExt.β-r {r = args} v₀) r)
         ∙ ap (λ p → app= p shift)
             ( ap (_∙ app= (WedgeExt.β-r {r = args} v₀) r)
                (!-ap (_$ r) (WedgeExt.β-l {r = args} u₀))
             ∙ ∙-ap (_$ r)
                (! (WedgeExt.β-l {r = args} u₀))
                (WedgeExt.β-r {r = args} v₀)) ⟩
      app= (app= (! (WedgeExt.β-l {r = args} u₀) ∙ WedgeExt.β-r {r = args} v₀) r) shift
        =⟨ ap (λ p → app= (app= p r) shift) (WedgeExt.coh {r = args}) ⟩
      app= (app= (λ= λ r → λ= λ shift → p' r shift) r) shift
        =⟨ ap (λ p → app= p shift) (app=-β (λ r → λ= λ shift → p' r shift) r)
         ∙ app=-β (λ shift → p' r shift) shift ⟩
      p' r shift
        =∎

to' : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁)
  → (r : bmleft a₀ == bmright b₁)
  → hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r
  → Trunc (m +2+ n) (hfiber bmglue r)
to' q₀₀ q₁₁ r (q₁₀ , shift) = To.ext q₁₀ (_ , q₀₀) (_ , q₁₁) r shift

to : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁)
  → (r : bmleft a₀ == bmright b₁)
  → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r)
  → Trunc (m +2+ n) (hfiber bmglue r)
to q₀₀ q₁₁ r = Trunc-rec (to' q₀₀ q₁₁ r)

module From {a₀ b₁} (q₀₁ : Q a₀ b₁) where
  U = Σ A λ a → Q a b₁
  u₀ : U
  u₀ = (a₀ , q₀₁)

  V = Σ B λ b → Q a₀ b
  v₀ : V
  v₀ = (b₁ , q₀₁)

  P : U → V → Type (lmax i (lmax j k))
  P u v = (r : bmleft a₀ == bmright b₁)
    → bmglue q₀₁ == r
    → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue (snd v) ∙' ! (bmglue q₁₀) ∙' bmglue (snd u)) r)

  template : ∀ (u : U) (v : V)
    → (r : bmleft a₀ == bmright b₁)
    → (shift : bmglue q₀₁ == r)
    → ∀ q₁₀ → bmglue q₀₁ == bmglue (snd v) ∙' ! (bmglue q₁₀) ∙' bmglue (snd u)
    → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue (snd v) ∙' ! (bmglue q₁₀) ∙' bmglue (snd u)) r)
  template u v r shift q₁₀ path = [ q₁₀ , ! path ∙' shift ]

  f = λ u r shift → template u v₀ r shift (snd u) (path-lemma₁ q₀₁ (snd u))
  g = λ v r shift → template u₀ v r shift (snd v) (path-lemma₂ q₀₁ (snd v))
  p' = λ r shift → ap (template u₀ v₀ r shift q₀₁) (path-coherence q₀₁)
  p = λ= λ r → λ= λ shift → p' r shift

  args : WedgeExt.args {A = U} {a₀ = u₀} {B = V} {b₀ = v₀}
  args = record {
    n = n; m = m;
    cA = g-conn b₁;
    cB = f-conn a₀;
    P = λ u v → swap-level $ P u v , Π-level λ _ → Π-level λ _ → Trunc-level;
    f = f; g = g; p = p}

  ext : ∀ u v → P u v
  ext = WedgeExt.ext args

  β-l : ∀ u r shift → ext u v₀ r shift == f u r shift
  β-l u r shift = app= (app= (WedgeExt.β-l u) r) shift

  β-r : ∀ v r shift → ext u₀ v r shift == g v r shift
  β-r v r shift = app= (app= (WedgeExt.β-r v) r) shift

  abstract
    coh : ∀ r shift → ! (β-l u₀ r shift) ∙ β-r v₀ r shift == p' r shift
    coh r shift =
      ! (β-l u₀ r shift) ∙ β-r v₀ r shift
        =⟨ ap (_∙ β-r v₀ r shift) (!-ap (_$ shift) (app= β-l' r))
         ∙ ∙-ap (_$ shift) (! (app= β-l' r)) (app= β-r' r)
         ∙ ap (λ p → app= p shift)
             ( ap (_∙ app= β-r' r) (!-ap (_$ r) β-l')
             ∙ ∙-ap (_$ r) (! β-l') β-r') ⟩
      app= (app= (! β-l' ∙ β-r') r) shift
        =⟨ ap (λ p → app= (app= p r) shift) (WedgeExt.coh {r = args}) ⟩
      app= (app= (λ= λ r → λ= λ shift → p' r shift) r) shift
        =⟨ ap (λ p → app= p shift) (app=-β (λ r → λ= λ shift → p' r shift) r)
         ∙ app=-β (λ shift → p' r shift) shift ⟩
      p' r shift
        =∎
      where β-l' = WedgeExt.β-l {r = args} u₀
            β-r' = WedgeExt.β-r {r = args} v₀

from' : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁)
  → (r : bmleft a₀ == bmright b₁)
  → hfiber bmglue r
  → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r)
from' q₀₀ q₁₁ r (q₀₁ , shift) = From.ext q₀₁ (_ , q₁₁) (_ , q₀₀) r shift

from : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁)
  → (r : bmleft a₀ == bmright b₁)
  → Trunc (m +2+ n) (hfiber bmglue r)
  → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r)
from q₀₀ q₁₁ r = Trunc-rec (from' q₀₀ q₁₁ r)

-- Equivalence

{-
    First step:  Pack relevant rules into records.
-}

record βPair {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀)
  (q₁₁ : Q a₁ b₁) (q₀₁ : Q a₀ b₁) (q₁₀ : Q a₁ b₀)
  (r : bmleft a₀ == bmright b₁) : Type (lmax i (lmax j k)) where
  constructor βpair
  field
    path : bmglue q₀₁ == bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁
    to-β : ∀ shift → To.ext q₁₀ (_ , q₀₀) (_ , q₁₁) r shift
                  == To.template q₁₀ (_ , q₀₀) (_ , q₁₁) r shift q₀₁ path
    from-β : ∀ shift → From.ext q₀₁ (_ , q₁₁) (_ , q₀₀) r shift
                    == From.template q₀₁ (_ , q₁₁) (_ , q₀₀) r shift q₁₀ path

βpair-bmleft : ∀ {a₀ a₁ b} (q₀ : Q a₀ b) (q₁ : Q a₁ b) r
  → βPair q₀ q₁ q₀ q₁ r
βpair-bmleft q₀ q₁ r = record
  { path = path-lemma₁ q₀ q₁
  ; to-β = To.β-l q₁ (_ , q₀) r
  ; from-β = From.β-l q₀ (_ , q₁) r
  }

βpair-bmright : ∀ {a b₀ b₁} (q₀ : Q a b₀) (q₁ : Q a b₁) r
  → βPair q₀ q₁ q₁ q₀ r
βpair-bmright q₀ q₁ r = record
  { path = path-lemma₂ q₁ q₀
  ; to-β = To.β-r q₀ (_ , q₁) r
  ; from-β = From.β-r q₁ (_ , q₀) r
  }

abstract
  βpair= : ∀ {a₀ a₁} {b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁)
    (q₀₁ : Q a₀ b₁) (q₁₀ : Q a₁ b₀) (r : bmleft a₀ == bmright b₁)
    {p₁ p₂ : bmglue q₀₁ == bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁} (p= : p₁ == p₂)
    {toβ₁} {toβ₂}
    (toβ= : ∀ shift → toβ₁ shift ∙ ap (To.template q₁₀ (_ , q₀₀) (_ , q₁₁) r shift q₀₁) p=
                   == toβ₂ shift)
    {fromβ₁} {fromβ₂}
    (fromβ= : ∀ shift → fromβ₁ shift ∙ ap (From.template q₀₁ (_ , q₁₁) (_ , q₀₀) r shift q₁₀) p=
                     == fromβ₂ shift)
    → βpair p₁ toβ₁ fromβ₁ == βpair p₂ toβ₂ fromβ₂
  βpair= q₀₀ q₁₁ q₀₁ q₁₀ r {p} idp toβ= fromβ= = lemma
    (λ= λ shift → ! (∙-unit-r _) ∙ toβ= shift)
    (λ= λ shift → ! (∙-unit-r _) ∙ fromβ= shift)
    where
      lemma : ∀ {toβ₁} {toβ₂} (toβ= : toβ₁ == toβ₂) {fromβ₁} {fromβ₂} (fromβ= : fromβ₁ == fromβ₂)
        → βpair p toβ₁ fromβ₁ == βpair p toβ₂ fromβ₂
      lemma idp idp = idp

abstract
  βpair-glue : ∀ {a} {b} (q : Q a b) r
    → βpair-bmleft q q r == βpair-bmright q q r
  βpair-glue q r = βpair= q q q q r
    (path-coherence q)
    (λ shift →
      To.β-l q (_ , q) r shift ∙ To.p' q r shift
          =⟨ ! $ ap (To.β-l q (_ , q) r shift ∙_) (To.coh q r shift) ⟩
      To.β-l q (_ , q) r shift ∙ ! (To.β-l q (_ , q) r shift) ∙ To.β-r q (_ , q) r shift
          =⟨ ! (∙-assoc (To.β-l q (_ , q) r shift) (! (To.β-l q (_ , q) r shift)) (To.β-r q (_ , q) r shift))
           ∙ ap (_∙ To.β-r q (_ , q) r shift) (!-inv-r (To.β-l q (_ , q) r shift)) ⟩
      To.β-r q (_ , q) r shift
          ∎)
    (λ shift →
      From.β-l q (_ , q) r shift ∙ From.p' q r shift
          =⟨ ! $ ap (From.β-l q (_ , q) r shift ∙_) (From.coh q r shift) ⟩
      From.β-l q (_ , q) r shift ∙ ! (From.β-l q (_ , q) r shift) ∙ From.β-r q (_ , q) r shift
          =⟨ ! (∙-assoc (From.β-l q (_ , q) r shift) (! (From.β-l q (_ , q) r shift)) (From.β-r q (_ , q) r shift))
           ∙ ap (_∙ From.β-r q (_ , q) r shift) (!-inv-r (From.β-l q (_ , q) r shift)) ⟩
      From.β-r q (_ , q) r shift
          ∎)

-- Lemmas

private
  abstract
    to-from-template : ∀ {a₀ a₁ b₀ b₁} {q₀₀ : Q a₀ b₀}
      {q₁₁ : Q a₁ b₁} {q₀₁ : Q a₀ b₁} {q₁₀ : Q a₁ b₀} {r}
      (params : βPair q₀₀ q₁₁ q₀₁ q₁₀ r) shift
      → to q₀₀ q₁₁ r (from q₀₀ q₁₁ r [ q₀₁ , shift ]) == [ q₀₁ , shift ]
    to-from-template {q₀₀ = q₀₀} {q₁₁} {q₀₁} {q₁₀} {r} params shift =
      to q₀₀ q₁₁ r (from q₀₀ q₁₁ r [ q₀₁ , shift ])
        =⟨ ap (to q₀₀ q₁₁ r) $ from-β shift ⟩
      to q₀₀ q₁₁ r [ q₁₀ , ! path ∙' shift ]
        =⟨ to-β (! path ∙' shift) ⟩
      [ q₀₁ , path ∙' ! path ∙' shift ]
        =⟨ ap (λ p → [ q₀₁ , p ]) $ ! (∙'-assoc path (! path) shift) ∙ ap (_∙' shift) (!-inv'-r path) ∙ ∙'-unit-l shift ⟩
      [ q₀₁ , shift ]
        =∎
      where open βPair params

module FromTo {a₁ b₀} (q₁₀ : Q a₁ b₀) where
  -- upper
  U = To.U q₁₀
  u₀ = To.u₀ q₁₀
  -- lower
  V = To.V q₁₀
  v₀ = To.v₀ q₁₀

  P : U → V → Type (lmax i (lmax j k))
  P u v = (r : bmleft (fst u) == bmright (fst v))
    → (shift : bmglue (snd u) ∙' ! (bmglue q₁₀) ∙' bmglue (snd v) == r)
    → from (snd u) (snd v) r (to (snd u) (snd v) r [ q₁₀ , shift ]) == [ q₁₀ , shift ]

  abstract
    template : ∀ (u : U) (v : V) r shift q₀₁
      → βPair (snd u) (snd v) q₀₁ q₁₀ r
      → from (snd u) (snd v) r (to (snd u) (snd v) r [ q₁₀ , shift ]) == [ q₁₀ , shift ]
    template (_ , q₀₀) (_ , q₁₁) r shift q₀₁ params =
      from q₀₀ q₁₁ r (to q₀₀ q₁₁ r [ q₁₀ , shift ])
        =⟨ ap (from q₀₀ q₁₁ r) $ to-β shift ⟩
      from q₀₀ q₁₁ r [ q₀₁ , path ∙' shift ]
        =⟨ from-β (path ∙' shift) ⟩
      [ q₁₀ , ! path ∙' path ∙' shift ]
        =⟨ ap (λ p → [ q₁₀ , p ]) $ ! (∙'-assoc (! path) path shift) ∙ ap (_∙' shift) (!-inv'-l path) ∙ ∙'-unit-l shift ⟩
      [ q₁₀ , shift ]
        =∎
      where open βPair params

  f = λ u r shift → template u v₀ r shift (snd u) (βpair-bmleft (snd u) q₁₀ r)
  g = λ v r shift → template u₀ v r shift (snd v) (βpair-bmright q₁₀ (snd v) r)

  abstract
    p : f u₀ == g v₀
    p = λ= λ r → λ= λ shift → ap (template u₀ v₀ r shift q₁₀) (βpair-glue q₁₀ r)

  args : WedgeExt.args {A = U} {a₀ = u₀} {B = V} {b₀ = v₀}
  args = record {
    n = n; m = m;
    cA = g-conn b₀;
    cB = f-conn a₁;
    P = λ u v → swap-level $ P u v , Π-level λ _ → Π-level λ _ → =-preserves-level Trunc-level;
    f = f; g = g; p = p}

  abstract
    ext : ∀ u v → P u v
    ext = WedgeExt.ext args

abstract
  from-to' : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁) r fiber
    → from q₀₀ q₁₁ r (to q₀₀ q₁₁ r [ fiber ]) == [ fiber ]
  from-to' q₀₀ q₁₁ r (q₁₀ , shift) = FromTo.ext q₁₀ (_ , q₀₀) (_ , q₁₁) r shift

  from-to : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁) r fiber
    → from q₀₀ q₁₁ r (to q₀₀ q₁₁ r fiber) == fiber
  from-to q₀₀ q₁₁ r = Trunc-elim (from-to' q₀₀ q₁₁ r)

module ToFrom {a₀ b₁} (q₀₁ : Q a₀ b₁) where
  -- upper
  U = From.U q₀₁
  u₀ = From.u₀ q₀₁
  -- lower
  V = From.V q₀₁
  v₀ = From.v₀ q₀₁

  P : U → V → Type (lmax i (lmax j k))
  P u v = (r : bmleft a₀ == bmright b₁)
    → (shift : bmglue q₀₁ == r)
    → to (snd v) (snd u) r (from (snd v) (snd u) r [ q₀₁ , shift ]) == [ q₀₁ , shift ]

  abstract
    template : ∀ (u : U) (v : V) r shift q₁₀
      → βPair (snd v) (snd u) q₀₁ q₁₀ r
      → to (snd v) (snd u) r (from (snd v) (snd u) r [ q₀₁ , shift ]) == [ q₀₁ , shift ]
    template (_ , q₁₁) (_ , q₀₀) r shift q₁₀ params =
      to q₀₀ q₁₁ r (from q₀₀ q₁₁ r [ q₀₁ , shift ])
        =⟨ ap (to q₀₀ q₁₁ r) $ from-β shift ⟩
      to q₀₀ q₁₁ r [ q₁₀ , ! path ∙' shift ]
        =⟨ to-β (! path ∙' shift) ⟩
      [ q₀₁ , path ∙' ! path ∙' shift ]
        =⟨ ap (λ p → [ q₀₁ , p ]) $ ! (∙'-assoc path (! path) shift) ∙ ap (_∙' shift) (!-inv'-r path) ∙ ∙'-unit-l shift ⟩
      [ q₀₁ , shift ]
        =∎
      where open βPair params

  f = λ u r shift → template u v₀ r shift (snd u) (βpair-bmleft q₀₁ (snd u) r)
  g = λ v r shift → template u₀ v r shift (snd v) (βpair-bmright (snd v) q₀₁ r)

  abstract
    p : f u₀ == g v₀
    p = λ= λ r → λ= λ shift → ap (template u₀ v₀ r shift q₀₁) (βpair-glue q₀₁ r)

  args : WedgeExt.args {A = U} {a₀ = u₀} {B = V} {b₀ = v₀}
  args = record {
    n = n; m = m;
    cA = g-conn b₁;
    cB = f-conn a₀;
    P = λ u v → swap-level $ P u v , Π-level λ _ → Π-level λ _ → =-preserves-level Trunc-level;
    f = f; g = g; p = p}

  abstract
    ext : ∀ u v → P u v
    ext = WedgeExt.ext args

abstract
  to-from' : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁) r fiber
    → to q₀₀ q₁₁ r (from q₀₀ q₁₁ r [ fiber ]) == [ fiber ]
  to-from' q₀₀ q₁₁ r (q₀₁ , shift) = ToFrom.ext q₀₁ (_ , q₁₁) (_ , q₀₀) r shift

  to-from : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁) r fiber
    → to q₀₀ q₁₁ r (from q₀₀ q₁₁ r fiber) == fiber
  to-from q₀₀ q₁₁ r = Trunc-elim (to-from' q₀₀ q₁₁ r)

eqv : ∀ {a₀ a₁ b₀ b₁} (q₀₀ : Q a₀ b₀) (q₁₁ : Q a₁ b₁) r
  → Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' bmglue q₁₁) r)
  ≃ Trunc (m +2+ n) (hfiber bmglue r)
eqv q₀₀ q₁₁ r = equiv (to q₀₀ q₁₁ r) (from q₀₀ q₁₁ r) (to-from q₀₀ q₁₁ r) (from-to q₀₀ q₁₁ r)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module examplesPaperJFP.StateDependentIO where

open import Size
open import NativeIO
open import Function
open import Agda.Primitive
open import Level using (_⊔_) renaming (suc to lsuc)

module _  {σ γ ρ} where

  record IOInterfaceˢ : Set (lsuc (σ ⊔ γ ⊔ ρ )) where
    field  Stateˢ     :  Set σ
           Commandˢ   :  Stateˢ → Set γ
           Responseˢ  :  (s : Stateˢ) → Commandˢ s → Set ρ
           nextˢ      :  (s : Stateˢ) → (c : Commandˢ s) → Responseˢ s c → Stateˢ

open IOInterfaceˢ public

module _  {α σ γ ρ}(i   : IOInterfaceˢ {σ} {γ} {ρ} )
                                (let S = Stateˢ i)     (let C  = Commandˢ i)
                                (let  R  = Responseˢ i) (let next = nextˢ i)
  where
    mutual

      record IOˢ (i : Size)  (A : S → Set α) (s : S) : Set (lsuc (α ⊔ σ ⊔ γ ⊔ ρ )) where
        coinductive

        constructor delay
        field forceˢ : {j : Size< i} → IOˢ′ j A s

      data IOˢ′ (i : Size)  (A : S → Set α) : S → Set (lsuc (α ⊔ σ ⊔ γ ⊔ ρ )) where
        doˢ′      :  {s : S} → (c : C s) → (f : (r : R s c) → IOˢ i A (next s c r) )
                     → IOˢ′ i A s
        returnˢ′  :  {s : S} → (a : A s) → IOˢ′ i A s

      data IOˢ+ (i : Size)  (A : S → Set α ) : S → Set (lsuc (α ⊔ σ ⊔ γ ⊔ ρ ))  where
        doˢ′ : {s : S} → (c : C s) (f : (r : R s c) → IOˢ i A  (next s c r))
            → IOˢ+ i A s

open IOˢ public

module _  {α σ γ ρ}{I   : IOInterfaceˢ {σ} {γ} {ρ}}
                   (let S = Stateˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextˢ I) where

  returnˢ : ∀{i}{A : S → Set α} {s : S} (a : A s) → IOˢ  I i A s
  forceˢ (returnˢ a) = returnˢ′ a

  doˢ  :  ∀{i}{A : S → Set α} {s : S}
          (c : C s) (f : (r : R s c) → IOˢ I i A (next s c r)) → IOˢ I i A s
  forceˢ (doˢ c f) = doˢ′ c f

module _  {σ γ}{I   : IOInterfaceˢ {σ} {γ} {lzero}}
                (let S = Stateˢ I)     (let C  = Commandˢ I)
                (let  R  = Responseˢ I) (let next = nextˢ I) where
  {-# NON_TERMINATING #-}

  translateIOˢ : ∀{A : Set }{s : S}
    →  (translateLocal : (s : S) → (c : C s) → NativeIO (R s c))
    →  IOˢ I ∞ (λ s → A) s
    →  NativeIO A

  translateIOˢ {A} {s} translateLocal p = case (forceˢ p {_}) of
    λ{ (doˢ′ {.s} c f)    → (translateLocal s c)     native>>= λ r →
                             translateIOˢ translateLocal (f r)
     ; (returnˢ′ a) → nativeReturn a
     }

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Tree where

open import Data.Vec
open import Data.Nat

data Head : Set where
  H : Head

infixr 5 _⇒_
data Expr : Set where
  S   :                             Expr -- something
  _⇒_ :               Expr → Expr → Expr -- "->" expression
  E   : Head → ∀{n} →  Vec Expr n → Expr -- arbitrary expression

-- the termination checker is very unhappy with this one
leftBalance : Expr → Expr
leftBalance S                 = S
leftBalance (e ⇒ S)           = e ⇒ S
leftBalance (e ⇒ (f ⇒ g))     = leftBalance ((leftBalance (e ⇒ f)) ⇒ g)
leftBalance (e ⇒ E H [])      = (e ⇒ E H [])
leftBalance (e ⇒ E H (a ∷ x)) = E H (leftBalance (leftBalance e ⇒ a) ∷ (map leftBalance x))
leftBalance (E H x)           = E H (map leftBalance x)

-- leftBalance (e ⇒ E H (a ∷ x)) = E H ((leftBalance (e ⇒ a)) ∷ (map leftBalance x))


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

module Categories.NaturalTransformation.NaturalIsomorphism where

open import Level
open import Data.Product using (_×_; _,_; map; zip)
open import Function using (flip)

open import Categories.Category
open import Categories.Functor as ℱ renaming (id to idF)
import Categories.NaturalTransformation as NT
open NT hiding (id)
import Categories.Morphism as Morphism
import Categories.Morphism.Properties as Morphismₚ
import Categories.Morphism.Reasoning as MR
open import Categories.Functor.Properties

open import Relation.Binary

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    B C D E : Category o ℓ e

record NaturalIsomorphism {C : Category o ℓ e}
                          {D : Category o′ ℓ′ e′}
                          (F G : Functor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

  private
    module F = Functor F
    module G = Functor G

  field
    F⇒G : NaturalTransformation F G
    F⇐G : NaturalTransformation G F

  module ⇒ = NaturalTransformation F⇒G
  module ⇐ = NaturalTransformation F⇐G

  field
    iso : ∀ X → Morphism.Iso D (⇒.η X) (⇐.η X)

  module iso X = Morphism.Iso (iso X)

  open Morphism D

  FX≅GX : ∀ {X} → F.F₀ X ≅ G.F₀ X
  FX≅GX {X} = record
    { from = _
    ; to   = _
    ; iso  = iso X
    }

  op : NaturalIsomorphism G.op F.op
  op = record
    { F⇒G = ⇒.op
    ; F⇐G = ⇐.op
    ; iso = λ X → record
      { isoˡ = iso.isoʳ X
      ; isoʳ = iso.isoˡ X
      }
    }

  op′ : NaturalIsomorphism F.op G.op
  op′ = record
    { F⇒G = ⇐.op
    ; F⇐G = ⇒.op
    ; iso = λ X → record
      { isoˡ = iso.isoˡ X
      ; isoʳ = iso.isoʳ X
      }
    }

-- This helper definition lets us specify only one of the commuting
-- squares and have the other one derived.

record NIHelper {C : Category o ℓ e}
                {D : Category o′ ℓ′ e′}
                (F G : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  open Functor F using (F₀; F₁)
  open Functor G using () renaming (F₀ to G₀; F₁ to G₁)
  open Category D
  field
    η           : ∀ X → D [ F₀ X , G₀ X ]
    η⁻¹         : ∀ X → D [ G₀ X , F₀ X ]
    commute     : ∀ {X Y} (f : C [ X , Y ]) → η Y ∘ F₁ f ≈ G₁ f ∘ η X
    iso         : ∀ X → Morphism.Iso D (η X) (η⁻¹ X)

niHelper : ∀ {F G : Functor C D} → NIHelper F G → NaturalIsomorphism F G
niHelper {D = D} {F = F} {G = G} α = record
  { F⇒G = ntHelper record { η = η ; commute = commute }
  ; F⇐G = ntHelper record
    { η = η⁻¹
    ; commute = λ {X Y} f → begin
        η⁻¹ Y ∘ F₁ G f                     ≈˘⟨ cancelʳ (isoʳ (iso X)) ⟩
        ((η⁻¹ Y ∘ F₁ G f) ∘ η X) ∘ η⁻¹ X   ≈˘⟨ pushʳ (commute f) ⟩∘⟨refl ⟩
        (η⁻¹ Y ∘ (η Y ∘ F₁ F f)) ∘ η⁻¹ X   ≈⟨ cancelˡ (isoˡ (iso Y)) ⟩∘⟨refl ⟩
        F₁ F f ∘ η⁻¹ X                     ∎
    }
  ; iso = iso
  }
  where
    open Morphism.Iso
    open NIHelper α
    open Functor
    open Category D
    open HomReasoning
    open MR D

open NaturalIsomorphism

infixr 9 _ⓘᵥ_ _ⓘₕ_ _ⓘˡ_ _ⓘʳ_
infix 4 _≃_

-- commonly used short-hand in CT for NaturalIsomorphism
_≃_ : (F G : Functor C D) → Set _
_≃_ = NaturalIsomorphism

_ⓘᵥ_ : {F G H : Functor C D} → G ≃ H → F ≃ G → F ≃ H
_ⓘᵥ_ {D = D} α β = record
  { F⇒G = F⇒G α ∘ᵥ F⇒G β
  ; F⇐G = F⇐G β ∘ᵥ F⇐G α
  ; iso = λ X → Iso-∘ (iso β X) (iso α X)
  }
  where open NaturalIsomorphism
        open Morphismₚ D

_ⓘₕ_ : {H I : Functor D E} {F G : Functor C D} → H ≃ I → F ≃ G → (H ∘F F) ≃ (I ∘F G)
_ⓘₕ_ {E = E} {I = I} α β = record
  { F⇒G = F⇒G α ∘ₕ F⇒G β
  ; F⇐G = F⇐G α ∘ₕ F⇐G β
  ; iso = λ X → Iso-resp-≈ (Iso-∘ (iso α _) ([ I ]-resp-Iso (iso β X)))
                           E.Equiv.refl (commute (F⇐G α) (η (F⇐G β) X))
  }
  where open NaturalIsomorphism
        open NaturalTransformation
        module E = Category E
        open E.Equiv
        open Morphismₚ E

_ⓘˡ_ : {F G : Functor C D} → (H : Functor D E) → (η : F ≃ G) → H ∘F F ≃ H ∘F G
H ⓘˡ η = record
  { F⇒G = H ∘ˡ F⇒G η
  ; F⇐G = H ∘ˡ F⇐G η
  ; iso = λ X → [ H ]-resp-Iso (iso η X)
  }
  where open Functor H

_ⓘʳ_ : {F G : Functor C D} → (η : F ≃ G) → (K : Functor E C) → F ∘F K ≃ G ∘F K
η ⓘʳ K = record
  { F⇒G = F⇒G η ∘ʳ K
  ; F⇐G = F⇐G η ∘ʳ K
  ; iso = λ X → iso η (F₀ X)
  }
  where open Functor K

refl : Reflexive (NaturalIsomorphism {C = C} {D = D})
refl {D = D} = record
  { F⇒G = NT.id
  ; F⇐G = NT.id
  ; iso = λ _ → record
    { isoˡ = Category.identityˡ D
    ; isoʳ = Category.identityʳ D
    }
  }

sym : Symmetric (NaturalIsomorphism {C = C} {D = D})
sym {D = D} F≃G = record
  { F⇒G = F⇐G F≃G
  ; F⇐G = F⇒G F≃G
  ; iso = λ X →
    let open Iso (iso F≃G X) in record
    { isoˡ = isoʳ
    ; isoʳ = isoˡ
    }
  }
  where open Morphism D

trans : Transitive (NaturalIsomorphism {C = C} {D = D})
trans = flip _ⓘᵥ_

isEquivalence : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → IsEquivalence (NaturalIsomorphism {C = C} {D = D})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

module ≃ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} = IsEquivalence (isEquivalence {C = C} {D = D})

Functor-NI-setoid : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Setoid _ _
Functor-NI-setoid C D = record
  { Carrier       = Functor C D
  ; _≈_           = NaturalIsomorphism
  ; isEquivalence = isEquivalence
  }

module LeftRightId (F : Functor C D) where
  module D = Category D

  iso-id-id : (X : Category.Obj C) → Morphism.Iso D {A = Functor.F₀ F X} D.id D.id
  iso-id-id X = record { isoˡ = D.identityˡ ; isoʳ = D.identityʳ }

-- Left and Right and 'Central' Unitors, Natural Isomorphisms.
module _ {F : Functor C D} where
  open Category.HomReasoning D
  open Functor F
  open LeftRightId F
  open Category D

  unitorˡ : ℱ.id ∘F F ≃ F
  unitorˡ = record { F⇒G = id∘F⇒F ; F⇐G = F⇒id∘F ; iso = iso-id-id }

  unitorʳ : F ∘F ℱ.id ≃ F
  unitorʳ = record { F⇒G = F∘id⇒F ; F⇐G = F⇒F∘id ; iso = iso-id-id }

unitor² : {C : Category o ℓ e} → ℱ.id ∘F ℱ.id ≃ ℱ.id {C = C}
unitor² = record { F⇒G = id∘id⇒id ; F⇐G = id⇒id∘id ; iso = LeftRightId.iso-id-id ℱ.id }

-- associator
module _ (F : Functor B C) (G : Functor C D) (H : Functor D E) where
  open Category.HomReasoning E
  open Category E
  open Functor
  open LeftRightId (H ∘F (G ∘F F))

  private
    -- components of α
    assocʳ : NaturalTransformation ((H ∘F G) ∘F F) (H ∘F (G ∘F F))
    assocʳ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E  }

    assocˡ : NaturalTransformation (H ∘F (G ∘F F)) ((H ∘F G) ∘F F)
    assocˡ = ntHelper record { η = λ _ → id ; commute = λ _ → MR.id-comm-sym E }

  associator : (H ∘F G) ∘F F ≃ H ∘F (G ∘F F)
  associator = record { F⇒G = assocʳ ; F⇐G = assocˡ ; iso = iso-id-id }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Point where

open import Nat
open import Bool

-- A record can be seen as a one constructor datatype. In this case:
data Point' : Set where
  mkPoint : (x : Nat)(y : Nat) -> Point'

getX : Point' -> Nat
getX (mkPoint x y) = x

getY : Point' -> Nat
getY (mkPoint x y) = y


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Groups.Definition

module Rings.Orders.Total.Bounded {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (tRing : TotallyOrderedRing pRing) where

open import Rings.Orders.Partial.Bounded pRing
open Ring R
open Group additiveGroup
open import Groups.Lemmas (Ring.additiveGroup R)
open Setoid S
open Equivalence eq
open SetoidPartialOrder pOrder
open import Rings.Orders.Total.Lemmas tRing
open PartiallyOrderedRing pRing

boundGreaterThanZero : {s : Sequence A} → (b : Bounded s) → 0G < underlying b
boundGreaterThanZero {s} (a , b) with b 0
... | (l ,, r) = halvePositive a (<WellDefined invLeft reflexive (orderRespectsAddition (<Transitive l r) a))


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

module Ch2-2 where

open import Ch2-1

open import Level

-- Lemma 2.2.1 (ap)
ap : ∀ {a b} {A : Set a} {B : Set b} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → f x ≡ f y
ap {a} {b} {A} {B} {x} {y} f p = J {a} {a ⊔ b} A D d x y p f
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set (a ⊔ b)
    D x y p = (f : A → B) → f x ≡ f y

    -- base case
    d : (x : A) → D x x refl
    d x f = refl

-- ap2 : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} {x y : A} {z w : B}
--   → (f : A → B → C) (p : x ≡ y) (q : z ≡ w)
--   → f x z ≡ f y w
-- ap2 {a} {b} {c} {A} {B} {C} {x} {y} {z} {w} f p q = J A D d x y p z w q f
--   where
--     -- the predicate
--     D : (x y : A) (p : x ≡ y) → Set _
--     D x y p = (a b : B) (q : z ≡ w) (f : A → B → C) → f x z ≡ f y w
--
--     -- base case
--     d : (x : A) → D x x refl
--     d x z w q f = ap (f x) q

[_]∙ : ∀ {a} {A : Set a} {x y z : A}
  → (p : x ≡ y) (q : y ≡ z)
  → x ≡ z
[ p ]∙ q = p ∙ q

∙[_] : ∀ {a} {A : Set a} {x y z : A}
  → (q : y ≡ z) (p : x ≡ y)
  → x ≡ z
∙[ p ] q = q ∙ p

-- -- -- cong₂ ::
-- [_]∙[_] : ∀ {a} {A : Set a} {x y z : A}
--   → (p q : x ≡ y) (r s : y ≡ z)
--   → p ∙ r ≡ q ∙ s
-- [_]∙[_] {a} {A} {x} {y} {z} p q r s = {! ap2  !}

ap-refl : ∀ {a b} {A : Set a} {B : Set b} {x : A}
  → (f : A → B)
  → ap {a} {b} {A} {B} {x} f refl ≡ refl
ap-refl f = refl

-- Lemma 2.2.2.i (ap respects _∙_)
ap-∙ : ∀ {a b} {A : Set a} {B : Set b} {x y z : A}
  → (f : A → B)
  → (p : x ≡ y) (q : y ≡ z)
  → ap f (p ∙ q) ≡ ap f p ∙ ap f q
ap-∙ {a} {b} {A} {B} {x} {y} {z} f p q = J A D d x y p f z q
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (f : A → B) (z : A) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q

    -- base case
    d : (x : A) → D x x refl
    d x f z q = J A E e x z q
      where
      -- the predicate
      E : (x z : A) (q : x ≡ z) → Set _
      E x z q = ap f (refl ∙ q) ≡ ap f refl ∙ ap f q
      -- base case
      e : (x : A) → E x x refl
      e x = refl

-- Lemma 2.2.2.ii (ap respects ¬_)
ap-¬ : ∀ {a b} {A : Set a} {B : Set b} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → ap f (¬ p) ≡ ¬ ap f p
ap-¬ {a} {b} {A} {B} {x} {y} f p = J A D d x y p f
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (f : A → B) → ap f (¬ p) ≡ ¬ ap f p

    -- base case
    d : (x : A) → D x x refl
    d x f = refl

open import Function using (_∘_; id)

-- Lemma 2.2.2.iii (ap respects function compos)
ap-∘ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} {x y : A}
  → (f : A → B) (g : B → C)
  → (p : x ≡ y)
  → ap g (ap f p) ≡ ap (g ∘ f) p
ap-∘ {_} {_} {_} {A} {B} {C} {x} {y} f g p = J A D d x y p f g
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (f : A → B) → (g : B → C) → ap g (ap f p) ≡ ap (g ∘ f) p

    -- base case
    d : (x : A) → D x x refl
    d x f g = refl

-- Lemma 2.2.2.iv (ap respects identity function)
ap-id : ∀ {a} {A : Set a} {x y : A}
  → (p : x ≡ y)
  → ap id p ≡ p
ap-id {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = ap id p ≡ p

    -- base case
    d : (x : A) → D x x refl
    d x = refl

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
------------------------------------------------------------------------
-- Well-typed binary relations lifted to substitutions
------------------------------------------------------------------------

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

module Data.Fin.Substitution.TypedRelation where

open import Data.Context hiding (map)
open import Data.Context.WellFormed
open import Data.Fin using (Fin; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product as Prod using (_×_; _,_)
open import Data.Vec as Vec using (_∷_; map; zip; unzip)
open import Data.Vec.Properties
open import Function using (flip)
open import Level using (_⊔_) renaming (zero to lzero; suc to lsuc)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Abstract typed binary relations lifted point-wise to substitutions

-- A shorthand.

infixr 2 _⊗_

_⊗_ : ∀ {t₁ t₂ } → Pred ℕ t₁ → Pred ℕ t₂ → Pred ℕ (t₁ ⊔ t₂)
(T₁ ⊗ T₂) n = T₁ n × T₂ n

-- Abstract typed binary relations on terms.
--
-- An abtract typed term relation _⊢_∼_∈_ : TypedRel Bnd Term₁ Term₂
-- Type is a four-place relation which, in a given Bnd-context,
-- relates Term₁ to Term₂-terms and their Type-types.

-- An abtract typing judgment _⊢_∈_ : Typing Bnd Term Type is a
-- ternary relation which, in a given Bnd-context, relates Term-terms
-- to their Type-types.

TypedRel : ∀ {t₁ t₂ t₃ t₄} →
         Pred ℕ t₁ → Pred ℕ t₂ → Pred ℕ t₃ → Pred ℕ t₄ → ∀ ℓ →
         Set (t₁ ⊔ t₂ ⊔ t₃ ⊔ t₄ ⊔ lsuc ℓ)
TypedRel Bnd Term₁ Term₂ Type ℓ =
  ∀ {n} → Ctx Bnd n → Term₁ n → Term₂ n → Type n → Set ℓ

module _ {t₁ t₂ t₃ t₄ ℓ} {Bnd : Pred ℕ t₁}
         {Term₁ : Pred ℕ t₂} {Term₂ : Pred ℕ t₃} {Type : Pred ℕ t₄} where

  -- The following maps witness the obvious correspondence between typed
  -- relations on Term₁ and Term₂ terms and typings of Term₁-Term₂ pairs.

  toTyping : TypedRel Bnd Term₁ Term₂ Type ℓ →
             Typing Bnd (Term₁ ⊗ Term₂) Type ℓ
  toTyping _⊢_∼_∈_ Γ = Prod.uncurry (_⊢_∼_∈_ Γ)

  fromTyping : Typing Bnd (Term₁ ⊗ Term₂) Type ℓ →
               TypedRel Bnd Term₁ Term₂ Type ℓ
  fromTyping _⊢_∈_ Γ = Prod.curry (_⊢_∈_ Γ)

record TypedRelation {t}
                     (Type : Pred ℕ t)      -- Type syntax
                     (Term : Pred ℕ lzero)  -- Term syntax
                     ℓ
                     : Set (lsuc (t ⊔ ℓ)) where

  infix 4 _⊢_∼_∈_ _⊢_wf

  field
    _⊢_wf   : Wf Type Type ℓ                   -- Type formation judgment
    _⊢_∼_∈_ : TypedRel Type Term Term Type ℓ   -- Typed relation judgment

------------------------------------------------------------------------
-- Abstract typed term relations lifted point-wise to substitutions

record TypedSubRel {t}
                   (Type : Pred ℕ t)      -- Type syntax
                   (Term : Pred ℕ lzero)  -- Term syntax
                   ℓ
                   : Set (lsuc (t ⊔ ℓ)) where

  -- The underlying typed relation

  field typedRelation : TypedRelation Type Term ℓ

  open TypedRelation typedRelation public

  -- Weakening and term substitutions in types.

  field
    typeExtension       : Extension Type                  -- type weakening
    typeTermApplication : Application Type (Term ⊗ Term)  -- term subst. app.
    termSimple          : Simple Term                     -- simple term subst.

  open ContextFormation _⊢_wf          using (_wf)
  open Application typeTermApplication using (_/_)

  -- We associate with every typed relation _⊢_∼_∈_ lifted to a pair
  -- of Term-substitutions a single typed substitution of pairs of
  -- Term-terms.

  termPairSimple : Simple (Term ⊗ Term)
  termPairSimple = record
    { var    = Prod.< var , var >
    ; weaken = Prod.map weaken weaken
    }
    where open Simple termSimple

  typedSub : TypedSub Type (Term ⊗ Term) ℓ
  typedSub = record
    { _⊢_wf               = _⊢_wf
    ; _⊢_∈_               = toTyping _⊢_∼_∈_
    ; typeExtension       = typeExtension
    ; typeTermApplication = typeTermApplication
    ; termSimple          = termPairSimple
    }

  open TypedSub typedSub using (_⊢_∈_; _⊢/_∈_; /∈-wf) public

  infix  4 _⊢/_∼_∈_

  -- Typed relations lifted to substitutions.
  --
  -- A typed substitution relation Δ ⊢/ σ ∼ ρ ∈ Γ is a pair σ, ρ of
  -- substitutions which, when applied to related terms Γ ⊢ s ∼ t ∈ a
  -- in a source context Γ, yield related well-typed terms Δ ⊢ s / σ ∼
  -- t / ρ ∈ a / zip σ ρ in a well-formed target context Δ.

  _⊢/_∼_∈_ : ∀ {m n} →
             Ctx Type n → Sub Term m n → Sub Term m n → Ctx Type m →
             Set (t ⊔ ℓ)
  Δ ⊢/ σ ∼ ρ ∈ Γ = Δ ⊢/ zip σ ρ ∈ Γ

------------------------------------------------------------------------
-- Operations on abstract well-typed substitutions

-- Helpers functions for relating extensions of (untyped) zipped
-- substitutions to their projections.

module ZipUnzipExtension {Tm₁ Tm₂ : ℕ → Set}
                         (ext₁ : Extension Tm₁)
                         (ext₂ : Extension Tm₂)
                         where

  private
    module E₁ = Extension ext₁
    module E₂ = Extension ext₂

  -- Extensions of (untyped) Tm⊗Tm substitutions.
  zippedExtension : Extension (Tm₁ ⊗ Tm₂)
  zippedExtension = record { weaken = Prod.map E₁.weaken E₂.weaken }
  open Extension zippedExtension

  -- Some useful shorthands

  π₁ : ∀ {n m} → Sub (Tm₁ ⊗ Tm₂) m n → Sub Tm₁ m n
  π₁ σ = Prod.proj₁ (unzip σ)

  π₂ : ∀ {n m} → Sub (Tm₁ ⊗ Tm₂) m n → Sub Tm₂ m n
  π₂ σ = Prod.proj₂ (unzip σ)

  -- π₁ and π₂ are projections (w.r.t. zipping)

  π₁-zip : ∀ {n m} (σ : Sub Tm₁ m n) (τ : Sub Tm₂ m n) → π₁ (zip σ τ) ≡ σ
  π₁-zip σ τ = cong Prod.proj₁ (unzip∘zip σ τ)

  π₂-zip : ∀ {n m} (σ : Sub Tm₁ m n) (τ : Sub Tm₂ m n) → π₂ (zip σ τ) ≡ τ
  π₂-zip σ τ = cong Prod.proj₂ (unzip∘zip σ τ)

  -- Weakening commutes with zipping and unzipping.

  map-weaken-zip : ∀ {m n} (σ : Sub Tm₁ m n) τ →
                   Vec.map weaken (zip σ τ) ≡
                     zip (Vec.map E₁.weaken σ) (Vec.map E₂.weaken τ)
  map-weaken-zip σ τ = map-zip E₁.weaken E₂.weaken σ τ

  map-weaken-unzip : ∀ {m n} (στ : Sub (Tm₁ ⊗ Tm₂) m n) →
                     (Vec.map E₁.weaken (π₁ στ) , Vec.map E₂.weaken (π₂ στ)) ≡
                       unzip (Vec.map weaken στ)
  map-weaken-unzip στ = map-unzip E₁.weaken E₂.weaken στ

  -- Extension commutes with zipping and unzipping.

  /∷-zip : ∀ {m n s t} (σ : Sub Tm₁ m n) τ →
           (s , t) /∷ zip σ τ ≡ zip (s E₁./∷ σ) (t E₂./∷ τ)
  /∷-zip σ τ = cong (_∷_ _) (map-weaken-zip σ τ)

  /∷-unzip : ∀ {m n s t} (στ : Sub (Tm₁ ⊗ Tm₂) m n) →
             (s E₁./∷ π₁ στ , t E₂./∷ π₂ στ) ≡ unzip ((s , t) /∷ στ)
  /∷-unzip στ = cong (Prod.map (_∷_ _) (_∷_ _)) (map-weaken-unzip στ)

-- Operations on related abstract typed substitutions that require
-- weakening of derivations of the typed relation

record TypedRelWeakenOps {t ℓ} {Type : Pred ℕ t} {Term : Pred ℕ lzero}
                         (typedSubRel : TypedSubRel Type Term ℓ)
                         : Set (lsuc (t ⊔ ℓ)) where

  open TypedSubRel      typedSubRel
  open ContextFormation _⊢_wf               using (_wf)
  open Application      typeTermApplication using (_/_)

  -- Operations on contexts and raw terms that require weakening

  private
    termExtension : Extension Term
    termExtension = record { weaken = Simple.weaken termSimple }

    module E = Extension termExtension
    module C = WeakenOps typeExtension
    module P = Simple    termPairSimple

  field

    -- Weakening preserves well-typed terms.

    ∼∈-weaken : ∀ {n} {Δ : Ctx Type n} {t u a b} →
                Δ ⊢ a wf → Δ ⊢ t ∼ u ∈ b →
                (a ∷ Δ) ⊢ E.weaken t ∼ E.weaken u ∈ C.weaken b

    -- Well-typedness implies well-formedness of contexts.

    ∼∈-wf : ∀ {n} {Δ : Ctx Type n} {t u a} → Δ ⊢ t ∼ u ∈ a → Δ wf

    -- Lemmas relating type weakening to term substitutions

    /-wk : ∀ {n} {a : Type n} → a / P.wk ≡ C.weaken a

    /-weaken : ∀ {m n} {στ : Sub (Term ⊗ Term) m n} a →
               a / Vec.map P.weaken στ ≡ a / στ / P.wk

    weaken-/-∷ : ∀ {n m} {tu} {στ : Sub (Term ⊗ Term) m n} (a : Type m) →
                 C.weaken a / (tu ∷ στ) ≡ a / στ

  -- Operations on the underlying abstract typed substitutions that
  -- require weakening.

  typedWeakenOps : TypedWeakenOps typedSub
  typedWeakenOps = record
    { ∈-weaken   = ∼∈-weaken
    ; ∈-wf       = ∼∈-wf
    ; /-wk       = /-wk
    ; /-weaken   = /-weaken
    ; weaken-/-∷ = weaken-/-∷
    }

  open TypedWeakenOps typedWeakenOps using (∈-/∷)
  open ZipUnzipExtension termExtension termExtension using (/∷-zip)

  -- Look up a pair of related entries in a pair of related
  -- substitutions.

  lookup : ∀ {m n Δ} {σ τ : Sub Term m n} {Γ} →
           Δ ⊢/ σ ∼ τ ∈ Γ → (x : Fin m) →
           Δ ⊢ Vec.lookup σ x ∼ Vec.lookup τ x ∈ C.lookup Γ x / zip σ τ
  lookup {σ = σ} {τ} σ∼τ∈Γ x =
    subst₂ (toTyping _⊢_∼_∈_ _) (lookup-zip x σ τ) refl
           (TypedWeakenOps.lookup typedWeakenOps σ∼τ∈Γ x)

  -- Extension by a pair of related typed terms.

  ∼∈-/∷ : ∀ {m n Γ} {σ τ : Sub Term m n} {Δ t u a b} →
          b ∷ Δ ⊢ t ∼ u ∈ C.weaken (a / zip σ τ) → Δ ⊢/ σ ∼ τ ∈ Γ →
          b ∷ Δ ⊢/ (t E./∷ σ) ∼ (u E./∷ τ) ∈ a ∷ Γ
  ∼∈-/∷ t∼u∈a/στ σ∼τ∈Γ =
    subst (flip (_⊢/_∈_ _) _) (/∷-zip _ _) (∈-/∷ t∼u∈a/στ σ∼τ∈Γ)

-- Helpers functions for relating simple (untyped) zipped
-- substitutions to their projections.

module ZipUnzipSimple {Tm₁ Tm₂ : ℕ → Set}
                      (simple₁ : Simple Tm₁)
                      (simple₂ : Simple Tm₂)
                      where

  private
    module S₁ = SimpleExt simple₁
    module S₂ = SimpleExt simple₂

  open ZipUnzipExtension S₁.extension S₂.extension public

  -- Simple (untyped) Tm⊗Tm substitutions.
  zippedSimple : Simple (Tm₁ ⊗ Tm₂)
  zippedSimple = record
    { weaken = Prod.map S₁.weaken S₂.weaken
    ; var    = λ x → S₁.var x , S₂.var x
    }
  open SimpleExt zippedSimple

  -- Lifting commutes with zipping.

  ↑-zip : ∀ {m n} (σ : Sub Tm₁ m n) τ →
          zip σ τ ↑ ≡ zip (σ S₁.↑) (τ S₂.↑)
  ↑-zip σ τ = /∷-zip σ τ

  ↑⋆-zip : ∀ {m n} (σ : Sub Tm₁ m n) τ k →
           zip σ τ ↑⋆ k ≡ zip (σ S₁.↑⋆ k) (τ S₂.↑⋆ k)
  ↑⋆-zip σ τ zero    = refl
  ↑⋆-zip σ τ (suc k) = cong (var zero ∷_) (begin
      map weaken (zip σ τ ↑⋆ k)
    ≡⟨ cong (map weaken) (↑⋆-zip σ τ k) ⟩  --
      map weaken (zip (σ S₁.↑⋆ k) (τ S₂.↑⋆ k))
    ≡⟨ map-weaken-zip (σ S₁.↑⋆ k) (τ S₂.↑⋆ k) ⟩
      zip (map S₁.weaken (σ S₁.↑⋆ k)) (map S₂.weaken (τ S₂.↑⋆ k))
    ∎)

  -- Lifting commutes with unzipping.
  ↑-unzip : ∀ {m n} (σ : Sub (Tm₁ ⊗ Tm₂) m n) →
            (π₁ σ S₁.↑ , π₂ σ S₂.↑) ≡ unzip (σ ↑)
  ↑-unzip σ = /∷-unzip σ

  -- Zipping preserves identity substitutions.
  id-zip : ∀ {n} → id {n} ≡ zip S₁.id S₂.id
  id-zip {zero}  = refl
  id-zip {suc n} = begin
    id {n} ↑                         ≡⟨ cong _↑ id-zip ⟩
    (zip S₁.id S₂.id) ↑              ≡⟨ ↑-zip S₁.id S₂.id ⟩
    zip (S₁.id S₁.↑) (S₂.id S₂.↑)    ∎

  -- Unzipping preserves identity substitutions.
  id-unzip : ∀ {n} → (S₁.id , S₂.id) ≡ unzip (id {n})
  id-unzip {zero}  = refl
  id-unzip {suc n} = begin
    (S₁.id S₁.↑ , S₂.id S₂.↑)   ≡⟨ cong (Prod.map S₁._↑ S₂._↑) id-unzip ⟩
    (π₁ id S₁.↑ , π₂ id S₂.↑)   ≡⟨ ↑-unzip id ⟩
    unzip (id {n} ↑)            ∎

  -- Zipping preserves weakening substitutions.
  wk-zip : ∀ {n} → wk {n} ≡ zip S₁.wk S₂.wk
  wk-zip {n} = begin
      map weaken id
    ≡⟨ cong (map weaken) id-zip ⟩
      map weaken (zip S₁.id S₂.id)
    ≡⟨ map-zip S₁.weaken S₂.weaken _ _ ⟩
      zip (map S₁.weaken S₁.id) (map S₂.weaken S₂.id)
    ∎

  -- Unzipping preserves weakening substitutions.
  wk-unzip : ∀ {n} → (S₁.wk , S₂.wk) ≡ unzip (wk {n})
  wk-unzip {n} = begin
      (map S₁.weaken S₁.id , map S₂.weaken S₂.id)
    ≡⟨ cong (Prod.map (map S₁.weaken) (map S₂.weaken)) id-unzip ⟩
      (map S₁.weaken (π₁ id) , map S₂.weaken (π₂ id))
    ≡⟨ map-unzip S₁.weaken S₂.weaken id ⟩
      unzip (map weaken id)
    ∎

  -- Zipping preserves sigle-variable substitutions.
  sub-zip : ∀ {n} (s : Tm₁ n) t → sub (s , t) ≡ zip (S₁.sub s) (S₂.sub t)
  sub-zip s t = cong (_∷_ (s , t)) id-zip

  -- Unzipping preserves sigle-variable substitutions.
  sub-unzip : ∀ {n} (s : Tm₁ n) t → (S₁.sub s , S₂.sub t) ≡ unzip (sub (s , t))
  sub-unzip s t = cong (Prod.map (_∷_ s) (_∷_ t)) id-unzip

-- Operations on abstract typed substitutions that require simple term
-- substitutions

record TypedRelSimple {t ℓ} {Type : Pred ℕ t} {Term : Pred ℕ lzero}
                      (typedSubRel : TypedSubRel Type Term ℓ)
                      : Set (lsuc (t ⊔ ℓ)) where

  -- Operations on related abstract typed substitutions that require
  -- weakening.

  field typedRelWeakenOps : TypedRelWeakenOps typedSubRel

  open TypedRelWeakenOps typedRelWeakenOps public
  open TypedSubRel       typedSubRel
  open ContextFormation  _⊢_wf               using (_wf; _⊢_wfExt)
  open Application       typeTermApplication using (_/_)

  private
    module S = Simple    termSimple
    module C = WeakenOps typeExtension
    module P = Simple    termPairSimple
  open S using (_↑; _↑⋆_; id; wk; sub)

  -- Context operations that require term substitutions in types.

  open SubstOps typeTermApplication termPairSimple using (_E/_)

  field

    -- Takes equal variables to well-typed related terms.

    ∼∈-var : ∀ {n} {Γ : Ctx Type n} →
             ∀ x → Γ wf → Γ ⊢ S.var x ∼ S.var x ∈ C.lookup Γ x

    -- Well-formedness of related types implies well-formedness of
    -- contexts.

    wf-wf : ∀ {n} {Γ : Ctx Type n} {a} → Γ ⊢ a wf → Γ wf

    -- The identity substitution in types is an identity

    id-vanishes : ∀ {n} (a : Type n) → a / P.id ≡ a

  -- Operations on the underlying abstract typed substitutions that
  -- require simple typed term substitutions.

  typedSimple : TypedSimple typedSub
  typedSimple = record
    { typedWeakenOps = typedWeakenOps
    ; ∈-var          = ∼∈-var
    ; wf-wf          = wf-wf
    ; id-vanishes    = id-vanishes
    }

  open TypedSimple typedSimple using (∈-↑; ∈-↑⋆; ∈-id; ∈-wk; ∈-sub; ∈-tsub)
  open ZipUnzipSimple termSimple termSimple

  -- Lifting.

  ∼∈-↑ : ∀ {m n Δ} {σ τ : Sub Term m n} {a Γ} →
         Δ ⊢ a / zip σ τ wf → Δ ⊢/ σ ∼ τ ∈ Γ →
         a / zip σ τ ∷ Δ ⊢/ σ ↑ ∼ τ ↑ ∈ a ∷ Γ
  ∼∈-↑ a/στ-wf σ∼τΓ =
    subst (flip (_⊢/_∈_ _) _) (↑-zip _ _) (∈-↑ a/στ-wf σ∼τΓ)

  ∼∈-↑⋆ : ∀ {k m n Δ} {E : CtxExt Type m k} {σ τ : Sub Term m n} {Γ} →
          Δ ⊢ (E E/ zip σ τ) wfExt → Δ ⊢/ σ ∼ τ ∈ Γ →
          (E E/ zip σ τ) ++ Δ ⊢/ σ ↑⋆ k ∼ τ ↑⋆ k ∈ (E ++ Γ)
  ∼∈-↑⋆ {k} E/στ-wfExt σ∼τ∈Γ =
    subst (flip (_⊢/_∈_ _) _) (↑⋆-zip _ _ k) (∈-↑⋆ E/στ-wfExt σ∼τ∈Γ)

  -- The identity substitution.

  ∼∈-id : ∀ {n} {Γ : Ctx Type n} → Γ wf → Γ ⊢/ id ∼ id ∈ Γ
  ∼∈-id Γ-wf = subst (flip (_⊢/_∈_ _) _) id-zip (∈-id Γ-wf)

  -- Weakening.

  ∼∈-wk : ∀ {n} {Γ : Ctx Type n} {a} → Γ ⊢ a wf → a ∷ Γ ⊢/ wk ∼ wk ∈ Γ
  ∼∈-wk a-wf = subst (flip (_⊢/_∈_ _) _) wk-zip (∈-wk a-wf)

  -- A substitution which only replaces the first variable.

  ∼∈-sub : ∀ {n} {Γ : Ctx Type n} {t u a} → Γ ⊢ t ∼ u ∈ a →
           Γ ⊢/ sub t ∼ sub u ∈ a ∷ Γ
  ∼∈-sub s∼t∈a =
    subst (flip (_⊢/_∈_ _) _) (sub-zip _ _) (∈-sub s∼t∈a)

  -- A substitution which only changes the type of the first variable.

  ∼∈-tsub : ∀ {n} {Γ : Ctx Type n} {a b} →
            b ∷ Γ ⊢ S.var zero ∼ S.var zero ∈ C.weaken a →
            b ∷ Γ ⊢/ id ∼ id ∈ a ∷ Γ
  ∼∈-tsub z∈a = subst (flip (_⊢/_∈_ _) _) id-zip (∈-tsub z∈a)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of interleaving using propositional equality
------------------------------------------------------------------------

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

module Data.List.Relation.Ternary.Interleaving.Propositional.Properties
  {a} {A : Set a} where

import Data.List.Relation.Ternary.Interleaving.Setoid.Properties
  as SetoidProperties
open import Relation.Binary.PropositionalEquality using (setoid)

------------------------------------------------------------------------
-- Re-exporting existing properties

open SetoidProperties (setoid A) public


text:
-- Andreas, 2012-07-01, issue reported by patrickATparcs.ath...
-- {-# OPTIONS -v tc.term.let.pattern:20 #-}
module Issue671 where

open import Common.Prelude

record Foo : Set where
  constructor foo
  field
    foo₁ : Nat

bar : Nat → Nat
bar a  = let
     b = a
     c = b
     foo x = foo 5
  in b
-- should succeed, used to throw a panic from Open'ing a let assigned value
-- in a wrong Context

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2020-02-15, issue #4447, reported by zraffer

record Wrap : Set₁ where
  constructor ↑
  field ↓ : Set
open Wrap public

data Unit : Set

-- The type checker sees through this definition,
-- thus, the positivity checker should as well:
𝕌nit = ↑ Unit

data Unit where
  unit : ↓ 𝕌nit

-- WAS: internal error in the positivity checker.

max_forks_repo_name: shlevy/agda


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

open import HoTT

module homotopy.OneSkeleton {i} {A : Type i} {j} {B : Type j} where

  private
    module _ (map : A → B) where
      data #OneSkeleton-aux : Type i where
        #point : A → #OneSkeleton-aux

      data #OneSkeleton : Type i where
        #one-skeleton : #OneSkeleton-aux → (Unit → Unit) → #OneSkeleton

  OneSkeleton : (A → B) → Type i
  OneSkeleton = #OneSkeleton

  module _ {map : A → B} where

    point : A → OneSkeleton map
    point a = #one-skeleton (#point a) _

    postulate  -- HIT
      link : ∀ a₁ a₂ → map a₁ == map a₂ → point a₁ == point a₂

    module OneSkeletonElim
      {l} {P : OneSkeleton map → Type l}
      (point* : ∀ a → P (point a))
      (link* : ∀ a₁ a₂ p → point* a₁ == point* a₂ [ P ↓ link a₁ a₂ p ]) where

      f : Π (OneSkeleton map) P
      f = f-aux phantom where

        f-aux : Phantom link* → Π (OneSkeleton map) P
        f-aux phantom (#one-skeleton (#point a) _) = point* a

      postulate
        link-β : ∀ a₁ a₂ p → apd f (link a₁ a₂ p) == link* a₁ a₂ p

    open OneSkeletonElim public using () renaming (f to OneSkeleton-elim)

    module OneSkeletonRec
      {l} {P : Type l}
      (point* : ∀ a → P)
      (link* : ∀ a₁ a₂ p → point* a₁ == point* a₂) where

      private
        module M = OneSkeletonElim point*
          (λ a₁ a₂ p → ↓-cst-in (link* a₁ a₂ p))

      f : OneSkeleton map → P
      f = M.f

      link-β : ∀ a₁ a₂ p → ap f (link a₁ a₂ p) == link* a₁ a₂ p
      link-β a₁ a₂ p = apd=cst-in {f = f} (M.link-β a₁ a₂ p)

    open OneSkeletonRec public using () renaming (f to OneSkeleton-rec)

    OneSkeleton-lift : OneSkeleton map → B
    OneSkeleton-lift = OneSkeleton-rec map (λ _ _ p → p)

{-
module _ {i} {A B : Set i} where
  skeleton₁ : (A → B) → Set i
  skeleton₁ f = Graveyard.skeleton₁ {i} {A} {B} {f}

-}

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.NaturalTransformation.Extranatural where

-- Although there is a notion of Extranatural in Categories.NaturalTransformation.Dinatural,
-- it isn't the most general form, thus the need for this as well.

open import Level
open import Data.Product
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

open import Categories.Category
open import Categories.NaturalTransformation as NT hiding (_∘ʳ_)
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Category.Product
import Categories.Morphism.Reasoning as MR

private
  variable
    o₁ o₂ o₃ o₄ ℓ₁ ℓ₂ ℓ₃ ℓ₄ e₁ e₂ e₃ e₄ : Level

record ExtranaturalTransformation
    {A : Category o₁ ℓ₁ e₁}
    {B : Category o₂ ℓ₂ e₂}
    {C : Category o₃ ℓ₃ e₃}
    {D : Category o₄ ℓ₄ e₄}
    (P : Functor (Product A (Product (Category.op B) B)) D)
    (Q : Functor (Product A (Product (Category.op C) C)) D) : Set (o₁ ⊔ o₂ ⊔ o₃ ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄ ⊔ e₄)  where

  private
    module A = Category A
    module B = Category B
    module C = Category C
    module D = Category D
    module P = Functor P
    module Q = Functor Q

  open D hiding (op)
  open Commutation D

  field
    α          : ∀ a b c → D [ P.₀ (a , (b , b)) , Q.₀ (a , (c , c)) ]
    commute    : ∀ {a a′ b b′ c c′} (f : A [ a , a′ ]) (g : B [ b , b′ ])
                  (h : C [ c , c′ ]) →
                [ P.₀ (a , (b′ , b) ) ⇒ Q.₀ (a′ , (c , c′)) ]⟨
                  P.₁ (f , B.id , g)         ⇒⟨ P.₀ (a′ , (b′ , b′)) ⟩
                  α a′ b′ c                  ⇒⟨ Q.₀ (a′ , (c , c)) ⟩
                  Q.₁ (A.id , C.id , h)
                ≈ P.₁ (A.id , g , B.id)      ⇒⟨ P.₀ (a , (b , b)) ⟩
                  α a b c′                   ⇒⟨ Q.₀ (a , (c′ , c′)) ⟩
                  Q.₁ (f , h , C.id)
                ⟩

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories