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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Irrelevance {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Tools.Empty using (⊥; ⊥-elim)

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView

open import Tools.Product
import Tools.PropositionalEquality as PE

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

-- Irrelevance for propositionally equal types
irrelevance′ : ∀ {A A′ Γ r l}
             → A PE.≡ A′
             → Γ ⊩⟨ l ⟩ A ^ r
             → Γ ⊩⟨ l ⟩ A′ ^ r
irrelevance′ PE.refl [A] = [A]

irrelevance′′ : ∀ {A A′ Γ r r' ll ll' l}
             → A PE.≡ A′
             → r PE.≡ r'
             → ll PE.≡ ll'
             → Γ ⊩⟨ l ⟩ A ^ [ r , ll ]
             → Γ ⊩⟨ l ⟩ A′ ^ [ r' , ll' ]
irrelevance′′ PE.refl PE.refl PE.refl [A] = [A]

-- Irrelevance for propositionally equal types and contexts
irrelevanceΓ′ : ∀ {l A A′ r Γ Γ′}
              → Γ PE.≡ Γ′
              → A PE.≡ A′
              → Γ  ⊩⟨ l ⟩ A ^ r
              → Γ′ ⊩⟨ l ⟩ A′ ^ r
irrelevanceΓ′ PE.refl PE.refl [A] = [A]

-- helper function to deal with relevance

reduction-irrelevant-Univ : ∀ {Γ A t l l' ll ll' l< l<' r r' el el' D D'}
        (e : r PE.≡ r') →
        Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r ll l< el D) →
        Γ ⊩⟨ l' ⟩ t ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r' ll' l<' el' D')
reduction-irrelevant-Univ {Γ} {A} {t} {ι ¹} {ι ¹} {⁰} {⁰} PE.refl (Uₜ K d typeK K≡K [t]) = Uₜ K d typeK K≡K [t]
reduction-irrelevant-Univ {Γ} {A} {t} {∞} {∞} {¹} {¹} PE.refl (Uₜ K d typeK K≡K [t]) = Uₜ K d typeK K≡K [t]

reduction-irrelevant-Univ= : ∀ {Γ A t u l l' ll ll' l< l<' r r' el el' D D'}
        (e : r PE.≡ r') →
        Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r ll l< el D) →
        Γ ⊩⟨ l' ⟩ t ≡ u ∷ A ^ [ ! , next ll ] / Uᵣ (Uᵣ r' ll' l<' el' D')
reduction-irrelevant-Univ= {l = ι ¹} {ι ¹} {⁰} {⁰} PE.refl (Uₜ₌ [t] [u] A≡B [t≡u]) = Uₜ₌ (reduction-irrelevant-Univ PE.refl [t]) (reduction-irrelevant-Univ PE.refl [u]) A≡B [t≡u]
reduction-irrelevant-Univ= {l = ∞} {∞} {¹} {¹} {l<} {l<'} PE.refl (Uₜ₌ [t] [u] A≡B [t≡u]) = Uₜ₌ (reduction-irrelevant-Univ PE.refl [t]) (reduction-irrelevant-Univ PE.refl [u]) A≡B [t≡u]

-- NB: for Pi cases it seems like it would be cleaner to do
-- irrelevanceFoo (Pi ...) rewrite whrDet* ...
-- instead of messing with PE.subst and irrelevanceEq′ etc
-- however for some reason the termination checker doesn't accept it

mutual
  -- Irrelevance for type equality
  irrelevanceEq : ∀ {Γ A B r l l′} (p : Γ ⊩⟨ l ⟩ A ^ r) (q : Γ ⊩⟨ l′ ⟩ A ^ r)
                → Γ ⊩⟨ l ⟩ A ≡ B ^ r / p → Γ ⊩⟨ l′ ⟩ A ≡ B ^ r / q
  irrelevanceEq p q A≡B = irrelevanceEqT (goodCasesRefl p q) A≡B

  -- Irrelevance for type equality with propositionally equal first types
  irrelevanceEq′ : ∀ {Γ A A′ B r r' l l′ ll ll'} (eq : A PE.≡ A′) (eqr : r PE.≡ r') (eql : ll PE.≡ ll')
                   (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                 → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ A′ ≡ B ^ [ r' , ll' ] / q
  irrelevanceEq′ PE.refl PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Irrelevance for type equality with propositionally equal types
  irrelevanceEq″ : ∀ {Γ A A′ B B′ r r' ll ll' l l′} (eqA : A PE.≡ A′) (eqB : B PE.≡ B′) (eqr : r PE.≡ r') (eql : ll PE.≡ ll')
                    (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                  → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ A′ ≡ B′ ^ [ r' , ll' ] / q
  irrelevanceEq″ PE.refl PE.refl PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Irrelevance for type equality with propositionally equal second types
  irrelevanceEqR′ : ∀ {Γ A B B′ r l} (eqB : B PE.≡ B′) (p : Γ ⊩⟨ l ⟩ A ^ r)
                  → Γ ⊩⟨ l ⟩ A ≡ B ^ r / p → Γ ⊩⟨ l ⟩ A ≡ B′ ^ r / p
  irrelevanceEqR′ PE.refl p A≡B = A≡B

  -- Irrelevance for type equality with propositionally equal types and
  -- a lifting of propositionally equal types
  irrelevanceEqLift″ : ∀ {Γ A A′ B B′ C C′ rC r l l′}
                        (eqA : A PE.≡ A′) (eqB : B PE.≡ B′) (eqC : C PE.≡ C′)
                        (p : Γ ∙ C ^ rC ⊩⟨ l ⟩ A ^ r) (q : Γ ∙ C′ ^ rC ⊩⟨ l′ ⟩ A′ ^ r)
                      → Γ ∙ C ^ rC ⊩⟨ l ⟩ A ≡ B ^ r / p → Γ ∙ C′ ^ rC ⊩⟨ l′ ⟩ A′ ≡ B′ ^ r / q
  irrelevanceEqLift″ PE.refl PE.refl PE.refl p q A≡B = irrelevanceEq p q A≡B

  -- Helper for irrelevance of type equality using shape view
  irrelevanceEqT : ∀ {Γ A B r l l′} {p : Γ ⊩⟨ l ⟩ A ^ r} {q : Γ ⊩⟨ l′ ⟩ A ^ r}
                       → ShapeView Γ l l′ A A r r p q
                       → Γ ⊩⟨ l ⟩ A ≡ B ^ r / p → Γ ⊩⟨ l′ ⟩ A ≡ B ^ r / q
  irrelevanceEqT (ℕᵥ D D′) A≡B = A≡B
  irrelevanceEqT (Emptyᵥ D D′) A≡B = A≡B
  irrelevanceEqT (ne (ne K D neK _) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
                 rewrite whrDet* (red D , ne neK) (red D₁ , ne neK₁) =
    ne₌ M D′ neM K≡M
  irrelevanceEqT {Γ} {r = r} (Πᵥ (Πᵣ 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′]) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , rF≡rF₁ , lF≡lF₁ , G≡G₁ , lG≡lG₁ , lΠ≡lΠ₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
    in  Π₌ F′ G′ (PE.subst₃ _ rF≡rF₁ lF≡lF₁ lG≡lG₁ D′)
        (PE.subst5 (λ x rx lx lx' lx'' → Γ ⊢ x ≅ Π F′ ^ rx ° lx ▹ G′ ° lx' ° lx'' ^ r) ΠFG≡ΠF₁G₁ rF≡rF₁ lF≡lF₁ lG≡lG₁ lΠ≡lΠ₁ A≡B)
           (λ {ρ} [ρ] ⊢Δ → irrelevanceEq′ (PE.cong (wk ρ) F≡F₁) rF≡rF₁ (PE.cong ι lF≡lF₁) ([F] [ρ] ⊢Δ)
                                          ([F]₁ [ρ] ⊢Δ)
                                          ([F≡F′] [ρ] ⊢Δ))
           (λ {ρ} [ρ] ⊢Δ [a]₁ →
              let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                         ([F]₁ [ρ] ⊢Δ)
                                         ([F] [ρ] ⊢Δ)
                                         [a]₁
              in  irrelevanceEq′ (PE.cong (λ y → wk (lift ρ) y [ _ ]) G≡G₁) PE.refl (PE.cong ι lG≡lG₁)
                                 ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([G≡G′] [ρ] ⊢Δ [a]))
  irrelevanceEqT {Γ} {r = r} (∃ᵥ (∃ᵣ 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′]) =
    let ∃FG≡∃F₁G₁   = whrDet* (red D , ∃ₙ) (red D₁ , ∃ₙ)
        F≡F₁ , G≡G₁ = ∃-PE-injectivity ∃FG≡∃F₁G₁
    in  ∃₌ F′ G′ D′
    (PE.subst (λ x → Γ ⊢ x ≅ ∃ F′ ▹ G′ ^ r) ∃FG≡∃F₁G₁ A≡B)
           (λ {ρ} [ρ] ⊢Δ → irrelevanceEq′ (PE.cong (wk ρ) F≡F₁) PE.refl PE.refl ([F] [ρ] ⊢Δ)
                                          ([F]₁ [ρ] ⊢Δ)
                                          ([F≡F′] [ρ] ⊢Δ))
           (λ {ρ} [ρ] ⊢Δ [a]₁ →
              let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.refl) (PE.refl)
                                         ([F]₁ [ρ] ⊢Δ)
                                         ([F] [ρ] ⊢Δ)
                                         [a]₁
              in  irrelevanceEq′ (PE.cong (λ y → wk (lift ρ) y [ _ ]) G≡G₁) PE.refl PE.refl
                                 ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([G≡G′] [ρ] ⊢Δ [a]))
  irrelevanceEqT (Uᵥ (Uᵣ _ _ _ PE.refl D) (Uᵣ _ _ _ e D')) A≡B = let U≡U  = whrDet* (red D , Uₙ) (red D' , Uₙ) in
                                                                let r≡r , l≡l = Univ-PE-injectivity U≡U in
                                                                 PE.subst _ l≡l (PE.subst _ r≡r A≡B)
  irrelevanceEqT (emb⁰¹ x) A≡B = irrelevanceEqT x A≡B
  irrelevanceEqT (emb¹⁰ x) A≡B = irrelevanceEqT x A≡B
  irrelevanceEqT (emb¹∞ x) A≡B = irrelevanceEqT x A≡B
  irrelevanceEqT (emb∞¹ x) A≡B = irrelevanceEqT x A≡B

  irrelevance-level : ∀ {A Γ r l l'}
                    → l <∞ l'
                    → Γ ⊩⟨ l ⟩ A ^ r
                    → Γ ⊩⟨ l' ⟩ A ^ r
  irrelevance-level l< (ℕᵣ x) = ℕᵣ x
  irrelevance-level l< (Emptyᵣ x) = Emptyᵣ x
  irrelevance-level l< (ne x) = ne x
  irrelevance-level l< (Πᵣ′ 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 (λ x ⊢Δ → irrelevance-level l< ([F] x ⊢Δ ))
                                                                          (λ [ρ] ⊢Δ x → irrelevance-level l< ([G] [ρ] ⊢Δ
                                                                             (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) x)))
                                                                           λ [ρ] ⊢Δ [a] [b] x →
                                                                           irrelevanceEq
                                                                                ([G] [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a]))
                                                                                (irrelevance-level l< ([G] [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a])))
                                                                                (G-ext [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a])
                                                                                (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [b])
                                                                                (irrelevanceEqTerm (irrelevance-level l< ([F] [ρ] ⊢Δ )) ([F] [ρ] ⊢Δ) x))
  irrelevance-level l< (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) = ∃ᵣ′ F G D ⊢F ⊢G A≡A (λ x ⊢Δ → irrelevance-level l< ([F] x ⊢Δ ))
                                                                          (λ [ρ] ⊢Δ x → irrelevance-level l< ([G] [ρ] ⊢Δ
                                                                             (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) x)))
                                                                           λ [ρ] ⊢Δ [a] [b] x →
                                                                           irrelevanceEq
                                                                                ([G] [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a]))
                                                                                (irrelevance-level l< ([G] [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a])))
                                                                                (G-ext [ρ] ⊢Δ (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [a])
                                                                                (irrelevanceTerm (irrelevance-level l< ([F] [ρ] ⊢Δ)) ([F] [ρ] ⊢Δ) [b])
                                                                                (irrelevanceEqTerm (irrelevance-level l< ([F] [ρ] ⊢Δ )) ([F] [ρ] ⊢Δ) x))
  irrelevance-level {r = [ .! , ll ]} ∞< (Uᵣ (Uᵣ r .⁰ emb< eq d)) = emb ∞< (Uᵣ (Uᵣ r _ emb< eq d))
  irrelevance-level ∞< (emb emb< [A]) = emb ∞< (emb emb< [A])

--------------------------------------------------------------------------------

  -- Irrelevance for terms
  irrelevanceTerm : ∀ {Γ A t r l l′} (p : Γ ⊩⟨ l ⟩ A ^ r) (q : Γ ⊩⟨ l′ ⟩ A ^ r)
                  → Γ ⊩⟨ l ⟩ t ∷ A ^ r / p → Γ ⊩⟨ l′ ⟩ t ∷ A ^ r / q
  irrelevanceTerm p q t = irrelevanceTermT (goodCasesRefl p q) t

  -- Irrelevance for terms with propositionally equal types
  irrelevanceTerm′ : ∀ {Γ A A′ t r r' l l′ ll ll'} (eq : A PE.≡ A′) (req : r PE.≡ r') (leq : ll PE.≡ ll')
                     (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                   → Γ ⊩⟨ l ⟩ t ∷ A ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ t ∷ A′ ^ [ r' , ll' ] / q
  irrelevanceTerm′ PE.refl PE.refl PE.refl p q t = irrelevanceTerm p q t

  -- Irrelevance for terms with propositionally equal types and terms
  irrelevanceTerm″ : ∀ {Γ A A′ t t′ r r' ll ll' l l′}
                      (eqA : A PE.≡ A′) (req : r PE.≡ r') (leq : ll PE.≡ ll') (eqt : t PE.≡ t′)
                      (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                    → Γ ⊩⟨ l ⟩ t ∷ A ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ t′ ∷ A′ ^ [ r' , ll' ] / q
  irrelevanceTerm″ PE.refl PE.refl PE.refl PE.refl p q t = irrelevanceTerm p q t

  -- Irrelevance for terms with propositionally equal types, terms and contexts
  irrelevanceTermΓ″ : ∀ {l l′ A A′ t t′ r Γ Γ′}
                     → Γ PE.≡ Γ′
                     → A PE.≡ A′
                     → t PE.≡ t′
                     → ([A]  : Γ  ⊩⟨ l  ⟩ A ^ r)
                       ([A′] : Γ′ ⊩⟨ l′ ⟩ A′ ^ r)
                     → Γ  ⊩⟨ l  ⟩ t ∷ A ^ r / [A]
                     → Γ′ ⊩⟨ l′ ⟩ t′ ∷ A′ ^ r / [A′]
  irrelevanceTermΓ″ PE.refl PE.refl PE.refl [A] [A′] [t] = irrelevanceTerm [A] [A′] [t]

  -- Helper for irrelevance of terms using shape view
  irrelevanceTermT : ∀ {Γ A t r l l′} {p : Γ ⊩⟨ l ⟩ A ^ r} {q : Γ ⊩⟨ l′ ⟩ A ^ r}
                         → ShapeView Γ l l′ A A r r p q
                         → Γ ⊩⟨ l ⟩ t ∷ A ^ r / p → Γ ⊩⟨ l′ ⟩ t ∷ A ^ r / q
  irrelevanceTermT (ℕᵥ D D′) t = t
  irrelevanceTermT (Emptyᵥ D D′) t = t
  irrelevanceTermT { r = [ ! , ll ]  } (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ k d nf)
                   with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceTermT {r = [ ! , ll ]} (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (neₜ k d nf)
    | PE.refl = neₜ k d nf
  irrelevanceTermT { r = [ % , ll ] } (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ d)
                   with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceTermT {r = [ % , ll ]} (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (neₜ d)
    | PE.refl = neₜ d
  irrelevanceTermT {Γ} {t = t} {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 d funcF f≡f [f] [f]₁) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , rF≡rF₁ , lF≡lF₁ , G≡G₁ , lG≡lG₁ , lΠ≡lΠ₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
    in  Πₜ f (PE.subst (λ x → Γ ⊢ t :⇒*: f ∷ x ^ ll) ΠFG≡ΠF₁G₁ d) funcF
           (PE.subst (λ x → Γ ⊢ f ≅ f ∷ x ^ [ ! , ll ]) ΠFG≡ΠF₁G₁ f≡f)
           (λ {ρ} [ρ] ⊢Δ [a]₁ [b]₁ [a≡b]₁ →
              let [a]   = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                           ([F]₁ [ρ] ⊢Δ)
                                           ([F] [ρ] ⊢Δ)
                                           [a]₁
                  [b]   = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                           ([F]₁ [ρ] ⊢Δ)
                                           ([F] [ρ] ⊢Δ)
                                           [b]₁
                  [a≡b] = irrelevanceEqTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                             ([F]₁ [ρ] ⊢Δ)
                                             ([F] [ρ] ⊢Δ)
                                             [a≡b]₁
              in  irrelevanceEqTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁) PE.refl (PE.cong ι lG≡lG₁)
                                     ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁)
                                     ([f] [ρ] ⊢Δ [a] [b] [a≡b]))
          (λ {ρ} [ρ] ⊢Δ [a]₁ →
             let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                        ([F]₁ [ρ] ⊢Δ)
                                        ([F] [ρ] ⊢Δ)
                                        [a]₁
             in  irrelevanceTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁) PE.refl (PE.cong ι lG≡lG₁)
                                  ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([f]₁ [ρ] ⊢Δ [a]))
  irrelevanceTermT {Γ} {t = t} {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₁))
                  d = let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
                       in PE.subst (λ x → Γ ⊢ t ∷ x ^ [ % , ll ]) ΠFG≡ΠF₁G₁ d
  irrelevanceTermT {Γ} {t = t} {r = [ % , ll ]} (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                                   (∃ᵣ  F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
                   d = let ∃FG≡∃F₁G₁   = whrDet* (red D , ∃ₙ) (red D₁ , ∃ₙ)
                       in PE.subst (λ x → Γ ⊢ t ∷ x ^ [ % , ll ]) ∃FG≡∃F₁G₁ d
  irrelevanceTermT (Uᵥ (Uᵣ r ll l< PE.refl D) (Uᵣ r' ll' l<' _ D')) t =
    let U≡U   = whrDet* (red D , Uₙ) (red D' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity U≡U
    in reduction-irrelevant-Univ r≡r t
  irrelevanceTermT (emb⁰¹ x) t = irrelevanceTermT x t
  irrelevanceTermT (emb¹⁰ x) t = irrelevanceTermT x t
  irrelevanceTermT (emb¹∞ x) t = irrelevanceTermT x t
  irrelevanceTermT (emb∞¹ x) t = irrelevanceTermT x t

--------------------------------------------------------------------------------

  -- Irrelevance for term equality
  irrelevanceEqTerm : ∀ {Γ A t u r l l′} (p : Γ ⊩⟨ l ⟩ A ^ r) (q : Γ ⊩⟨ l′ ⟩ A ^ r)
                    → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A ^ r / q
  irrelevanceEqTerm p q t≡u = irrelevanceEqTermT (goodCasesRefl p q) t≡u

  -- Irrelevance for term equality with propositionally equal types
  irrelevanceEqTerm′ : ∀ {Γ A A′ t u r r' l l′ ll ll'} (eq : A PE.≡ A′) (req : r PE.≡ r') (leq : ll PE.≡ ll')
                       (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                     → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A′ ^ [ r' , ll' ] / q
  irrelevanceEqTerm′ PE.refl PE.refl PE.refl p q t≡u = irrelevanceEqTerm p q t≡u

  -- Irrelevance for term equality with propositionally equal types and terms
  irrelevanceEqTerm″ : ∀ {Γ A A′ t t′ u u′ r r' ll ll' l l′} (req : r PE.≡ r') (leq : ll PE.≡ ll')
                        (eqt : t PE.≡ t′) (equ : u PE.≡ u′) (eqA : A PE.≡ A′)
                        (p : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) (q : Γ ⊩⟨ l′ ⟩ A′ ^ [ r' , ll' ])
                      → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ r , ll ] / p → Γ ⊩⟨ l′ ⟩ t′ ≡ u′ ∷ A′ ^ [ r' , ll' ] / q
  irrelevanceEqTerm″ PE.refl PE.refl PE.refl PE.refl PE.refl p q t≡u = irrelevanceEqTerm p q t≡u

  -- Helper for irrelevance of term equality using shape view
  irrelevanceEqTermT : ∀ {Γ A t u r} {l l′} {p : Γ ⊩⟨ l ⟩ A ^ r} {q : Γ ⊩⟨ l′ ⟩ A ^ r}
                           → ShapeView Γ l l′ A A r r p q
                           → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / p → Γ ⊩⟨ l′ ⟩ t ≡ u ∷ A ^ r / q
  irrelevanceEqTermT (ℕᵥ D D′) t≡u = t≡u
  irrelevanceEqTermT (Emptyᵥ D D′) t≡u = t≡u
  irrelevanceEqTermT { r = [ ! , ll ] } (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ₌ k m d d′ nf)
                     with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceEqTermT (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (neₜ₌ k m d d′ nf)
    | PE.refl = neₜ₌ k m d d′ nf
  irrelevanceEqTermT { r = [ % , ll ] } (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (neₜ₌ d d′)
                     with whrDet* (red D₁ , ne neK₁) (red D , ne neK)
  irrelevanceEqTermT (ne (ne K D neK K≡K) (ne .K D₁ neK₁ K≡K₁)) (neₜ₌ d d′)
    | PE.refl = neₜ₌ d d′
  irrelevanceEqTermT {Γ} {t = t} {u = u} {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 d′ funcF funcG f≡g [f] [g] [f≡g]) =
    let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ)
        F≡F₁ , rF≡rF₁ , lF≡lF₁ , G≡G₁ , lG≡lG₁ , lΠ≡lΠ₁ = Π-PE-injectivity ΠFG≡ΠF₁G₁
        [A]         = Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext
        [A]₁        = Πᵣ′ rF₁ lF₁ lG₁ lF₁≤ lG₁≤ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁
    in  Πₜ₌ f g (PE.subst (λ x → Γ ⊢ t :⇒*: f ∷ x ^ ll) ΠFG≡ΠF₁G₁ d)
            (PE.subst (λ x → Γ ⊢ u :⇒*: g ∷ x ^ ll) ΠFG≡ΠF₁G₁ d′) funcF funcG
            (PE.subst (λ x → Γ ⊢ f ≅ g ∷ x ^ [ ! , ll ]) ΠFG≡ΠF₁G₁ f≡g)
            (irrelevanceTerm [A] [A]₁ [f]) (irrelevanceTerm [A] [A]₁ [g])
            (λ {ρ} [ρ] ⊢Δ [a]₁ →
               let [a] = irrelevanceTerm′ (PE.cong (wk ρ) (PE.sym F≡F₁)) (PE.sym rF≡rF₁) (PE.cong ι (PE.sym lF≡lF₁))
                                          ([F]₁ [ρ] ⊢Δ)
                                          ([F] [ρ] ⊢Δ)
                                          [a]₁
               in  irrelevanceEqTerm′ (PE.cong (λ G → wk (lift ρ) G [ _ ]) G≡G₁) PE.refl (PE.cong ι lG≡lG₁)
                                     ([G] [ρ] ⊢Δ [a]) ([G]₁ [ρ] ⊢Δ [a]₁) ([f≡g] [ρ] ⊢Δ [a]))
  irrelevanceEqTermT {Γ} {t = t} {u = u} {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₁))
                     (d , d′) = let ΠFG≡ΠF₁G₁   = whrDet* (red D , Πₙ) (red D₁ , Πₙ) in
                                (PE.subst (λ x → Γ ⊢ t ∷ x ^ [ % , ll ]) ΠFG≡ΠF₁G₁ d , PE.subst (λ x → Γ ⊢ u ∷ x ^ [ % , ll ]) ΠFG≡ΠF₁G₁ d′)
  irrelevanceEqTermT {Γ} {t = t} {u = u} {r = [ % , ll ]}
                     (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                         (∃ᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
                     (d , d′) = let ∃FG≡∃F₁G₁   = whrDet* (red D , ∃ₙ) (red D₁ , ∃ₙ) in
                                (PE.subst (λ x → Γ ⊢ t ∷ x ^ [ % , ll ]) ∃FG≡∃F₁G₁ d , PE.subst (λ x → Γ ⊢ u ∷ x ^ [ % , ll ]) ∃FG≡∃F₁G₁ d′)
  irrelevanceEqTermT (Uᵥ (Uᵣ r ll l< PE.refl D) (Uᵣ r' ll' l<' _ D')) t =
    let U≡U   = whrDet* (red D , Uₙ) (red D' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity U≡U
    in reduction-irrelevant-Univ= r≡r t
  irrelevanceEqTermT (emb⁰¹ x) t≡u = irrelevanceEqTermT x t≡u
  irrelevanceEqTermT (emb¹⁰ x) t≡u = irrelevanceEqTermT x t≡u
  irrelevanceEqTermT (emb¹∞ x) t≡u = irrelevanceEqTermT x t≡u
  irrelevanceEqTermT (emb∞¹ x) t≡u = irrelevanceEqTermT x t≡u

irrelevance-≤ : ∀ {A Γ r l l'}
                  → l ≤ l'
                  → Γ ⊩⟨ ι l ⟩ A ^ r
                  → Γ ⊩⟨ ι l' ⟩ A ^ r
irrelevance-≤ (<is≤ 0<1) [A] = irrelevance-level emb< [A]
irrelevance-≤ (≡is≤ PE.refl) [A] = [A]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Solver for equations in commutative monoids
--
-- Adapted from Algebra.Monoid-solver
------------------------------------------------------------------------

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

open import Algebra

open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
open import Data.Fin using (Fin; zero; suc)
open import Data.Maybe as Maybe
  using (Maybe; decToMaybe; From-just; from-just)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; uncurry)
open import Data.Vec using (Vec; []; _∷_; lookup; replicate)

open import Function using (_∘_)

import Relation.Binary.Reasoning.Setoid  as EqReasoning
import Relation.Binary.Reflection            as Reflection
import Relation.Nullary.Decidable            as Dec
import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise

open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
open import Relation.Nullary using (Dec)

module Algebra.Solver.IdempotentCommutativeMonoid
  {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where

open IdempotentCommutativeMonoid M
open EqReasoning setoid

------------------------------------------------------------------------
-- Monoid expressions

-- There is one constructor for every operation, plus one for
-- variables; there may be at most n variables.

infixr 5 _⊕_
infixr 10 _•_

data Expr (n : ℕ) : Set where
  var : Fin n → Expr n
  id  : Expr n
  _⊕_ : Expr n → Expr n → Expr n

-- An environment contains one value for every variable.

Env : ℕ → Set _
Env n = Vec Carrier n

-- The semantics of an expression is a function from an environment to
-- a value.

⟦_⟧ : ∀ {n} → Expr n → Env n → Carrier
⟦ var x   ⟧ ρ = lookup ρ x
⟦ id      ⟧ ρ = ε
⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ

------------------------------------------------------------------------
-- Normal forms

-- A normal form is a vector of bits (a set).

Normal : ℕ → Set
Normal n = Vec Bool n

-- The semantics of a normal form.

⟦_⟧⇓ : ∀ {n} → Normal n → Env n → Carrier
⟦ []    ⟧⇓ _ = ε
⟦ b ∷ v ⟧⇓ (a ∷ ρ) = if b then a ∙ (⟦ v ⟧⇓ ρ) else (⟦ v ⟧⇓ ρ)

------------------------------------------------------------------------
-- Constructions on normal forms

-- The empty bag.

empty : ∀{n} → Normal n
empty = replicate false

-- A singleton bag.

sg : ∀{n} (i : Fin n) → Normal n
sg zero    = true ∷ empty
sg (suc i) = false ∷ sg i

-- The composition of normal forms.

_•_  : ∀{n} (v w : Normal n) → Normal n
[]      • []      = []
(l ∷ v) • (m ∷ w) = (l ∨ m) ∷ v • w

------------------------------------------------------------------------
-- Correctness of the constructions on normal forms

-- The empty bag stands for the unit ε.

empty-correct : ∀{n} (ρ : Env n) → ⟦ empty ⟧⇓ ρ ≈ ε
empty-correct [] = refl
empty-correct (a ∷ ρ) = empty-correct ρ

-- The singleton bag stands for a single variable.

sg-correct : ∀{n} (x : Fin n) (ρ : Env n) →  ⟦ sg x ⟧⇓ ρ ≈ lookup ρ x
sg-correct zero (x ∷ ρ) = begin
    x ∙ ⟦ empty ⟧⇓ ρ   ≈⟨ ∙-congˡ (empty-correct ρ) ⟩
    x ∙ ε              ≈⟨ identityʳ _ ⟩
    x                  ∎
sg-correct (suc x) (m ∷ ρ) = sg-correct x ρ

-- Normal form composition corresponds to the composition of the monoid.

flip12 : ∀ a b c → a ∙ (b ∙ c) ≈ b ∙ (a ∙ c)
flip12 a b c = begin
    a ∙ (b ∙ c)  ≈⟨ sym (assoc _ _ _) ⟩
    (a ∙ b) ∙ c  ≈⟨ ∙-congʳ (comm _ _) ⟩
    (b ∙ a) ∙ c  ≈⟨ assoc _ _ _ ⟩
    b ∙ (a ∙ c)  ∎

distr : ∀ a b c → a ∙ (b ∙ c) ≈ (a ∙ b) ∙ (a ∙ c)
distr a b c = begin
    a ∙ (b ∙ c)  ≈⟨ ∙-cong (sym (idem a)) refl ⟩
    (a ∙ a) ∙ (b ∙ c)  ≈⟨ assoc _ _ _ ⟩
    a ∙ (a ∙ (b ∙ c))  ≈⟨ ∙-congˡ (sym (assoc _ _ _)) ⟩
    a ∙ ((a ∙ b) ∙ c)  ≈⟨ ∙-congˡ (∙-congʳ (comm _ _)) ⟩
    a ∙ ((b ∙ a) ∙ c)  ≈⟨ ∙-congˡ (assoc _ _ _) ⟩
    a ∙ (b ∙ (a ∙ c))  ≈⟨ sym (assoc _ _ _) ⟩
    (a ∙ b) ∙ (a ∙ c)  ∎

comp-correct : ∀ {n} (v w : Normal n) (ρ : Env n) →
              ⟦ v • w ⟧⇓ ρ ≈ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ)
comp-correct [] [] ρ = sym (identityˡ _)
comp-correct (true ∷ v) (true ∷ w) (a ∷ ρ) =
  trans (∙-congˡ (comp-correct v w ρ)) (distr _ _ _)
comp-correct (true ∷ v) (false ∷ w) (a ∷ ρ) =
  trans (∙-congˡ (comp-correct v w ρ)) (sym (assoc _ _ _))
comp-correct (false ∷ v) (true ∷ w) (a ∷ ρ) =
  trans (∙-congˡ (comp-correct v w ρ)) (flip12 _ _ _)
comp-correct (false ∷ v) (false ∷ w) (a ∷ ρ) =
  comp-correct v w ρ

------------------------------------------------------------------------
-- Normalization

-- A normaliser.

normalise : ∀ {n} → Expr n → Normal n
normalise (var x)   = sg x
normalise id        = empty
normalise (e₁ ⊕ e₂) = normalise e₁ • normalise e₂

-- The normaliser preserves the semantics of the expression.

normalise-correct : ∀ {n} (e : Expr n) (ρ : Env n) →
    ⟦ normalise e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
normalise-correct (var x)   ρ = sg-correct x ρ
normalise-correct id        ρ = empty-correct ρ
normalise-correct (e₁ ⊕ e₂) ρ =  begin

    ⟦ normalise e₁ • normalise e₂ ⟧⇓ ρ

  ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩

    ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ

  ≈⟨ ∙-cong (normalise-correct e₁ ρ) (normalise-correct e₂ ρ) ⟩

    ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
  ∎

------------------------------------------------------------------------
-- "Tactics"

open module R = Reflection
                  setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) normalise-correct
  public using (solve; _⊜_)

-- We can decide if two normal forms are /syntactically/ equal.

infix 5 _≟_

_≟_ : ∀ {n} (nf₁ nf₂ : Normal n) → Dec (nf₁ ≡ nf₂)
nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂)
  where open Pointwise

-- We can also give a sound, but not necessarily complete, procedure
-- for determining if two expressions have the same semantics.

prove′ : ∀ {n} (e₁ e₂ : Expr n) → Maybe (∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
prove′ e₁ e₂ =
  Maybe.map lemma (decToMaybe (normalise e₁ ≟ normalise e₂))
  where
  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
  lemma eq ρ =
    R.prove ρ e₁ e₂ (begin
      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
      ⟦ normalise e₂ ⟧⇓ ρ  ∎)

-- This procedure can be combined with from-just.

prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
prove _ e₁ e₂ = from-just (prove′ e₁ e₂)

-- prove : ∀ n (es : Expr n × Expr n) →
--         From-just (uncurry prove′ es)
-- prove _ = from-just ∘ uncurry prove′

-- -}

ext: agda


text:
open import Agda.Primitive

postulate
  ℓ : Level
  F : Level → Set

module Two where

  mutual

    α : Level
    α = _

    G : F (α ⊔ ℓ) → F ℓ
    G A = A

    H : F (α ⊔ ℓ) → F α
    H A = A

module Three where

  mutual

    α : Level
    α = _

    β : Level
    β = _

    G : F (α ⊔ β ⊔ ℓ) → F ℓ
    G A = A

    H : F (α ⊔ β ⊔ ℓ) → F α
    H A = A

    I : F (α ⊔ β ⊔ ℓ) → F β
    I A = A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The lenses fst and snd
------------------------------------------------------------------------

-- This module uses univalence without tracking such uses in the types
-- of functions, and it is not parametrised by a notion of equality,
-- it uses path equality.

{-# OPTIONS --guardedness #-}

module README.Fst-snd where

open import Equality.Path
open import Equality.Path.Univalence
open import Prelude

open import Equivalence.Erased.Cubical equality-with-paths as EEq
  using (_≃ᴱ_)

import Lens.Non-dependent.Higher.Coinductive.Small.Erased
  equality-with-paths as S
import Lens.Non-dependent.Higher.Erased equality-with-paths as E

private
  variable
    a   : Level
    A B : Type a

-- A static variant of one consequence of S.Lens≃ᴱLensᴱ. Applications
-- of static functions are normalised by (at least) the GHC backend.

Lens→Lens : E.Lens A B → S.Lens univ A B
Lens→Lens = _≃ᴱ_.from (S.Lens≃ᴱLensᴱ ⊠ univ)

{-# STATIC Lens→Lens #-}

-- A lens for the first projection.

fst : S.Lens univ (A × B) A
fst = Lens→Lens E.fst

-- A lens for the second projection.
--
-- With the implementation that this lens had at the time of writing
-- (dependencies may later have changed) it turned out that when the
-- lens was compiled using the non-strict GHC backend of a certain
-- development version of Agda and GHC 9.0.1, then GHC's flag
-- -ddump-simpl suggested that you ended up with code that could lead
-- to a space leak: the code for the setter was something like
--
--   \p y -> Pair (case p of { Pair x _ -> x }) y
--
-- (where names have been changed, and code related to coercions and
-- casts has been removed).
--
-- Note that, unlike the lens snd^C discussed in "Compiling Programs
-- with Erased Univalence", this one (as well as the one below) takes
-- two universe level arguments.

snd-with-space-leak : S.Lens univ (A × B) B
snd-with-space-leak = Lens→Lens E.snd

-- A lens for the second projection.
--
-- This variant did not seem to have the problem exhibited by
-- snd-with-space-leak: the code for the setter was something like
--
--   \p y -> case p of { Pair x _ -> Pair x y }.

snd : S.Lens univ (A × B) B
snd =
  S.with-other-setter
    (Lens→Lens E.snd)
    (λ { (x , _) y → (x , y) })
    ((λ (x , _) y → (x , y))       ≡⟨⟩
     E.Lens.set E.snd              ≡⟨ sym $ proj₂ $ proj₂ (S.Lens≃ᴱLensᴱ-preserves-getters-and-setters ⊠ univ univ) E.snd ⟩∎
     S.Lens.set (Lens→Lens E.snd)  ∎)

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module Bughunting where

data Nat : Set where zero : Nat
                     suc  : Nat -> Nat

plus  : Nat ->  Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

plus  m n = {!   !}

data List2 (A : Set) : Nat -> Set where
      empty2 : List2 A 0
      cons2 : {n : Nat} -> A -> List2 A n -> List2 A (plus 1 n)


text:
{-# OPTIONS --without-K #-}
open import Library
open import Basic

--------------------------------------------------------------------------------
-- Universes for a Functor
--------------------------------------------------------------------------------

record FntrLevel : Set where
  field
    C : CatLevel
    D : CatLevel

  module C = CatLevel C
  module D = CatLevel D

  Fntr : Level
  Fntr = ℓ-max C.Cat D.Cat

--------------------------------------------------------------------------------
-- Definition of a Functor
--------------------------------------------------------------------------------

module _ {ℓ : FntrLevel}    (let module ℓ = FntrLevel ℓ)
         (C : Category ℓ.C) (let module C = Category C)
           (open C using () renaming (_⇒_ to _⇒ᶜ_ ; _∘_ to _∘ᶜ_))
         (D : Category ℓ.D) (let module D = Category D)
           (open D using () renaming (_⇒_ to _⇒ᵈ_ ; _∘_ to _∘ᵈ_)) where

  record Functor : Set ℓ.Fntr where
    field
      map  : C.Obj → D.Obj
      fmap : ∀{X Y} → X ⇒ᶜ Y → (map X) ⇒ᵈ (map Y)

    field
      id   : ∀{X} → fmap (C.id X) ≡ D.id (map X)
      comp : ∀{X Y Z}{f : X ⇒ᶜ Y}{g : Y ⇒ᶜ Z}
               → fmap (g ∘ᶜ f) ≡ (fmap g) ∘ᵈ (fmap f)

--------------------------------------------------------------------------------
-- Definition of a Natural Transformation and a Natural Isomorphism
--------------------------------------------------------------------------------

module _ {ℓ : FntrLevel}     (let module ℓ = FntrLevel ℓ)
         {C : Category ℓ.C}  (let module C = Category C)
           (open C using () renaming (_⇒_ to _⇒ᶜ_ ; _∘_ to _∘ᶜ_))
         {D : Category ℓ.D}  (let module D = Category D)
           (open D using () renaming (_⇒_ to _⇒ᵈ_ ; _∘_ to _∘ᵈ_))
         (F G : Functor C D) (let module F = Functor F)
                                 (let module G = Functor G) where

  record NaturalTrans : Set ℓ.Fntr where
    field
      map    : (X : C.Obj) → (F.map X) ⇒ᵈ (G.map X)
      nat-sq : {X Y : C.Obj}{f : X ⇒ᶜ Y} →
                 (G.fmap f) ∘ᵈ (map X) ≡ (map Y) ∘ᵈ (F.fmap f)

    is-natrual-isomorphism : Set (ℓ-max ℓ.C.Obj ℓ.D.Hom)
    is-natrual-isomorphism = ∀(X : C.Obj) → D.is-isomorphism (map X)

  NaturalIso : Set ℓ.Fntr
  NaturalIso = Σ NaturalTrans NaturalTrans.is-natrual-isomorphism

--------------------------------------------------------------------------------
-- Category of Functors
--------------------------------------------------------------------------------

module _ {ℓ : FntrLevel}     (let module ℓ = FntrLevel ℓ)
         (C : Category ℓ.C) (let module C = Category C)
           (open C using () renaming (_⇒_ to _⇒ᶜ_ ; _∘_ to _∘ᶜ_))
         (D : Category ℓ.D) (let module D = Category D)
           (open D using () renaming (_⇒_ to _⇒ᵈ_ ; _∘_ to _∘ᵈ_)) where

  FntrCat : Category (record { Obj = ℓ.Fntr ; Hom = ℓ.Fntr })
  FntrCat = record { Obj   = Functor C D
                   ; _⇒_   = NaturalTrans
                   ; id    = natural-trans-id
                   ; _∘_   = vertical-comp
                   ; idl   = {!!}
                   ; idr   = {!!}
                   ; assoc = {!!} }
    where
      natural-trans-id : (F : Functor C D) → NaturalTrans F F
      natural-trans-id F = record
        { map    = λ (X : C.Obj) → D.id (F.map X)
        ; nat-sq = λ {X Y : C.Obj} {f : X ⇒ᶜ Y} →               ≡-proof
            (F.fmap f) ∘ᵈ D.id (F.map X)                        ≡⟨ D.idr       ⟩
            F.fmap f                                            ≡⟨ ≡-sym D.idl ⟩
            D.id (F.map Y) ∘ᵈ (F.fmap f)                        ≡-qed
        } where module F = Functor F

      vertical-comp : {F G H : Functor C D}
                        → NaturalTrans G H → NaturalTrans F G → NaturalTrans F H
      vertical-comp {F} {G} {H} β α = record
        { map    = λ (X : C.Obj) → (β.map X) ∘ᵈ (α.map X)
        ; nat-sq = λ {X Y : C.Obj} {f : X ⇒ᶜ Y} →           ≡-proof
            H.fmap f ∘ᵈ (β.map X ∘ᵈ α.map X)          ≡⟨ ≡-sym D.assoc ⟩
            (H.fmap f ∘ᵈ β.map X) ∘ᵈ α.map X          ≡⟨ {!!} ⟩
            (β.map Y ∘ᵈ G.fmap f) ∘ᵈ α.map X          ≡⟨ D.assoc ⟩
            β.map Y ∘ᵈ (G.fmap f ∘ᵈ α.map X)          ≡⟨ {!!} ⟩
            β.map Y ∘ᵈ (α.map Y ∘ᵈ F.fmap f)          ≡⟨ ≡-sym D.assoc ⟩
            (β.map Y ∘ᵈ α.map Y) ∘ᵈ F.fmap f            ≡-qed
        } where module F = Functor F
                module G = Functor G
                module H = Functor H
                module α = NaturalTrans α
                module β = NaturalTrans β

--------------------------------------------------------------------------------
-- Definition of Presheaf
--------------------------------------------------------------------------------

-- module _ {C : CatLevel} (open CatLevel C)
--          (C : Category C) (let module C = Category C) where
--   Presheaf : Category (record { Obj = ℓ-suc Obj ; Hom = ℓ-suc Hom })
--   Presheaf C = record { Obj = Functor C.op (Type Hom)
--                       ; _⇒_ = NaturalTrans
--                       ; id  = NaturalTrans-id
--                       ; __}

max_stars_repo_name: gunpinyo/agda-cat

max_issues_repo_name: gunpinyo/agda-cat

max_forks_repo_name: gunpinyo/agda-cat


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

module Erased-cubical.Without-K where

data D : Set where
  c : D


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Paths
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.cubical.Square

module lib.types.LoopSpace where

module _ {i} where

  ⊙Ω : Ptd i → Ptd i
  ⊙Ω (A , a) = ⊙[ (a == a) , idp ]

  Ω : Ptd i → Type i
  Ω = fst ∘ ⊙Ω

  ⊙Ω^ : (n : ℕ) → Ptd i → Ptd i
  ⊙Ω^ O X = X
  ⊙Ω^ (S n) X = ⊙Ω (⊙Ω^ n X)

  Ω^ : (n : ℕ) → Ptd i → Type i
  Ω^ n X = fst (⊙Ω^ n X)

idp^ : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^ n X
idp^ n {X} = snd (⊙Ω^ n X)

{- for n ≥ 1, we have a group structure on the loop space -}
module _ {i} (n : ℕ) {X : Ptd i} where
  !^S : Ω^ (S n) X → Ω^ (S n) X
  !^S = !

  conc^S : Ω^ (S n) X → Ω^ (S n) X → Ω^ (S n) X
  conc^S = _∙_

{- pointed versions of functions on paths -}

private
  pt-lemma : ∀ {i} {A : Type i} {x y : A} (p : x == y)
    → ! p ∙ (idp ∙' p) == idp
  pt-lemma idp = idp

⊙conc : ∀ {i} {X : Ptd i} → fst (⊙Ω X ⊙× ⊙Ω X ⊙→ ⊙Ω X)
⊙conc = (uncurry _∙_ , idp)

⊙ap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙→ Y) → fst (⊙Ω X ⊙→ ⊙Ω Y)
⊙ap (f , fpt) = ((λ p → ! fpt ∙ ap f p ∙' fpt) , pt-lemma fpt)

⊙ap2 : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → fst (X ⊙× Y ⊙→ Z) → fst (⊙Ω X ⊙× ⊙Ω Y ⊙→ ⊙Ω Z)
⊙ap2 (f , fpt) = ((λ {(p , q) → ! fpt ∙ ap2 (curry f) p q ∙' fpt}) ,
                  pt-lemma fpt)

⊙ap-∘ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
  → ⊙ap (g ⊙∘ f) == ⊙ap g ⊙∘ ⊙ap f
⊙ap-∘ (g , idp) (f , idp) = ⊙λ= (λ p → ap-∘ g f p) idp

⊙ap-idf : ∀ {i} {X : Ptd i} → ⊙ap (⊙idf X) == ⊙idf _
⊙ap-idf = ⊙λ= ap-idf idp

⊙ap2-fst : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙ap2 {X = X} {Y = Y} ⊙fst == ⊙fst
⊙ap2-fst = ⊙λ= (uncurry ap2-fst) idp

⊙ap2-snd : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙ap2 {X = X} {Y = Y} ⊙snd == ⊙snd
⊙ap2-snd = ⊙λ= (uncurry ap2-snd) idp

⊙ap-ap2 : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : fst (Z ⊙→ W)) (F : fst (X ⊙× Y ⊙→ Z))
  → ⊙ap G ⊙∘ ⊙ap2 F == ⊙ap2 (G ⊙∘ F)
⊙ap-ap2 (g , idp) (f , idp) =
  ⊙λ= (uncurry (ap-ap2 g (curry f))) idp

⊙ap2-ap : ∀ {i j k l m}
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : fst ((U ⊙× V) ⊙→ Z)) (F₁ : fst (X ⊙→ U)) (F₂ : fst (Y ⊙→ V))
  → ⊙ap2 G ⊙∘ pair⊙→ (⊙ap F₁) (⊙ap F₂) == ⊙ap2 (G ⊙∘ pair⊙→ F₁ F₂)
⊙ap2-ap (g , idp) (f₁ , idp) (f₂ , idp) =
  ⊙λ= (λ {(p , q) → ap2-ap-l (curry g) f₁ p (ap f₂ q)
                  ∙ ap2-ap-r (λ x v → g (f₁ x , v)) f₂ p q})
      idp

⊙ap2-diag : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙× X ⊙→ Y))
  → ⊙ap2 F ⊙∘ ⊙diag == ⊙ap (F ⊙∘ ⊙diag)
⊙ap2-diag (f , idp) = ⊙λ= (ap2-diag (curry f)) idp

{- ap and ap2 for higher loop spaces -}

ap^ : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙→ Y) → fst (⊙Ω^ n X ⊙→ ⊙Ω^ n Y)
ap^ O F = F
ap^ (S n) F = ⊙ap (ap^ n F)

ap2^ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → fst ((X ⊙× Y) ⊙→ Z)
  → fst ((⊙Ω^ n X ⊙× ⊙Ω^ n Y) ⊙→ ⊙Ω^ n Z)
ap2^ O F = F
ap2^ (S n) F = ⊙ap2 (ap2^ n F)

ap^-idf : ∀ {i} (n : ℕ) {X : Ptd i} → ap^ n (⊙idf X) == ⊙idf _
ap^-idf O = idp
ap^-idf (S n) = ap ⊙ap (ap^-idf n) ∙ ⊙ap-idf

ap^-ap2^ : ∀ {i j k l} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : fst (Z ⊙→ W)) (F : fst ((X ⊙× Y) ⊙→ Z))
  → ap^ n G ⊙∘ ap2^ n F == ap2^ n (G ⊙∘ F)
ap^-ap2^ O G F = idp
ap^-ap2^ (S n) G F = ⊙ap-ap2 (ap^ n G) (ap2^ n F) ∙ ap ⊙ap2 (ap^-ap2^ n G F)

ap2^-fst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ap2^ n {X} {Y} ⊙fst == ⊙fst
ap2^-fst O = idp
ap2^-fst (S n) = ap ⊙ap2 (ap2^-fst n) ∙ ⊙ap2-fst

ap2^-snd : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ap2^ n {X} {Y} ⊙snd == ⊙snd
ap2^-snd O = idp
ap2^-snd (S n) = ap ⊙ap2 (ap2^-snd n) ∙ ⊙ap2-snd

ap2^-ap^ : ∀ {i j k l m} (n : ℕ)
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : fst ((U ⊙× V) ⊙→ Z)) (F₁ : fst (X ⊙→ U)) (F₂ : fst (Y ⊙→ V))
  → ap2^ n G ⊙∘ pair⊙→ (ap^ n F₁) (ap^ n F₂) == ap2^ n (G ⊙∘ pair⊙→ F₁ F₂)
ap2^-ap^ O G F₁ F₂ = idp
ap2^-ap^ (S n) G F₁ F₂ =
  ⊙ap2-ap (ap2^ n G) (ap^ n F₁) (ap^ n F₂) ∙ ap ⊙ap2 (ap2^-ap^ n G F₁ F₂)

ap2^-diag : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙× X ⊙→ Y))
  → ap2^ n F ⊙∘ ⊙diag == ap^ n (F ⊙∘ ⊙diag)
ap2^-diag O F = idp
ap2^-diag (S n) F = ⊙ap2-diag (ap2^ n F) ∙ ap ⊙ap (ap2^-diag n F)

module _ {i} {X : Ptd i} (n : ℕ) where

  {- Prove these as lemmas now
   - so we don't have to deal with the n = O case later -}

  conc^S-unit-l : (q : Ω^ (S n) X)
    → (conc^S n (idp^ (S n)) q) == q
  conc^S-unit-l _ = idp

  conc^S-unit-r : (q : Ω^ (S n) X)
    → (conc^S n q (idp^ (S n))) == q
  conc^S-unit-r = ∙-unit-r

  conc^S-assoc : (p q r : Ω^ (S n) X)
    → conc^S n (conc^S n p q) r == conc^S n p (conc^S n q r)
  conc^S-assoc = ∙-assoc

  !^S-inv-l : (p : Ω^ (S n) X)
    → conc^S n (!^S n p) p == idp^ (S n)
  !^S-inv-l = !-inv-l

  !^S-inv-r : (p : Ω^ (S n) X)
    → conc^S n p (!^S n p) == idp^ (S n)
  !^S-inv-r = !-inv-r

abstract
  ap^S-conc^S : ∀ {i j} (n : ℕ)
    {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙→ Y)) (p q : Ω^ (S n) X)
    → fst (ap^ (S n) F) (conc^S n p q)
      == conc^S n (fst (ap^ (S n) F) p) (fst (ap^ (S n) F) q)
  ap^S-conc^S n {X = X} {Y = Y} F p q =
    ! gpt ∙ ap g (p ∙ q) ∙' gpt
      =⟨ ap-∙ g p q |in-ctx (λ w → ! gpt ∙ w ∙' gpt) ⟩
    ! gpt ∙ (ap g p ∙ ap g q) ∙' gpt
      =⟨ lemma (ap g p) (ap g q) gpt ⟩
    (! gpt ∙ ap g p ∙' gpt) ∙ (! gpt ∙ ap g q ∙' gpt) ∎
    where
    g : Ω^ n X → Ω^ n Y
    g = fst (ap^ n F)

    gpt : g (idp^ n) == idp^ n
    gpt = snd (ap^ n F)

    lemma : ∀ {i} {A : Type i} {x y : A}
      → (p q : x == x) (r : x == y)
      → ! r ∙ (p ∙ q) ∙' r == (! r ∙ p ∙' r) ∙ (! r ∙ q ∙' r)
    lemma p q idp = idp

{- ap^ preserves (pointed) equivalences -}
module _ {i j} {X : Ptd i} {Y : Ptd j} where

  is-equiv-ap^ : (n : ℕ) (F : fst (X ⊙→ Y)) (e : is-equiv (fst F))
    → is-equiv (fst (ap^ n F))
  is-equiv-ap^ O F e = e
  is-equiv-ap^ (S n) F e =
         pre∙-is-equiv (! (snd (ap^ n F)))
    ∘ise post∙'-is-equiv (snd (ap^ n F))
    ∘ise snd (equiv-ap (_ , is-equiv-ap^ n F e) _ _)

  equiv-ap^ : (n : ℕ) (F : fst (X ⊙→ Y)) (e : is-equiv (fst F))
    → Ω^ n X ≃ Ω^ n Y
  equiv-ap^ n F e = (fst (ap^ n F) , is-equiv-ap^ n F e)

Ω^-level-in : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (has-level (⟨ n ⟩₋₂ +2+ m) (fst X) → has-level m (Ω^ n X))
Ω^-level-in m O X pX = pX
Ω^-level-in m (S n) X pX =
  Ω^-level-in (S m) n X
    (transport (λ k → has-level k (fst X)) (! (+2+-βr ⟨ n ⟩₋₂ m)) pX)
    (idp^ n) (idp^ n)

Ω^-conn-in : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (is-connected (⟨ n ⟩₋₂ +2+ m) (fst X)) → is-connected m (Ω^ n X)
Ω^-conn-in m O X pX = pX
Ω^-conn-in m (S n) X pX =
  path-conn $ Ω^-conn-in (S m) n X $
    transport (λ k → is-connected k (fst X)) (! (+2+-βr ⟨ n ⟩₋₂ m)) pX

{- Eckmann-Hilton argument -}
module _ {i} {X : Ptd i} where

  ap2-conc-is-conc^S : (α β : Ω^ 2 X) → ap2 _∙_ α β == conc^S 1 α β
  ap2-conc-is-conc^S α β = ap2-out _∙_ α β ∙ ap2 _∙_ (lemma α) (ap-idf β)
    where
    lemma : ∀ {i} {A : Type i} {x y : A} {p q : x == y} (α : p == q)
      → ap (λ r → r ∙ idp) α == ∙-unit-r p ∙ α ∙' ! (∙-unit-r q)
    lemma {p = idp} idp = idp

  ⊙ap2-conc-is-conc : ⊙ap2 (⊙conc {X = X}) == ⊙conc
  ⊙ap2-conc-is-conc = ⊙λ= (uncurry ap2-conc-is-conc^S) idp

  conc^2-comm : (α β : Ω^ 2 X) → conc^S 1 α β == conc^S 1 β α
  conc^2-comm α β = ! (⋆2=conc^ α β) ∙ ⋆2=⋆'2 α β ∙ ⋆'2=conc^ α β
    where
      ⋆2=conc^ : (α β : Ω^ 2 X) → α ⋆2 β == conc^S 1 α β
      ⋆2=conc^ α β = ap (λ π → π ∙ β) (∙-unit-r α)

      ⋆'2=conc^ : (α β : Ω^ 2  X) → α ⋆'2 β == conc^S 1 β α
      ⋆'2=conc^ α β = ap (λ π → β ∙ π) (∙-unit-r α)

{- Pushing truncation through loop space -}
module _ {i} where

  Trunc-Ω^ : (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
    → ⊙Trunc m (⊙Ω^ n X) == ⊙Ω^ n (⊙Trunc (⟨ n ⟩₋₂ +2+ m) X)
  Trunc-Ω^ m O X = idp
  Trunc-Ω^ m (S n) X =
    ⊙Trunc m (⊙Ω^ (S n) X)
      =⟨ ! (pair= (Trunc=-path [ _ ] [ _ ]) (↓-idf-ua-in _ idp)) ⟩
    ⊙Ω (⊙Trunc (S m) (⊙Ω^ n X))
      =⟨ ap ⊙Ω (Trunc-Ω^ (S m) n X) ⟩
    ⊙Ω^ (S n) (⊙Trunc (⟨ n ⟩₋₂ +2+ S m) X)
      =⟨ +2+-βr ⟨ n ⟩₋₂ m |in-ctx (λ k → ⊙Ω^ (S n) (⊙Trunc k X)) ⟩
    ⊙Ω^ (S n) (⊙Trunc (S ⟨ n ⟩₋₂ +2+ m) X) ∎

  Ω-Trunc-equiv : (m : ℕ₋₂) (X : Ptd i)
    → Ω (⊙Trunc (S m) X) ≃ Trunc m (Ω X)
  Ω-Trunc-equiv m X = Trunc=-equiv [ snd X ] [ snd X ]

{- A loop space is a pregroup, and a group if it has the right level -}
module _ {i} (n : ℕ) (X : Ptd i) where

  Ω^S-group-structure : GroupStructure (Ω^ (S n) X)
  Ω^S-group-structure = record {
    ident = idp^ (S n);
    inv = !^S n;
    comp = conc^S n;
    unitl = conc^S-unit-l n;
    unitr = conc^S-unit-r n;
    assoc = conc^S-assoc n;
    invr = !^S-inv-r n;
    invl = !^S-inv-l n
    }

  Ω^S-group : has-level ⟨ S n ⟩ (fst X) → Group i
  Ω^S-group pX = group
    (Ω^ (S n) X)
    (Ω^-level-in 0 (S n) X $
       transport (λ t → has-level t (fst X)) (+2+-comm 0 ⟨ S n ⟩₋₂) pX)
    Ω^S-group-structure

{- Our definition of Ω^ builds up loops on the outside,
 - but this is equivalent to building up on the inside -}
module _ {i} where
  ⊙Ω^-inner-path : (n : ℕ) (X : Ptd i)
    → ⊙Ω^ (S n) X == ⊙Ω^ n (⊙Ω X)
  ⊙Ω^-inner-path O X = idp
  ⊙Ω^-inner-path (S n) X = ap ⊙Ω (⊙Ω^-inner-path n X)

  ⊙Ω^-inner-out : (n : ℕ) (X : Ptd i)
    → fst (⊙Ω^ (S n) X ⊙→ ⊙Ω^ n (⊙Ω X))
  ⊙Ω^-inner-out O _ = (idf _ , idp)
  ⊙Ω^-inner-out (S n) X = ap^ 1 (⊙Ω^-inner-out n X)

  Ω^-inner-out : (n : ℕ) (X : Ptd i)
    → (Ω^ (S n) X → Ω^ n (⊙Ω X))
  Ω^-inner-out n X = fst (⊙Ω^-inner-out n X)

  Ω^S-inner-out-conc^S : (n : ℕ)
    (X : Ptd i) (p q : Ω^ (S (S n)) X)
    → Ω^-inner-out (S n) X (conc^S (S n) p q)
      == conc^S n (Ω^-inner-out (S n) X p) (Ω^-inner-out (S n) X q)
  Ω^S-inner-out-conc^S n X p q =
    ap^S-conc^S 0 (⊙Ω^-inner-out n X) p q

  Ω^-inner-is-equiv : (n : ℕ) (X : Ptd i)
    → is-equiv (fst (⊙Ω^-inner-out n X))
  Ω^-inner-is-equiv O X = is-eq (idf _) (idf _) (λ _ → idp) (λ _ → idp)
  Ω^-inner-is-equiv (S n) X =
    is-equiv-ap^ 1 (⊙Ω^-inner-out n X) (Ω^-inner-is-equiv n X)

  Ω^-inner-equiv : (n : ℕ) (X : Ptd i) → Ω^ (S n) X ≃ Ω^ n (⊙Ω X)
  Ω^-inner-equiv n X = _ , Ω^-inner-is-equiv n X

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

module Cubical.Data.Fin.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat using (ℕ ; zero ; suc ; _+_ ; znots)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Order.Recursive using () renaming (_≤_ to _≤′_)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum using (_⊎_; _⊎?_; inl; inr)

open import Cubical.Relation.Nullary

-- Finite types.
--
-- Currently it is most convenient to define these as a subtype of the
-- natural numbers, because indexed inductive definitions don't behave
-- well with cubical Agda. This definition also has some more general
-- attractive properties, of course, such as easy conversion back to
-- ℕ.
Fin : ℕ → Type₀
Fin n = Σ[ k ∈ ℕ ] k < n

private
  variable
    ℓ : Level
    k : ℕ

fzero : Fin (suc k)
fzero = (0 , suc-≤-suc zero-≤)

fone : Fin (suc (suc k))
fone = (1 , suc-≤-suc (suc-≤-suc zero-≤))

fzero≠fone : ¬ fzero {k = suc k} ≡ fone
fzero≠fone p = znots (cong fst p)

-- It is easy, using this representation, to take the successor of a
-- number as a number in the next largest finite type.
fsuc : Fin k → Fin (suc k)
fsuc (k , l) = (suc k , suc-≤-suc l)

-- Conversion back to ℕ is trivial...
toℕ : Fin k → ℕ
toℕ = fst

-- ... and injective.
toℕ-injective : ∀{fj fk : Fin k} → toℕ fj ≡ toℕ fk → fj ≡ fk
toℕ-injective {fj = fj} {fk} = Σ≡Prop (λ _ → m≤n-isProp)

-- Conversion from ℕ with a recursive definition of ≤

fromℕ≤ : (m n : ℕ) → m ≤′ n → Fin (suc n)
fromℕ≤ zero    _       _    = fzero
fromℕ≤ (suc m) (suc n) m≤n = fsuc (fromℕ≤ m n m≤n)

-- A case analysis helper for induction.
fsplit
  : ∀(fj : Fin (suc k))
  → (fzero ≡ fj) ⊎ (Σ[ fk ∈ Fin k ] fsuc fk ≡ fj)
fsplit (0 , k<sn) = inl (toℕ-injective refl)
fsplit (suc k , k<sn) = inr ((k , pred-≤-pred k<sn) , toℕ-injective refl)

inject< : ∀ {m n} (m<n : m < n) → Fin m → Fin n
inject< m<n (k , k<m) = k , <-trans k<m m<n

flast : Fin (suc k)
flast {k = k} = k , suc-≤-suc ≤-refl

-- Fin 0 is empty
¬Fin0 : ¬ Fin 0
¬Fin0 (k , k<0) = ¬-<-zero k<0

-- The full inductive family eliminator for finite types.
elim
  : ∀(P : ∀{k} → Fin k → Type ℓ)
  → (∀{k} → P {suc k} fzero)
  → (∀{k} {fn : Fin k} → P fn → P (fsuc fn))
  → {k : ℕ} → (fn : Fin k) → P fn
elim P fz fs {zero} = ⊥.rec ∘ ¬Fin0
elim P fz fs {suc k} fj
  = case fsplit fj return (λ _ → P fj) of λ
  { (inl p) → subst P p fz
  ; (inr (fk , p)) → subst P p (fs (elim P fz fs fk))
  }

any? : ∀ {n} {P : Fin n → Type ℓ} → (∀ i → Dec (P i)) → Dec (Σ (Fin n) P)
any? {n = zero}  {P = _} P? = no (λ (x , _) → ¬Fin0 x)
any? {n = suc n} {P = P} P? =
  mapDec
    (λ
      { (inl P0) → fzero , P0
      ; (inr (x , Px)) → fsuc x , Px
      }
    )
    (λ n h → n (helper h))
    (P? fzero ⊎? any? (P? ∘ fsuc))
  where
    helper : Σ (Fin (suc n)) P → P fzero ⊎ Σ (Fin n) λ z → P (fsuc z)
    helper (x , Px) with fsplit x
    ... | inl x≡0 = inl (subst P (sym x≡0) Px)
    ... | inr (k , x≡sk) = inr (k , subst P (sym x≡sk) Px)

FinPathℕ : {n : ℕ} (x : Fin n) (y : ℕ) → fst x ≡ y → Σ[ p ∈ _ ] (x ≡ (y , p))
FinPathℕ {n = n} x y p =
    ((fst (snd x)) , (cong (λ y → fst (snd x) + y) (cong suc (sym p)) ∙ snd (snd x)))
  , (Σ≡Prop (λ _ → m≤n-isProp) p)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Monoid.Instances.Nat where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat

open import Cubical.Algebra.Monoid

NatMonoid : Monoid ℓ-zero
fst NatMonoid = ℕ
MonoidStr.ε (snd NatMonoid) = 0
MonoidStr._·_ (snd NatMonoid) = _+_
MonoidStr.isMonoid (snd NatMonoid) = makeIsMonoid isSetℕ +-assoc +-zero (λ _ → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2016-12-03, issue 2307
-- preserve record (vs. constructor) in internal syntax

open import Common.Equality

postulate
  A : Set
  a : A

record R : Set where
  constructor c
  field f : A
open R

postulate
  r : R
  g h : R → R

fail1 : g (c a) ≡ h (record{ f = a })
fail1 = refl

-- ERROR:     g (c a) != h (c a)
-- Expected:  g (c a) != h (record{ f = a })


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Numbers.Naturals.Definition
open import Sets.FinSet.Definition
open import Setoids.Setoids

module Setoids.Cardinality.Finite.Definition where

record FiniteSetoid {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
  field
    size : ℕ
    mapping : FinSet size → A
    bij : SetoidBijection (reflSetoid (FinSet size)) S mapping


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Representable where

-- A Presheaf (into Setoids) is representation if it is naturally isomorphic to a Hom functor
--  over a particular object A of the base category.
open import Level

open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids
open import Categories.Functor using (Functor)
open import Categories.Functor.Hom
open import Categories.Functor.Presheaf
open import Categories.NaturalTransformation.NaturalIsomorphism

record Representable {o ℓ e} {C : Category o ℓ e} (F : Presheaf C (Setoids ℓ e)) : Set (o ⊔ suc ℓ ⊔ suc e ) where
  open Category C
  open Hom C
  field
    A : Obj
    Iso : NaturalIsomorphism F Hom[-, A ]

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module _ where

open import Agda.Primitive.Cubical hiding (PathP)

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Numeral.Integer.Relation.Divisibility.Proofs where

open import Functional
open import Logic.Propositional
import      Numeral.Natural.Relation.Divisibility as ℕ
import      Numeral.Natural.Relation.Divisibility.Proofs as ℕ
open import Numeral.Natural using (ℕ)
import      Numeral.Natural.Oper as ℕ
open import Numeral.Integer.Oper
open import Numeral.Integer.Proofs
open import Numeral.Integer.Relation.Divisibility
open import Numeral.Integer
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function.Multi
open import Structure.Operator.Properties
open import Structure.Relator
open import Structure.Relator.Properties
open import Type

instance
  [∣][−𝐒ₙ]-sub : ((_∣_) on₂ (−𝐒ₙ_)) ⊆₂ ((ℕ._∣_) on₂ ℕ.𝐒)
  [∣][−𝐒ₙ]-sub = intro id

instance
  [∣][+ₙ]-sub : ((_∣_) on₂ (+ₙ_)) ⊆₂ (ℕ._∣_)
  [∣][+ₙ]-sub = intro id

instance
  [∣][−ₙ]-sub : ((_∣_) on₂ (−ₙ_)) ⊆₂ (ℕ._∣_)
  _⊆₂_.proof [∣][−ₙ]-sub {ℕ.𝟎}   {ℕ.𝟎}   p = p
  _⊆₂_.proof [∣][−ₙ]-sub {ℕ.𝟎}   {ℕ.𝐒 y} p = p
  _⊆₂_.proof [∣][−ₙ]-sub {ℕ.𝐒 x} {ℕ.𝟎}   p = p
  _⊆₂_.proof [∣][−ₙ]-sub {ℕ.𝐒 x} {ℕ.𝐒 y} p = p

instance
  [∣][−𝐒ₙ]-super : ((_∣_) on₂ (−𝐒ₙ_)) ⊇₂ ((ℕ._∣_) on₂ ℕ.𝐒)
  [∣][−𝐒ₙ]-super = intro id

instance
  [∣][+ₙ]-super : ((_∣_) on₂ (+ₙ_)) ⊇₂ (ℕ._∣_)
  [∣][+ₙ]-super = intro id

instance
  [∣][−ₙ]-super : ((_∣_) on₂ (−ₙ_)) ⊇₂ (ℕ._∣_)
  _⊆₂_.proof [∣][−ₙ]-super {ℕ.𝟎}   {ℕ.𝟎}   p = p
  _⊆₂_.proof [∣][−ₙ]-super {ℕ.𝟎}   {ℕ.𝐒 y} p = p
  _⊆₂_.proof [∣][−ₙ]-super {ℕ.𝐒 x} {ℕ.𝟎}   p = p
  _⊆₂_.proof [∣][−ₙ]-super {ℕ.𝐒 x} {ℕ.𝐒 y} p = p

divides-with-[−ₙ] : ∀{a b c} → ((absₙ a) ℕ.∣ b) → ((absₙ a) ℕ.∣ c) → (a ∣ (b −ₙ c))
divides-with-[−ₙ] {a} ℕ.Div𝟎 ℕ.Div𝟎 = ℕ.Div𝟎
divides-with-[−ₙ] {a} (ℕ.Div𝐒 ab) ℕ.Div𝟎 = ℕ.Div𝐒 ab
divides-with-[−ₙ] {a} ℕ.Div𝟎 (ℕ.Div𝐒 {x = x} ac)
  with p ← ℕ.divides-with-[+] (reflexivity(ℕ._∣_)) ((super₂((_∣_) on₂ (−ₙ_))(ℕ._∣_) ac))
  rewrite absₙ-of-[−ₙ] {x}
  rewrite absₙ-of-[−ₙ] {absₙ a}
  rewrite [−ₙ]-antiidentityₗ {absₙ a ℕ.+ x}
  rewrite absₙ-of-[−ₙ] {absₙ(a) ℕ.+ x}
  = p
divides-with-[−ₙ] {a} (ℕ.Div𝐒 {x = x} ab) (ℕ.Div𝐒 {x = y} ac)
  rewrite [−ₙ]-on-[+]ₗ-redundancy{absₙ a}{x}{y}
  = divides-with-[−ₙ] {a} ab ac

divides-with-[+] : ∀{a b c} → (a ∣ b) → (a ∣ c) → (a ∣ (b + c))
divides-with-[+] {+ₙ  a} {+ₙ  b} {+ₙ  c} ab ac = ℕ.divides-with-[+] ab ac
divides-with-[+] {+ₙ  a} {+ₙ  b} {−𝐒ₙ c} ab ac = divides-with-[−ₙ] {+ₙ a} ab ac
divides-with-[+] {+ₙ  a} {−𝐒ₙ b} {+ₙ  c} ab ac = divides-with-[−ₙ] {+ₙ a} ac ab
divides-with-[+] {+ₙ  a} {−𝐒ₙ b} {−𝐒ₙ c} ab ac = ℕ.divides-with-[+] ab ac
divides-with-[+] {−𝐒ₙ a} {+ₙ  b} {+ₙ  c} ab ac = ℕ.divides-with-[+] ab ac
divides-with-[+] {−𝐒ₙ a} {+ₙ  b} {−𝐒ₙ c} ab ac = divides-with-[−ₙ] {−𝐒ₙ a} ab ac
divides-with-[+] {−𝐒ₙ a} {−𝐒ₙ b} {+ₙ  c} ab ac = divides-with-[−ₙ] {−𝐒ₙ a} ac ab
divides-with-[+] {−𝐒ₙ a} {−𝐒ₙ b} {−𝐒ₙ c} ab ac = ℕ.divides-with-[+] ab ac

divides-with-[⋅] : ∀{a b c} → ((a ∣ b) ∨ (a ∣ c)) → (a ∣ (b ⋅ c))
divides-with-[⋅] {a} {b} {c} p = substitute₂ᵣ(ℕ._∣_) {absₙ a} (symmetry(_≡_) (preserving₂(absₙ)(_⋅_)(ℕ._⋅_) {b}{c})) (ℕ.divides-with-[⋅] {absₙ a}{absₙ b}{absₙ c} p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Nat
open import lib.types.Subtype

module lib.types.Fin where

Fin : ℕ → Type₀
Fin n = Σ ℕ (_< n)

instance
  Fin-reader : ∀ {n} → FromNat (Fin n)
  FromNat.in-range (Fin-reader {n}) m = m < n
  FromNat.read (Fin-reader {n}) m ⦃ m<n ⦄ = m , m<n

Fin-S : ∀ {n} → Fin n → Fin (S n)
Fin-S (n , lt) = n , ltSR lt

Fin-S^ : ∀ {n} → (m : ℕ) → Fin n → Fin (m + n)
Fin-S^ O <n = <n
Fin-S^ (S m) <n = Fin-S (Fin-S^ m <n)

Fin-S^' : ∀ {n} → (m : ℕ) → Fin n → Fin (ℕ-S^' m n)
Fin-S^' O <n = <n
Fin-S^' (S m) <n = Fin-S^' m (Fin-S <n)

Fin-to-≠ : ∀ {n} (<n : Fin n) → fst <n ≠ n
Fin-to-≠ <n = <-to-≠ (snd <n)

Fin-prop : ℕ → SubtypeProp ℕ lzero
Fin-prop n = ((_< n) , λ _ → <-is-prop)

abstract
  Fin-is-set : {n : ℕ} → is-set (Fin n)
  Fin-is-set {n} = Subtype-level (Fin-prop n)

  Fin-has-dec-eq : {n : ℕ} → has-dec-eq (Fin n)
  Fin-has-dec-eq {n} = Subtype-has-dec-eq (Fin-prop n) ℕ-has-dec-eq

private
  Fin-pred=-type : {n : ℕ} → Fin n → Fin n → Type₀
  Fin-pred=-type (_ , ltSR _) (_ , ltS) = ⊤
  Fin-pred=-type (_ , ltS) (_ , ltSR _) = ⊤
  Fin-pred=-type (m , ltS) (n , ltS) = m == n :> ℕ
  Fin-pred=-type {S n} (m , ltSR m<n) (o , ltSR o<n) = (m , m<n) == (o , o<n) :> Fin n

  Fin-pred= : {n : ℕ} {x y : Fin n} → x == y → Fin-pred=-type x y
  Fin-pred= {x = (_ , ltS)} idp = idp
  Fin-pred= {x = (_ , ltSR _)} idp = idp

abstract
  ltSR≠ltS : ∀ {m} (<m : Fin m) → Fin-S <m ≠ (m , ltS)
  ltSR≠ltS <m = Fin-to-≠ <m ∘ ap fst

  ltS≠ltSR : ∀ {m} (<m : Fin m) → (m , ltS) ≠ Fin-S <m
  ltS≠ltSR <m = Fin-to-≠ <m ∘ ! ∘ ap fst

abstract
  Fin-S-is-inj : ∀ {n} → is-inj (Fin-S {n = n})
  Fin-S-is-inj _ _ = Fin-pred=

  Fin-S-≠ : ∀ {n} {<n₀ <n₁ : Fin n} (p : <n₀ ≠ <n₁) → Fin-S <n₀ ≠ Fin-S <n₁
  Fin-S-≠ {<n₀ = <n₀} {<n₁} p = p ∘ Fin-S-is-inj <n₀ <n₁

  Fin-S^-≠ : ∀ {n} m {<n₀ <n₁ : Fin n} (p : <n₀ ≠ <n₁) → Fin-S^ m <n₀ ≠ Fin-S^ m <n₁
  Fin-S^-≠ O p = p
  Fin-S^-≠ (S n) p = Fin-S-≠ (Fin-S^-≠ n p)

  Fin-S^'-≠ : ∀ {n} m {<n₀ <n₁ : Fin n} (p : <n₀ ≠ <n₁) → Fin-S^' m <n₀ ≠ Fin-S^' m <n₁
  Fin-S^'-≠ O p = p
  Fin-S^'-≠ (S n) p = Fin-S^'-≠ n (Fin-S-≠ p)

Fin-equiv-Empty : Fin 0 ≃ Empty
Fin-equiv-Empty = equiv to from to-from from-to where
  to : Fin 0 → Empty
  to (_ , ())

  from : Empty → Fin 0
  from ()

  abstract
    to-from : ∀ x → to (from x) == x
    to-from ()

    from-to : ∀ x → from (to x) == x
    from-to (_ , ())

Fin-equiv-Coprod : {n : ℕ} → Fin (S n) ≃ Fin n ⊔ Unit
Fin-equiv-Coprod {n} = equiv to from to-from from-to where
  to : Fin (S n) → Fin n ⊔ Unit
  to (m , ltS) = inr unit
  to (m , ltSR lt) = inl (m , lt)

  from : Fin n ⊔ Unit → Fin (S n)
  from (inr _) = n , ltS
  from (inl fin) = Fin-S fin

  abstract
    to-from : ∀ x → to (from x) == x
    to-from (inr _) = idp
    to-from (inl _) = idp

    from-to : ∀ x → from (to x) == x
    from-to (_ , ltS) = idp
    from-to (_ , ltSR _) = idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Logic.Names where

open import Functional
import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Propositional

module _ {ℓ} where
  ExcludedMiddleOn : Stmt{ℓ} → Stmt
  ExcludedMiddleOn(X) = (X ∨ (¬ X))
  ExcludedMiddle = ∀ₗ(ExcludedMiddleOn)

  WeakExcludedMiddleOn = ExcludedMiddleOn ∘ (¬_)
  WeakExcludedMiddle = ∀ₗ(WeakExcludedMiddleOn)

  NonContradictionOn : Stmt{ℓ} → Stmt
  NonContradictionOn(X) = ¬(X ∧ (¬ X))
  NonContradiction = ∀ₗ(NonContradictionOn)

  DoubleNegationOn : Stmt{ℓ} → Stmt
  DoubleNegationOn(X) = (¬(¬ X)) → X
  DoubleNegation = ∀ₗ(DoubleNegationOn)

module _ where
  private variable ℓ₁ ℓ₂ : Lvl.Level

  TopOrBottom : (Stmt{ℓ₁} → Stmt{Lvl.𝟎} → Stmt{ℓ₂}) → Stmt{ℓ₁} → Stmt
  TopOrBottom(_≡_)(P) = (P ≡ ⊤) ∨ (P ≡ ⊥)

module _ {ℓ₁ ℓ₂} where
  CallCCOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  CallCCOn(X)(Y) = (((X → Y) → X) → X)
  CallCC = ∀²(CallCCOn)

  ContrapositiveOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  ContrapositiveOn(X)(Y) = (X → Y) → ((¬ Y) → (¬ X))
  Contrapositive = ∀²(ContrapositiveOn)

  DisjunctiveSyllogismₗOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  DisjunctiveSyllogismₗOn(X)(Y) = ((X ∨ Y) ∧ (¬ Y)) → X
  DisjunctiveSyllogismₗ = ∀²(DisjunctiveSyllogismₗOn)

  DisjunctiveSyllogismᵣOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  DisjunctiveSyllogismᵣOn(X)(Y) = ((X ∨ Y) ∧ (¬ X)) → Y
  DisjunctiveSyllogismᵣ = ∀²(DisjunctiveSyllogismᵣOn)

  MaterialImplicationOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  MaterialImplicationOn(X)(Y) = (X → Y) ↔ ((¬ X) ∨ Y)
  MaterialImplication = ∀²(MaterialImplicationOn)

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where
  ConstructiveDilemmaOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt{ℓ₃} → Stmt{ℓ₄} → Stmt
  ConstructiveDilemmaOn(X₁)(X₂)(Y₁)(Y₂) = ((X₁ → X₂) ∧ (Y₁ → Y₂) ∧ (X₁ ∨ Y₁)) → (X₂ ∨ Y₂)
  ConstructiveDilemma = ∀⁴(ConstructiveDilemmaOn)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- Classical names

module _ {ℓ₁ ℓ₂} where
  ModusTollensOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  ModusTollensOn(X)(Y) = ((X → Y) ∧ (¬ Y)) → (¬ X)
  ModusTollens = ∀²(ModusTollensOn)

  ModusPonensOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  ModusPonensOn(X)(Y) = ((X → Y) ∧ X) → Y
  ModusPonens = ∀²(ModusPonensOn)

  ReductioAdAbsurdumOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  ReductioAdAbsurdumOn(X)(Y) = ((X → Y) ∧ (X → (¬ Y))) → (¬ X)
  ReductioAdAbsurdum = ∀²(ReductioAdAbsurdumOn)

  ReductioAdAbsurdumNegatedOn : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  ReductioAdAbsurdumNegatedOn(X)(Y) = (((¬ X) → Y) ∧ ((¬ X) → (¬ Y))) → (¬ X)
  ReductioAdAbsurdumNegated = ∀²(ReductioAdAbsurdumNegatedOn)


text:
module Web.URI.Everything where

import Web.URI
import Web.URI.Examples.HelloWorld
import Web.URI.Primitive
import Web.URI.Port
import Web.URI.Port.Primitive
import Web.URI.Scheme
import Web.URI.Scheme.Primitive

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri


text:
------------------------------------------------------------------------------
-- Example of a partial function
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- From (Bove, A. and Capretta, V. (2001)).

module FOT.FOTC.Program.Min.Min where

open import Data.Nat renaming ( suc to succ )
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------
-- Note: Although the function is partial the problem is that it is
-- rejected by Agda's termination checker.

{-# NON_TERMINATING #-}
min : (ℕ → ℕ) → ℕ
min f with f 0
... | 0      = 0
... | succ x = succ (min (λ n → f (succ n)))

------------------------------------------------------------------------------
-- References
--
-- Bove, A. and Capretta, V. (2001). Nested General Recursion and
-- Partiality in Type Theory. In: Theorem Proving in Higher Order
-- Logics (TPHOLs 2001). Ed. by Boulton, R. J. and Jackson,
-- P. B. Vol. 2152. LNCS. Springer, pp. 121–135.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Integer10 where

open import Relation.Binary.PropositionalEquality
  as PropEq using (_≡_; refl)

-- 整数の素朴な定義
--（succ (succ (pred zero))などが有効、という弱点がある）
data ℤ : Set where
  zero : ℤ
  succ : ℤ → ℤ
  pred : ℤ → ℤ

-- 加法
_+_ : ℤ → ℤ → ℤ
zero + y = y
succ x + zero = succ x
succ x + succ y = succ (succ x + y)
succ x + pred y = x + y
pred x + zero = pred x
pred x + succ y = x + y
pred x + pred y = pred (pred x + y)

-- 反数
opposite : ℤ → ℤ
opposite zero = zero
opposite (succ x) = pred (opposite x)
opposite (pred x) = succ (opposite x)

-- 乗法
_*_ : ℤ → ℤ → ℤ
x * zero = zero
x * succ y = (x * y) + x
x * pred y = (x * y) + (opposite x)

infixl 40 _+_
infixl 60 _*_

-- (-1) * (-1) = (+1)
theorem : pred zero * pred zero ≡ succ zero
theorem = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing how the Function.Reasoning module
-- can be used to perform "functional reasoning" similar to what is being
-- described in: https://stackoverflow.com/q/22676703/3168666
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module README.Function.Reasoning where

-- Function.Reasoning exports a flipped application (_|>_) combinator
-- as well as a type annotation (_∶_) combinator.

open import Function.Reasoning

------------------------------------------------------------------------
-- A simple example

module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where

-- Using the combinators we can, starting from a value, chain various
-- functions whilst tracking the types of the intermediate results.

  A→C : A → C
  A→C a =
       a    ∶ A
    |> A→B  ∶ B
    |> B→C  ∶ C

------------------------------------------------------------------------
-- A more concrete example

open import Data.Nat
open import Data.List.Base
open import Data.Char.Base
open import Data.String using (String; toList; fromList; _==_)
open import Function
open import Data.Bool hiding (_≤?_)
open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
open import Agda.Builtin.Equality

-- This can give us for instance this decomposition of a function
-- collecting all of the substrings of the input which happen to be
-- palindromes:

subpalindromes : String → List String
subpalindromes str = let Chars = List Char in
     str                                   ∶ String
  -- first generate the substrings
  |> toList                                ∶ Chars
  |> inits                                 ∶ List Chars
  |> concatMap tails                       ∶ List Chars
  -- then only keeps the ones which are not singletons
  |> filter (λ cs → 2 ≤? length cs)        ∶ List Chars
  -- only keep the ones that are palindromes
  |> map < fromList , fromList ∘ reverse > ∶ List (String × String)
  |> boolFilter (uncurry _==_)             ∶ List (String × String)
  |> map proj₁                             ∶ List String

-- Test cases

_ : subpalindromes "doctoresreverse" ≡ "eve" ∷ "rever" ∷ "srevers" ∷ "esreverse" ∷ []
_ = refl

_ : subpalindromes "elle-meme" ≡ "ll" ∷ "elle" ∷ "mem" ∷ "eme" ∷ []
_ = refl


text:
------------------------------------------------------------------------
-- Safe modules that use --without-K
------------------------------------------------------------------------

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

module README.Safe.Without-K where

-- Definitions of some basic types and some related functions.

import Prelude

-- Logical equivalences.

import Logical-equivalence

-- Some definitions related to Dec.

import Dec

-- Two logically equivalent axiomatisations of equality. Many of the
-- modules below are parametrised by a definition of equality that
-- satisfies these axioms.
--
-- The reason for this parametrisation was that I thought that I might
-- later want to use a definition of equality where the application
-- elim P r (refl x) did not compute to r x, unlike the equality in
-- Equality.Propositional. Now, with the advent of cubical type theory
-- and paths, there is such an equality (see Equality.Path).
--
-- (Note that Equality.Tactic contains a definition of equality which,
-- roughly speaking, computes like the one in Equality.Propositional.)

import Equality

-- One model of the axioms: propositional equality.

import Equality.Propositional

-- A simple tactic for proving equality of equality proofs.

import Equality.Tactic

-- Injections.

import Injection

-- Split surjections.

import Surjection

-- Some definitions related to and properties of natural numbers.

import Nat

-- H-levels, along with some general properties.

import H-level

-- Types with decidable equality have unique identity proofs, and
-- related results.

import Equality.Decidable-UIP

-- Some decision procedures for equality.

import Equality.Decision-procedures

-- Bijections.

import Bijection

-- Integers.

import Integer.Basics

-- Groupoids.

import Groupoid

-- Closure properties for h-levels.

import H-level.Closure

-- Excluded middle.

import Excluded-middle

-- Equivalence relations

import Equivalence-relation

-- Preimages.

import Preimage

-- Is-equivalence, defined in terms of contractible fibres.

import Equivalence.Contractible-preimages

-- Half adjoint equivalences.

import Equivalence.Half-adjoint

-- Equivalences.

import Equivalence

-- A type for values that should be erased at run-time.

import Erased.Basics

-- Equivalences with erased "proofs".

import Equivalence.Erased.Basics

-- Embeddings.

import Embedding

-- A universe which includes several kinds of functions (ordinary
-- functions, logical equivalences, injections, embeddings,
-- surjections, bijections and equivalences).

import Function-universe

-- Some alternative definitions of the concept of being an
-- equivalence.

import Equivalence.Path-split

-- Results relating different instances of certain axioms related to
-- equality.

import Equality.Instances-related

-- A parametrised specification of "natrec", along with a proof that
-- the specification is propositional (assuming extensionality).

import Nat.Eliminator

-- A solver for certain natural number equalities.

import Nat.Solver

-- Some definitions related to the binary sum type former.

import Sum

-- Some definitions related to and properties of booleans.

import Bool

-- Raw monads.

import Monad.Raw

-- Monads.

import Monad

-- The reader monad transformer.

import Monad.Reader

-- The state monad transformer.

import Monad.State

-- The double-negation monad.

import Double-negation

-- Lists.

import List

-- Pullbacks.

import Pullback

-- The univalence axiom.

import Univalence-axiom

-- Pointed types and loop spaces.

import Pointed-type

-- Equalities can be turned into groupoids which are sometimes
-- commutative.

import Equality.Groupoid

-- Groups.

import Group

-- Integers.

import Integer

-- Some definitions related to and properties of finite sets.

import Fin

-- Some definitions related to and properties of the Maybe type.

import Maybe

-- Vectors, defined using a recursive function.

import Vec

-- Vectors, defined using an inductive family.

import Vec.Data

-- Vectors, defined as functions from finite sets.

import Vec.Function

-- Some properties related to the const function.

import Const

-- Support for reflection.

import TC-monad

-- Tactics for proving instances of Σ-cong (and Surjection.Σ-cong)
-- with "better" computational behaviour.

import Tactic.Sigma-cong

-- Code used to construct tactics aimed at making equational reasoning
-- proofs more readable.

import Tactic.By

-- A tactic aimed at making equational reasoning proofs more readable
-- in modules that are parametrised by an implementation of equality.

import Tactic.By.Parametrised
import Tactic.By.Parametrised.Tests

-- Some tactics aimed at making equational reasoning proofs more
-- readable for propositional equality.

import Tactic.By.Propositional

-- A type for values that should be erased at run-time.

import Erased.Level-1

-- Equivalences with erased "proofs", defined in terms of partly
-- erased contractible fibres.

import Equivalence.Erased.Contractible-preimages

-- Equivalences with erased "proofs".

import Equivalence.Erased

-- Embeddings with erased "proofs".

import Embedding.Erased

-- A type for values that should be erased at run-time.

import Erased.Level-2

-- Some results related to the For-iterated-equality predicate
-- transformer.

import For-iterated-equality

-- Properties related to stability for Erased.

import Erased.Stability

-- Some properties that hold for Erased do not hold for every
-- topological modality.

import Erased.Counterexamples

-- Truncation, defined using a kind of Church encoding.

import H-level.Truncation.Church

-- Some omniscience principles.

import Omniscience

-- Bag equivalence for lists.

import Bag-equivalence

-- The All predicate, defined using _∈_.

import List.All

-- The All predicate, defined recursively.

import List.All.Recursive

-- Quotients, defined as families of equivalence classes.

import Quotient.Families-of-equivalence-classes

-- A type for values that should be erased at run-time.

import Erased
import Erased.Without-box-cong

-- A wrapper that turns a representation of natural numbers (with a
-- unique representative for every number) into a representation that
-- computes roughly like the unary natural numbers (at least for some
-- operations).

import Nat.Wrapper

-- A binary representation of natural numbers.

import Nat.Binary

-- Specifications of output-restricted deques (single-ended queues
-- with cons).

import Queue

-- Simple queues, implemented in the usual way using two lists
-- (following Hood and Melville).

import Queue.Simple

-- Queue instances for the queues in Queue.Simple.

import Queue.Simple.Instances

-- Banker's queues (following Okasaki).

import Queue.Bankers

-- Queue instances for the queues in Queue.Bankers.

import Queue.Bankers.Instances

-- Isomorphism of monoids on sets coincides with equality (assuming
-- univalence).

import Univalence-axiom.Isomorphism-is-equality.Monoid

-- In fact, several large classes of algebraic structures satisfy the
-- property that isomorphism coincides with equality (assuming
-- univalence).

import Univalence-axiom.Isomorphism-is-equality.Simple
import Univalence-axiom.Isomorphism-is-equality.Simple.Variant
import Univalence-axiom.Isomorphism-is-equality.More
import Univalence-axiom.Isomorphism-is-equality.More.Examples

-- A class of structures that satisfies the property that isomorphic
-- instances of a structure are equal (assuming univalence). This code
-- is superseded by the code above, but preserved because it is
-- mentioned in a blog post.

import Univalence-axiom.Isomorphism-implies-equality

-- 1-categories.

import Category
import Functor
import Adjunction

-- Aczel's structure identity principle (for 1-categories).

import Structure-identity-principle

-- The structure identity principle can be used to establish that
-- isomorphism coincides with equality (assuming univalence).

import
  Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle

-- Bi-invertibility.

import Bi-invertibility
import Bi-invertibility.Erased

-- Binary trees.

import Tree

-- Implementations of tree sort. One only establishes that the
-- algorithm permutes its input, the other one also establishes
-- sortedness.

import Tree-sort.Partial
import Tree-sort.Full
import Tree-sort.Examples

-- Containers, including a definition of bag equivalence.

import Container

-- An implementation of tree sort which uses containers to represent
-- trees and lists.
--
-- In the module Tree-sort.Full indexed types are used to enforce
-- sortedness, but Containers contains a definition of non-indexed
-- containers, so sortedness is not enforced in this development.
--
-- The implementation using containers has the advantage of uniform
-- definitions of Any/membership/bag equivalence, but the other
-- implementations use more direct definitions and are perhaps a bit
-- "leaner".

import Container.List
import Container.Tree
import Container.Tree-sort
import Container.Tree-sort.Example

-- The stream container.

import Container.Stream

-- Indexed containers.

import Container.Indexed

-- Another definition of indexed containers.

import Container.Indexed.Variant

-- M-types for indexed containers, defined using functions.

import Container.Indexed.M.Function

-- Record types with manifest fields and "with".

import Records-with-with

-- Overview of code related to some papers.

import README.Bag-equivalence
import README.Isomorphism-is-equality
import README.Weak-J

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- An implementation of terminating parsers due to Conor McBride and
-- James McKinna, as presented in the talk Seeing and Doing at the
-- Workshop on Termination and Type Theory, Hindås, Sweden, 2002.

{-# OPTIONS --type-in-type #-}

module SeeingAndDoing where

open import Data.Unit
open import Data.Bool
open import Data.List
open import Data.Maybe as Maybe
open import Data.String renaming (_==_ to _=S=_)
open import Category.Monad
open RawMonadPlus Maybe.monadPlus
open import Data.Function using (_∘_; const)
open import Relation.Binary.PropositionalEquality

data Token : Set where
  V     : (s : String) → Token
  IF    : Token
  THEN  : Token
  ELSE  : Token
  TRUE  : Token
  FALSE : Token

_==_ : Token → Token → Bool
V s₁  == V s₂  = s₁ =S= s₂
IF    == IF    = true
THEN  == THEN  = true
ELSE  == ELSE  = true
TRUE  == TRUE  = true
FALSE == FALSE = true
_     == _     = false

data Pos : Set where
  L : Pos
  R : Pos

Memo : (Pos → Set) → Pos → Set
Memo P L = ⊤
Memo P R = P L

PosOrder : ∀ j P → (∀ i → Memo P i → P i) → P j
PosOrder L P p = p L _
PosOrder R P p = p R (p L _)

module Combinators (Rec : Set) where

  infixl 25 _∙_ _!_
  infixl 15 _+_

  data _⟨_⟩_ : Pos → Set → Pos → Set where
    rec  : R ⟨ Rec ⟩ R
    η    : ∀ {i X} (x : Maybe X) → i ⟨ X ⟩ i
    tok  : ∀ {i} (u : Token) → i ⟨ ⊤ ⟩ R
    vart : ∀ {i} → i ⟨ String ⟩ R
    _+_  : ∀ {i j X} (x y : i ⟨ X ⟩ j) → i ⟨ X ⟩ j
    _∙_  : ∀ {j i k S T}
           (f : i ⟨ (S → T) ⟩ j) (s : j ⟨ S ⟩ k) → i ⟨ T ⟩ k

  for : ∀ {i X} → X → i ⟨ X ⟩ i
  for = η ∘ just

  fail : ∀ {i X} → i ⟨ X ⟩ i
  fail = η nothing

  _!_ : ∀ {i j k S T} → i ⟨ S ⟩ j → j ⟨ T ⟩ k → i ⟨ S ⟩ k
  s ! t = for const ∙ s ∙ t

Grammar : Set → Set
Grammar Rec = L ⟨ Rec ⟩ R
  where open Combinators Rec

module Parser {Rec : Set} (grammar : Grammar Rec) where

  open Combinators Rec

  ⇓ : ∀ {i j X} → i ⟨ X ⟩ j → Maybe X
  ⇓ (η x)   = x
  ⇓ (x + y) = ⇓ x ∣ ⇓ y
  ⇓ (f ∙ s) = ⇓ f ⊛ ⇓ s
  ⇓ _       = nothing

  eat : ∀ {i X} → i ⟨ X ⟩ R → Token → R ⟨ X ⟩ R
  eat {i} x t = PosOrder i P eat′ x t
    where
    P = λ i → ∀ {X} → i ⟨ X ⟩ R → Token → R ⟨ X ⟩ R

    eat′ : ∀ i → Memo P i → P i
    eat′ _ _    (tok u)       t     with u == t
    eat′ _ _    (tok u)       t     | true  = for _
    eat′ _ _    (tok u)       t     | false = fail
    eat′ _ _    vart          (V x) = for x
    eat′ _ eat  (x + y)       t     = eat′ _ eat x t
                                    + eat′ _ eat y t
    eat′ L _    (_∙_ {L} f s) t     = η (⇓ f) ∙ eat′ L _ s t
    eat′ L _    (_∙_ {R} f s) t     = eat′ L _ f t ∙ s
    eat′ R eatL (_∙_ {R} f s) t     = η (⇓ f) ∙ eat′ R eatL s t
                                    + eat′ R eatL f t ∙ s
    eat′ R eatL rec           t     = eatL grammar t
    eat′ _ _    _             _     = fail

  parse : List Token → Maybe Rec
  parse is = ⇓ (foldr (λ t x → eat x t) rec (reverse is))

data CE : Set where
  var : (s : String) → CE
  val : (b : Bool) → CE
  if  : (i t e : CE) → CE

grammar : Grammar CE
grammar = for var ∙ vart
        + for (val true)  ! tok TRUE
        + for (val false) ! tok FALSE
        + for (λ i → if i (val true) (val true)) ! tok IF ∙ rec
        + for if ! tok IF ∙ rec ! tok THEN ∙ rec
                                ! tok ELSE ∙ rec
  where open Combinators CE

test₁ : let open Parser grammar in
        parse (IF ∷ V "x" ∷ THEN ∷ TRUE ∷ ELSE ∷ FALSE ∷ []) ≡
        just (if (var "x") (val true) (val false))
test₁ = refl

-- Takes ages to type check:

-- test₂ : let open Parser grammar in
--         parse (IF ∷ V "x" ∷
--                     THEN ∷ IF ∷ V "y" ∷ THEN ∷ V "z" ∷ ELSE ∷ V "x" ∷
--                     ELSE ∷ FALSE ∷ []) ≡
--         just (if (var "x") (if (var "y") (var "z") (var "x"))
--                            (val false))
-- test₂ = refl

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module IrrelevantLambda where

postulate
  A : Set
  P : A -> Set

f : _ -> Set
f = λ .x -> P x
-- fails because irrelevant lambda may not introduce relevant function type

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NonLinearConstraint where

import Common.Level
open import Common.Equality

test : let X : Set -> Set -> Set
           X = _
       in (A : Set) -> X A A ≡ A
test A = refl
-- should not be solved, solution not uniquely determined


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

module Categories.Object.BinaryProducts {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

open import Level

import Categories.Object.Product as Product
import Categories.Object.Product.Morphisms as ProductMorphisms

open import Categories.Morphisms C

open Product C
open ProductMorphisms C

record BinaryProducts : Set (o ⊔ ℓ ⊔ e) where

  infixr 2 _×_
  infix 10 _⁂_

  field
    product : ∀ {A B} → Product A B

  _×_ : Obj → Obj → Obj
  A × B = Product.A×B (product {A} {B})

  ×-comm : ∀ {A B} → _≅_ (A × B) (B × A)
  ×-comm = Commutative product product

  ×-assoc : ∀ {X Y Z} → _≅_ (X × (Y × Z)) ((X × Y) × Z)
  ×-assoc = Associative product product product product

  -- Convenience!
  π₁ : {A B : Obj} → ((A × B) ⇒ A)
  π₁ = Product.π₁ product

  π₂ : {A B : Obj} → ((A × B) ⇒ B)
  π₂ = Product.π₂ product

  ⟨_,_⟩ : ∀ {A B Q} → (Q ⇒ A) → (Q ⇒ B) → (Q ⇒ (A × B))
  ⟨_,_⟩ = Product.⟨_,_⟩ product

  .commute₁ : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} → π₁ ∘ ⟨ f , g ⟩ ≡ f
  commute₁ = Product.commute₁ product

  .commute₂ : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} → π₂ ∘ ⟨ f , g ⟩ ≡ g
  commute₂ = Product.commute₂ product

  .universal : ∀ {A B C} {f : C ⇒ A} {g : C ⇒ B} {i : C ⇒ (A × B)}
               → π₁ ∘ i ≡ f → π₂ ∘ i ≡ g → ⟨ f , g ⟩ ≡ i
  universal = Product.universal product

  assocˡ : ∀ {A B C} → (((A × B) × C) ⇒ (A × (B × C)))
  assocˡ = _≅_.g ×-assoc

  assocʳ : ∀ {A B C} → ((A × (B × C)) ⇒ ((A × B) × C))
  assocʳ = _≅_.f ×-assoc

  .assocʳ∘assocˡ : ∀ {A B C} → assocʳ {A}{B}{C} ∘ assocˡ {A}{B}{C} ≡ id
  assocʳ∘assocˡ = Iso.isoʳ (_≅_.iso ×-assoc)

  .assocˡ∘assocʳ : ∀ {A B C} → assocˡ {A}{B}{C} ∘ assocʳ {A}{B}{C} ≡ id
  assocˡ∘assocʳ = Iso.isoˡ (_≅_.iso ×-assoc)

  .g-η : ∀ {A B C} {f : C ⇒ (A × B)} → ⟨ π₁ ∘ f , π₂ ∘ f ⟩ ≡ f
  g-η = Product.g-η product

  .η : ∀ {A B} → ⟨ π₁ , π₂ ⟩ ≡ id {A × B}
  η = Product.η product

  .⟨⟩-cong₂ : ∀ {A B C} → {f f′ : C ⇒ A} {g g′ : C ⇒ B} → f ≡ f′ → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g′ ⟩
  ⟨⟩-cong₂ = Product.⟨⟩-cong₂ product

  .⟨⟩-congˡ : ∀ {A B C} → {f f′ : C ⇒ A} {g : C ⇒ B} → f ≡ f′ → ⟨ f , g ⟩ ≡ ⟨ f′ , g ⟩
  ⟨⟩-congˡ pf = ⟨⟩-cong₂ pf refl

  .⟨⟩-congʳ : ∀ {A B C} → {f : C ⇒ A} {g g′ : C ⇒ B} → g ≡ g′ → ⟨ f , g ⟩ ≡ ⟨ f , g′ ⟩
  ⟨⟩-congʳ pf = ⟨⟩-cong₂ refl pf

  _⁂_ : ∀ {A B C D} → (A ⇒ B) → (C ⇒ D) → ((A × C) ⇒ (B × D))
  f ⁂ g = [ product ⇒ product ] f ⁂ g

  swap : ∀ {A B} → ((A × B) ⇒ (B × A))
  swap = ⟨ π₂ , π₁ ⟩

  -- TODO: this is probably harder to use than necessary because of this definition. Maybe make a version
  -- that doesn't have an explicit id in it, too?
  first : ∀ {A B C} → (A ⇒ B) → ((A × C) ⇒ (B × C))
  first f = f ⁂ id

  second : ∀ {A C D} → (C ⇒ D) → ((A × C) ⇒ (A × D))
  second g = id ⁂ g

  -- Just to make this more obvious
  .π₁∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → π₁ ∘ (f ⁂ g) ≡ f ∘ π₁
  π₁∘⁂ {f = f} {g} = commute₁

  .π₂∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D} → π₂ ∘ (f ⁂ g) ≡ g ∘ π₂
  π₂∘⁂ {f = f} {g} = commute₂

  .⁂-cong₂ : ∀ {A B C D}{f g : A ⇒ B}{h i : C ⇒ D}
    → f ≡ g → h ≡ i → f ⁂ h ≡ g ⁂ i
  ⁂-cong₂ = [ product ⇒ product ]⁂-cong₂

  .⁂∘⟨⟩ : ∀ {A B C D E} → {f : B ⇒ C} {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D} → (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f ∘ f′ , g ∘ g′ ⟩
  ⁂∘⟨⟩ = [ product ⇒ product ]⁂∘⟨⟩

  .first∘⟨⟩ : ∀ {A B C D} → {f : B ⇒ C} {f′ : A ⇒ B} {g′ : A ⇒ D} → first f ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f ∘ f′ , g′ ⟩
  first∘⟨⟩ = [ product ⇒ product ]first∘⟨⟩

  .second∘⟨⟩ : ∀ {A B D E} → {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D} → second g ∘ ⟨ f′ , g′ ⟩ ≡ ⟨ f′ , g ∘ g′ ⟩
  second∘⟨⟩ = [ product ⇒ product ]second∘⟨⟩

  .⁂∘⁂ : ∀ {A B C D E F} → {f : B ⇒ C} → {f′ : A ⇒ B} {g : E ⇒ F} {g′ : D ⇒ E} → (f ⁂ g) ∘ (f′ ⁂ g′) ≡ (f ∘ f′) ⁂ (g ∘ g′)
  ⁂∘⁂ = [ product ⇒ product ⇒ product ]⁂∘⁂

  .⟨⟩∘ : ∀ {A B C D} {f : A ⇒ B} {g : A ⇒ C} {q : D ⇒ A} → ⟨ f , g ⟩ ∘ q ≡ ⟨ f ∘ q , g ∘ q ⟩
  ⟨⟩∘ = sym (universal (trans (sym assoc) (∘-resp-≡ˡ commute₁)) (trans (sym assoc) (∘-resp-≡ˡ commute₂)))

  .first∘first : ∀ {A B C D}{f : B ⇒ C} {g : A ⇒ B}
    → first f ∘ first g ≡ first {C = D} (f ∘ g)
  first∘first = [ product ⇒ product ⇒ product ]first∘first

  .second∘second : ∀ {A B C D}{f : B ⇒ C} {g : A ⇒ B}
    → second f ∘ second g ≡ second {A = D} (f ∘ g)
  second∘second = [ product ⇒ product ⇒ product ]second∘second

  .first↔second : ∀ {A B C D}{f : A ⇒ B}{g : C ⇒ D}
    → first f ∘ second g ≡ second g ∘ first f
  first↔second = [ product ⇒ product , product ⇒ product ]first↔second

  .swap∘⟨⟩ : ∀ {A B C} {f : A ⇒ B} {g : A ⇒ C}
    → swap ∘ ⟨ f , g ⟩ ≡ ⟨ g , f ⟩
  swap∘⟨⟩ {A}{B}{C}{f}{g} =
    begin
      ⟨ π₂ , π₁ ⟩ ∘ ⟨ f , g ⟩
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ π₂ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ f , g ⟩ ⟩
    ↓⟨ ⟨⟩-cong₂ commute₂ commute₁ ⟩
      ⟨ g , f ⟩
    ∎ where open HomReasoning

  .swap∘⁂ : ∀ {A B C D} {f : A ⇒ B} {g : C ⇒ D}
    → swap ∘ (f ⁂ g) ≡ (g ⁂ f) ∘ swap
  swap∘⁂ {f = f}{g} =
    begin
      swap ∘ (f ⁂ g)
    ↓⟨ swap∘⟨⟩ ⟩
      ⟨ g ∘ π₂ , f ∘ π₁ ⟩
    ↑⟨ ⁂∘⟨⟩ ⟩
      (g ⁂ f) ∘ swap
    ∎ where open HomReasoning

  .swap∘swap : ∀ {A B} → (swap {A}{B}) ∘ (swap {B}{A}) ≡ id
  swap∘swap = trans swap∘⟨⟩ η

  .assocʳ∘⟨⟩ : ∀ {A B C D} {f : A ⇒ B} {g : A ⇒ C} {h : A ⇒ D}
    → assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡ ⟨ ⟨ f , g ⟩ , h ⟩
  assocʳ∘⟨⟩ {f = f}{g}{h} =
    begin
      assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ↓⟨ ⟨⟩∘ ⟩
      ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      , (π₂ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      ⟩
    ↓⟨ ⟨⟩-cong₂ ⟨⟩∘ assoc ⟩
      ⟨ ⟨ π₁        ∘ ⟨ f , ⟨ g , h ⟩ ⟩
        , (π₁ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
        ⟩
      , π₂ ∘ π₂ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      ⟩
    ↓⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ commute₁ assoc ) (∘-resp-≡ʳ commute₂) ⟩
      ⟨ ⟨ f , π₁ ∘ π₂ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ⟩
      , π₂ ∘ ⟨ g , h ⟩
      ⟩
    ↓⟨ ⟨⟩-cong₂ (⟨⟩-congʳ (∘-resp-≡ʳ commute₂)) commute₂ ⟩
      ⟨ ⟨ f , π₁ ∘ ⟨ g , h ⟩ ⟩ , h ⟩
    ↓⟨ ⟨⟩-congˡ (⟨⟩-congʳ commute₁) ⟩
      ⟨ ⟨ f , g ⟩ , h ⟩
    ∎ where open HomReasoning

  .assocˡ∘⟨⟩ : ∀ {A B C D} {f : A ⇒ B} {g : A ⇒ C} {h : A ⇒ D}
    → assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ≡ ⟨ f , ⟨ g , h ⟩ ⟩
  assocˡ∘⟨⟩ {f = f}{g}{h} =
    begin
      assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩
    ↑⟨ refl ⟩∘⟨ assocʳ∘⟨⟩ ⟩
      assocˡ ∘ assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ↑⟨ assoc ⟩
      (assocˡ ∘ assocʳ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ↓⟨ assocˡ∘assocʳ ⟩∘⟨ refl ⟩
      id ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ↓⟨ identityˡ ⟩
      ⟨ f , ⟨ g , h ⟩ ⟩
    ∎ where open HomReasoning

  .assocʳ∘⁂ : ∀ {A₁ A₂ B₁ B₂ C₁ C₂} {f : A₁ ⇒ A₂} {g : B₁ ⇒ B₂} {h : C₁ ⇒ C₂}
    → assocʳ ∘ (f ⁂ (g ⁂ h)) ≡ ((f ⁂ g) ⁂ h) ∘ assocʳ
  assocʳ∘⁂ {f = f}{g}{h} =
    begin
      assocʳ ∘ (f ⁂ (g ⁂ h))
    ↓⟨ refl ⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
      assocʳ ∘ ⟨ f ∘ π₁ , ⟨ (g ∘ π₁) ∘ π₂ , (h ∘ π₂) ∘ π₂ ⟩ ⟩
    ↓⟨ assocʳ∘⟨⟩ ⟩
      ⟨ ⟨ f ∘ π₁ , (g ∘ π₁) ∘ π₂ ⟩ , (h ∘ π₂) ∘ π₂ ⟩
    ↓⟨ ⟨⟩-cong₂ (⟨⟩-congʳ assoc) assoc ⟩
      ⟨ ⟨ f ∘ π₁ , g ∘ π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ↑⟨ ⟨⟩-congˡ ⁂∘⟨⟩ ⟩
      ⟨ (f ⁂ g) ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ↑⟨ ⁂∘⟨⟩ ⟩
      ((f ⁂ g) ⁂ h) ∘ assocʳ
    ∎ where open HomReasoning

  .assocˡ∘⁂ : ∀ {A₁ A₂ B₁ B₂ C₁ C₂} {f : A₁ ⇒ A₂} {g : B₁ ⇒ B₂} {h : C₁ ⇒ C₂}
    → assocˡ ∘ ((f ⁂ g) ⁂ h) ≡ (f ⁂ (g ⁂ h)) ∘ assocˡ
  assocˡ∘⁂ {f = f}{g}{h} =
    begin
      assocˡ ∘ ((f ⁂ g) ⁂ h)
    ↓⟨ refl ⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
      assocˡ ∘ ⟨ ⟨ (f ∘ π₁) ∘ π₁ , (g ∘ π₂) ∘ π₁ ⟩ , h ∘ π₂ ⟩
    ↓⟨ assocˡ∘⟨⟩ ⟩
      ⟨ (f ∘ π₁) ∘ π₁ , ⟨ (g ∘ π₂) ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ↓⟨ ⟨⟩-cong₂ assoc (⟨⟩-congˡ assoc) ⟩
      ⟨ f ∘ π₁ ∘ π₁ , ⟨ g ∘ π₂ ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ↑⟨ ⟨⟩-congʳ ⁂∘⟨⟩ ⟩
      ⟨ f ∘ π₁ ∘ π₁ , (g ⁂ h) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
    ↑⟨ ⁂∘⟨⟩ ⟩
      (f ⁂ (g ⁂ h)) ∘ assocˡ
    ∎ where open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Relation.Binary.Core

module InsertSort.Impl1.Correctness.Permutation.Base {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Data.List
open import Data.Sum
open import InsertSort.Impl1 _≤_ tot≤
open import List.Permutation.Base A

lemma-insert∼/ : (x : A)(xs : List A) → (insert x xs) / x ⟶ xs
lemma-insert∼/ x [] = /head
lemma-insert∼/ x (y ∷ ys)
    with tot≤ x y
... | inj₁ _ = /head
... | inj₂ _ = /tail (lemma-insert∼/ x ys)

lemma-insert∼ : {xs ys : List A}(x : A) → xs ∼ ys → (x ∷ xs) ∼ insert x ys
lemma-insert∼ {xs} {ys} x xs∼ys = ∼x  /head (lemma-insert∼/ x ys) xs∼ys

theorem-insertSort∼ : (xs : List A) → xs ∼ insertSort xs
theorem-insertSort∼ [] = ∼[]
theorem-insertSort∼ (x ∷ xs) = lemma-insert∼ x (theorem-insertSort∼ xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Lifting of substitutions, and instance of strength for δ
module SOAS.Coalgebraic.Lift {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Families.Core {T}
import SOAS.Families.Delta {T} as δ; open δ.Sorted
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □ ; open □.Sorted
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Strength

private
  variable
    Γ Δ Θ : Ctx
    α : T

module _ {𝒫 : Familyₛ} (𝒫ᴮ : Coalgₚ 𝒫) where
  open Coalgₚ 𝒫ᴮ

  -- General lifting over an arbitrary context
  lift : (Ξ : Ctx) → Γ ~[ 𝒫 ]↝ Δ → (Ξ ∔ Γ) ~[ 𝒫 ]↝ (Ξ ∔ Δ)
  lift ∅ σ v             = σ v
  lift (τ ∙ Ξ) σ new     = η new
  lift (τ ∙ Ξ) σ (old v) = r (lift Ξ σ v) old

  -- Single-variable lifting
  lift₁ : {τ : T} → Γ ~[ 𝒫 ]↝ Δ → (τ ∙ Γ) ~[ 𝒫 ]↝ (τ ∙ Δ)
  lift₁ {τ = τ} = lift ⌈ τ ⌋

-- General lifting of renaming
rlift : (Ξ : Ctx) → Γ ↝ Δ → (Ξ ∔ Γ) ↝ (Ξ ∔ Δ)
rlift Ξ = lift ℐᴮ Ξ

-- Strength for context extension
δ:Strength : (Ξ : Ctx) → Strength (δF Ξ)
δ:Strength Ξ = record
  { str = λ 𝒫ᴮ 𝒳 h σ → h (lift 𝒫ᴮ Ξ σ)
  ; str-nat₁ = λ fᴮ⇒ h σ → cong h (dext (str-nat₁ Ξ fᴮ⇒ σ))
  ; str-nat₂ = λ f h σ → refl
  ; str-unit = λ 𝒳 h → cong h (dext (str-unit Ξ 𝒳))
  ; str-assoc = λ 𝒳 fᶜ h σ ς → cong h (dext (str-assoc Ξ 𝒳 fᶜ σ ς))
  }
  where
  open ≡-Reasoning
  open Coalgₚ
  open Coalgₚ⇒

  str-nat₁ : (Ξ : Ctx){𝒫 𝒬 : Familyₛ} {𝒫ᴮ : Coalgₚ 𝒫}
             {𝒬ᴮ : Coalgₚ 𝒬} {f : 𝒬 ⇾̣ 𝒫}
           → Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f
           → (σ : Γ ~[ 𝒬 ]↝ Δ)(v : ℐ α (Ξ ∔ Γ))
    → lift 𝒫ᴮ Ξ (f ∘ σ) v
    ≡ f (lift 𝒬ᴮ Ξ σ v)
  str-nat₁ ∅ fᴮ⇒ σ v = refl
  str-nat₁ (α ∙ Ξ) {𝒫ᴮ = 𝒫ᴮ} fᴮ⇒ σ new = sym (Coalgₚ⇒.⟨η⟩ fᴮ⇒)
  str-nat₁ (α ∙ Ξ) {𝒫ᴮ = 𝒫ᴮ} {𝒬ᴮ}{f}fᴮ⇒ σ (old v) = begin
       lift 𝒫ᴮ (α ∙ Ξ) (f ∘ σ) (old v)
     ≡⟨ congr (str-nat₁ Ξ fᴮ⇒ σ v) (λ - → r 𝒫ᴮ - old) ⟩
       r 𝒫ᴮ (f (lift 𝒬ᴮ Ξ σ v)) old
     ≡˘⟨ ⟨r⟩ fᴮ⇒ ⟩
       f (lift 𝒬ᴮ (α ∙ Ξ) σ (old v))
     ∎

  str-unit : (Ξ : Ctx) (𝒳 : Familyₛ) (v : ℐ α (Ξ ∔ Γ))
    → lift ℐᴮ Ξ id v ≡ v
  str-unit ∅ 𝒳 v = refl
  str-unit (α ∙ Ξ) 𝒳 new = refl
  str-unit (α ∙ Ξ) 𝒳 (old v) = cong old (str-unit Ξ 𝒳 v)

  str-assoc : (Ξ : Ctx) (𝒳 : Familyₛ) {𝒫 𝒬 ℛ : Familyₛ}
              {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
              {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
              (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f) (open Coalgebraic fᶜ)
              (σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)(v : ℐ α (Ξ ∔ Γ))
    → lift ℛᴮ Ξ (λ u → f (σ u) ς) v
    ≡ lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (lift 𝒬ᴮ Ξ ς)
  str-assoc ∅ 𝒳 fᶜ σ ς v = refl
  str-assoc (β ∙ Ξ) 𝒳 {𝒫ᴮ = 𝒫ᴮ}{𝒬ᴮ}{ℛᴮ} {f} fᶜ σ ς new = begin
       η ℛᴮ new                          ≡˘⟨ f∘η ⟩
       f (η 𝒫ᴮ new) (η 𝒬ᴮ)               ≡⟨ eq-at-new refl ⟩
       f (η 𝒫ᴮ new) (lift 𝒬ᴮ (β ∙ Ξ) ς)  ∎
     where open Coalgebraic fᶜ

  str-assoc {Γ = Γ} (β ∙ Ξ)  𝒳 {𝒫 = 𝒫}{𝒬}{𝒫ᴮ = 𝒫ᴮ}{𝒬ᴮ}{ℛᴮ}{f} fᶜ σ ς (old v) =
     begin
         r ℛᴮ   (lift ℛᴮ Ξ (λ u → f (σ u) ς) v)   old
     ≡⟨ congr (str-assoc Ξ 𝒳 fᶜ σ ς v) (λ - → r ℛᴮ - old) ⟩
         r ℛᴮ (  lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v   (lift 𝒬ᴮ Ξ ς)) old
     ≡⟨ congr (str-nat₁ Ξ fᴮ⇒ (σ) v) (λ - → r ℛᴮ (- (lift 𝒬ᴮ Ξ ς)) old) ⟩
         r ℛᴮ (f (lift 𝒫ᴮ Ξ σ v) (lift 𝒬ᴮ Ξ ς)) old
     ≡⟨ r∘f ⟩
         f (lift 𝒫ᴮ Ξ σ v)   (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)
     ≡˘⟨ congr (str-nat₁ Ξ fᴮ⇒ σ v) (λ - → - (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)) ⟩
         lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (λ u → r 𝒬ᴮ (lift 𝒬ᴮ Ξ ς u) old)
     ∎
     where open Coalgebraic fᶜ renaming (ᴮ⇒ to fᴮ⇒)

module δ:Str Θ = Strength (δ:Strength Θ)

-- Derived lifting properties
rlift-id : (𝒳 : Familyₛ)(Ξ : Ctx)(b : δ Ξ (□ 𝒳) α Γ)
         → b (rlift Ξ id) ≡ b id
rlift-id 𝒳 Ξ = Strength.str-unit (δ:Strength Ξ) 𝒳

lift-comp : {𝒫 𝒬 : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}{𝒬ᴮ : Coalgₚ 𝒬}
            (𝒳 : Familyₛ)(Ξ : Ctx){f : 𝒬 ⇾̣ 𝒫}
            (fᴮ⇒ : Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f)
            (h : δ Ξ 〖 𝒫 , 𝒳 〗 α Γ) (σ : Γ ~[ 𝒬 ]↝ Δ)
  → h (lift 𝒫ᴮ Ξ (f ∘ σ))
  ≡ h (f ∘ lift 𝒬ᴮ Ξ σ)
lift-comp 𝒳 Ξ fᴮ⇒ h σ = Strength.str-nat₁ (δ:Strength Ξ) {𝒳 = 𝒳} fᴮ⇒ h σ

lift-assoc : {𝒫 𝒬 ℛ : Familyₛ}
            {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
            (𝒳 : Familyₛ)(Ξ : Ctx) {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
            (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
            (open Coalgebraic fᶜ)
            (h : δ Ξ 〖 ℛ , 𝒳 〗 α Γ)
            (σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)
  → h (lift ℛᴮ Ξ (λ v → f (σ v) ς))
  ≡ h (λ v → lift 〖𝒫,𝒴〗ᴮ Ξ (f ∘ σ) v (lift 𝒬ᴮ Ξ ς))
lift-assoc 𝒳 Ξ fᶜ h σ ς = Strength.str-assoc (δ:Strength Ξ) 𝒳 fᶜ h σ ς

lift-dist : {𝒫 𝒬 ℛ : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}{𝒬ᴮ : Coalgₚ 𝒬}{ℛᴮ : Coalgₚ ℛ}
            (𝒳 : Familyₛ){Ξ : Ctx}{f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
            (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
            (h : δ Ξ 〖 ℛ , 𝒳 〗 α Γ)
            (σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)
  → h (lift ℛᴮ Ξ (λ v → f (σ v) ς))
  ≡ h (λ v → f (lift 𝒫ᴮ Ξ σ v) (lift 𝒬ᴮ Ξ ς))
lift-dist 𝒳 {Ξ} = Strength.str-dist (δ:Strength Ξ) 𝒳

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)

module Algebra.FunctionProperties.Consequences
  {a ℓ} (S : Setoid a ℓ) where

{-# WARNING_ON_IMPORT
"Algebra.FunctionProperties.Consequences was deprecated in v1.3.
Use Algebra.Consequences.Setoid instead."
#-}

open import Algebra.Consequences.Setoid S public


text:
module Issue453 where

postulate
  A     : Set
  fails : {x : _} → A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Unit where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₋₁ ; ∣_∣ to ∣_∣₋₁)
open import Cubical.HITs.Nullification
open import Cubical.Data.Int hiding (_+_ ; +-comm)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation
open import Cubical.Homotopy.Connected
open import Cubical.Data.Unit
open import Cubical.Algebra.Group

-- H⁰(Unit)
open GroupHom
open GroupIso
H⁰-Unit≅ℤ : GroupIso (coHomGr 0 Unit) intGroup
fun (GroupIso.map H⁰-Unit≅ℤ) = sRec isSetInt (λ f → f tt)
isHom (GroupIso.map H⁰-Unit≅ℤ) = sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _) λ a b → addLemma (a tt) (b tt)
inv H⁰-Unit≅ℤ a = ∣ (λ _ → a) ∣₂
rightInv H⁰-Unit≅ℤ _ = refl
leftInv H⁰-Unit≅ℤ = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) λ a → refl

{- Hⁿ(Unit) for n ≥ 1 -}
isContrHⁿ-Unit : (n : ℕ) → isContr (coHom (suc n) Unit)
isContrHⁿ-Unit n = subst isContr (λ i → ∥ UnitToTypePath (coHomK (suc n)) (~ i) ∥₂) (helper' n)
  where
  helper' : (n : ℕ) → isContr (∥ coHomK (suc n) ∥₂)
  helper' n =
    subst isContr
      ((isoToPath (truncOfTruncIso {A = S₊ (1 + n)} 2 (1 + n)))
         ∙∙ sym propTrunc≡Trunc2
         ∙∙ λ i → ∥ hLevelTrunc (suc (+-comm n 2 i)) (S₊ (1 + n)) ∥₂)
      (isConnectedSubtr 2 (helper2 n .fst)
        (subst (λ x → isConnected x (S₊ (suc n))) (sym (helper2 n .snd)) (sphereConnected (suc n))) )
    where
    helper2 : (n : ℕ) → Σ[ m ∈ ℕ ] m + 2  ≡ 2 + n
    helper2 zero = 0 , refl
    helper2 (suc n) = (suc n) , λ i → suc (+-comm n 2 i)

Hⁿ-Unit≅0 : (n : ℕ) → GroupIso (coHomGr (suc n) Unit) trivialGroup
GroupHom.fun (GroupIso.map (Hⁿ-Unit≅0 n)) _ = _
GroupHom.isHom (GroupIso.map (Hⁿ-Unit≅0 n)) _ _ = refl
GroupIso.inv (Hⁿ-Unit≅0 n) _ = 0ₕ (suc n)
GroupIso.rightInv (Hⁿ-Unit≅0 n) _ = refl
GroupIso.leftInv (Hⁿ-Unit≅0 n) _ = isOfHLevelSuc 0 (isContrHⁿ-Unit n) _ _

{- Hⁿ for arbitrary contractible types -}
private
  Hⁿ-contrTypeIso : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A
                   → Iso (coHom (suc n) A) (coHom (suc n) Unit)
  Hⁿ-contrTypeIso n contr = compIso (setTruncIso (isContr→Iso2 contr))
                                    (setTruncIso (invIso (isContr→Iso2 isContrUnit)))

Hⁿ-contrType≅0 : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A
              → GroupIso (coHomGr (suc n) A) trivialGroup
fun (GroupIso.map (Hⁿ-contrType≅0 _ _)) _ = _
isHom (GroupIso.map (Hⁿ-contrType≅0 _ _)) _ _ = refl
inv (Hⁿ-contrType≅0 n _) _ = 0ₕ (suc n)
rightInv (Hⁿ-contrType≅0 _ _) _ = refl
leftInv (Hⁿ-contrType≅0 {A = A} n contr) _ = isOfHLevelSuc 0 helper _ _
  where
  helper : isContr (coHom (suc n) A)
  helper = (Iso.inv (Hⁿ-contrTypeIso n contr) (0ₕ (suc n)))
          , λ y →  cong (Iso.inv (Hⁿ-contrTypeIso n contr))
                         (isOfHLevelSuc 0 (isContrHⁿ-Unit n) (0ₕ (suc n)) (Iso.fun (Hⁿ-contrTypeIso n contr) y))
                  ∙ Iso.leftInv (Hⁿ-contrTypeIso n contr) y

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical