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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped as U
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Symmetry
import Definition.LogicalRelation.Weakening as W

open import Tools.Product
import Tools.PropositionalEquality as PE

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

-- Neutral reflexive types are reducible.
neu : ∀ {l Γ A r ll} (neA : Neutral A)
    → Γ ⊢ A ^ [ r , ι ll ]
    → Γ ⊢ A ~ A ∷ Univ r ll ^ [ ! , next ll ]
    → Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ]
neu neA A A~A = ne′ _ (idRed:*: A) neA A~A

  -- Helper function for reducible neutral equality of a specific type of derivation.
neuEq′ : ∀ {l Γ A B r ll} ([A] : Γ ⊩⟨ l ⟩ne A ^[ r , ll ])
         (neA : Neutral A)
         (neB : Neutral B)
       → Γ ⊢ A ^ [ r , ι ll ] → Γ ⊢ B ^ [ r , ι ll ]
       → Γ ⊢ A ~ B ∷ Univ r ll ^ [ ! , next ll ]
       → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ι ll ] / ne-intr [A]
neuEq′ (noemb (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neA neB A B A~B =
  let A≡K = whnfRed* D (ne neA)
  in  ne₌ _ (idRed:*: B) neB (PE.subst (λ x → _ ⊢ x ~ _ ∷ _ ^ _) A≡K A~B)
neuEq′ {ι ¹} (emb emb< X) = neuEq′ X
neuEq′ {∞} (emb ∞< X) = neuEq′ X

-- Neutrally equal types are of reducible equality.
neuEq : ∀ {l Γ A B r ll} ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ])
        (neA : Neutral A)
        (neB : Neutral B)
      → Γ ⊢ A ^ [ r , ι ll ] → Γ ⊢ B ^ [ r , ι ll ]
      → Γ ⊢ A ~ B ∷ Univ r ll ^ [ ! , next ll ]
      → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ι ll ] / [A]
neuEq [A] neA neB A B A~B =
  irrelevanceEq (ne-intr (ne-elim neA [A]))
                [A]
                (neuEq′ (ne-elim neA [A]) neA neB A B A~B)

mutual
  neuTerm⁰ : ∀ {Γ A r n} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ r) (neN : Neutral n)
          → Γ ⊢ n ∷ A ^ r
          → Γ ⊢ n ~ n ∷ A ^ r
          → Γ ⊩⟨ ι ⁰ ⟩ n ∷ A ^ r / [A]

  neuTerm⁰ (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN n n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in  ℕₜ _ (idRedTerm:*: (conv n A≡ℕ)) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′))
  neuTerm⁰ {r = [ ! , ll ]} (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in  neₜ _ (idRedTerm:*: (conv n A≡K)) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K))
  neuTerm⁰ {r = [ ! , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (idRedTerm:*: (conv n A≡ΠFG)) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm⁰ ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b
                            (ρn ∘ⱼ a)
                            (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                            (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm⁰ ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))
  neuTerm⁰ (Emptyᵣ [[ ⊢A , ⊢B , D ]]) neN n n~n =
    let A≡ℕ  = subset* D
    in Emptyₜ (ne (conv n A≡ℕ))
  neuTerm⁰ {r = [ % , ll ]} (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in  neₜ n
  neuTerm⁰ {r = [ % , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n = let A≡ΠFG = subset* (red D) in conv n A≡ΠFG
  neuTerm⁰ {r = [ % , ll ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n = let A≡ΠFG = subset* (red D) in conv n A≡ΠFG

  neuEqTerm⁰ : ∀ {Γ A n n′ r} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ r)
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ n  ∷ A ^ r
            → Γ ⊢ n′ ∷ A ^ r
            → Γ ⊢ n ~ n′ ∷ A ^ r
            → Γ ⊩⟨ ι ⁰ ⟩ n ≡ n′ ∷ A ^ r / [A]

  neuEqTerm⁰ (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ n n′ n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  ℕₜ₌ _ _ (idRedTerm:*: (conv n A≡ℕ)) (idRedTerm:*: (conv n′ A≡ℕ))
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm⁰ (Emptyᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ n n′ n~n′ =
    let A≡Empty = subset* D
    in  Emptyₜ₌  (ne (conv n A≡Empty) (conv n′ A≡Empty))
  neuEqTerm⁰ {r = [ ! , ll ]} (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in  neₜ₌ _ _ (idRedTerm:*: (conv n A≡K)) (idRedTerm:*: (conv n′ A≡K))
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K))
  neuEqTerm⁰ {r = [ % , ll ]} (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in neₜ₌ n n′
  neuEqTerm⁰ {r = [ ! , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let [ΠFG] = Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (idRedTerm:*: (conv n A≡ΠFG)) (idRedTerm:*: (conv n′ A≡ΠFG))
            (ne neN) (ne neN′) n≡n′
            (neuTerm⁰ [ΠFG] neN n n~n) (neuTerm⁰ [ΠFG] neN′ n′ n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = wkTerm [ρ] ⊢Δ n
                   ρn′ = wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm⁰ ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a))
  neuEqTerm⁰ {r = [ % , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let A≡ΠFG = subset* D
    in conv n A≡ΠFG , conv n′ A≡ΠFG
  neuEqTerm⁰ {r = [ % , ll ]} (∃ᵣ′ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let A≡ΠFG = subset* D
    in conv n A≡ΠFG , conv n′ A≡ΠFG

mutual
  -- Neutral reflexive terms are reducible.
  neuTerm : ∀ {l Γ A r n} ([A] : Γ ⊩⟨ l ⟩ A ^ r) (neN : Neutral n)
          → Γ ⊢ n ∷ A ^ r
          → Γ ⊢ n ~ n ∷ A ^ r
          → Γ ⊩⟨ l ⟩ n ∷ A ^ r / [A]
  neuTerm {ι ¹} (Uᵣ′ A .(next ⁰) r ⁰ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN n n~n =
    let n' = (conv n (subset* D))
        n~n' = ~-conv  n~n (subset* D)
        [n] = neu {l = ι ¹} neN (univ n') n~n'
    in Uₜ _ (idRedTerm:*: n') (ne neN) (~-to-≅ₜ n~n')
            (λ {ρ} [ρ] ⊢Δ → let n'ρ = wkTerm [ρ] ⊢Δ n'
                                n~n'ρ = ~-wk [ρ] ⊢Δ n~n'
                                [nρ] = neu (wkNeutral ρ neN) (univ n'ρ) n~n'ρ
                            in [nρ])
  neuTerm {∞} (Uᵣ′ A .(next ¹) r ¹ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN n n~n =
    let n' = (conv n (subset* D))
        n~n' = ~-conv  n~n (subset* D)
        [n] = neu {l = ∞} neN (univ n') n~n'
    in Uₜ _ (idRedTerm:*: n') (ne neN) (~-to-≅ₜ n~n')
            (λ {ρ} [ρ] ⊢Δ → let n'ρ = wkTerm [ρ] ⊢Δ n'
                                n~n'ρ = ~-wk [ρ] ⊢Δ n~n'
                                [nρ] = neu (wkNeutral ρ neN) (univ n'ρ) n~n'ρ
                            in [nρ])
  neuTerm (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN n n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in  ℕₜ _ (idRedTerm:*: (conv n A≡ℕ)) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′))
  neuTerm {r = [ ! , ll ]} (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in  neₜ _ (idRedTerm:*: (conv n A≡K)) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K))
  neuTerm {r = [ ! , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (idRedTerm:*: (conv n A≡ΠFG)) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b
                            (ρn ∘ⱼ a)
                            (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                            (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))
  neuTerm (Emptyᵣ [[ ⊢A , ⊢B , D ]]) neN n n~n =
    let A≡ℕ  = subset* D
    in Emptyₜ (ne (conv n A≡ℕ))
  neuTerm {r = [ % , ll ]} (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN n n~n =
    let A≡K = subset* D
    in  neₜ n
  neuTerm {r = [ % , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n = let A≡ΠFG = subset* (red D) in conv n A≡ΠFG
  neuTerm {r = [ % , ll ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN n n~n = let A≡ΠFG = subset* (red D) in conv n A≡ΠFG
  neuTerm {ι ¹} (emb l< X) neN n = neuTerm X neN n
  neuTerm {∞} (emb l< X) neN n = neuTerm X neN n

  -- Neutrally equal terms are of reducible equality.
  neuEqTerm : ∀ {l Γ A n n′ r} ([A] : Γ ⊩⟨ l ⟩ A ^ r)
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ n  ∷ A ^ r
            → Γ ⊢ n′ ∷ A ^ r
            → Γ ⊢ n ~ n′ ∷ A ^ r
            → Γ ⊩⟨ l ⟩ n ≡ n′ ∷ A ^ r / [A]
  neuEqTerm {ι ¹} (Uᵣ′ A _ r ⁰ l< PE.refl D) neN neN′ n n′ n~n' =
    let n~n = ~-trans n~n' (~-sym n~n')
        n'~n' = ~-trans (~-sym n~n') n~n'
        [[n]]   = neuTerm (Uᵣ (Uᵣ r ⁰ l< PE.refl D)) neN n n~n
        [[n']]  = neuTerm (Uᵣ (Uᵣ r ⁰ l< PE.refl D)) neN′ n′ n'~n'
        n' = conv n (subset* (red D))
        n′' = conv n′ (subset* (red D))
        n~n'U = ~-conv n~n' (subset* (red D))
        [n]  = neu {l = ι ¹} neN  (univ n') (~-conv n~n (subset* (red D)))
        [n′] = neu {l = ι ¹} neN′ (univ n′') (~-conv n'~n' (subset* (red D)))
    in Uₜ₌ [[n]] [[n']] (~-to-≅ₜ n~n'U)
           (λ [ρ] ⊢Δ → W.wkEq [ρ] ⊢Δ [n] ((neuEq [n] neN neN′ (univ n') (univ n′') n~n'U)))
  neuEqTerm {∞} (Uᵣ′ A _ r ¹ l< PE.refl D) neN neN′ n n′ n~n' =
    let n~n = ~-trans n~n' (~-sym n~n')
        n'~n' = ~-trans (~-sym n~n') n~n'
        [[n]]   = neuTerm (Uᵣ (Uᵣ r ¹ l< PE.refl D)) neN n n~n
        [[n']]  = neuTerm (Uᵣ (Uᵣ r ¹ l< PE.refl D)) neN′ n′ n'~n'
        n' = conv n (subset* (red D))
        n′' = conv n′ (subset* (red D))
        n~n'U = ~-conv n~n' (subset* (red D))
        [n]  = neu {l = ∞} neN  (univ n') (~-conv n~n (subset* (red D)))
        [n′] = neu {l = ∞} neN′ (univ n′') (~-conv n'~n' (subset* (red D)))
    in Uₜ₌ [[n]] [[n']] (~-to-≅ₜ n~n'U)
           (λ [ρ] ⊢Δ → W.wkEq [ρ] ⊢Δ [n] ((neuEq [n] neN neN′ (univ n') (univ n′') n~n'U)))
  neuEqTerm (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ n n′ n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  ℕₜ₌ _ _ (idRedTerm:*: (conv n A≡ℕ)) (idRedTerm:*: (conv n′ A≡ℕ))
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm (Emptyᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ n n′ n~n′ =
    let A≡Empty = subset* D
    in  Emptyₜ₌  (ne (conv n A≡Empty) (conv n′ A≡Empty))
  neuEqTerm {r = [ ! , ll ]} (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in  neₜ₌ _ _ (idRedTerm:*: (conv n A≡K)) (idRedTerm:*: (conv n′ A≡K))
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K))
  neuEqTerm {r = [ % , ll ]} (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ n n′ n~n′ =
    let A≡K = subset* D
    in neₜ₌ n n′
  neuEqTerm {r = [ ! , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let [ΠFG] = Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (idRedTerm:*: (conv n A≡ΠFG)) (idRedTerm:*: (conv n′ A≡ΠFG))
            (ne neN) (ne neN′) n≡n′
            (neuTerm [ΠFG] neN n n~n) (neuTerm [ΠFG] neN′ n′ n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = wkTerm [ρ] ⊢Δ n
                   ρn′ = wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a))
  neuEqTerm {r = [ % , ll ]} (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let A≡ΠFG = subset* D
    in conv n A≡ΠFG , conv n′ A≡ΠFG
  neuEqTerm {r = [ % , ll ]} (∃ᵣ′ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ n n′ n~n′ =
    let A≡ΠFG = subset* D
    in conv n A≡ΠFG , conv n′ A≡ΠFG
  neuEqTerm {ι ¹} (emb l< X) neN n neN′ n:≡:n′ = neuEqTerm X neN n neN′ n:≡:n′
  neuEqTerm {∞} (emb l< X) neN n neN′ n:≡:n′ = neuEqTerm X neN n neN′ n:≡:n′

-- Neutral reflexive types are reducible.
neu:⇒*: : ∀ {l Γ A K r ll} (neK : Neutral K)
    → Γ ⊢ A :⇒*: K ^ [ r , ι ll ]
    → Γ ⊢ K ~ K ∷ Univ r ll ^ [ ! , next ll ]
    → Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ]
neu:⇒*: neK D K~K = ne′ _ D neK K~K

  -- Helper function for reducible neutral equality of a specific type of derivation.
neuEq:⇒*:′ : ∀ {l Γ A B K L r ll} ([A] : Γ ⊩⟨ l ⟩ne A ^[ r , ll ])
         (neK : Neutral K)
         (neL : Neutral L)
       → Γ ⊢ A :⇒*: K ^ [ r , ι ll ]
       → Γ ⊢ B :⇒*: L ^ [ r , ι ll ]
       → Γ ⊢ K ~ L ∷ Univ r ll ^ [ ! , next ll ]
       → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ι ll ] / ne-intr [A]
neuEq:⇒*:′ (noemb (ne A' [[ ⊢A , ⊢B , D ]] neA A≡A)) neK neL [[ ⊢A' , ⊢K , D' ]] [B] A~B =
  let A≡K = whrDet* (D , ne neA) (D' , ne neK) -- (ne neA)
  in ne₌ _ [B] neL (PE.subst (λ x → _ ⊢ x ~ _ ∷ _ ^ _) (PE.sym A≡K) A~B)
neuEq:⇒*:′ {ι ¹} (emb emb< X) = neuEq:⇒*:′ X
neuEq:⇒*:′ {∞} (emb ∞< X) = neuEq:⇒*:′ X

-- Neutrally equal types are of reducible equality.
neuEq:⇒*: : ∀ {l Γ A B K L r ll} ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ι ll ])
         (neK : Neutral K)
         (neL : Neutral L)
       → Γ ⊢ A :⇒*: K ^ [ r , ι ll ]
       → Γ ⊢ B :⇒*: L ^ [ r , ι ll ]
       → Γ ⊢ K ~ L ∷ Univ r ll ^ [ ! , next ll ]
      → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ι ll ] / [A]
neuEq:⇒*: [A] neK neL [[ ⊢A , ⊢K , D ]] B A~B =
  let ne-intrA = ne-elim′ D neK [A] PE.refl
  in irrelevanceEq (ne-intr ne-intrA)
                [A]
                (neuEq:⇒*:′ ne-intrA neK neL [[ ⊢A , ⊢K , D ]] B A~B)

app:⇒*: : ∀ {Γ a t u A B rA lA lB l}
          (⊢a : Γ ⊢ a ∷ A ^ [ rA , ι lA ])
          (D : Γ ⊢ t :⇒*: u ∷ (Π A ^ rA ° lA ▹ B ° lB ° l) ^ ι l)
        → Γ ⊢ t ∘ a ^ l :⇒*: u ∘ a ^ l ∷ B [ a ] ^ ι lB
app:⇒*: ⊢a [[ ⊢t , ⊢u , D ]] = [[ ⊢t ∘ⱼ ⊢a , ⊢u ∘ⱼ ⊢a , appRed* ⊢a D ]]

mutual
  neuTerm:⇒*:⁰ : ∀ {Γ A ll t n} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ ! , ll ]) (neN : Neutral n)
          → Γ ⊢ t :⇒*: n ∷ A ^ ll
          → Γ ⊢ n ~ n ∷ A ^ [ ! , ll ]
          → Γ ⊩⟨ ι ⁰ ⟩ t ∷ A ^ [ ! , ll ] / [A]

  neuTerm:⇒*:⁰ (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN [[ ⊢t , n , D' ]] n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in  ℕₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ℕ) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′))
  neuTerm:⇒*:⁰ (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN [[ ⊢t , n , D' ]] n~n =
    let A≡K = subset* D
    in  neₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡K) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K))
  neuTerm:⇒*:⁰ (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN [[ ⊢t , n , D' ]] n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ΠFG) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm⁰ ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b (ρn ∘ⱼ a) (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                             ((~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b)))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))

  neuEqTerm:⇒*:⁰ : ∀ {Γ A n n′ t u ll} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ [ ! , ll ])
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ t :⇒*: n ∷ A ^ ll
            → Γ ⊢ u :⇒*: n′ ∷ A ^ ll
            → Γ ⊢ n ~ n′ ∷ A ^ [ ! , ll ]
            → Γ ⊩⟨ ι ⁰ ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]

  neuEqTerm:⇒*:⁰ (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  ℕₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ℕ) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡ℕ)
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm:⇒*:⁰ (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let A≡K = subset* D
    in  neₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡K) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡K)
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K))
  neuEqTerm:⇒*:⁰ (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let [ΠFG] = Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ΠFG) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡ΠFG)
            (ne neN) (ne neN′) n≡n′
            (neuTerm:⇒*:⁰ [ΠFG] neN [[ ⊢t , n , D' ]] n~n) (neuTerm:⇒*:⁰ [ΠFG] neN′ [[ ⊢u , n′ , D′ ]] n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = wkTerm [ρ] ⊢Δ n
                   ρn′ = wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a) )

mutual
  -- Neutral reflexive terms are reducible.
  neuTerm:⇒*: : ∀ {l Γ A ll t n} ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ]) (neN : Neutral n)
          → Γ ⊢ t :⇒*: n ∷ A ^ ll
          → Γ ⊢ n ~ n ∷ A ^ [ ! , ll ]
          → Γ ⊩⟨ l ⟩ t ∷ A ^ [ ! , ll ] / [A]
  neuTerm:⇒*: {ι ¹} (Uᵣ′ A .(next ⁰) r ⁰ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN [[ ⊢t , n , D' ]] n~n =
    let D'' = conv:⇒*: [[ ⊢t , n , D' ]] (subset* D)
        n~n' = ~-conv  n~n (subset* D)
    in Uₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] (subset* D))
            (ne neN) (~-to-≅ₜ n~n')
            (λ {ρ} [ρ] ⊢Δ → let ρD' = wkRed:*:Term [ρ] ⊢Δ D''
                                n~n'ρ = ~-wk [ρ] ⊢Δ n~n'
                            in neu:⇒*: (wkNeutral ρ neN) (univ:⇒*: ρD') n~n'ρ)
  neuTerm:⇒*: {∞} (Uᵣ′ A .(next ¹) r ¹ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN  [[ ⊢t , n , D' ]] n~n =
    let D'' = conv:⇒*: [[ ⊢t , n , D' ]] (subset* D)
        n~n' = ~-conv  n~n (subset* D)
    in Uₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] (subset* D))
            (ne neN) (~-to-≅ₜ n~n')
            (λ {ρ} [ρ] ⊢Δ → let ρD' = wkRed:*:Term [ρ] ⊢Δ D''
                                n~n'ρ = ~-wk [ρ] ⊢Δ n~n'
                            in neu:⇒*: (wkNeutral ρ neN) (univ:⇒*: ρD') n~n'ρ)
  neuTerm:⇒*: (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN [[ ⊢t , n , D' ]] n~n =
    let A≡ℕ  = subset* D
        n~n′ = ~-conv n~n A≡ℕ
        n≡n  = ~-to-≅ₜ n~n′
    in  ℕₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ℕ) n≡n (ne (neNfₜ neN (conv n A≡ℕ) n~n′))
  neuTerm:⇒*: (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) neN [[ ⊢t , n , D' ]] n~n =
    let A≡K = subset* D
    in  neₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡K) (neNfₜ neN (conv n A≡K)
            (~-conv n~n A≡K))
  neuTerm:⇒*: (Πᵣ′ rF lF lG lF≤ lG≤ F G D ⊢F ⊢G A≡A [F] [G] G-ext) neN [[ ⊢t , n , D' ]] n~n =
    let A≡ΠFG = subset* (red D)
    in  Πₜ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ΠFG) (ne neN) (~-to-≅ₜ (~-conv n~n A≡ΠFG))
           (λ {ρ} [ρ] ⊢Δ [a] [b] [a≡b] →
              let A≡ΠFG = subset* (red D)
                  ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  G[a]≡G[b] = escapeEq ([G] [ρ] ⊢Δ [b])
                                          (symEq ([G] [ρ] ⊢Δ [a]) ([G] [ρ] ⊢Δ [b])
                                                 (G-ext [ρ] ⊢Δ [a] [b] [a≡b]))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  b = escapeTerm ([F] [ρ] ⊢Δ) [b]
                  a≡b = escapeTermEq ([F] [ρ] ⊢Δ) [a≡b]
                  ρn = conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG
                  neN∘a = ∘ₙ (wkNeutral ρ neN)
                  neN∘b = ∘ₙ (wkNeutral ρ neN)
              in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∘a neN∘b (ρn ∘ⱼ a) (conv (ρn ∘ⱼ b) (≅-eq G[a]≡G[b]))
                            ((~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡b)))
           (λ {ρ} [ρ] ⊢Δ [a] →
              let ρA≡ρΠFG = wkEq [ρ] ⊢Δ (subset* (red D))
                  a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                  a≡a = escapeTermEq ([F] [ρ] ⊢Δ) (reflEqTerm ([F] [ρ] ⊢Δ) [a])
              in  neuTerm ([G] [ρ] ⊢Δ [a]) (∘ₙ (wkNeutral ρ neN))
                          (conv (wkTerm [ρ] ⊢Δ n) ρA≡ρΠFG ∘ⱼ a)
                          (~-app (~-wk [ρ] ⊢Δ (~-conv n~n A≡ΠFG)) a≡a))
  neuTerm:⇒*: {ι ¹} (emb l< X) neN n n:≡:n′ = neuTerm:⇒*: X neN n n:≡:n′
  neuTerm:⇒*: {∞} (emb l< X) neN n n:≡:n′ = neuTerm:⇒*: X neN n n:≡:n′

  -- Neutrally equal terms are of reducible equality.
  neuEqTerm:⇒*: : ∀ {l Γ A t u n n′ ll} ([A] : Γ ⊩⟨ l ⟩ A ^ [ ! , ll ])
              (neN : Neutral n) (neN′ : Neutral n′)
            → Γ ⊢ t :⇒*: n ∷ A ^ ll
            → Γ ⊢ u :⇒*: n′ ∷ A ^ ll
            → Γ ⊢ n ~ n′ ∷ A ^ [ ! , ll ]
            → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ ! , ll ] / [A]
  neuEqTerm:⇒*: {ι ¹} (Uᵣ′ A _ r ⁰ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN neN′  [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n' =
    let n~n = ~-trans n~n' (~-sym n~n')
        n'~n' = ~-trans (~-sym n~n') n~n'
        n~n'U = ~-conv n~n' (subset* D)
        n~nU = ~-conv n~n (subset* D)
        [t] = neuTerm:⇒*: (Uᵣ′ A _ r ⁰ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN [[ ⊢t , n , D' ]] n~n
        Uₜ _ _ _ _ [Δt] = [t]
        D'' = conv:⇒*: [[ ⊢t , n , D' ]] (subset* D)
        D′' = conv:⇒*: [[ ⊢u , n′ , D′ ]] (subset* D)
    in Uₜ₌ [t]
           (neuTerm:⇒*: (Uᵣ′ A _ r ⁰ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN′ [[ ⊢u , n′ , D′ ]] n'~n')
           (~-to-≅ₜ n~n'U)
           λ {ρ} [ρ] ⊢Δ → let ρD' = wkRed:*:Term [ρ] ⊢Δ D''
                              ρD′ = wkRed:*:Term [ρ] ⊢Δ D′'
                              n~nUρ = ~-wk [ρ] ⊢Δ n~nU
                              n~n'Uρ = ~-wk [ρ] ⊢Δ n~n'U
                          in neuEq:⇒*: {l = ι ¹} (neu:⇒*: (wkNeutral ρ neN) (univ:⇒*: ρD') n~nUρ) (wkNeutral ρ neN) (wkNeutral ρ neN′)
                                       (univ:⇒*: ρD') (univ:⇒*: ρD′) n~n'Uρ
  neuEqTerm:⇒*: {∞} (Uᵣ′ A _ r ¹ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN neN′  [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n' =
    let n~n = ~-trans n~n' (~-sym n~n')
        n'~n' = ~-trans (~-sym n~n') n~n'
        n~n'U = ~-conv n~n' (subset* D)
        n~nU = ~-conv n~n (subset* D)
        [t] = neuTerm:⇒*: (Uᵣ′ A _ r ¹ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN [[ ⊢t , n , D' ]] n~n
        Uₜ _ _ _ _ [Δt] = [t]
        D'' = conv:⇒*: [[ ⊢t , n , D' ]] (subset* D)
        D′' = conv:⇒*: [[ ⊢u , n′ , D′ ]] (subset* D)
    in Uₜ₌ [t]
           (neuTerm:⇒*: (Uᵣ′ A _ r ¹ l< PE.refl [[ ⊢A , ⊢U , D ]]) neN′ [[ ⊢u , n′ , D′ ]] n'~n')
           (~-to-≅ₜ n~n'U)
           λ {ρ} [ρ] ⊢Δ → let ρD' = wkRed:*:Term [ρ] ⊢Δ D''
                              ρD′ = wkRed:*:Term [ρ] ⊢Δ D′'
                              n~nUρ = ~-wk [ρ] ⊢Δ n~nU
                              n~n'Uρ = ~-wk [ρ] ⊢Δ n~n'U
                          in neuEq:⇒*: {l = ∞} (neu:⇒*: (wkNeutral ρ neN) (univ:⇒*: ρD') n~nUρ) (wkNeutral ρ neN) (wkNeutral ρ neN′)
                                       (univ:⇒*: ρD') (univ:⇒*: ρD′) n~n'Uρ
  neuEqTerm:⇒*: (ℕᵣ [[ ⊢A , ⊢B , D ]]) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let A≡ℕ = subset* D
        n~n′₁ = ~-conv n~n′ A≡ℕ
        n≡n′ = ~-to-≅ₜ n~n′₁
    in  ℕₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ℕ) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡ℕ)
            n≡n′ (ne (neNfₜ₌ neN neN′ n~n′₁))
  neuEqTerm:⇒*: (ne (ne K [[ ⊢A , ⊢B , D ]] neK K≡K)) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let A≡K = subset* D
    in  neₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡K) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡K)
             (neNfₜ₌ neN neN′ (~-conv n~n′ A≡K))
  neuEqTerm:⇒*: (Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) neN neN′ [[ ⊢t , n , D' ]] [[ ⊢u , n′ , D′ ]] n~n′ =
    let [ΠFG] = Πᵣ′ rF lF lG lF≤ lG≤ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext
        A≡ΠFG = subset* D
        n~n′₁ = ~-conv n~n′ A≡ΠFG
        n≡n′ = ~-to-≅ₜ n~n′₁
        n~n = ~-trans n~n′ (~-sym n~n′)
        n′~n′ = ~-trans (~-sym n~n′) n~n′
    in  Πₜ₌ _ _ (conv:⇒*: [[ ⊢t , n , D' ]] A≡ΠFG) (conv:⇒*: [[ ⊢u , n′ , D′ ]] A≡ΠFG)
            (ne neN) (ne neN′) n≡n′
            (neuTerm:⇒*: [ΠFG] neN [[ ⊢t , n , D' ]] n~n) (neuTerm:⇒*: [ΠFG] neN′ [[ ⊢u , n′ , D′ ]] n′~n′)
            (λ {ρ} [ρ] ⊢Δ [a] →
               let ρA≡ρΠFG = wkEq [ρ] ⊢Δ A≡ΠFG
                   ρn = wkTerm [ρ] ⊢Δ n
                   ρn′ = wkTerm [ρ] ⊢Δ n′
                   a = escapeTerm ([F] [ρ] ⊢Δ) [a]
                   a≡a = escapeTermEq ([F] [ρ] ⊢Δ)
                                          (reflEqTerm ([F] [ρ] ⊢Δ) [a])
                   neN∙a   = ∘ₙ (wkNeutral ρ neN)
                   neN′∙a′ = ∘ₙ (wkNeutral ρ neN′)
               in  neuEqTerm ([G] [ρ] ⊢Δ [a]) neN∙a neN′∙a′
                             (conv ρn  ρA≡ρΠFG ∘ⱼ a)
                             (conv ρn′ ρA≡ρΠFG ∘ⱼ a)
                             (~-app (~-wk [ρ] ⊢Δ n~n′₁) a≡a) )
  neuEqTerm:⇒*: {ι ¹} (emb l< X) neN n neN′ n:≡:n′ = neuEqTerm:⇒*: X neN n neN′ n:≡:n′
  neuEqTerm:⇒*: {∞} (emb l< X) neN n neN′ n:≡:n′ = neuEqTerm:⇒*: X neN n neN′ n:≡:n′

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
-- Intuitionistic propositional logic, PHOAS approach, final encoding

module Pf.Ip where

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set1
Cx = Ty -> Set

isTrue : Ty -> Cx -> Set
isTrue a tc = tc a

-- Terms

TmRepr : Set1
TmRepr = Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    field
      var  : forall {tc a}   -> isTrue a tc               -> tr tc a
      lam' : forall {tc a b} -> (isTrue a tc -> tr tc b)  -> tr tc (a => b)
      _$_  : forall {tc a b} -> tr tc (a => b) -> tr tc a -> tr tc b

    lam'' : forall {tc a b} -> (tr tc a -> tr tc b) -> tr tc (a => b)
    lam'' f = lam' \x -> f (var x)

    syntax lam'' (\a -> b) = lam a => b
  open Tm {{...}} public

module Mp where
  record Tm (tr : TmRepr) : Set1 where
    field
      pair' : forall {tc a b}   -> tr tc a        -> tr tc b -> tr tc (a && b)
      fst   : forall {tc a b}   -> tr tc (a && b)            -> tr tc a
      snd   : forall {tc a b}   -> tr tc (a && b)            -> tr tc b
      left  : forall {tc a b}   -> tr tc a                   -> tr tc (a || b)
      right : forall {tc a b}   -> tr tc b                   -> tr tc (a || b)
      case' : forall {tc a b c} -> tr tc (a || b) -> (isTrue a tc -> tr tc c) -> (isTrue b tc -> tr tc c) -> tr tc c

      isArrMp : ArrMp.Tm tr
    open ArrMp.Tm isArrMp public

    case'' : forall {tc a b c} -> tr tc (a || b) -> (tr tc a -> tr tc c) -> (tr tc b -> tr tc c) -> tr tc c
    case'' xy f g = case' xy (\x -> f (var x)) (\y -> g (var y))

    syntax pair'  x y = [ x , y ]
    syntax case'' xy (\x -> z1) (\y -> z2) = case xy of x => z1 or y => z2
  open Tm {{...}} public

module Ip where
  record Tm (tr : TmRepr) : Set1 where
    field
      abort : forall {tc a} -> tr tc FALSE -> tr tc a

      isMp : Mp.Tm tr
    open Mp.Tm isMp public
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr tc} {{_ : Tm tr}} -> tr tc a
open Ip public

-- Example theorems

t1 : forall {a b} -> Thm (a => NOT a => b)
t1 =
  lam x =>
    lam f => abort (f $ x)

t2 : forall {a b} -> Thm (NOT a => a => b)
t2 =
  lam f =>
    lam x => abort (f $ x)

t3 : forall {a} -> Thm (a => NOT (NOT a))
t3 =
  lam x =>
    lam f => f $ x

t4 : forall {a} -> Thm (NOT a <=> NOT (NOT (NOT a)))
t4 =
  [ lam f =>
      lam g => g $ f
  , lam g =>
      lam x => g $ (lam f => f $ x)
  ]

ext: agda

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
-- Issue #2814 reported by tomjack on 2017-10-18

{-# OPTIONS --cubical --rewriting #-}

-- prelude stolen from Saizan/cubical-demo

open import Agda.Primitive.Cubical public

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

{-# BUILTIN PATHP        PathP     #-}

infix 4 _≡_
_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = PathP (λ _ → A)

Path = _≡_

refl : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≡ x
refl {x = x} = λ _ → x

postulate
  Rewrite : ∀ {ℓ} {A : Set ℓ} → A → A → Set

{-# BUILTIN REWRITE Rewrite #-}

module Good where
  postulate
    Unit : Set
    unit : Unit

  module UnitElim (P : Unit → Set) (unit* : P unit) where
    postulate
      Unit-elim : (x : Unit) → P x
      unit-β : Rewrite (Unit-elim unit) unit*
  open UnitElim public
  {-# REWRITE unit-β #-}

  test₁ : {C : Set} {c₀ : C} → Path {A = C} (Unit-elim (λ _ → C) c₀ unit) c₀
  test₁ = refl

  test₂ : {C : Set} {c₀ : C} → Path {A = Path c₀ c₀} (λ j → Unit-elim (λ _ → C) c₀ unit) refl
  test₂ = refl

-- same code, but with a dummy module parameter
module Bad (Dummy : Set) where
  postulate
    Unit : Set
    unit : Unit

  module UnitElim (P : Unit → Set) (unit* : P unit) where
    postulate
      Unit-elim : (x : Unit) → P x
      unit-β : Rewrite (Unit-elim unit) unit*
  open UnitElim public
  {-# REWRITE unit-β #-}

  test₁ : {C : Set} {c₀ : C} → Path {A = C} (Unit-elim (λ _ → C) c₀ unit) c₀
  test₁ = refl
  test₂ : {C : Set} {c₀ : C} → Path {A = Path c₀ c₀} (λ j → Unit-elim (λ _ → C) c₀ unit) refl
  test₂ = refl

-- WAS:
-- Unit-elim (λ _ → .C) .c₀ unit != .c₀ of type .C
-- when checking that the expression refl has type
-- Path (λ j → Unit-elim (λ _ → .C) .c₀ unit) refl

-- SHOULD: succeed

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module LecIC where

open import CS410-Prelude
open import CS410-Nat

_-:>_ : {I : Set}(S T : I -> Set) -> I -> Set
(S -:> T) i = S i -> T i
infixr 3 _-:>_

-- notation for indexed sets

[_] : {I : Set}(X : I -> Set) -> Set
[ X ] = forall {i} -> X i

record MonadIx {W : Set}(F : (W -> Set) -> (W -> Set)) : Set1 where
  field
    retIx : forall {P} -> [ P -:> F P ]
    extendIx : forall {P Q} -> [ P -:> F Q ] -> [ F P -:> F Q ]
  _?>=_ : forall {P Q w} ->
          F P w -> (forall {v} -> P v -> F Q v) -> F Q w
  fp ?>= k = extendIx k fp

IC : (W : Set)
     (C : W -> Set)
     (R : (w : W) -> C w -> Set)
     (n : (w : W)(c : C w)(r : R w c) -> W)
     -> (W -> Set) -> (W -> Set)
IC W C R n G w = Sg (C w) \ c -> (r : R w c) -> G (n w c r)

data FreeIx (W : Set)
            (C : W -> Set)
            (R : (w : W) -> C w -> Set)
            (n : (w : W)(c : C w)(r : R w c) -> W)
            (G : W -> Set)
            (w : W)
            : Set
            where
  ret : G w -> FreeIx W C R n G w
  do  : IC W C R n (FreeIx W C R n G) w -> FreeIx W C R n G w

postulate
  FileName : Set
  Char : Set
  foo : FileName
  blah : Char

data WriteFileW : Set where
  opened closed : WriteFileW

data WriteFileC : WriteFileW -> Set where
  write : Char -> WriteFileC opened
  openW : FileName -> WriteFileC closed
  closeW : WriteFileC opened

WriteFileR : (w : WriteFileW)(c : WriteFileC w) -> Set
WriteFileR .opened (write x) = One
WriteFileR .closed (openW x) = WriteFileW
WriteFileR .opened closeW = One

WriteFileN : (w : WriteFileW)(c : WriteFileC w)(r : WriteFileR w c) -> WriteFileW
WriteFileN .opened (write x) <> = opened
WriteFileN .closed (openW x) r = r
WriteFileN .opened closeW <> = closed

WRITE : (WriteFileW -> Set) -> (WriteFileW -> Set)
WRITE = FreeIx WriteFileW WriteFileC WriteFileR WriteFileN

Goal : WriteFileW -> Set
Goal opened = Zero
Goal closed = One

play : WRITE Goal closed
play = do (openW foo , \
  { opened  -> do (write blah , (\ _ -> do (closeW , (\ _ -> ret <>))))
  ; closed  -> ret <>
  })

FreeMonadIx : (W : Set)
     (C : W -> Set)
     (R : (w : W) -> C w -> Set)
     (n : (w : W)(c : C w)(r : R w c) -> W)
     -> MonadIx (FreeIx W C R n)
FreeMonadIx W C R n =
  record { retIx = ret
         ; extendIx = help
         } where
  help : {P Q : W → Set} ->
         [ P -:> FreeIx W C R n Q ] ->
         [ FreeIx W C R n P -:> FreeIx W C R n Q ]
  help k (ret p) = k p
  help k (do (c , j)) = do (c , \ r -> help k (j r))

data HType : Set where hTwo hNat : HType

-- mapping names for types to real types.

THVal : HType -> Set
THVal hTwo = Two
THVal hNat = Nat

-- A syntax for types expressions, indexed by typed variables. Compare
-- with the untyped HExp and fill in the missing expression formers,
-- we have shown you the way with _+H_. think: what can be guaranteed?

data THExp (X : HType -> Set) : HType -> Set where
  var : forall {T} -> X T -> THExp X T
  val : forall {T} -> THVal T -> THExp X T
  _+H_ : THExp X hNat -> THExp X hNat -> THExp X hNat
  -- ??? fill in the other two constructs, typed appropriately
  -- (remember that "if then else" can compute values at any type)

THExpMonadIx : MonadIx THExp
THExpMonadIx = record
  {  retIx    = var
  ;  extendIx = help
  }  where
  help : forall {P Q} -> [ P -:> THExp Q ] -> [ THExp P -:> THExp Q ]
  help f (var x) = f x
  help f (val v) = val v
  help f (e1 +H e2) = help f e1 +H help f e2

WH : Set
WH = Nat * Nat

data Tiling (X : WH -> Set)(wh : WH) : Set where
  ! : X wh -> Tiling X wh
  joinH : (wl wr : Nat)(wq : wl +N wr == fst wh) ->
          Tiling X (wl , snd wh) ->  Tiling X (wr , snd wh) -> Tiling X wh
  joinV : (ht hb : Nat)(hq : ht +N hb == snd wh) ->
          Tiling X (fst wh , ht) ->  Tiling X (fst wh , hb) -> Tiling X wh

TilingMonadIx : MonadIx Tiling
TilingMonadIx = record
  { retIx = !
  ; extendIx = help
  } where
  help : {P Q : WH -> Set} -> [ P -:> Tiling Q ] -> [ Tiling P -:> Tiling Q ]
  help f (! p) = f p
  help f (joinH wl wr wq t-l t-r) = joinH wl wr wq (help f t-l) (help f t-r)
  help f (joinV ht hb hq t-t t-b) = joinV ht hb hq (help f t-t) (help f t-b)

IsZero : Nat -> Set
IsZero zero = One
IsZero (suc n) = Zero

CanCons : Set -> Nat -> Set
CanCons X zero = Zero
CanCons X (suc n) = X

afterCons : {X : Set}(n : Nat) -> CanCons X n -> One -> Nat
afterCons zero () <>
afterCons (suc n) c <> = n

VEC : Set -> Nat -> Set
VEC X = FreeIx Nat (CanCons X) (\ _ _ -> One) afterCons IsZero


text:
data Bool : Set where
  true  : Bool
  false : Bool

data Nat : Set where
  suc : Nat -> Nat
  zer : Nat
{-# BUILTIN NATURAL Nat #-}

data Vec (A : Set) : (n : Nat) -> Set where
  _,_ : ∀ {n} -> A -> Vec A n -> Vec A (suc n)
  []  : Vec A zer

data Sig (A : Set) (B : A → Set) : Set where
  sig : (a : A) → B a → Sig A B

Exists : ∀ {A : Set} → (A → Set) → Set
Exists = Sig _

Pair : ∀ (A B : Set) → Set
Pair A B = Sig A (λ x → B)

-- variable
  -- m n : Nat
  -- b : Bool
  -- Γ Δ Ξ T I O : Vec Bool n

-- A Linear term has an output and an output usage annotation
-- For each variable (i.e. index in the Vec):
--  * true: available
--  * false: already consumed
Linear : Set₁
Linear = ∀ n (Γa Γb : Vec Bool n) → Set

data Var : Linear where
  z : ∀ {n Γ} → Var (suc n) (true , Γ) (false , Γ)
  s : ∀ {n Γa Γb x} → Var n Γa Γb → Var (suc n) (x , Γa) (x , Γb)

data Lam : Linear where
  var : ∀ {n Γa Γb} → Var n Γa Γb → Lam n Γa Γb
  app : ∀ {n Γa Γb Γc} → Lam n Γa Γb → Lam n Γb Γc → Lam n Γa Γc
  lam : ∀ {n Γa Γb} → Lam (suc n) (true , Γa) (false , Γb) → Lam n Γa Γb

-- Γi Γo: input and output usage of the env
-- Γt: target usage covered by the content of the env
data Env : ∀ n m → (Γi Γo : Vec Bool n) (Γt : Vec Bool m) → Set where
  -- empty environment
  []  : ∀ {n Γi Γo} → Env n zer Γi Γo []
  -- 0th variable is available so we have a value for it
  _,_ : ∀ {n m Γi Γm Γo Γt} → Lam n Γi Γm → Env n m Γm Γo Γt → Env n (suc m) Γi Γo (true , Γt)
  -- -- 0th variable has already been consumed: we don't have a term for it anymore
  ─,_ : ∀ {n m Γi Γo Γt} → Env n m Γi Γo Γt → Env n (suc m) Γi Γo (false , Γt)
  -- -- When we go under binders, we need to be able to extend the input/output
  -- -- context to cope with the extended context
  [v]∷_ : ∀ {n m Γi Γo Γt} → Env n m Γi Γo Γt → Env (suc n) (suc m) (true , Γi)  (false , Γo) (false , Γt)
  ]v[∷_ : ∀ {n m Γi Γo Γt} → Env n m Γi Γo Γt → Env (suc n) (suc m) (false , Γi) (false , Γo) (false , Γt)

-- Input/output usage pairs that have the same consumption pattern
data Equiv : ∀ n → (Γ0i Γ0o Γ1i Γ1o : Vec Bool n) → Set where
  -- Empty pairs have the same consumption pattern
  empty   : Equiv zer [] [] [] []
  -- If a resource is untouched in one side, then it must be untouched on the other
  skip    : ∀ {n} Γ0i Γ0o Γ1i Γ1o A B → Equiv (suc n) (A , Γ0i) (A , Γ0o) (B , Γ1i) (B , Γ1o)
  -- If a resource is used in one side, then it must be used on the other
  consume : ∀ {n} Γ0i Γ0o Γ1i Γ1o → Equiv (suc n) (true , Γ0i) (false , Γ0o) (true , Γ1i) (false , Γ1o)

-- R: target of the substitution
-- V: output (e.g. substituting for vars yields terms)
Subst : (R : Linear) (V : Linear) → Set
Subst R V = ∀ {n m Γi Γo I O}
          -- environment targetting I
          → Env n m Γi Γo I
          -- R consuming resources in I, returning O leftovers
          → R m I O
          -- the result is a usage annotation, a value V consuming in the input, returning M leftovers, an environment of leftovers for whatever is still true in O
          → Exists (λ M → Pair (V n Γi M) (Env n m M Γo O))

-- substVar : Subst Var Lam
-- substVar (t ∷ ρ)  z     = -, t     , ─∷ ρ
-- substVar (x ∷ ρ)  (s v) = {!!}
-- substVar (─∷ ρ)   (s v) = {!!}
-- substVar ([v]∷ ρ) (s v) = {!!}
-- substVar (]v[∷ ρ) (s v) = {!!}

max_issues_repo_name: moonad/Elementary-Affine-Calculus

max_forks_repo_name: moonad/Elementary-Affine-Calculus


text:
open import Type
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

module Structure.Sets.ZFC {ℓₛ ℓₗ ℓₑ} {S : Type{ℓₛ}} ⦃ equiv : Equiv{ℓₑ}(S) ⦄ (_∈_ : S → S → Type{ℓₗ}) ⦃ [∈]-binaryRelator : BinaryRelator(_∈_) ⦄ where

open import Functional
open import Function.Equals
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Type.Properties.Inhabited
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Proofs renaming ([≡]-binaryRelator to [≡ₑ]-binaryRelator)
open import Structure.Setoid.Uniqueness
import      Structure.Sets.Names
open import Syntax.Function
open import Syntax.Implication

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ : Lvl.Level
private variable A B C D E a b c d e x y z As : S
private variable f g h : S → S
private variable P Q R : S → Type{ℓ}
private variable ⦃ func ⦄ : Function ⦃ equiv ⦄ ⦃ equiv ⦄ (f)
private variable ⦃ unaryRel ⦄ : UnaryRelator ⦃ equiv ⦄ (P)

open        Structure.Sets.Names.From-[∈] (_∈_)
open        Structure.Sets.Names.Relations (_∈_)
open        Structure.Sets.Names.One                     (_∈_)
open        Structure.Sets.Names.Two                     (_∈_)(_∈_)
open        Structure.Sets.Names.TwoDifferent            (_∈_)(_∈_)
open        Structure.Sets.Names.TwoSame                 (_∈_)(_∈_)
open        Structure.Sets.Names.Three                   (_∈_)(_∈_)(_∈_)
open        Structure.Sets.Names.ThreeNestedTwoDifferent (_∈_)
open        Structure.Sets.Names.ThreeTwoNested          (_∈_)(_∈_)(_∈_)
open import Structure.Sets.Quantifiers(_∈_)
open import Structure.Sets.Quantifiers.Proofs(_∈_) ⦃ [∈]-binaryRelator ⦄

{-
-- The statement that the sets in ss are all pairwise disjoint
PairwiseDisjoint : S → Type
PairwiseDisjoint(ss) = ∀ₛ(ss)(s₁ ↦ ∀ₛ(ss)(s₂ ↦ ∀ₗ(x ↦ ((x ∈ s₁) → (x ∈ s₂) → (s₁ ≡ s₂)))))
-- ∀ₛ(ss)(s₁ ↦ ∀ₛ(ss)(s₂ ↦ (s₁ ≢ s₂) → Disjoint(s₁)(s₂)))

-- The statement that the relation predicate F can be interpreted as a partial function
PartialFunction : (S → S → Type{ℓ}) → S → Type
PartialFunction(F) (dom) = ∀ₛ(dom)(x ↦ Unique(y ↦ F(x)(y)))

-- The statement that the relation predicate F can be interpreted as a total function
TotalFunction : (S → S → Type{ℓ}) → S → Type
TotalFunction(F) (dom) = ∀ₛ(dom)(x ↦ ∃!(y ↦ F(x)(y)))

-- A binary relator modifier which makes the binary relator to a statement about all distinct pairs in a set.
-- Note: This is specifically for irreflexive binary relations.
DistinctivelyPairwise : (S → S → Type{ℓ}) → (S → Type)
DistinctivelyPairwise Related (S) = ∀ₛ(S)(a ↦ ∀ₛ(S)(b ↦ ((a ≢ b) → Related(a)(b))))
-}

record ZFC : Typeω where
  field
    -- Empty set
    -- The set consisting of no elements.
    ∅ : S

    -- Pair set.
    -- The set consisting of only two elements.
    pair : S → S → S

    -- Subset filtering.
    -- The subset of the specified set where all elements satisfy the specified formula.
    filter : (P : S → Type{ℓ}) ⦃ rel-P : UnaryRelator(P) ⦄ → (S → S)

    -- Union over arbitrary sets.
    -- Constructs a set which consists of elements which are in any of the specified sets.
    ⋃ : S → S

    -- Power set.
    -- The set of all subsets of the specified set.
    ℘ : S → S

    -- The map of a set.
    -- The set of values when a function is applied to every element of a set.
    -- Or: The image of the function on the set.
    -- Or: The image of the function.
    map : (f : S → S) ⦃ func-f : Function(f) ⦄ → (S → S)

    -- The set of all finite ordinals.
    -- A set which has the `Inductive`-property. Also infinite.
    ω₀ : S

    -- A choice function for non-empty sets in a family of sets.
    -- Chooses an arbitrary element in a non-empty set from a family of sets.
    -- Example: choose {ℕ,ℤ,ℚ,ℝ} ℝ ∈ ℝ.
    choose : S → S → S

  -- Singleton set.
  -- A set consisting of only a single element.
  singleton : S → S
  singleton(s) = pair(s)(s)

  -- Union operator.
  -- Constructs a set which consists of both elements from LHS and RHS.
  _∪_ : S → S → S
  a ∪ b = ⋃(pair a b)
  infixl 3000 _∪_

  -- The zero constant expressed in the standard inductive set definition of ℕ in ZFC set theory.
  𝟎 : S
  𝟎 = ∅

  -- The successor function expressed in the standard inductive set definition of ℕ in ZFC set theory.
  -- This definition implies that natural numbers are sets that contain all numbers lesser than themselves.
  -- Examples:
  -- • 0: {}
  -- • 1: 0∪{0} = {0} = {{},{{}}}
  -- • 2: 1∪{1} = {0}∪{1} = {0,1} = {{},{{},{{}}}}
  -- • 3: 2∪{2} = {0,1}∪{2} = {0,1,2} = {{{},{{},{{}}}},{{{},{{},{{}}}}}}
  -- • 4: 3∪{3} = {0,1,2}∪{3} = {0,1,2,3} = {{{{},{{},{{}}}},{{{},{{},{{}}}}}},{{{{},{{},{{}}}},{{{},{{},{{}}}}}}}}
  𝐒 : S → S
  𝐒(n) = n ∪ singleton(n)

  𝟏 : S
  𝟏 = 𝐒(𝟎)

  -- A set is ℕ-inductive when has zero and all its successors.
  -- In loose terms: Inductive(I) means (I ⊆ ℕ)
  Inductive : S → Type
  Inductive(I) = (𝟎 ∈ I) ∧ (∀ₗ(x ↦ ((x ∈ I) → (𝐒(x) ∈ I))))

  field
    -- Set identity is extensionally determined. More specifically by its contents.
    set-extensionality : SetEqualityMembership(_≡ₑ_)

    -- `∅` is a set which is empty.
    -- • Allows a construction of an empty set.
    empty : EmptyMembership(∅)

    -- `pair` is the construction of a set with two elements.
    -- • Allows a construction of a set with two elements.
    pairing : PairMembership(pair)

    -- `filter` is the set which is the subset of a set where all elements satisfies a predicate.
    restricted-comprehension : FilterMembership{ℓ = ℓ}(filter)

    -- `⋃` is the construction of a set which contains all the elements of a collection of sets.
    -- • Allows a construction of a set that is the union of some sets.
    union : BigUnionMembership(⋃)

    -- `℘` is the construction of a set which contains all the subsets of a set.
    -- • Allows a construction of a set that is the powerset of a set.
    power : PowerMembership(_⊆_)(℘)

    -- `map` is the construction of the image of a function restricted to a set.
    -- • The `map`-function on a function is a function from sets to sets.
    replacement : MapMembership(map)

    -- `inductiveSet` is ℕ-inductive.
    -- • An inductive set is infinite, so this implies that an infinite set exists.
    -- • Makes it possible to construct the set of natural numbers (ℕ).
    infinity : Inductive(ω₀)

    -- A non-empty set contain sets that are disjoint to it.
    -- • Prevents sets from containing themselves.
    -- • Makes every set have an ordinal rank.
    regularity :  ∀ₗ(s₁ ↦ (NonEmpty(s₁) → ∃(s₂ ↦ (s₂ ∈ s₁) ∧ Disjoint(s₁)(s₂))))

    --choice : (∀{a} → (a ∈ A) → NonEmpty(a)) → PairwiseDisjoint(A) → ∃(b ↦ ∀{a} → (a ∈ A) → ∃!(_∈ (a ∩ b)))
    --choice : ∀{A B} ⦃ AB : A ⊇ B ⦄ ⦃ ne-B ⦄ → (choose(A)(B) ⦃ AB ⦄ ⦃ ne-B ⦄ ∈ B)
    -- The values of a choice function of a family of sets are all in the given sets.
    -- This states that a choice function actually chooses an element from the specified set.
    -- Note: A variant without the mentioning of `A` and a proof of `a ∈ A` would instead lead to the formulation of the axiom of global choice. The reason for not using global choice as an axiom is because unlike global choice, this variant makes every choice function expressable as a set. This variant should be interpreted as there being different choice functions for every family of sets. For example, when `A ≢ B`, `x ∈ A` and `x ∈ B` is satisfied, then `choose(A)(x) ≡ choose(B)(x)` should not neccesarily be satisfied while still (choose(A)(x) ∈ x) and (choose(B)(x) ∈ x).
    -- Examples:
    --   choose {ℕ,ℤ,ℚ,ℝ} ℝ ∈ ℝ
    --   choose {ℕ,ℤ,ℚ,ℝ} ℝ ≢ choose {ℤ,ℚ,ℝ} ℝ
    --   For example, it could be the case that (choose {ℕ,ℤ,ℚ,ℝ} ℝ = 0) but (choose {ℤ,ℚ,ℝ} ℝ = 1).
    -- Note: Without `choose-function`, `choice` would not be an actual choice function.
    choice : ∀{A a} → ⦃ ne : NonEmpty(a) ⦄ ⦃ aA : a ∈ A ⦄ → (choose A a ∈ a)
    ⦃ choose-function ⦄ : BinaryOperator(choose)

  𝑇 = 𝟎
  𝐹 = 𝟏
  BoolSet = pair 𝑇 𝐹

  instance
    Inductive-unaryRelator : UnaryRelator(Inductive)
    Inductive-unaryRelator = [∧]-unaryRelator ⦃ rel-P = binary-unaryRelatorₗ ⦄ ⦃ rel-Q = [∀]-unaryRelator ⦃ rel-P = [→]-unaryRelator ⦃ rel-P = binary-unaryRelatorₗ ⦄ ⦃ rel-Q = binary-unaryRelatorₗ ⦄ ⦄ ⦄

  open import Logic.Predicate.Theorems
  open import Logic.Propositional.Theorems
  open import Structure.Relator.Properties
  open import Structure.Relator.Proofs renaming ([≡]-binaryRelator to [≡ₑ]-binaryRelator)

  instance
    [≡]-binaryRelator : BinaryRelator(_≡_)
    BinaryRelator.substitution [≡]-binaryRelator xy₁ xy₂ x₁x₂ = [↔]-to-[→] set-extensionality (BinaryRelator.substitution [≡ₑ]-binaryRelator xy₁ xy₂ ([↔]-to-[←] set-extensionality x₁x₂))

  instance
    [⊆]-binaryRelator : BinaryRelator(_⊆_)
    BinaryRelator.substitution [⊆]-binaryRelator p1 p2 sub = [↔]-to-[→] ([↔]-to-[→] set-extensionality p2) ∘ sub ∘ [↔]-to-[←] ([↔]-to-[→] set-extensionality p1)

  instance
    pair-binaryOperator : BinaryOperator(pair)
    BinaryOperator.congruence pair-binaryOperator p1 p2 = [↔]-to-[←] set-extensionality (\{x} → [↔]-transitivity pairing ([↔]-transitivity ([∨]-map-[↔] (substitute₂ₗᵣ(_≡ₑ_) ⦃ [≡ₑ]-binaryRelator ⦄ (reflexivity(_≡ₑ_) {x}) p1) (substitute₂ₗᵣ(_≡ₑ_) ⦃ [≡ₑ]-binaryRelator  ⦄ (reflexivity(_≡ₑ_) {x}) p2)) ([↔]-symmetry pairing)))

  instance
    ℘-function : Function(℘)
    Function.congruence ℘-function xy = [↔]-to-[←] set-extensionality \{x} → [↔]-transitivity power ([↔]-transitivity ([↔]-intro (substitute₂ᵣ(_⊆_) ⦃ [⊆]-binaryRelator ⦄ (symmetry(_≡ₑ_) xy)) (substitute₂ᵣ(_⊆_) ⦃ [⊆]-binaryRelator ⦄ xy)) ([↔]-symmetry power))

  instance
    ⋃-function : Function(⋃)
    Function.congruence ⋃-function xy = [↔]-to-[←] set-extensionality \{x} → [↔]-transitivity union ([↔]-transitivity ([∃]-map-proof-[↔] ([∧]-map-[↔] ([↔]-to-[→] set-extensionality xy) [↔]-reflexivity)) ([↔]-symmetry union))

  filter-function : ∀ ⦃ rel-P : UnaryRelator(P) ⦄ ⦃ rel-Q : UnaryRelator(Q) ⦄ → (∀{x} → P(x) ↔ Q(x)) → ∀{A B} → (A ≡ₑ B) → (filter P(A) ≡ₑ filter Q(B))
  filter-function PQ AB = [↔]-to-[←] set-extensionality ([↔]-transitivity restricted-comprehension ([↔]-transitivity ([∧]-map-[↔] ([↔]-to-[→] set-extensionality AB) PQ) ([↔]-symmetry restricted-comprehension)))

  map-function : ∀{f} ⦃ func-f : Function(f) ⦄ {g} ⦃ func-g : Function(g) ⦄ → (f ⊜ g) → ∀{A B} → (A ≡ₑ B) → (map f(A) ≡ₑ map g(B))
  map-function {f = f}{g = g} (intro fg) {A = A}{B = B} AB = [↔]-to-[←] set-extensionality $ \{y} →
    (y ∈ map f A)        ⇔-[ replacement ]
    ∃ₛ(A)(x ↦ f(x) ≡ₑ y) ⇔-[ [∃]-map-proof-[↔] (\{x} → [∧]-map-[↔] ([↔]-to-[→] set-extensionality AB) (substitute₂ₗᵣ(_≡ₑ_) ⦃ [≡ₑ]-binaryRelator ⦄ (fg{x}) (reflexivity(_≡ₑ_)))) ]
    ∃ₛ(B)(x ↦ g(x) ≡ₑ y) ⇔-[ replacement ]-sym
    (y ∈ map g B)        ⇔-end

  [∪]-inclusion : UnionMembership(_∪_)
  [∪]-inclusion {A = A}{B = B}{x = x} =
    (x ∈ ⋃ (pair A B))                                    ⇔-[ union ]
    ∃(y ↦ (y ∈ pair A B) ∧ (x ∈ y))                       ⇔-[ [∃]-map-proof-[↔] (\{y} →
      (y ∈ pair A B) ∧ (x ∈ y)                    ⇔-[ [∧]-map-[↔] pairing [↔]-reflexivity ]
      ((y ≡ₑ A) ∨ (y ≡ₑ B)) ∧ (x ∈ y)             ⇔-[ [∧][∨]-distributivityᵣ ]
      ((y ≡ₑ A) ∧ (x ∈ y)) ∨ ((y ≡ₑ B) ∧ (x ∈ y)) ⇔-end
    ) ]
    ∃(y ↦ ((y ≡ₑ A) ∧ (x ∈ y)) ∨ ((y ≡ₑ B) ∧ (x ∈ y)))    ⇔-[ [∃][∨]-distributivity ]
    ∃(y ↦ (y ≡ₑ A) ∧ (x ∈ y)) ∨ ∃(y ↦ (y ≡ₑ B) ∧ (x ∈ y)) ⇔-[ [∨]-map-[↔] (p ⦃ rel = binary-unaryRelatorₗ ⦄) (p ⦃ rel = binary-unaryRelatorₗ ⦄) ]
    (x ∈ A) ∨ (x ∈ B)                                     ⇔-end
    where
      -- TODO: Maybe move this somewhere else
      p : ∀{T : Type{ℓ₁}} ⦃ equiv : Equiv{ℓₑ₁}(T) ⦄ {P : T → Type{ℓ₂}} ⦃ rel : UnaryRelator(P) ⦄ {y} → ∃(x ↦ (x ≡ₑ y) ∧ P(x)) ↔ P(y)
      p {P = P} = [↔]-intro (py ↦ [∃]-intro _ ⦃ [∧]-intro (reflexivity(_≡ₑ_)) py ⦄) (\([∃]-intro x ⦃ [∧]-intro xy px ⦄) → substitute₁(P) xy px)

  BoolSet-inclusion : (x ∈ BoolSet) ↔ (x ≡ₑ 𝑇) ∨ (x ≡ₑ 𝐹)
  BoolSet-inclusion = pairing

  pair-contains-left : a ∈ pair a b
  pair-contains-left = [↔]-to-[←] pairing ([∨]-introₗ (reflexivity(_≡ₑ_)))

  pair-contains-right : b ∈ pair a b
  pair-contains-right = [↔]-to-[←] pairing ([∨]-introᵣ (reflexivity(_≡ₑ_)))

  𝑇-in-BoolSet : 𝑇 ∈ BoolSet
  𝑇-in-BoolSet = pair-contains-left

  𝐹-in-BoolSet : 𝐹 ∈ BoolSet
  𝐹-in-BoolSet = pair-contains-right

  ℘-self : (A ∈ ℘(A))
  ℘-self = [↔]-to-[←] power id

  pair-superset : (x ∈ A) → (y ∈ A) → (pair x y ⊆ A)
  pair-superset pa pb p = [∨]-elim
    (eq ↦ substitute₂ₗ(_∈_) (symmetry(_≡ₑ_) eq) pa)
    (eq ↦ substitute₂ₗ(_∈_) (symmetry(_≡ₑ_) eq) pb)
    ([↔]-to-[→] pairing p)

  pair-superset-union : (a ∈ A) → (b ∈ B) → (pair a b ⊆ (A ∪ B))
  pair-superset-union pa pb p = pair-superset (([↔]-to-[←] [∪]-inclusion ∘ [∨]-introₗ) pa) (([↔]-to-[←] [∪]-inclusion ∘ [∨]-introᵣ) pb) p

  instance
    postulate [≡][⊆]-sub : (_≡_) ⊆₂ (_⊆_)

  instance
    postulate [⊆]-transitivity : Transitivity(_⊆_)

  open import Data.Either as Either using ()
  import      Data.Tuple as Tuple
  open import Syntax.Transitivity
  open import Syntax.Implication

  [≡][≢]-semitransitivityₗ : (a ≡ₑ b) → (b ≢ c) → (a ≢ c)
  [≡][≢]-semitransitivityₗ ab nbc ac = nbc(symmetry(_≡ₑ_) ab 🝖 ac)

  [≡][≢]-semitransitivityᵣ : (a ≢ b) → (b ≡ₑ c) → (a ≢ c)
  [≡][≢]-semitransitivityᵣ nab bc ac = nab(ac 🝖 symmetry(_≡ₑ_) bc)

  nonEmpty-filter : NonEmpty(filter P ⦃ unaryRel ⦄ A) ↔ ∃ₛ(A) P
  nonEmpty-filter = [∃]-map-proof-[↔] restricted-comprehension

  open import Function.Proofs

  instance
    singleton-function : Function(singleton)
    singleton-function = [$₂]-function

  singleton-inclusion : SingletonMembership(singleton)
  singleton-inclusion {y = y}{x = x} =
    x ∈ pair y y        ⇔-[ pairing ]
    (x ≡ₑ y) ∨ (x ≡ₑ y) ⇔-[ [∨]-redundancy ]
    x ≡ₑ y              ⇔-end

  singleton-contains-element : a ∈ singleton a
  singleton-contains-element = [↔]-to-[←] singleton-inclusion (reflexivity(_≡ₑ_))

  singleton-nonempty : NonEmpty(singleton x)
  singleton-nonempty{x = x} = [∃]-intro x ⦃ singleton-contains-element ⦄

  singleton-superset : (a ∈ A) → (singleton a ⊆ A)
  singleton-superset pa p = substitute₂ₗ(_∈_) (symmetry(_≡ₑ_) ([↔]-to-[→] singleton-inclusion p)) pa

  zero-one-ineq : (𝟎 ≢ 𝟏)
  zero-one-ineq p =
    p ⇒
    𝟎 ≡ₑ 𝟏            ⇒-[ p ↦ [↔]-to-[→] set-extensionality p {𝟎} ]
    (𝟎 ∈ 𝟎) ↔ (𝟎 ∈ 𝟏) ⇒-[ [↔]-to-[←] ]
    (𝟎 ∈ 𝟎) ← (𝟎 ∈ 𝟏) ⇒-[ apply ([↔]-to-[←] [∪]-inclusion ([∨]-introᵣ ([↔]-to-[←] singleton-inclusion (reflexivity(_≡ₑ_))))) ]
    (𝟎 ∈ 𝟎)           ⇒-[ empty ]
    ⊥                 ⇒-end

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of general interleavings
------------------------------------------------------------------------

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

module Data.List.Relation.Ternary.Interleaving.Properties where

open import Data.Nat
open import Data.Nat.Properties using (+-suc)
open import Data.List.Base hiding (_∷ʳ_)
open import Data.List.Properties using (reverse-involutive)
open import Data.List.Relation.Ternary.Interleaving hiding (map)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; module ≡-Reasoning)
open ≡-Reasoning

------------------------------------------------------------------------
-- length

module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
         {L : REL A C l} {R : REL B C r} where

  interleave-length : ∀ {as l r} → Interleaving L R l r as →
                      length as ≡ length l + length r
  interleave-length []        = refl
  interleave-length (l ∷ˡ sp) = cong suc (interleave-length sp)
  interleave-length {as} {l} {r ∷ rs} (_ ∷ʳ sp) = begin
    length as                   ≡⟨ cong suc (interleave-length sp) ⟩
    suc (length l + length rs)  ≡⟨ sym $ +-suc _ _ ⟩
    length l + length (r ∷ rs)  ∎

------------------------------------------------------------------------
-- _++_

  ++⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
        Interleaving L R as₁ l₁ r₁ → Interleaving L R as₂ l₂ r₂ →
        Interleaving L R (as₁ ++ as₂) (l₁ ++ l₂) (r₁ ++ r₂)
  ++⁺ []         sp₂ = sp₂
  ++⁺ (l ∷ˡ sp₁) sp₂ = l ∷ˡ (++⁺ sp₁ sp₂)
  ++⁺ (r ∷ʳ sp₁) sp₂ = r ∷ʳ (++⁺ sp₁ sp₂)

  ++-disjoint : ∀ {as₁ as₂ l₁ r₂} →
                Interleaving L R l₁ [] as₁ → Interleaving L R [] r₂ as₂ →
                Interleaving L R l₁ r₂ (as₁ ++ as₂)
  ++-disjoint []         sp₂ = sp₂
  ++-disjoint (l ∷ˡ sp₁) sp₂ = l ∷ˡ ++-disjoint sp₁ sp₂

------------------------------------------------------------------------
-- map

module _ {a b c d e f l r}
         {A : Set a} {B : Set b} {C : Set c}
         {D : Set d} {E : Set e} {F : Set f}
         {L : REL A C l} {R : REL B C r}
         (f : E → A) (g : F → B) (h : D → C)
         where

  map⁺ : ∀ {as l r} →
         Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as  →
         Interleaving L R (map f l) (map g r) (map h as)
  map⁺ []        = []
  map⁺ (l ∷ˡ sp) = l ∷ˡ map⁺ sp
  map⁺ (r ∷ʳ sp) = r ∷ʳ map⁺ sp

  map⁻ : ∀ {as l r} →
         Interleaving L R (map f l) (map g r) (map h as) →
         Interleaving (λ x z → L (f x) (h z)) (λ y z → R (g y) (h z)) l r as
  map⁻ {[]}    {[]}    {[]}    []        = []
  map⁻ {_ ∷ _} {[]}    {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
  map⁻ {_ ∷ _} {_ ∷ _} {[]}    (l ∷ˡ sp) = l ∷ˡ map⁻ sp
  map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (l ∷ˡ sp) = l ∷ˡ map⁻ sp
  map⁻ {_ ∷ _} {_ ∷ _} {_ ∷ _} (r ∷ʳ sp) = r ∷ʳ map⁻ sp
  -- impossible cases needed until 2.6.0
  map⁻ {[]} {_} {_ ∷ _} ()
  map⁻ {[]} {_ ∷ _} {_} ()
  map⁻ {_ ∷ _} {[]} {[]} ()

------------------------------------------------------------------------
-- reverse

module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
         {L : REL A C l} {R : REL B C r}
         where

  reverseAcc⁺ : ∀ {as₁ as₂ l₁ l₂ r₁ r₂} →
                Interleaving L R l₁ r₁ as₁ →
                Interleaving L R l₂ r₂ as₂ →
                Interleaving L R (reverseAcc l₁ l₂) (reverseAcc r₁ r₂) (reverseAcc as₁ as₂)
  reverseAcc⁺ sp₁ []         = sp₁
  reverseAcc⁺ sp₁ (l ∷ˡ sp₂) = reverseAcc⁺ (l ∷ˡ sp₁) sp₂
  reverseAcc⁺ sp₁ (r ∷ʳ sp₂) = reverseAcc⁺ (r ∷ʳ sp₁) sp₂

  reverse⁺ : ∀ {as l r} → Interleaving L R l r as →
             Interleaving L R (reverse l) (reverse r) (reverse as)
  reverse⁺ = reverseAcc⁺ []

  reverse⁻ : ∀ {as l r} → Interleaving L R (reverse l) (reverse r) (reverse as) →
             Interleaving L R l r as
  reverse⁻ {as} {l} {r} sp with reverse⁺ sp
  ... | sp′ rewrite reverse-involutive as
                  | reverse-involutive l
                  | reverse-involutive r = sp′


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

module Lens.Definition where

open import Prelude

record LensPart (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  constructor lens-part
  eta-equality
  field
    get : B
    set : B → A
open LensPart public

map-lens-part : LensPart A C → (A → B) → LensPart B C
get (map-lens-part xs f) = get xs
set (map-lens-part xs f) x = f (set xs x)

record LensLaws {A : Type a} {B : Type b} (into : A → LensPart A B) : Type (a ℓ⊔ b) where
  no-eta-equality
  field
    get-set : ∀ s v → into (into s .set v) .get ≡ v
    set-get : ∀ s → into s .set (into s .get) ≡ s
    set-set : ∀ s v₁ v₂ → into (into s .set v₁) .set v₂ ≡ into s .set v₂
open LensLaws public

Lens : Type a → Type b → Type (a ℓ⊔ b)
Lens A B = Σ (A → LensPart A B) LensLaws

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

-- The category of partially ordered sets and order-preserving maps.

open import Level
open import Relation.Binary using (Poset; IsEquivalence; _Preserves_⟶_)
open import Relation.Binary.Morphism using (IsOrderHomomorphism)
import Relation.Binary.Morphism.Construct.Identity as Id
import Relation.Binary.Morphism.Construct.Composition as Comp

open import Categories.Category

open Poset renaming (_≈_ to ₍_₎_≈_; _≤_ to ₍_₎_≤_)

private
  variable
    a₁ a₂ a₃ b₁ b₂ b₃ : Level
    A B C : Poset a₁ a₂ a₃

record _⇒-Poset_ (A : Poset a₁ a₂ a₃) (B : Poset b₁ b₂ b₃) : Set (a₁ ⊔ a₂ ⊔ a₃ ⊔ b₁ ⊔ b₂ ⊔ b₃)  where
  field
    fun : Carrier A → Carrier B
    isOrderHomomorphism : IsOrderHomomorphism ₍ A ₎_≈_ ₍ B ₎_≈_ ₍ A ₎_≤_ ₍ B ₎_≤_ fun

  open IsOrderHomomorphism isOrderHomomorphism public
    renaming (mono to monotone)

open _⇒-Poset_

⇒-Poset-id : A ⇒-Poset A
⇒-Poset-id = record
  { isOrderHomomorphism = Id.isOrderHomomorphism _ _
  }

⇒-Poset-∘ : B ⇒-Poset C → A ⇒-Poset B → A ⇒-Poset C
⇒-Poset-∘ B⇒C A⇒B = record
  { isOrderHomomorphism = Comp.isOrderHomomorphism (isOrderHomomorphism A⇒B) (isOrderHomomorphism B⇒C)
  }

module _ {A : Poset a₁ a₂ a₃} {B : Poset b₁ b₂ b₃} where

  infix 4 _≗_

  -- Order morphisms preserve equality.
  mono⇒cong : ∀ {f} → f Preserves ₍ A ₎_≤_ ⟶ ₍ B ₎_≤_ → f Preserves ₍ A ₎_≈_ ⟶ ₍ B ₎_≈_
  mono⇒cong {f} monotone x≈y = antisym B
    (monotone (reflexive A x≈y))
    (monotone (reflexive A (Eq.sym A x≈y)))

  ⇒-Poset-helper : ∀ f → f Preserves ₍ A ₎_≤_ ⟶ ₍ B ₎_≤_ → A ⇒-Poset B
  ⇒-Poset-helper f mono = record
    { isOrderHomomorphism = record
      { cong = mono⇒cong mono
      ; mono = mono
      }
    }

  -- Pointwise equality (on order preserving maps).

  _≗_ : (f g : A ⇒-Poset B) → Set (a₁ ⊔ b₂)
  f ≗ g = ∀ {x} → ₍ B ₎ fun f x ≈ fun g x

  ≗-isEquivalence : IsEquivalence _≗_
  ≗-isEquivalence = record
    { refl    = Eq.refl B
    ; sym     = λ f≈g → Eq.sym B f≈g
    ; trans   = λ f≈g g≈h → Eq.trans B f≈g g≈h
    }

  module ≗ = IsEquivalence ≗-isEquivalence

-- The category of posets and order-preserving maps.

Posets : ∀ c ℓ₁ ℓ₂ → Category (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) (c ⊔ ℓ₁ ⊔ ℓ₂) (c ⊔ ℓ₁)
Posets c ℓ₁ ℓ₂ = record
  { Obj       = Poset c ℓ₁ ℓ₂
  ; _⇒_       = _⇒-Poset_
  ; _≈_       = _≗_
  ; id        = ⇒-Poset-id
  ; _∘_       = ⇒-Poset-∘
  ; assoc     = λ {_ _ _ D} → Eq.refl D
  ; sym-assoc = λ {_ _ _ D} → Eq.refl D
  ; identityˡ = λ {_ B} → Eq.refl B
  ; identityʳ = λ {_ B} → Eq.refl B
  ; identity² = λ {A} → Eq.refl A
  ; equiv     = ≗-isEquivalence
  ; ∘-resp-≈  = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i)
  }

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


text:
{- --- 3. Natural numbers --- -}

{- 3.1 Definition -}
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{- 3.2 Addition -}
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

{- 3.3 Multiplication -}
_*_ : ℕ → ℕ → ℕ
zero * b = zero
suc a * b = b + (a * b)

{- 3.4 Equality is a congruence for successor -}
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 4 _≡_

suc-≡ : {m n : ℕ} → (m ≡ n) → (suc m ≡ suc n)
suc-≡ refl = refl

{- 3.5 Some properties -}
zeroL : (n : ℕ) → zero + n ≡ n
zeroL n = refl

zeroR : (n : ℕ) → n + zero ≡ n
zeroR zero = refl
zeroR (suc n) = suc-≡ (zeroR n)

+-assoc : (m n p : ℕ) → ((m + n) + p) ≡ (m + (n + p))
+-assoc zero n p = refl
+-assoc (suc m) n p = suc-≡ (+-assoc m n p)

one : ℕ
one = suc zero

+-assoc1 : (m n : ℕ) → ((m + n) + one) ≡ (m + (n + one))
+-assoc1 m n = +-assoc m n one

{- Falsity type, needed for the next property -}
data ⊥ : Set where

{- ¬ : Set → Set
¬ A = A → ⊥ -}

open import Relation.Nullary

suc-notzero : (n : ℕ) → ¬ (zero ≡ suc n)
suc-notzero n ()

{- 3.6 The recurrence principle -}
rec : (P : ℕ → Set) → (P zero) → ((n : ℕ) → (P n) → (P (suc n))) → ((n : ℕ) → P n)
rec p z h zero = z
rec p z h (suc n) = h n (rec p z h n)

{- 3.7 Properties of equality -}
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

p : {m n : ℕ} → (e : m ≡ n) → suc-≡ e ≡ cong suc e
p refl = refl

subst : {A : Set} (P : A → Set) → {x y : A} → x ≡ y → P x → P y
subst P refl p = p

{- 3.8 Commutativity of addition -}
+-suc : (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n = suc-≡ (+-suc m n)

+-commut : (m n : ℕ) → m + n ≡ n + m
+-commut m zero = zeroR m
+-commut m (suc n) = trans (+-suc m n) (suc-≡ (+-commut m n))

{- 3.9 Injectivity of successor -}
suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ n
suc-inj refl = refl

{- 3.10 Decidability of equality -}
open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)

ℕ-≡-dec : (m n : ℕ) → (m ≡ n) ∨ ¬ (m ≡ n)
ℕ-≡-dec zero zero = left refl
ℕ-≡-dec zero (suc n) = right (suc-notzero n)
ℕ-≡-dec (suc m) zero = right λ ()
ℕ-≡-dec (suc m) (suc n) with ℕ-≡-dec m n
ℕ-≡-dec (suc m) (suc n) | left e = left (suc-≡ e)
ℕ-≡-dec (suc m) (suc n) | right e' = right λ x → e' (suc-inj x)

{- 3.11 Recurrence for equality -}
J : (A : Set) → (P : (x : A) → (y : A) → (p : x ≡ y) → Set) → (r : (x : A) → P x x refl) → (x : A) → (y : A) → (p : x ≡ y) → P x y p
J A P r x .x refl = r x

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Booleans
------------------------------------------------------------------------

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

module Data.Bool where

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

------------------------------------------------------------------------
-- The boolean type and some operations

open import Data.Bool.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Bool.Properties public
  using (_≟_; _≤?_; _<?_)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

decSetoid = Data.Bool.Properties.≡-decSetoid
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.1.
Please use ≡-decSetoid from Data.Bool.Properties instead."
#-}


text:
{-# OPTIONS --copatterns  #-}

module TestsInstances where

open import Function
open import Data.Product
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

open import Data.Empty renaming (⊥ to Empty)
open import Data.Unit renaming (⊤ to One) hiding (_≟_)
open import Data.Bool hiding (_≟_)
open import Data.Bool.Properties using (¬-not; T-not-≡)
open import Data.Nat hiding (_⊔_)

open import Isomorphisms
open import Tests

-- | Functions are testable if their codomain is
FunTestable : {A B : Set} → Testable B → Testable (A → B)
FunTestable {A} {B} TB =
  record
  { index = A
  ; parts = λ _ → B
  ; kind = coind
  ; obs = λ f → record { app = f }
  ; partsTestable = λ _ → TB
  }

FunIsoTestable : {A B : Set} → IsoTestable B → IsoTestable (A → B)
FunIsoTestable T =
  record
  { testable = FunTestable (testable T)
  ; obsIso = (record { inv = app
                     ; isLeftInv = λ a → refl
                     ; isRightInv = λ b → refl })
  }

-- | We get extensionality for functions under observational equivalence.
ext : {A B : Set} → (T : Testable B) →
      (f : A → B) → (g : A → B) →
      ((a : A) →  f a ≃⟨ T ⟩ g a) →  f ≃⟨ FunTestable T ⟩ g
ext {A} {B} TB f g p = record { eqProof = q }
  where
    q : (φ : Test (FunTestable TB)) → f ⊨ φ ≡ g ⊨ φ
    q ⊤ = refl
    q ⊥ = refl
    q (nonTriv (i , ψ)) = eqProof (p i) ψ

-- | Make unit type testable
⊤-testable : Testable One
index  ⊤-testable = One
parts  ⊤-testable = λ _ → One
kind   ⊤-testable = coind
obs    ⊤-testable = λ { tt  → record { app = λ x → x } }
partsTestable ⊤-testable = λ i → ⊤-testable

⊤-IsoTestable : IsoTestable One
⊤-IsoTestable =
  record
  { testable = ⊤-testable
  ; obsIso =
    record { inv = λ f → app f tt
           ; isLeftInv = λ a → refl
           ; isRightInv = λ b → refl
           }
  }

-- | Obs. equiv. is a congruence on ⊤.
≃-cong-⊤ : {A : Set} → {T : Testable A} → {x y : One} →
           (f : One → A) → x ≃⟨ ⊤-testable ⟩ y → f x ≃⟨ T ⟩ f y
≃-cong-⊤ f p = record { eqProof = λ φ → refl }

Parts-ℕ : Bool → Set
Parts-ℕ true = One
Parts-ℕ false = ℕ

rep-ℕ : ℕ → Σ Bool Parts-ℕ
rep-ℕ ℕ.zero = (true , tt)
rep-ℕ (ℕ.suc n) = (false , n)

unrep-ℕ : Σ Bool Parts-ℕ → ℕ
unrep-ℕ (true , tt) = ℕ.zero
unrep-ℕ (false , n) = ℕ.suc n

-- | Make naturals testable
ℕ-testable : Testable ℕ
index  ℕ-testable = Bool
parts  ℕ-testable = Parts-ℕ
kind   ℕ-testable = ind
obs    ℕ-testable = rep-ℕ
partsTestable ℕ-testable = λ
  { true → ⊤-testable
  ; false → ℕ-testable }

ℕ-IsoTestable : IsoTestable ℕ
ℕ-IsoTestable =
  record
  { testable = ℕ-testable
  ; obsIso =
    record { inv = unrep-ℕ
           ; isLeftInv = li
           ; isRightInv = ri
           }
  }
  where
    li : (n : ℕ) → unrep-ℕ (rep-ℕ n) ≡ n
    li ℕ.zero = refl
    li (ℕ.suc a) = refl
    ri : (x : Σ Bool Parts-ℕ) → rep-ℕ (unrep-ℕ x) ≡ x
    ri (true , tt) = refl
    ri (false , n) = refl

¬zero→suc : (n : ℕ) → n ≢ zero → ∃ (λ m → n ≡ suc m)
¬zero→suc n p with n ≟ zero
¬zero→suc zero    p | yes n=z = ⊥-elim (p n=z)
¬zero→suc (suc m) p | yes sm=z = ⊥-elim (p sm=z)
¬zero→suc zero    p | no ¬n=z = ⊥-elim (p refl)
¬zero→suc (suc n) p | no ¬n=z = n , refl

lem-tt≢ff : (a : Bool) → a ≡ true → a ≢ false
lem-tt≢ff true   _ ()
lem-tt≢ff false () _

-- | If a number is observationally equivalent to 0, then it is
-- actually 0.
lem-≃→≡-ℕ-zero : {n : ℕ} → n ≃⟨ ℕ-testable ⟩ zero → n ≡ zero
lem-≃→≡-ℕ-zero {n} p = q
  where
    -- Test to distinguish zero
    ψs : SubTests ℕ-testable ind
    ψs = record { app = λ {
        true → ⊤ ;
        false → ⊥ } }

    φ : Test ℕ-testable
    φ = nonTriv ψs

    -- n fulfils test, ...
    u : n ⊨ φ ≡ true
    u = eqProof p φ

    -- ... hence is 0.
    q : n ≡ zero
    q with n ≟ zero
    q | yes n=z = n=z
    q | no ¬n=z = ⊥-elim (lem (¬zero→suc n ¬n=z))
      where
        -- If n ≡ suc n, then we get a contradiction to u
        lem : (∃ (λ m → n ≡ suc m)) → Empty
        lem (m , q) with (n ≟ suc m)
        ... | yes n=sm = lem-tt≢ff (n ⊨ φ) u contradict
          where
            contradict : n ⊨ φ ≡ false
            contradict =
              begin
                n ⊨ φ
              ≡⟨ refl ⟩
                cotuple (λ i y → y ⊨ app ψs i) (rep-ℕ n)
              ≡⟨ cong (λ u → cotuple (λ i y → y ⊨ app ψs i) (rep-ℕ u)) n=sm ⟩
                cotuple (λ i y → y ⊨ app ψs i) (false , n)
              ≡⟨ refl ⟩
                false
              ∎
        ... | no ¬n=sm = ¬n=sm q

-- | If a number is observationally equivalent to a successor, then it is
-- actually a succesor.
lem-≃→≡-ℕ-suc : (n m : ℕ) → n ≃⟨ ℕ-testable ⟩ suc m →
       ∃ λ n' → (n ≡ suc n') × (n' ≃⟨ ℕ-testable ⟩ m)
lem-≃→≡-ℕ-suc = {!!}

-- | Observational equivalence for natural numbers implies equivalence.
≃→≡-ℕ : {n m : ℕ} → n ≃⟨ ℕ-testable ⟩ m → n ≡ m
≃→≡-ℕ {n} {zero} p = lem-≃→≡-ℕ-zero p
≃→≡-ℕ {n} {(suc m)} p with lem-≃→≡-ℕ-suc n m p
... | n' , q , p' =
  begin
    n
  ≡⟨ q ⟩
    suc n'
  ≡⟨ cong suc (≃→≡-ℕ {n'} {m} p') ⟩
    suc m
  ∎

-- | Obs. equiv. is a congruence for natural numbers.
≃-cong-ℕ : {A : Set} → {T : Testable A} → {x y : ℕ} →
           (f : ℕ → A) → x ≃⟨ ℕ-testable ⟩ y → f x ≃⟨ T ⟩ f y
≃-cong-ℕ {A} {T} {x} {y} f p = record { eqProof = q }
  where
    q : (φ : Test T) → f x ⊨ φ ≡ f y ⊨ φ
    q φ = cong (λ u → f u ⊨ φ) (≃→≡-ℕ p)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable vector equality over propositional equality
------------------------------------------------------------------------

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

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Data.Vec.Relation.Binary.Equality.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where

import Data.Vec.Relation.Binary.Equality.Propositional as PEq
import Data.Vec.Relation.Binary.Equality.DecSetoid as DSEq

------------------------------------------------------------------------
-- Publicly re-export everything from decSetoid and propositional
-- equality

open PEq public
open DSEq (decSetoid _≟_) public
  using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid)


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Integers.Definition

module Numbers.Integers.Multiplication where

infix 25 _*Z_
_*Z_ : ℤ → ℤ → ℤ
nonneg x *Z nonneg y = nonneg (x *N y)
nonneg zero *Z negSucc y = nonneg zero
nonneg (succ x) *Z negSucc y = negSucc ((succ x) *N y +N x)
negSucc x *Z nonneg zero = nonneg zero
negSucc x *Z nonneg (succ y) = negSucc ((succ y) *N x +N y)
negSucc x *Z negSucc y = nonneg ((succ x) *N (succ y))

*ZInherits : (a b : ℕ) → nonneg (a *N b) ≡ (nonneg a) *Z (nonneg b)
*ZInherits a b = refl


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

open import Prelude
open import Relation.Binary

module Relation.Binary.Construct.Decision
  {a ℓ₁ ℓ₂} {A : Type a}
  (ord : TotalOrder A ℓ₁ ℓ₂)
  where

open TotalOrder ord renaming (refl to ≤-refl)

_<′_ : A → A → Type
x <′ y = T (does (x <? y))

_≤′_ : A → A → Type
x ≤′ y = T (not (does (y <? x)))

witness-< : ∀ {x y} → x <′ y → x < y
witness-< {x} {y} p with x <? y
witness-< {x} {y} p | yes q = q

witness-≤ : ∀ {x y} → x ≤′ y → x ≤ y
witness-≤ {x} {y} p with y <? x
witness-≤ {x} {y} p | no q = ≮⇒≥ q

compute-< : ∀ {x y} → x < y → x <′ y
compute-< {x} {y} p with x <? y
compute-< {x} {y} p | yes q = tt
compute-< {x} {y} p | no ¬p = ⊥-elim (¬p p)

compute-≤ : ∀ {x y} → x ≤ y → x ≤′ y
compute-≤ {x} {y} ¬p with y <? x
compute-≤ {x} {y} ¬p | yes p = ⊥-elim (<⇒≱ p ¬p)
compute-≤ {x} {y} ¬p | no  _ = tt

≰⇒>′ : ∀ {x y} → ¬ (x ≤′ y) → y <′ x
≰⇒>′ {x} {y} p with y <? x
≰⇒>′ {x} {y} p | no  _ = p tt
≰⇒>′ {x} {y} p | yes _ = tt

≮⇒≥′ : ∀ {x y} → ¬ (x <′ y) → y ≤′ x
≮⇒≥′ {x} {y} p with x <? y
≮⇒≥′ {x} {y} p | no  _ = tt
≮⇒≥′ {x} {y} p | yes _ = p tt

dec-ord : TotalOrder A ℓzero ℓzero
StrictPreorder._<_    (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder dec-ord)) = _<′_
StrictPreorder.trans  (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder dec-ord)) p q = compute-< (<-trans (witness-< p) (witness-< q))
StrictPreorder.irrefl (StrictPartialOrder.strictPreorder (TotalOrder.strictPartialOrder dec-ord)) p = irrefl (witness-< p)
StrictPartialOrder.conn (TotalOrder.strictPartialOrder dec-ord) p q = conn (p ∘ compute-<) (q ∘ compute-<)
Preorder._≤_  (PartialOrder.preorder (TotalOrder.partialOrder dec-ord)) = _≤′_
Preorder.refl (PartialOrder.preorder (TotalOrder.partialOrder dec-ord)) = compute-≤ ≤-refl
PartialOrder.antisym (TotalOrder.partialOrder dec-ord) p q = antisym (witness-≤ p) (witness-≤ q)
Preorder.trans (PartialOrder.preorder (TotalOrder.partialOrder dec-ord)) p q = compute-≤ (≤-trans (witness-≤ p) (witness-≤ q))
TotalOrder._<?_ dec-ord x y = iff-dec (compute-< iff witness-<) (x <? y)
TotalOrder.≰⇒> dec-ord = ≰⇒>′
TotalOrder.≮⇒≥ dec-ord = ≮⇒≥′


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

open import HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver

{- Splitting Lemma - Left Split
   Assume an exact sequence:

             φ   ψ
           G → H → K → 0

   where H is abelian. If φ has a left inverse χ, then H == G × K. Over
   this path φ becomes the natural injection and ψ the natural projection.

   The only non-private terms are [iso], [φ-over-iso], and [ψ-over-iso].
-}

module cohomology.SplitExactLeft {i} {G H K L : Group i}
  (H-abelian : is-abelian H) (φ : G →ᴳ H) (ψ : H →ᴳ K) where

private
  module G = Group G
  module H = Group H
  module K = Group K
  module φ = GroupHom φ
  module ψ = GroupHom ψ

module SplitExactLeft
  (ex : is-exact-seq (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ K ⟨ cst-hom ⟩→ L ⊣|))
  (χ : H →ᴳ G) (χ-linv : (g : G.El) → GroupHom.f χ (φ.f g) == g)
  where

  private
    module χ = GroupHom χ

    {- H == Im φ ×G Ker χ -}

    im-part : H →ᴳ Im φ
    im-part = im-in-hom φ ∘ᴳ χ

    im-part-imφ : (h : H.El) (s : Trunc -1 (Σ G.El (λ g → φ.f g == h)))
      → GroupHom.f im-part h == (h , s)
    im-part-imφ h s = pair=
      (Trunc-rec (Group.El-level H _ _)
        (λ {(g , p) →
          φ.f (χ.f h)        =⟨ ap (φ.f ∘ χ.f) (! p) ⟩
          φ.f (χ.f (φ.f g))  =⟨ ap φ.f (χ-linv g) ⟩
          φ.f g              =⟨ p ⟩
          h ∎})
        s)
      (prop-has-all-paths-↓ Trunc-level)

    im-part-kerχ :  (h : H.El) (p : χ.f h == G.ident)
      → GroupHom.f im-part h == Group.ident (Im φ)
    im-part-kerχ h p = pair=
      (ap φ.f p ∙ φ.pres-ident)
      (prop-has-all-paths-↓ Trunc-level)

    ker-part : H →ᴳ Ker χ
    ker-part = ker-hom χ
      (comp-hom H-abelian (idhom H) (inv-hom H H-abelian ∘ᴳ (φ ∘ᴳ χ)))
      (λ h →
        χ.f (H.comp h (H.inv (φ.f (χ.f h))))
          =⟨ χ.pres-comp h (H.inv (φ.f (χ.f h))) ⟩
        G.comp (χ.f h) (χ.f (H.inv (φ.f (χ.f h))))
          =⟨ ! (φ.pres-inv (χ.f h))
             |in-ctx (λ w → G.comp (χ.f h) (χ.f w)) ⟩
        G.comp (χ.f h) (χ.f (φ.f (G.inv (χ.f h))))
          =⟨ χ-linv (G.inv (χ.f h)) |in-ctx (λ w → G.comp (χ.f h) w) ⟩
        G.comp (χ.f h) (G.inv (χ.f h))
          =⟨ G.invr (χ.f h) ⟩
        G.ident ∎)

    ker-part-imφ : (h : H.El) → Trunc -1 (Σ G.El (λ g → φ.f g == h))
      → GroupHom.f ker-part h == Group.ident (Ker χ)
    ker-part-imφ h = Trunc-rec (Group.El-level (Ker χ) _ _) $
      λ {(g , p) → pair=
       (H.comp h (H.inv (φ.f (χ.f h)))
          =⟨ ! p |in-ctx (λ w → H.comp w (H.inv (φ.f (χ.f w)))) ⟩
        H.comp (φ.f g) (H.inv (φ.f (χ.f (φ.f g))))
          =⟨ χ-linv g |in-ctx (λ w → H.comp (φ.f g) (H.inv (φ.f w))) ⟩
        H.comp (φ.f g) (H.inv (φ.f g))
          =⟨ H.invr (φ.f g) ⟩
        H.ident ∎)
       (prop-has-all-paths-↓ (Group.El-level G _ _))}

    ker-part-kerχ : (h : H.El) (p : χ.f h == G.ident)
      → GroupHom.f ker-part h == (h , p)
    ker-part-kerχ h p = pair=
      (H.comp h (H.inv (φ.f (χ.f h)))
         =⟨ p |in-ctx (λ w → H.comp h (H.inv (φ.f w))) ⟩
       H.comp h (H.inv (φ.f G.ident))
         =⟨ φ.pres-ident |in-ctx (λ w → H.comp h (H.inv w)) ⟩
       H.comp h (H.inv H.ident)
         =⟨ group-inv-ident H |in-ctx H.comp h ⟩
       H.comp h H.ident
         =⟨ H.unitr h ⟩
       h ∎)
      (prop-has-all-paths-↓ (Group.El-level G _ _))

    decomp : H →ᴳ Im φ ×ᴳ Ker χ
    decomp = ×ᴳ-hom-in im-part ker-part

    decomp-is-equiv : is-equiv (GroupHom.f decomp)
    decomp-is-equiv = is-eq _ dinv decomp-dinv dinv-decomp
      where
      dinv : Group.El (Im φ ×ᴳ Ker χ) → H.El
      dinv ((h₁ , _) , (h₂ , _)) = H.comp h₁ h₂

      decomp-dinv : ∀ s → GroupHom.f decomp (dinv s) == s
      decomp-dinv ((h₁ , im) , (h₂ , kr)) = pair×=
        (GroupHom.f im-part (H.comp h₁ h₂)
           =⟨ GroupHom.pres-comp im-part h₁ h₂ ⟩
         Group.comp (Im φ) (GroupHom.f im-part h₁) (GroupHom.f im-part h₂)
           =⟨ im-part-imφ h₁ im
              |in-ctx (λ w → Group.comp (Im φ) w (GroupHom.f im-part h₂)) ⟩
         Group.comp (Im φ) (h₁ , im) (GroupHom.f im-part h₂)
           =⟨ im-part-kerχ h₂ kr
              |in-ctx (λ w → Group.comp (Im φ) (h₁ , im) w) ⟩
         Group.comp (Im φ) (h₁ , im) (Group.ident (Im φ))
           =⟨ Group.unitr (Im φ) (h₁ , im) ⟩
         (h₁ , im) ∎)
        (GroupHom.f ker-part (H.comp h₁ h₂)
           =⟨ GroupHom.pres-comp ker-part h₁ h₂ ⟩
         Group.comp (Ker χ) (GroupHom.f ker-part h₁) (GroupHom.f ker-part h₂)
           =⟨ ker-part-imφ h₁ im
              |in-ctx (λ w → Group.comp (Ker χ) w (GroupHom.f ker-part h₂)) ⟩
         Group.comp (Ker χ) (Group.ident (Ker χ)) (GroupHom.f ker-part h₂)
           =⟨ ker-part-kerχ h₂ kr
              |in-ctx (λ w → Group.comp (Ker χ) (Group.ident (Ker χ)) w) ⟩
         Group.comp (Ker χ) (Group.ident (Ker χ)) (h₂ , kr)
           =⟨ Group.unitl (Ker χ) (h₂ , kr) ⟩
         (h₂ , kr) ∎)

      dinv-decomp : ∀ h → dinv (GroupHom.f decomp h) == h
      dinv-decomp h =
        H.comp (φ.f (χ.f h)) (H.comp h (H.inv (φ.f (χ.f h))))
          =⟨ H-abelian (φ.f (χ.f h)) (H.comp h (H.inv (φ.f (χ.f h)))) ⟩
        H.comp (H.comp h (H.inv (φ.f (χ.f h)))) (φ.f (χ.f h))
          =⟨ H.assoc h (H.inv (φ.f (χ.f h))) (φ.f (χ.f h)) ⟩
        H.comp h (H.comp (H.inv (φ.f (χ.f h))) (φ.f (χ.f h)))
          =⟨ H.invl (φ.f (χ.f h)) |in-ctx (λ w → H.comp h w)  ⟩
        H.comp h H.ident
          =⟨ H.unitr h ⟩
        h ∎

    decomp-equiv : H.El ≃ Group.El (Im φ ×ᴳ Ker χ)
    decomp-equiv = (_ , decomp-is-equiv)

    decomp-iso : H == Im φ ×ᴳ Ker χ
    decomp-iso = group-ua (decomp , decomp-is-equiv)

    {- K == Ker χ -}

    ψ|kerχ-inj : (h : Group.El (Ker χ))
      → ψ.f (GroupHom.f (ker-inj χ) h) == K.ident → h == Group.ident (Ker χ)
    ψ|kerχ-inj (h , p) q = pair=
      (Trunc-rec (H.El-level _ _)
        (λ {(g , r) →
          ! r ∙ ap φ.f (! (χ-linv g) ∙ ap χ.f r ∙ p) ∙ φ.pres-ident})
        (ktoi (exact-get ex 0) h q))
      (prop-has-all-paths-↓ (G.El-level _ _))

    ψ|kerχ-surj : (k : K.El)
      → Trunc -1 (Σ (Group.El (Ker χ))
                      (λ h → ψ.f (GroupHom.f (ker-inj χ) h) == k))
    ψ|kerχ-surj k = Trunc-fmap
      (λ {(h , p) → (GroupHom.f ker-part h ,
         ψ.f (H.comp h (H.inv (φ.f (χ.f h))))
           =⟨ ψ.pres-comp h (H.inv (φ.f (χ.f h))) ⟩
         K.comp (ψ.f h) (ψ.f (H.inv (φ.f (χ.f h))))
           =⟨ ψ.pres-inv (φ.f (χ.f h))
              |in-ctx (λ k → K.comp (ψ.f h) k) ⟩
         K.comp (ψ.f h) (K.inv (ψ.f (φ.f (χ.f h))))
           =⟨ itok (exact-get ex 0) (φ.f (χ.f h)) [ χ.f h , idp ]
              |in-ctx (λ k → K.comp (ψ.f h) (K.inv k)) ⟩
         K.comp (ψ.f h) (K.inv K.ident)
           =⟨ group-inv-ident K |in-ctx (λ k → K.comp (ψ.f h) k) ⟩
         K.comp (ψ.f h) K.ident
           =⟨ K.unitr (ψ.f h) ⟩
         ψ.f h
           =⟨ p ⟩
         k ∎)})
      (ktoi (exact-get ex 1) k idp)

    ψ|kerχ-is-equiv : is-equiv (GroupHom.f (ψ ∘ᴳ ker-inj χ))
    ψ|kerχ-is-equiv = surj-inj-is-equiv (ψ ∘ᴳ ker-inj χ)
      (zero-kernel-injective (ψ ∘ᴳ ker-inj χ) ψ|kerχ-inj)
      ψ|kerχ-surj

    Kerχ-iso-K : Ker χ == K
    Kerχ-iso-K = group-ua (ψ ∘ᴳ ker-inj χ , ψ|kerχ-is-equiv)

    {- G == Im φ -}

    im-in-φ-is-equiv : is-equiv (GroupHom.f (im-in-hom φ))
    im-in-φ-is-equiv = surj-inj-is-equiv (im-in-hom φ) inj (im-in-surj φ)
      where
      inj = zero-kernel-injective (im-in-hom φ)
        (λ g p → ! (χ-linv g) ∙ ap (χ.f ∘ fst) p ∙ χ.pres-ident)

    G-iso-Imφ : G == Im φ
    G-iso-Imφ = group-ua (im-in-hom φ , im-in-φ-is-equiv)

  {- H == G ×ᴳ K -}

  iso : H == G ×ᴳ K
  iso = decomp-iso ∙ ap2 _×ᴳ_ (! G-iso-Imφ) Kerχ-iso-K

  private
    decomp-φ = ×ᴳ-hom-in (im-in-hom φ) (cst-hom {G = G} {H = Ker χ})

    φ-over-decomp : φ == decomp-φ [ (λ J → G →ᴳ J) ↓ decomp-iso ]
    φ-over-decomp = codomain-over-iso $ codomain-over-equiv φ.f _ ▹ lemma
      where
      lemma : GroupHom.f decomp ∘ φ.f == GroupHom.f decomp-φ
      lemma = λ= $ λ g → pair×=
        (im-part-imφ (φ.f g) [ g , idp ])
        (ker-part-imφ (φ.f g) [ g , idp ])

    ψ-dinv : Im φ ×ᴳ Ker χ →ᴳ K
    ψ-dinv = ψ ∘ᴳ ×ᴳ-sum-hom H-abelian (im-inj φ) (ker-inj χ)

    ψ-over-decomp : ψ == ψ-dinv [ (λ J → J →ᴳ K) ↓ decomp-iso ]
    ψ-over-decomp = domain-over-iso $ domain!-over-equiv ψ.f _

    id-over-G-iso : idhom _ == im-in-hom φ [ (λ J → G →ᴳ J) ↓ G-iso-Imφ ]
    id-over-G-iso = codomain-over-iso $ codomain-over-equiv (idf _) _

    φ-over-G-iso : φ == im-inj φ [ (λ J → J →ᴳ H) ↓ G-iso-Imφ ]
    φ-over-G-iso =
      domain-over-iso $ domain-over-equiv (GroupHom.f (im-inj φ)) _

    ψ|kerχ-over-K-iso :
      ψ ∘ᴳ ker-inj χ == idhom K [ (λ J → J →ᴳ K) ↓ Kerχ-iso-K ]
    ψ|kerχ-over-K-iso = domain-over-iso $ domain-over-equiv (idf _) _

    φ-over-G-K-isos : decomp-φ == ×ᴳ-inl
      [ (λ J → G →ᴳ J) ↓ ap2 _×ᴳ_ (! G-iso-Imφ) Kerχ-iso-K ]
    φ-over-G-K-isos = ↓-ap2-in _ _×ᴳ_ $ transport
      (λ q → decomp-φ == ×ᴳ-inl [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂}) ↓ q ])
      (! (pair×=-split-l (! G-iso-Imφ) (Kerχ-iso-K)))
      (l ∙ᵈ r)
      where
      l : decomp-φ == ×ᴳ-hom-in (idhom G) (cst-hom {G = G} {H = Ker χ})
          [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂})
            ↓ ap (λ J → J , Ker χ) (! G-iso-Imφ) ]
      l = ↓-ap-in _ (λ J → J , Ker χ)
            (ap↓ (λ θ → ×ᴳ-hom-in θ (cst-hom {G = G} {H = Ker χ}))
              (!ᵈ id-over-G-iso))

      r : ×ᴳ-hom-in (idhom G) (cst-hom {G = G} {H = Ker χ}) == ×ᴳ-inl
          [ (λ {(J₁ , J₂) → G →ᴳ J₁ ×ᴳ J₂}) ↓ ap (λ J → G , J) Kerχ-iso-K ]
      r = ↓-ap-in _ (λ J → G , J)
            (apd (λ J → ×ᴳ-hom-in (idhom G) (cst-hom {G = G} {H = J}))
              Kerχ-iso-K)

    ψ-over-G-K-isos : ψ-dinv == ×ᴳ-snd {G = G}
      [ (λ J → J →ᴳ K) ↓ ap2 _×ᴳ_ (! G-iso-Imφ) Kerχ-iso-K ]
    ψ-over-G-K-isos = ↓-ap2-in _ _×ᴳ_ $ transport
      (λ q → ψ-dinv == ×ᴳ-snd {G = G}
        [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K}) ↓ q ])
      (! (pair×=-split-l (! G-iso-Imφ) (Kerχ-iso-K)))
      (l ∙ᵈ (m ◃ r))
      where
      l : ψ-dinv == ψ ∘ᴳ ×ᴳ-sum-hom H-abelian φ (ker-inj χ)
          [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K})
            ↓ ap (λ J → J , Ker χ) (! G-iso-Imφ) ]
      l = ↓-ap-in _ (λ J → J , Ker χ)
        (ap↓ (λ θ → ψ ∘ᴳ ×ᴳ-sum-hom H-abelian θ (ker-inj χ))
          (!ᵈ φ-over-G-iso))

      m : ψ ∘ᴳ ×ᴳ-sum-hom H-abelian φ (ker-inj χ)
        == (ψ ∘ᴳ ker-inj χ) ∘ᴳ ×ᴳ-snd {G = G}
      m = hom= _ _ (λ= (λ {(g , (h , _)) →
        ψ.f (H.comp (φ.f g) h)
          =⟨ ψ.pres-comp (φ.f g) h ⟩
        K.comp (ψ.f (φ.f g)) (ψ.f h)
          =⟨ itok (exact-get ex 0) (φ.f g) [ g , idp ]
             |in-ctx (λ k → K.comp k (ψ.f h)) ⟩
        K.comp K.ident (ψ.f h)
          =⟨ K.unitl (ψ.f h) ⟩
        ψ.f h ∎}))

      r : (ψ ∘ᴳ ker-inj χ) ∘ᴳ ×ᴳ-snd {G = G} == ×ᴳ-snd {G = G}
          [ (λ {(J₁ , J₂) → J₁ ×ᴳ J₂ →ᴳ K})
            ↓ (ap (λ J → G , J) Kerχ-iso-K) ]
      r = ↓-ap-in _ (λ J → G , J)
            (ap↓ (λ θ → θ ∘ᴳ ×ᴳ-snd {G = G}) ψ|kerχ-over-K-iso)

  φ-over-iso : φ == ×ᴳ-inl [ (λ J → G →ᴳ J) ↓ iso ]
  φ-over-iso = φ-over-decomp ∙ᵈ φ-over-G-K-isos

  ψ-over-iso : ψ == (×ᴳ-snd {G = G}) [ (λ J → J →ᴳ K) ↓ iso ]
  ψ-over-iso = ψ-over-decomp ∙ᵈ ψ-over-G-K-isos

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Data.Real.Gauge where

import Data.Rational
open Data.Rational using (Rational)

Gauge = Rational

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Quasigroup.Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Level using (_⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Quasigroup.Definitions _≈_

record IsPique (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isQuasigroup : IsQuasigroup ∙ \\ //
    idem         : Idempotent ∙

  open IsQuasigroup isQuasigroup public


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

open import HoTT
open import homotopy.Freudenthal

module homotopy.IterSuspensionStable where

{- π (S k) (Ptd-Susp^ (S n) X) == π k (Ptd-Susp^ n X), where k = S k'
   Susp^Stable below assumes k ≠ O instead of taking k' as the argument -}
module Susp^StableSucc {i} (X : Ptd i) (cX : is-connected ⟨0⟩ (fst X))
  (n : ℕ) (k' : ℕ) (kle : S k' ≤ n *2) where

  {- need k,n ≥ 1 -}
  k : ℕ
  k = S k'

  {- some numeric computations -}
  private
    kle' : ⟨ k ⟩ ≤T S ((n -2) +2+ S (n -2))
    kle' = ≤T-trans (⟨⟩-monotone-≤ kle) (inl (lemma n))
      where lemma : (n : ℕ) → ⟨ n *2 ⟩ == S ((n -2) +2+ S (n -2))
            lemma O = idp
            lemma (S n') = ap S (ap S (lemma n')
                                 ∙ ! (+2+-βr (S n' -2) (S n' -2)))

    nlemma₁ : (n : ℕ) → (n -2) +2+ ⟨0⟩ == S (S (n -2))
    nlemma₁ n = +2+-comm (n -2) ⟨0⟩

    nlemma₂ : (k : ℕ) → (k -2) +2+ ⟨0⟩ == ⟨ k ⟩
    nlemma₂ O = idp
    nlemma₂ (S k) = ap S (nlemma₂ k)

  private
    module F = FreudenthalIso
      (n -2) k (ℕ-S≠O _) kle' (⊙Susp^ n X)
      (transport (λ t → is-connected t (fst (⊙Susp^ n X)))
                 (nlemma₁ n) (⊙Susp^-conn n cX))

  stable : (tk : k ≠ 0) (tsk : S k ≠ 0)
    → π (S k) tsk (⊙Susp^ (S n) X) == π k tk (⊙Susp^ n X)
  stable tk tsk =
    π (S k) tsk (⊙Susp^ (S n) X)
      =⟨ π-inner-iso k tk tsk (⊙Susp^ (S n) X) ⟩
    π k tk (⊙Ω (⊙Susp^ (S n) X))
      =⟨ ! (π-Trunc-shift-iso k tk (⊙Ω (⊙Susp^ (S n) X))) ⟩
    Ω^-Group k tk (⊙Trunc ⟨ k ⟩ (⊙Ω (⊙Susp^ (S n) X))) Trunc-level
      =⟨ ! (group-ua F.iso) ⟩
    Ω^-Group k tk (⊙Trunc ⟨ k ⟩ (⊙Susp^ n X)) Trunc-level
      =⟨ π-Trunc-shift-iso k tk (⊙Susp^ n X) ⟩
    π k tk (⊙Susp^ n X) ∎

{- π (S k) (⊙Susp^ (S n) X) == π k (⊙Susp^ n X), where k > 0 -}
module Susp^Stable {i} (X : Ptd i) (cX : is-connected ⟨0⟩ (fst X))
  (n : ℕ) (k : ℕ) (tk : k ≠ 0) (tsk : S k ≠ 0) (kle : k ≤ n *2) where

  private
    lemma : ∀ {i} (C : (n : ℕ) → n ≠ 0 → S n ≠ 0 → Type i)
      → ((n : ℕ) (tsn : S n ≠ 0) (tssn : S (S n) ≠ 0)
            → C (S n) tsn tssn)
      → ((n : ℕ) (tn : n ≠ 0) (tsn : S n ≠ 0)
            → C n tn tsn)
    lemma C f O tn _ = ⊥-rec (tn idp)
    lemma C f (S n) tsn tssn = f n tsn tssn

  abstract
    stable : π (S k) tsk (⊙Susp^ (S n) X) == π k tk (⊙Susp^ n X)
    stable = lemma
      (λ r tr tsr → (r ≤ n *2) →
         π (S r) tsr (⊙Susp^ (S n) X) == π r tr (⊙Susp^ n X))
      (λ r' tsr' tssr' → λ rle →
        Susp^StableSucc.stable X cX n r' rle tsr' tssr')
      k tk tsk kle

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module RecordUpdatePreservesType where

data ⊤ : Set where
  tt : ⊤

record R : Set where
  field
    a : ⊤

record Q : Set where
  field
    a : ⊤

old : R
old = record { a = tt }

new : Q
new = record old { a = tt }

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Dave.Algebra.Naturals.Ordering where
    open import Dave.Algebra.Naturals.Definition public
    open import Dave.Algebra.Naturals.Addition public
    open import Dave.Algebra.Naturals.Multiplication public

    -- TO-DO: define relation
    data _≤_ : ℕ → ℕ → Set where
        z≤n : ∀ {n : ℕ} → zero ≤ n
        s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

    infix 4 _≤_

    inv-s≤s : ∀ {m n : ℕ} → suc m ≤ suc n → m ≤ n
    inv-s≤s (s≤s m≤n) = m≤n

    inv-z≤n : ∀ {m : ℕ} → m ≤ zero → m ≡ zero
    inv-z≤n z≤n = refl

    -- TO-DO: define relation properties in general
    ≤-refl : ∀ {n : ℕ} → n ≤ n
    ≤-refl {zero} = z≤n
    ≤-refl {suc n} = s≤s ≤-refl

    ≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
    ≤-trans z≤n n≤p = z≤n
    ≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

    ≤-trans´ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p
    ≤-trans´ zero n p z≤n n≤p = z≤n
    ≤-trans´ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans´ m n p m≤n n≤p)

    ≤-antisym : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
    ≤-antisym z≤n z≤n = refl
    ≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

    data Total (m n : ℕ) : Set where
        forward : m ≤ n → Total m n
        flipped : n ≤ m → Total m n

    data Total´ : ℕ → ℕ → Set where
        forward´ : ∀ {m n : ℕ} → m ≤ n → Total´ m n
        flipped´ : ∀ {m n : ℕ} → n ≤ m → Total´ m n

    ≤-total : ∀ (m n : ℕ) → Total m n
    ≤-total zero n = forward z≤n
    ≤-total (suc m) zero = flipped z≤n
    ≤-total (suc m) (suc n) with ≤-total m n
    ...                         | forward m≤n = forward (s≤s m≤n)
    ...                         | flipped n≤m = flipped (s≤s n≤m)

    ≤-total´ : ∀ (m n : ℕ) → Total m n
    ≤-total´ zero n = forward z≤n
    ≤-total´ (suc m) zero = flipped z≤n
    ≤-total´ (suc m) (suc n) = helper (≤-total´ m n)
        where
        helper : Total m n → Total (suc m) (suc n)
        helper (forward m≤n) = forward (s≤s m≤n)
        helper (flipped n≤m) = flipped (s≤s n≤m)

    +-monoᵣ-≤ : ∀ (n p q : ℕ) → p ≤ q → n + p ≤ n + q
    +-monoᵣ-≤ zero p q p≤q = p≤q
    +-monoᵣ-≤ (suc n) p q p≤q = s≤s (+-monoᵣ-≤ n p q p≤q)

    +-monoₗ-≤ : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p
    +-monoₗ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p = +-monoᵣ-≤ p m n m≤n

    +-mono-≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q
    +-mono-≤ m n p q m≤n p≤q = ≤-trans (+-monoₗ-≤ m n p m≤n) (+-monoᵣ-≤ n p q p≤q)

    *-monoᵣ-≤ : ∀ (n p q : ℕ) → p ≤ q → n * p ≤ n * q
    *-monoᵣ-≤ zero p q p≤q = z≤n
    *-monoᵣ-≤ (suc n) p q p≤q = +-mono-≤ (n * p) (n * q) p q (*-monoᵣ-≤ n p q p≤q) p≤q

    *-monoₗ-≤ : ∀ (m n p : ℕ) → m ≤ n → m * p ≤ n * p
    *-monoₗ-≤ m n p m≤n  rewrite ℕ-*-comm m p | ℕ-*-comm n p = *-monoᵣ-≤ p m n m≤n

    *-mono-≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m * p ≤ n * q
    *-mono-≤ m n p q m≤n p≤q = ≤-trans (*-monoₗ-≤ m n p m≤n) (*-monoᵣ-≤ n p q p≤q)

    {- Strict inequality -}
    infix 4 _<_ _>_

    data _<_ : ℕ → ℕ → Set where
        z<s : ∀ {n : ℕ} → zero < suc n
        s<s : ∀ {m n : ℕ} → m < n → suc m < suc n

    <-trans : ∀ {m n p : ℕ} → m < n → n < p → m < p
    <-trans z<s (s<s n<p) = z<s
    <-trans (s<s m<n) (s<s n<p) = s<s (<-trans m<n n<p)

    +-monoᵣ-< : ∀ (n p q : ℕ) → p < q → n + p < n + q
    +-monoᵣ-< zero p q p<q = p<q
    +-monoᵣ-< (suc n) p q p<q = s<s (+-monoᵣ-< n p q p<q)

    +-monoₗ-< : ∀ (m n p : ℕ) → m < n → m + p < n + p
    +-monoₗ-< m n p m<n rewrite +-comm m p | +-comm n p = +-monoᵣ-< p m n m<n

    +-mono-< : ∀ (m n p q : ℕ) → m < n → p < q → m + p < n + q
    +-mono-< m n p q m<n p<q = <-trans (+-monoₗ-< m n p m<n) (+-monoᵣ-< n p q p<q)

    suc-≤→< : ∀ (m n : ℕ) → suc m ≤ n → m < n
    suc-≤→< zero (suc n) leq = z<s
    suc-≤→< (suc m) (suc n) (s≤s leq) = s<s (suc-≤→< m n leq)

    <→suc-≤ : ∀ (m n : ℕ) → m < n → suc m ≤ n
    <→suc-≤ zero (suc n) le = s≤s z≤n
    <→suc-≤ (suc m) (suc n) (s<s le) = s≤s (<→suc-≤ m n le)

    data _>_ : ℕ → ℕ → Set where
        co-m>n : ∀ {m n : ℕ} → n < m → m > n

    ℕ-suc-> : ∀ {m n : ℕ} → m > n → suc m > suc n
    ℕ-suc-> (co-m>n x) = co-m>n (s<s x)

    {- Trichotomy -}
    data Trichotomy (m n : ℕ) : Set where
        t-m>n : m > n → Trichotomy m n
        t-m≡n : m ≡ n → Trichotomy m n
        t-m<n : m < n → Trichotomy m n

    ℕ-suc-Trichotomy : ∀ {m n : ℕ} → Trichotomy m n → Trichotomy (suc m) (suc n)
    ℕ-suc-Trichotomy (t-m>n x) = t-m>n (ℕ-suc-> x)
    ℕ-suc-Trichotomy (t-m≡n refl) = t-m≡n refl
    ℕ-suc-Trichotomy (t-m<n x) = t-m<n (s<s x)

    ℕ-is-Trichotomy : ∀ (m n : ℕ) → Trichotomy m n
    ℕ-is-Trichotomy zero zero = t-m≡n refl
    ℕ-is-Trichotomy zero (suc n) = t-m<n z<s
    ℕ-is-Trichotomy (suc m) zero = t-m>n (co-m>n z<s)
    ℕ-is-Trichotomy (suc m) (suc n) = ℕ-suc-Trichotomy (ℕ-is-Trichotomy m n)


text:
{-# OPTIONS --type-in-type #-}

open import Agda.Primitive using (Setω)

-- No panic should be triggered

data A : Setω where

record B' : Set where
  field
    theA : A

data B : Set where
  b : A → B

data C : Set where
  c : Setω → C

data C' : Setω where
  c : Setω → C'

record C'' : Setω where
  field
    theSet : Setω
    thefield : theSet


text:
module Issue160 where

data Bool : Set where
  true  : Bool
  false : Bool

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

inj : ∀ {A} (f : A -> A) {a b : A} →
      f a ≡ f b -> a ≡ b
inj f refl = refl

absurd : true ≡ false
absurd = inj (λ _ → true) refl