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

module Definition.Conversion.Transitivity where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion
open import Definition.Conversion.Soundness
open import Definition.Conversion.Stability
open import Definition.Conversion.Conversion
open import Definition.Conversion.Whnf
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Injectivity
import Definition.Typed.Consequences.Inequality as WF
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.SucCong

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

mutual
  -- Transitivity of algorithmic equality of neutrals.
  trans~↑! : ∀ {t u v A B Γ Δ l l'}
         → l PE.≡ l'
         → ⊢ Γ ≡ Δ
         → Γ ⊢ t ~ u ↑! A ^ l
         → Δ ⊢ u ~ v ↑! B ^ l'
         → Γ ⊢ t ~ v ↑! A ^ l
         × Γ ⊢ A ≡ B ^ [ ! , l ]
  trans~↑! el Γ≡Δ (var-refl x₁ x≡y) (var-refl x₂ x≡y₁) =
    var-refl x₁ (PE.trans x≡y x≡y₁)
    , proj₂ (neTypeEq (var _) x₁
               (PE.subst (λ x → _ ⊢ var x ∷ _ ^ _) (PE.sym x≡y)
                         (stabilityTerm (symConEq Γ≡Δ) (PE.subst (λ lx → _ ⊢ _ ∷ _ ^ [ ! , lx ]) (PE.sym el) x₂))))
  trans~↑! el Γ≡Δ (app-cong {rF = !} t~u a<>b) (app-cong {rF = !} u~v b<>c) =
    let t~v , ΠFG≡ΠF′G′ = trans~↓! PE.refl Γ≡Δ t~u u~v
        F≡F₁ , rF≡rF₁ , lF≡lF₁ , lG≡lG₁ , G≡G₁ = injectivity ΠFG≡ΠF′G′
        a<>c = transConv↑Term Γ≡Δ F≡F₁ a<>b (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ _ ^ ι x) (PE.sym lF≡lF₁) b<>c)
    in  app-cong t~v a<>c , substTypeEq G≡G₁ (soundnessConv↑Term a<>b)
  trans~↑! el Γ≡Δ (app-cong {rF = %} t~u a<>b) (app-cong {rF = %} u~v b<>c) =
    let t~v , ΠFG≡ΠF′G′ = trans~↓! PE.refl Γ≡Δ t~u u~v
        F≡F₁ , rF≡rF₁ , lF≡lF₁ , lG≡lG₁ , G≡G₁ = injectivity ΠFG≡ΠF′G′
        ⊢Γ = proj₁ (proj₂ (contextConvSubst Γ≡Δ))
        a<>c = trans~↑% Γ≡Δ a<>b (conv~↑% (PE.subst (λ x → _ ⊢ _ ~ _ ↑%  _ ^ ι x) (PE.sym lF≡lF₁) b<>c) (stabilityEq Γ≡Δ (sym F≡F₁)))
        _ , _ , t≡v = soundness~↑% a<>b
    in  app-cong t~v a<>c , substTypeEq G≡G₁ t≡v
  trans~↑! el Γ≡Δ (app-cong {rF = !} t~u a<>b) (app-cong {rF = %} u~v b<>c) =
   let whnfA , neK , neL = ne~↓! t~u
       ⊢A , ⊢k , ⊢l₁ = syntacticEqTerm (soundness~↓! t~u)
       ⊢A' , ⊢l₁' , ⊢l = syntacticEqTerm (soundness~↓! u~v)
       _ , ΠFG≡ΠF₂G₂ = neTypeEq neL ⊢l₁ (stabilityTerm (symConEq Γ≡Δ) ⊢l₁')
       F≡F₂ , rF≡rF₂ , G≡G₂ = injectivity ΠFG≡ΠF₂G₂
   in ⊥-elim (relevance-discr rF≡rF₂)
  trans~↑! el Γ≡Δ (app-cong {rF = %} t~u a<>b) (app-cong {rF = !} u~v b<>c) =
   let whnfA , neK , neL = ne~↓! t~u
       ⊢A , ⊢k , ⊢l₁ = syntacticEqTerm (soundness~↓! t~u)
       ⊢A' , ⊢l₁' , ⊢l = syntacticEqTerm (soundness~↓! u~v)
       _ , ΠFG≡ΠF₂G₂ = neTypeEq neL ⊢l₁ (stabilityTerm (symConEq Γ≡Δ) ⊢l₁')
       F≡F₂ , rF≡rF₂ , G≡G₂ = injectivity ΠFG≡ΠF₂G₂
   in ⊥-elim (relevance-discr (PE.sym rF≡rF₂))
  trans~↑! PE.refl Γ≡Δ (natrec-cong A<>B a₀<>b₀ aₛ<>bₛ t~u) (natrec-cong B<>C b₀<>c₀ bₛ<>cₛ u~v) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        A≡B = soundnessConv↑ A<>B
        F[0]≡F₁[0] = substTypeEq A≡B (refl (zeroⱼ ⊢Γ))
        ΠℕFs≡ΠℕF₁s = sucCong A≡B
        A<>C = transConv↑ (Γ≡Δ ∙ (refl (univ (ℕⱼ ⊢Γ)))) A<>B B<>C
        a₀<>c₀ = transConv↑Term Γ≡Δ F[0]≡F₁[0] a₀<>b₀ b₀<>c₀
        aₛ<>cₛ = transConv↑Term Γ≡Δ ΠℕFs≡ΠℕF₁s aₛ<>bₛ bₛ<>cₛ
        t~v , _ = trans~↓! PE.refl Γ≡Δ t~u u~v
    in  natrec-cong A<>C a₀<>c₀ aₛ<>cₛ t~v
    ,   substTypeEq A≡B (soundness~↓! t~u)
  trans~↑! PE.refl Γ≡Δ (Emptyrec-cong A<>B t~u) (Emptyrec-cong B<>C u~v) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        A≡B = soundnessConv↑ A<>B
        A<>C = transConv↑ Γ≡Δ A<>B B<>C
        ⊢t , ⊢u , t≡u = soundness~↑% t~u
        _ , ⊢v , u≡v = soundness~↑% u~v
        t~v = %~↑ ⊢t (stabilityTerm (symConEq Γ≡Δ) ⊢v)
    in  Emptyrec-cong A<>C t~v , A≡B
  trans~↑! el Γ≡Δ (Id-cong X x x₁) (Id-cong Y x₂ x₃) =
    let XY , [U] = trans~↓! el Γ≡Δ X Y
        X≡Y = univ (soundness~↓! XY)
        Y≡Y = PE.subst (λ lx → _ ⊢ _ ≡ _ ^ [ ! , ι lx ]) (PE.sym (next-inj el)) (univ (soundness~↓! Y))
        x₂' = PE.subst (λ lx → _ ⊢ _ [conv↑] _ ∷ _ ^ ι lx) (PE.sym (next-inj el)) x₂
        t~t = transConv↑Term Γ≡Δ X≡Y x (convConvTerm x₂' Y≡Y)
        x₃' = PE.subst (λ lx → _ ⊢ _ [conv↑] _ ∷ _ ^ ι lx) (PE.sym (next-inj el)) x₃
        u~u = transConv↑Term Γ≡Δ X≡Y x₁ (convConvTerm x₃' Y≡Y)
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-cong XY t~t u~u , PE.subst (λ lx → _ ⊢ _ ≡ SProp lx ^ [ ! , _ ]) (next-inj el) (refl (Ugenⱼ ⊢Γ))
  trans~↑! el Γ≡Δ (Id-ℕ X x) (Id-ℕ Y x₁) =
    let t~t , ℕ≡ℕ = trans~↓! PE.refl Γ≡Δ X Y
        u~u = transConv↑Term Γ≡Δ ℕ≡ℕ x x₁
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-ℕ t~t u~u , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (Id-ℕ0 X) (Id-ℕ0 Y) =
    let t~t , ℕ≡ℕ = trans~↓! PE.refl Γ≡Δ X Y
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-ℕ0 t~t , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (Id-ℕS x X) (Id-ℕS x₁ Y) =
    let X~X , ℕ≡ℕ = trans~↓! PE.refl Γ≡Δ X Y
        t~t = transConv↑Term Γ≡Δ ℕ≡ℕ x x₁
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-ℕS t~t X~X , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (Id-U X x) (Id-U Y x₁) =
    let t~t , U≡U = trans~↓! PE.refl Γ≡Δ X Y
        u~u = transConv↑Term Γ≡Δ U≡U x x₁
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-U t~t u~u , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (Id-Uℕ X) (Id-Uℕ Y) =
    let t~t , _ = trans~↓! PE.refl Γ≡Δ X Y
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-Uℕ t~t , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (Id-UΠ x X) (Id-UΠ x₁ Y) =
    let t~t , U≡U = trans~↓! PE.refl Γ≡Δ X Y
        u~u = transConv↑Term Γ≡Δ U≡U x x₁
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in Id-UΠ u~u t~t , refl (Ugenⱼ ⊢Γ)
  trans~↑! el Γ≡Δ (cast-cong X x x₁ x₂ x₃) (cast-cong Y x₄ x₅ x₆ x₇) =
    let XY , [U] = trans~↓! PE.refl Γ≡Δ X Y
        X≡Y = univ (soundness~↓! XY)
        Y≡Y = univ (soundness~↓! Y)
        t~t = transConv↑Term Γ≡Δ [U] x x₄
        u~u = transConv↑Term Γ≡Δ X≡Y x₁ (convConvTerm x₅ Y≡Y)
        A₁≡B = trans (soundnessConv↑Term t~t) (sym (soundnessConv↑Term (stabilityConv↑Term (symConEq Γ≡Δ) x₄)))
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in cast-cong XY t~t u~u x₂ (stabilityTerm (symConEq Γ≡Δ) x₇) , univ A₁≡B
  trans~↑! el Γ≡Δ (cast-ℕ X x x₁ x₂) (cast-ℕ Y x₃ x₄ x₅) =
    let XY , [U] = trans~↓! PE.refl Γ≡Δ X Y
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        t~t = transConv↑Term Γ≡Δ (refl (univ (ℕⱼ  ⊢Γ))) x x₃
    in cast-ℕ XY t~t x₁ (stabilityTerm (symConEq Γ≡Δ) x₅) , univ (soundness~↓! X)
  trans~↑! el Γ≡Δ (cast-ℕℕ X x x₁) (cast-ℕℕ Y x₂ x₃) =
    let XY , N = trans~↓! PE.refl Γ≡Δ X Y
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in cast-ℕℕ XY x (stabilityTerm (symConEq Γ≡Δ) x₃) , N
  trans~↑! el Γ≡Δ (cast-Π x X x₁ x₂ x₃) (cast-Π x₄ Y x₅ x₆ x₇) =
    let XY , [U] = trans~↓! PE.refl Γ≡Δ X Y
        X≡Y = soundness~↓! XY
        Y≡Y = univ (soundnessConv↑Term x₄)
        t~t = transConv↑Term Γ≡Δ [U] x x₄
        u~u = transConv↑Term Γ≡Δ (univ (soundnessConv↑Term t~t)) x₁ (convConvTerm x₅ Y≡Y)
        A₁≡B = trans X≡Y (sym (soundness~↓! (stability~↓! (symConEq Γ≡Δ) Y)))
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in cast-Π t~t XY u~u x₂ (stabilityTerm (symConEq Γ≡Δ) x₇) , univ A₁≡B
  trans~↑! el Γ≡Δ (cast-Πℕ x x₁ x₂ x₃) (cast-Πℕ x₄ x₅ x₆ x₇) =
    let Y≡Y = univ (soundnessConv↑Term x₄)
        ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        t~t = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x x₄
        u~u = transConv↑Term Γ≡Δ (univ (soundnessConv↑Term t~t)) x₁ (convConvTerm x₅ Y≡Y)
    in cast-Πℕ t~t u~u x₂ (stabilityTerm (symConEq Γ≡Δ) x₇) , refl (univ (ℕⱼ  ⊢Γ))
  trans~↑! el Γ≡Δ (cast-ℕΠ x x₁ x₂ x₃) (cast-ℕΠ x₄ x₅ x₆ x₇) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        t~t = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x x₄
        u~u = transConv↑Term Γ≡Δ (refl (univ (ℕⱼ  ⊢Γ))) x₁ x₅
    in cast-ℕΠ t~t u~u x₂ (stabilityTerm (symConEq Γ≡Δ) x₇) , univ (soundnessConv↑Term x)
  trans~↑! el Γ≡Δ (cast-ΠΠ%! x x₁ x₂ x₃ x₄) (cast-ΠΠ%! x₅ x₆ x₇ x₈ x₉) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        A~A = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x x₅
        B~B = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x₁ x₆
        u~u = transConv↑Term Γ≡Δ (univ (soundnessConv↑Term x)) x₂ x₇
    in cast-ΠΠ%! A~A B~B u~u x₃ (stabilityTerm (symConEq Γ≡Δ) x₉) ,
       trans (univ (soundnessConv↑Term B~B)) (sym (univ (soundnessConv↑Term (stabilityConv↑Term (symConEq Γ≡Δ) x₆))))
  trans~↑! el Γ≡Δ (cast-ΠΠ!% x x₁ x₂ x₃ x₄) (cast-ΠΠ!% x₅ x₆ x₇ x₈ x₉) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        A~A = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x x₅
        B~B = transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ)) x₁ x₆
        u~u = transConv↑Term Γ≡Δ (univ (soundnessConv↑Term x)) x₂ x₇
    in cast-ΠΠ!% A~A B~B u~u x₃ (stabilityTerm (symConEq Γ≡Δ) x₉) ,
       trans (univ (soundnessConv↑Term B~B)) (sym (univ (soundnessConv↑Term (stabilityConv↑Term (symConEq Γ≡Δ) x₆))))

  trans~↑% : ∀ {t u v A Γ Δ  l}
         → ⊢ Γ ≡ Δ
         → Γ ⊢ t ~ u ↑% A ^ l
         → Δ ⊢ u ~ v ↑% A ^ l
         → Γ ⊢ t ~ v ↑% A ^ l
  trans~↑% Γ≡Δ (%~↑ ⊢t ⊢u) (%~↑ ⊢u′ ⊢v) =
    let ⊢Δu′ = stabilityTerm (symConEq Γ≡Δ) ⊢u′
        ⊢Δv = stabilityTerm (symConEq Γ≡Δ) ⊢v
    in %~↑ ⊢t ⊢Δv

  -- Transitivity of algorithmic equality of neutrals with types in WHNF.
  trans~↓! : ∀ {t u v A B Γ Δ l l'}
          → l PE.≡ l'
          → ⊢ Γ ≡ Δ
          → Γ ⊢ t ~ u ↓! A ^ l
          → Δ ⊢ u ~ v ↓! B ^ l'
          → Γ ⊢ t ~ v ↓! A ^ l
          × Γ ⊢ A ≡ B ^ [ ! , l ]
  trans~↓! PE.refl Γ≡Δ ([~] A₁ D whnfA k~l) ([~] A₂ D₁ whnfA₁ k~l₁) =
    let t~v , A≡B = trans~↑! PE.refl Γ≡Δ k~l k~l₁
    in  [~] A₁ D whnfA t~v
    ,   trans (sym (subset* D))
              (trans A≡B
                     (subset* (stabilityRed* (symConEq Γ≡Δ) D₁)))

  -- Transitivity of algorithmic equality of types.
  transConv↑ : ∀ {A B C r Γ Δ}
            → ⊢ Γ ≡ Δ
            → Γ ⊢ A [conv↑] B ^ r
            → Δ ⊢ B [conv↑] C ^ r
            → Γ ⊢ A [conv↑] C ^ r
  transConv↑ {r = r} Γ≡Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
             ([↑] A″ B″ D₁ D″ whnfA″ whnfB″ A′<>B″) =
    [↑] A′ B″ D (stabilityRed* (symConEq Γ≡Δ) D″) whnfA′ whnfB″
        (transConv↓ Γ≡Δ A′<>B′
                    (PE.subst (λ x → _ ⊢ x [conv↓] B″ ^ r)
                              (whrDet* (D₁ , whnfA″)
                                        (stabilityRed* Γ≡Δ D′ , whnfB′))
                              A′<>B″))

  -- Transitivity of algorithmic equality of types in WHNF.
  transConv↓ : ∀ {A B C r Γ Δ}
            → ⊢ Γ ≡ Δ
            → Γ ⊢ A [conv↓] B ^ r
            → Δ ⊢ B [conv↓] C ^ r
            → Γ ⊢ A [conv↓] C ^ r
  transConv↓ Γ≡Δ (U-refl e x) (U-refl e₁ x₁) = U-refl (PE.trans e e₁) x
  transConv↓ Γ≡Δ (univ x) (univ y) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        X = transConv↓Term Γ≡Δ (refl (Ugenⱼ ⊢Γ )) PE.refl x y
    in univ X

  -- Transitivity of algorithmic equality of terms.
  transConv↑Term : ∀ {t u v A B Γ Δ l}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B ^ [ ! , l ]
                → Γ ⊢ t [conv↑] u ∷ A ^ l
                → Δ ⊢ u [conv↑] v ∷ B ^ l
                → Γ ⊢ t [conv↑] v ∷ A ^ l
  transConv↑Term Γ≡Δ A≡B ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
                 ([↑]ₜ B₂ t″ u″ D₁ d₁ d″ whnfB₁ whnft″ whnfu″ t<>u₁) =
    let B₁≡B₂ = trans (sym (subset* D))
                      (trans A≡B
                             (subset* (stabilityRed* (symConEq Γ≡Δ) D₁)))
        d₁″ = conv* (stabilityRed*Term (symConEq Γ≡Δ) d″) (sym B₁≡B₂)
        d₁′  = stabilityRed*Term Γ≡Δ (conv* d′ B₁≡B₂)
    in  [↑]ₜ B₁ t′ u″ D d d₁″ whnfB whnft′ whnfu″
             (transConv↓Term Γ≡Δ B₁≡B₂ PE.refl t<>u
                             (PE.subst (λ x → _ ⊢ x [conv↓] u″ ∷ B₂ ^ _)
                                       (whrDet*Term (d₁ , whnft″)
                                                (d₁′ , whnfu′))
                                       t<>u₁))

  -- Transitivity of algorithmic equality of terms in WHNF.
  transConv↓Term : ∀ {t u v A B Γ Δ l l'}
                → ⊢ Γ ≡ Δ
                → Γ ⊢ A ≡ B ^ [ ! , l ]
                → l PE.≡ l'
                → Γ ⊢ t [conv↓] u ∷ A ^ l
                → Δ ⊢ u [conv↓] v ∷ B ^ l'
                → Γ ⊢ t [conv↓] v ∷ A ^ l

  transConv↓Term {Δ = Δ} Γ≡Δ A≡B el (ne x) (ne x₁) = ne (proj₁ (trans~↓! PE.refl Γ≡Δ x (PE.subst (λ lx → Δ ⊢ _ ~ _ ↓! Univ _ _ ^ lx) (PE.sym el) x₁)))
  transConv↓Term Γ≡Δ A≡B el (ℕ-ins x) (ℕ-ins x₁) =
    ℕ-ins (proj₁ (trans~↓! PE.refl Γ≡Δ x x₁))
  transConv↓Term {Δ = Δ} Γ≡Δ A≡B el (ne-ins t u x x₁) (ne-ins {k} {l} {M} {N} t′ u′ x₂ x₃) =
    ne-ins t (conv (stabilityTerm (symConEq Γ≡Δ) (PE.subst (λ lx → Δ ⊢ l ∷ N ^ [ ! , lx ]) (PE.sym el) u′))
                   (sym A≡B)) x
           (proj₁ (trans~↓! PE.refl Γ≡Δ x₁ (PE.subst (λ lx → Δ ⊢ k ~ l ↓! M ^ lx ) (PE.sym el) x₃)))
  transConv↓Term Γ≡Δ A≡B el (zero-refl x) (zero-refl x₁) =
    zero-refl x
  transConv↓Term Γ≡Δ A≡B el (suc-cong x) (suc-cong x₁) =
    suc-cong (transConv↑Term Γ≡Δ A≡B x x₁)
  transConv↓Term {Δ = Δ} Γ≡Δ A≡B el (η-eq {rF = rF₁} l< l<' x x₁ x₂ y y₁ x₃)
                                    (η-eq {u} {v} {F} {G} {rF} {lF} {lG} {l} l<'' l<''' x₄ x₅ x₆ y₂ y₃ x₇) =
    let F₁≡F , rF₁≡rF , lF₁≡lF , lG₁≡lG , G₁≡G = injectivity (PE.subst (λ lx → _ ⊢ _ ≡ Π _ ^ _ ° _ ▹ _ ° _ ° lx ^ _) (ιinj (PE.sym el)) A≡B )
    in  η-eq l< l<' x x₁ (conv (stabilityTerm (symConEq Γ≡Δ)
                                           (PE.subst (λ lx → Δ ⊢ v ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , lx ]) (PE.sym el) x₆))
                            (sym A≡B))
             y y₃ (transConv↑Term (Γ≡Δ ∙ F₁≡F) G₁≡G x₃
                                  (PE.subst (λ lx → Δ ∙ F ^ [ rF₁ , _ ] ⊢  _ ∘ _ ^ _ [conv↑] wk1 v ∘ var 0 ^ _ ∷ G ^ ι lx)
                                            (PE.sym lG₁≡lG)
                                  (PE.subst (λ lx → Δ ∙ F ^ [ rF₁ , _ ] ⊢  wk1 u ∘ var 0 ^ lx [conv↑] wk1 v ∘ var 0 ^ lx ∷ G ^ ι lG)
                                            (PE.sym (ιinj el))
                                  (PE.subst (λ lx → Δ ∙ F ^ [ rF₁ , lx ] ⊢  wk1 u ∘ var 0 ^ l [conv↑] wk1 v ∘ var 0 ^ l ∷ G ^ ι lG)
                                            (PE.sym (PE.cong ι lF₁≡lF))
                                  (PE.subst (λ rx → Δ ∙ F ^ [ rx , ι lF ] ⊢ _ [conv↑] _ ∷ _ ^ _) (PE.sym rF₁≡rF) x₇)))))
  transConv↓Term Γ≡Δ A≡B el (ℕ-refl x) (ℕ-refl x₁) = ℕ-refl x
  transConv↓Term Γ≡Δ A≡B el (Empty-refl PE.refl x) (Empty-refl PE.refl x₁) = Empty-refl PE.refl x
  transConv↓Term Γ≡Δ A≡B el (U-refl e x) (U-refl e₁ x₁) = U-refl (PE.trans e e₁) x
  transConv↓Term Γ≡Δ A≡B el (Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' x₅ x₆ x₇) (Π-cong PE.refl PE.refl PE.refl PE.refl x₁₁ x₁₂ x₁₃ x₁₄ x₁₅) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        rF≡rF₁ , _ = Uinjectivity A≡B
    in Π-cong PE.refl PE.refl PE.refl PE.refl l< l<' x₅ (transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ )) x₆ x₁₄)
              (transConv↑Term (Γ≡Δ ∙ univ (soundnessConv↑Term x₆))
                              (PE.subst (λ rx → _ ⊢ _ ≡ Univ rx _ ^ _) rF≡rF₁ (refl (Ugenⱼ (⊢Γ ∙ x₅)) ) ) x₇ x₁₅)
  transConv↓Term Γ≡Δ A≡B el (∃-cong PE.refl x₅ x₆ x₇) (∃-cong PE.refl x₁₃ x₁₄ x₁₅) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
        rF≡rF₁ , _ = Uinjectivity A≡B
    in ∃-cong PE.refl x₅ (transConv↑Term Γ≡Δ (refl (Ugenⱼ ⊢Γ )) x₆ (PE.subst (λ l → _ ⊢ _ [conv↑] _ ∷ SProp l ^ next l) (next-inj (PE.sym el)) x₁₄ ))
                 (transConv↑Term (Γ≡Δ ∙ univ (soundnessConv↑Term x₆)) (refl (Ugenⱼ (⊢Γ ∙ x₅))) x₇
                                 (PE.subst (λ l → _ ∙ _ ^ [ % , ι l ]  ⊢ _ [conv↑] _ ∷ SProp l ^ next l) (next-inj (PE.sym el)) x₁₅ ))

  transConv↓Term Γ≡Δ A≡B PE.refl (ℕ-refl x) (η-eq x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) = ⊥-elim (WF.U≢Π! A≡B)
  transConv↓Term Γ≡Δ A≡B el (Empty-refl {l} PE.refl x) (η-eq x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) =
    let X = PE.subst (λ lx → _ ⊢ SProp l ≡  Π _ ^ _ ° _ ▹ _ ° _ ° _ ^ [ _ , lx ]) el A≡B
    in ⊥-elim (WF.U≢Π! X)
  transConv↓Term Γ≡Δ A≡B el (Π-cong {rΠ = rΠ} {lΠ = lΠ} x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₀) (η-eq x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ x₁₅) =
    let X = PE.subst (λ lx → _ ⊢ Univ rΠ lΠ ≡ Π _ ^ _ ° _ ▹ _ ° _ ° _ ^ [ _ , lx ]) el A≡B
    in ⊥-elim (WF.U≢Π! X)
  transConv↓Term Γ≡Δ A≡B el (∃-cong {l = l} x₅ x₆ x₇ x₀) (η-eq x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ x₁₅) =
    let X = PE.subst (λ lx → _ ⊢ SProp l ≡ Π _ ^ _ ° _ ▹ _ ° _ ° _ ^ [ _ , lx ]) el A≡B
    in ⊥-elim (WF.U≢Π! X)

  transConv↓Term Γ≡Δ A≡B el (ne x) (ℕ-ins x₁) = ⊥-elim (WF.U≢ℕ! A≡B)
  transConv↓Term Γ≡Δ A≡B PE.refl (ne x) (ne-ins x₁ x₂ x₃ x₄) = ⊥-elim (WF.U≢ne! x₃ A≡B)
  transConv↓Term Γ≡Δ A≡B PE.refl (ne x) (η-eq x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) = ⊥-elim (WF.U≢Π! A≡B)
  --transConv↓Term Γ≡Δ A≡B el (zero-refl x) (zero-refl x₁) = {!!}
  transConv↓Term Γ≡Δ A≡B el (ℕ-ins x) (ne-ins t u x₂ x₃) = ⊥-elim (WF.ℕ≢ne! x₂ A≡B)
  transConv↓Term Γ≡Δ A≡B PE.refl (ℕ-ins x) (η-eq _ _ x₂ x₃ x₄ y y₁ x₅) = ⊥-elim (WF.ℕ≢Π! A≡B)
  transConv↓Term Γ≡Δ A≡B el (ℕ-ins x) (ne x₁) = ⊥-elim (WF.U≢ℕ! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B PE.refl (ne-ins x x₁ x₂ x₃) (ne x₄) = ⊥-elim (WF.U≢ne! x₂ (sym A≡B))
  transConv↓Term  Γ≡Δ A≡B PE.refl (ne-ins t u x x₁) (ℕ-ins x₂) =
    ⊥-elim (WF.ℕ≢ne! x (sym A≡B))
  transConv↓Term Γ≡Δ A≡B PE.refl (ne-ins x x₁ x₂ x₃) (η-eq x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁) = ⊥-elim (WF.Π≢ne x₂ (sym A≡B))
  transConv↓Term Γ≡Δ A≡B PE.refl (zero-refl x) (η-eq x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) =  ⊥-elim (WF.ℕ≢Π! A≡B)
  transConv↓Term Γ≡Δ A≡B PE.refl (suc-cong x) (η-eq x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) =  ⊥-elim (WF.ℕ≢Π! A≡B)
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (ne x₈) = ⊥-elim (WF.U≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (ℕ-refl x₈) = ⊥-elim (WF.U≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (Empty-refl x₀ x₈) = ⊥-elim (WF.U≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (Π-cong x₀ x₈ x₉ x₁₀ x₁₁ x₁₂ x₁₃ x₁₄ x₁₅) = ⊥-elim (WF.U≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (∃-cong x₀ x₁₃ x₁₄ x₁₅) = ⊥-elim (WF.U≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B PE.refl (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (ℕ-ins x₈) = ⊥-elim (WF.ℕ≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B el (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (ne-ins x₈ x₉ x₁₀ x₁₁) = ⊥-elim (WF.Π≢ne x₁₀ A≡B)
  transConv↓Term Γ≡Δ A≡B PE.refl (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (zero-refl x₈) = ⊥-elim (WF.ℕ≢Π! (sym A≡B))
  transConv↓Term Γ≡Δ A≡B PE.refl (η-eq x x₁ x₂ x₃ x₄ x₅ x₆ x₇) (suc-cong x₈) = ⊥-elim (WF.ℕ≢Π! (sym A≡B))

-- Transitivity of algorithmic equality of types of the same context.
transConv : ∀ {A B C r Γ}
          → Γ ⊢ A [conv↑] B ^ r
          → Γ ⊢ B [conv↑] C ^ r
          → Γ ⊢ A [conv↑] C ^ r
transConv A<>B B<>C =
  let Γ≡Γ = reflConEq (wfEq (soundnessConv↑ A<>B))
  in  transConv↑ Γ≡Γ A<>B B<>C

-- Transitivity of algorithmic equality of terms of the same context.
transConvTerm : ∀ {t u v A Γ l}
              → Γ ⊢ t [conv↑] u ∷ A ^ l
              → Γ ⊢ u [conv↑] v ∷ A ^ l
              → Γ ⊢ t [conv↑] v ∷ A ^ l
transConvTerm t<>u u<>v =
  let t≡u = soundnessConv↑Term t<>u
      Γ≡Γ = reflConEq (wfEqTerm t≡u)
      ⊢A , _ , _ = syntacticEqTerm t≡u
  in  transConv↑Term Γ≡Γ (refl ⊢A) t<>u u<>v

trans~↑!Term : ∀ {t u v A Γ l}
              → Γ ⊢ t ~ u ↑% A ^ l
              → Γ ⊢ u ~ v ↑% A ^ l
              → Γ ⊢ t ~ v ↑% A ^ l
trans~↑!Term t<>u u<>v =
  let _ , _ , t≡u = soundness~↑% t<>u
      Γ≡Γ = reflConEq (wfEqTerm t≡u)
  in  trans~↑% Γ≡Γ t<>u u<>v

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
------------------------------------------------------------------------
-- Mixfix operator grammars, and parsing of mixfix operators
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module Mixfix where

-- There are two separate developments here. One is very close to the
-- paper "Parsing Mixfix Operators" (by me and Ulf Norell), and uses
-- directed acyclic precedence graphs and grammars which are neither
-- left nor right recursive. The other uses precedence graphs which
-- may be cyclic and grammars which can be both left and right
-- recursive (following an alternative definition of grammars given in
-- the paper). The two grammar schemes are equivalent when restricted
-- to acyclic precedence graphs.

-- The grammars which use DAGs have the advantage that they can be
-- implemented using a larger variety of parser combinator libraries.
-- This could lead to a more efficient implementation. On the other
-- hand the definition of the other grammars does not attempt to avoid
-- left and right recursion, which means that it is arguably a bit
-- easier to understand and work with (compare the proofs in
-- Mixfix.Acyclic.Show and Mixfix.Cyclic.Show, for instance).

------------------------------------------------------------------------
-- Shared code

-- Fixity and associativity.

import Mixfix.Fixity

-- Operators.

import Mixfix.Operator

-- Precedence-correct expressions, parametrised on abstract precedence
-- graphs.

import Mixfix.Expr

------------------------------------------------------------------------
-- Acyclic graphs

-- A custom-made parser combinator library (with a formal semantics).

import Mixfix.Acyclic.Lib

-- Acyclic precedence graphs.

import Mixfix.Acyclic.PrecedenceGraph

-- Mixfix operator grammars. The resulting expressions are
-- precedence-correct by construction.

import Mixfix.Acyclic.Grammar

-- A minor lemma.

import Mixfix.Acyclic.Lemma

-- Linearisation of operators, and a proof showing that all the
-- generated strings are syntactically correct (although perhaps
-- ambiguous). If the result is combined with the one in
-- Mixfix.Cyclic.Uniqueness we get that every expression has a unique
-- representation. (Two different expressions may have the same
-- representation, though.)

import Mixfix.Acyclic.Show

-- An example.

import Mixfix.Acyclic.Example

------------------------------------------------------------------------
-- Cyclic graphs

-- A custom-made parser combinator library (with a formal semantics).

import Mixfix.Cyclic.Lib

-- Cyclic precedence graphs. (These graphs are not used below, because
-- Mixfix.Cyclic.Grammar can handle arbitrary precedence graphs.)

import Mixfix.Cyclic.PrecedenceGraph

-- Mixfix operator grammars. The resulting expressions are
-- precedence-correct by construction.

import Mixfix.Cyclic.Grammar

-- A constructive proof (i.e. a "show" function) showing that every
-- expression has at least one representation.

import Mixfix.Cyclic.Show

-- A proof showing that every expression has at most one
-- representation.

import Mixfix.Cyclic.Uniqueness

-- An example.

import Mixfix.Cyclic.Example

------------------------------------------------------------------------
-- Equivalence

-- For acyclic precedence graphs the two grammar definitions above are
-- equivalent.

-- Note that this proof only establishes language equivalence, not
-- parser equivalence (see TotalParserCombinators.Semantics). In other
-- words, the two definitions are seen as equivalent if they yield the
-- same language, even though the number of parse trees corresponding
-- to a certain (input string, result)-pair may vary between the two
-- definitions. For instance, when parsing the string s using one
-- grammar the result could contain the expression e once, whereas
-- parsing with the other grammar could yield a result containing two
-- copies of e. This is not a big problem: syntactic equality of
-- expressions is decidable, so extra occurrences of e can be filtered
-- out. The same considerations apply to the equivalence proofs in
-- Mixfix.Acyclic.Lib and Mixfix.Cyclic.Lib. Note that I believe that
-- it is easy (but tedious) to strengthen all these proofs so that
-- parser equivalence is established, but I have not tried to do this.

import Mixfix.Equivalence

ext: agda

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
import      Lvl
open import Functional
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Logic.Propositional.Theorems{Lvl.𝟎}
open import Relator.Equals{Lvl.𝟎}{Lvl.𝟎} renaming (_≡_ to _≡ₑ_)
open import Type{Lvl.𝟎}

-- Based on https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html (2017-10-13)
module Sets.IZF (S : Set(Lvl.𝟎)) (_∈_ : S → S → Stmt) where

module Relations where
  _∉_ : S → S → Stmt
  _∉_ x a = ¬(x ∈ a)

  _⊆_ : S → S → Stmt
  _⊆_ a b = (∀{x} → (x ∈ a) → (x ∈ b))

  _⊇_ : S → S → Stmt
  _⊇_ a b = (∀{x} → (x ∈ a) ← (x ∈ b))

  _≡_ : S → S → Stmt
  _≡_ a b = (∀{x} → (x ∈ a) ↔ (x ∈ b))

  -- The statement that the set s is empty
  Empty : S → Stmt
  Empty(s) = (∀{x} → (x ∉ s))

  -- The statement that the set s is inhabited/non-empty
  NonEmpty : S → Stmt
  NonEmpty(s) = ∃(x ↦ (x ∈ s))

  -- The statement that the set s is a singleton set containing only the single element x₁
  Singleton : S → S → Stmt
  Singleton(s) (x₁) = (∀{x} → (x ∈ s) ↔ (x ≡ x₁))

  -- The statement that the set s is a pair set containing only the two elements x₁, x₂
  Pair : S → S → S → Stmt
  Pair(s) (x₁)(x₂) = (∀{x} → (x ∈ s) ↔ (x ≡ x₁)∨(x ≡ x₂))

  -- The statement that the set sᵤ is the union of the sets s₁, s₂
  Union : S → S → S → Stmt
  Union(sᵤ) (s₁)(s₂) = (∀{x} → (x ∈ sᵤ) ↔ (x ∈ s₁)∨(x ∈ s₂))

  -- The statement that the set sᵤ is the intersection of the sets s₁, s₂
  Intersection : S → S → S → Stmt
  Intersection(sᵢ) (s₁)(s₂) = (∀{x} → (x ∈ sᵢ) ↔ (x ∈ s₁)∧(x ∈ s₂))

  -- The statement that the set sₚ is the power set of s
  Power : S → S → Stmt
  Power(sₚ) (s) = (∀{x} → (x ∈ sₚ) ↔ (x ⊆ s))

  -- The statement that the set sᵤ is the union of all sets in ss
  UnionAll : S → S → Stmt
  UnionAll(sᵤ) (ss) = (∀{x s} → (x ∈ sᵤ) ↔ (x ∈ s)∧(s ∈ ss))

  -- The statement that the set sᵤ is the intersection of all sets in ss
  IntersectionAll : S → S → Stmt
  IntersectionAll(sᵢ) (ss) = (∀{x} → (x ∈ sᵢ) ↔ (∀{s} → (s ∈ ss) → (x ∈ s)))

  -- The statement that the set sₛ is the subset of s where every element satisfies φ
  FilteredSubset : S → (s : S) → ((x : S) → ⦃ _ : (x ∈ s) ⦄ → Stmt) → Stmt
  FilteredSubset(sₛ) (s)(φ) = (∀{x} → (x ∈ sₛ) ↔ ∃{x ∈ s}(proof ↦ φ(x) ⦃ proof ⦄))

module RelationsTheorems where
  open Relations

  [≡]-reflexivity : ∀{s} → (s ≡ s)
  [≡]-reflexivity = [↔]-reflexivity

  [≡]-transitivity : ∀{s₁ s₂ s₃} → (s₁ ≡ s₂) → (s₂ ≡ s₃) → (s₁ ≡ s₃)
  [≡]-transitivity(s12)(s23){x} = [↔]-transitivity(s12{x})(s23{x})

  [≡]-symmetry : ∀{s₁ s₂} → (s₁ ≡ s₂) → (s₂ ≡ s₁)
  [≡]-symmetry(s12){x} = [↔]-symmetry(s12{x})

  -- TODO: Are these even provable with my def. of set equality?
  -- [≡]-substitute : ∀{φ : S → Stmt}{s₁ s₂} → (s₁ ≡ s₂) → ∀{x} → φ(s₁) ↔ φ(s₂)
  -- [≡]-substituteₗ : ∀{φ : Stmt → Stmt}{s₁ s₂} → (s₁ ≡ s₂) → ∀{x} → φ(s₁ ∈ x) ↔ φ(s₂ ∈ x)

  [⊆]-reflexivity : ∀{s} → (s ⊆ s)
  [⊆]-reflexivity = [→]-reflexivity

  [⊆]-transitivity : ∀{s₁ s₂ s₃} → (s₁ ⊆ s₂) → (s₂ ⊆ s₃) → (s₁ ⊆ s₃)
  [⊆]-transitivity(s12)(s23){x} = [→]-transitivity(s12{x})(s23{x})

  [⊆]-antisymmetry : ∀{s₁ s₂} → (s₁ ⊇ s₂) → (s₁ ⊆ s₂) → (s₁ ≡ s₂)
  [⊆]-antisymmetry(s21)(s12){x} = [↔]-intro (s21{x}) (s12{x})

module Axioms1 where
  open Relations

  -- Axiom of extensionality
  -- Sets are equal when they have the same elements.
  record SetEquality : Set(Lvl.𝟎) where
    field equality : ∀{s₁ s₂} → (s₁ ≡ s₂) → (s₁ ≡ₑ s₂)
  open SetEquality ⦃ ... ⦄ public

  -- Axiom of the empty set
  -- A set which is empty exists.
  record EmptySetExistence : Set(Lvl.𝟎) where
    field empty : ∃(s ↦ Empty(s))
  open EmptySetExistence ⦃ ... ⦄ public

  -- Axiom of pairing
  -- A set with two elements exists.
  record PairExistence : Set(Lvl.𝟎) where
    field pair : ∀{x₁ x₂} → ∃(s ↦ Pair(s)(x₁)(x₂))
  open PairExistence ⦃ ... ⦄ public

  -- Axiom of union
  -- A set which contains all the elements of a group of sets exists.
  record UnionExistence : Set(Lvl.𝟎) where
    field union : ∀{ss} → ∃(sᵤ ↦ UnionAll(sᵤ)(ss))
  open UnionExistence ⦃ ... ⦄ public

  -- Axiom of the power set
  -- A set which contains all the subsets of a set exists.
  record PowerSetExistence : Set(Lvl.𝟎) where
    field power : ∀{s} → ∃(sₚ ↦ Power(sₚ)(s))
  open PowerSetExistence ⦃ ... ⦄ public

  -- Axiom schema of restricted comprehension | Axiom schema of specification | Axiom schema of separation
  -- A set which is the subset of a set where all elements satisfies a predicate exists.
  record RestrictedComprehensionExistence : Set(Lvl.𝐒(Lvl.𝟎)) where
    field comprehension : ∀{s}{φ : (x : S) → ⦃ _ : (x ∈ s) ⦄ → Stmt} → ∃(sₛ ↦ FilteredSubset(sₛ)(s)(φ))
  open RestrictedComprehensionExistence ⦃ ... ⦄ public

  -- Axiom schema of collection
  -- A set which collects all RHS in a binary relation (and possibly more elements) exists.
  -- The image of a function has a superset?
  -- Detailed explanation:
  --   Given a set a and a formula φ:
  --   If ∀(x∊a)∃y. φ(x)(y)
  --     The binary relation φ describes a total multivalued function from the set a to b:
  --       φ: a→b
  --     Note: φ is not neccessarily a set.
  --   Then ∃b∀(x∊a)∃(y∊b). φ(x)(y)
  --     There exists a set b such that every argument of the function has one of its function values in it.
  record CollectionAxiom : Set(Lvl.𝐒(Lvl.𝟎)) where
    field collection : ∀{φ : S → S → Stmt} → ∀{a} → (∀{x} → (x ∈ a) → ∃(y ↦ φ(x)(y))) → ∃(b ↦ ∀{x} → (x ∈ a) → ∃(y ↦ ((y ∈ b) ∧ φ(x)(y))))
  open CollectionAxiom ⦃ ... ⦄ public

  -- Induction proof on sets.
  -- This can be used to prove stuff about all sets.
  -- This can be interpreted as:
  --   A proof of a predicate satisfying every element of an arbitrary set is a proof of this predicate satisfying every set.
  record InductionProof : Set(Lvl.𝐒(Lvl.𝟎)) where
    field induction : ∀{φ : S → Stmt} → (∀{s} → (∀{x} → (x ∈ s) → φ(x)) → φ(s)) → (∀{s} → φ(s))
  open InductionProof ⦃ ... ⦄ public

module Theorems1 where
  open Axioms1
  open Relations

  module _ ⦃ _ : PairExistence ⦄ where
      -- A set with only one element exists.
    single : ∀{x₁} → ∃(s ↦ (∀{x} → (x ∈ s) ↔ (x ≡ x₁)))
    single{x} with pair{x}{x}
    ... | [∃]-intro (z) ⦃ f ⦄ = ([∃]-intro (z) ⦃ \{w} → [↔]-transitivity (f{w}) [∨]-redundancy ⦄)

  module _ ⦃ _ : EmptySetExistence ⦄ where
    [∅]-uniqueness : ∀{x y} → Empty(x) → Empty(y) → (x ≡ y)
    [∅]-uniqueness (empty-x)(empty-y) =
      ([↔]-intro
        ([⊥]-elim ∘ empty-y)
        ([⊥]-elim ∘ empty-x)
      )

  {-
    Singleton-elem-uniqueness : ∀{x y₁ y₂} → (y₁ ∈ Singleton(x)) → (y₂ ∈ Singleton(x)) → (y₁ ≡ y₂)
    Singleton-elem-uniqueness (y₁-proof)(y₂-proof) =
      ([↔]-intro
        (y₁-proof)
        (y₂-proof)
      )
  -}

module Operations where
  open Axioms1
  open Relations
  open Theorems1

  module _ ⦃ _ : EmptySetExistence ⦄ where
    -- Definition of the empty set: ∅={}.
    -- This can be used to construct a set with no elements.
    ∅ : S
    ∅ = [∃]-witness(empty)

  module _ ⦃ _ : PairExistence ⦄ where
    -- Definition of a singleton set: {x} for some element x.
    -- This can be used to construct a set with a single element.
    • : S → S
    •(x) = [∃]-witness(single{x})

    -- Definition of a pair set: {x,y} for some elements x and y.
    -- This can be used to construct a set with a countable number of elements: x⟒y⟒z.
    _⟒_ : S → S → S
    _⟒_ (x)(y) = [∃]-witness(pair{x}{y})

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    -- Definition of the union of two sets: s₁∪s₂ for two sets s₁ and s₂.
    -- This can be used to construct a set that contains all elements from either of the two sets.
    _∪_ : S → S → S
    _∪_ s₁ s₂ = [∃]-witness(union{s₁ ⟒ s₂})

  module _ ⦃ _ : UnionExistence ⦄ where
    -- Definition of the union of a set of sets: ⋃(ss) for a set of sets ss.
    -- This can be used to construct a set that contains all elements from the sets.
    reduce-[∪] : S → S
    reduce-[∪] ss = [∃]-witness(union{ss})

  module _ ⦃ _ : PowerSetExistence ⦄ where
    -- Definition of the power set of a set: ℘(s) for some set s.
    -- This can be used to construct a set that contains all subsets of a set.
    ℘ : S → S
    ℘(s) = [∃]-witness(power{s})

  module _ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    -- Definition of the usual "set builder notation": {(x∊s). φ(x)} for some set s.
    -- This can be used to construct a set that is the subset which satisfies a certain predicate for every element.
    filter : S → (S → Stmt) → S
    filter(s)(φ) = [∃]-witness(comprehension{s}{x ↦ \ ⦃ _ ⦄ → φ(x)})

    -- Definition of a "set builder notation": {(x∊s). φ(x)} for some set s where the predicate φ gets a proof of (x∈s).
    -- This can be used to construct a set that is the subset which satisfies a certain predicate for every element.
    filter-dep : (s : S) → ((x : S) → ⦃ _ : (x ∈ s) ⦄ → Stmt) → S
    filter-dep(s)(φ) = [∃]-witness(comprehension{s}{φ})

    -- Definition of the intersection of two sets: s₁∩s₂ for two sets s₁ and s₂.
    -- This can be used to construct a set that contains all elements that only are in both sets.
    _∩_ : S → S → S
    _∩_ (s₁)(s₂) = filter(s₁)(x ↦ (x ∈ s₂))

    -- Definition of the subtraction of two sets: s₁∖s₂ for two sets s₁ and s₂.
    -- This can be used to construct a set that contains all elements from s₁ which is not in s₂.
    _∖_ : S → S → S
    _∖_ (s₁)(s₂) = filter(s₁)(_∉ s₂)

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    -- Definition of the intersection of a set of sets: ⋂(ss) for a set of sets ss.
    -- This can be used to construct a set that only contains the elements which all the sets have in common.
    reduce-[∩] : S → S
    reduce-[∩] ss = filter(reduce-[∪] (ss))(x ↦ ∀{s} → (s ∈ ss) → (x ∈ s))

module OperationsTheorems where
  open Axioms1
  open Operations
  open Relations
  open Theorems1
  open Relations
  open RelationsTheorems

  -- -- -- -- -- -- -- -- -- -- -- -- -- --
  -- Containment

  module _ ⦃ _ : EmptySetExistence ⦄ where
    [∅]-containment : Empty(∅)
    [∅]-containment = [∃]-proof(empty)

  module _ ⦃ _ : PairExistence ⦄ where
    [•]-containment : ∀{x₁} → (x₁ ∈ •(x₁))
    [•]-containment{x₁} = [↔]-elimₗ([∃]-proof(single{x₁})) ([≡]-reflexivity)

    [⟒]-containment : ∀{x₁ x₂}{x} → (x ∈ (x₁ ⟒ x₂)) ↔ (x ≡ x₁)∨(x ≡ x₂)
    [⟒]-containment{x₁}{x₂} = [∃]-proof(pair{x₁}{x₂})

    [⟒]-containmentₗ : ∀{x₁ x₂} → (x₁ ∈ (x₁ ⟒ x₂))
    [⟒]-containmentₗ{x₁}{x₂} = [↔]-elimₗ([∃]-proof(pair{x₁}{x₂})) ([∨]-introₗ([≡]-reflexivity))

    [⟒]-containmentᵣ : ∀{x₁ x₂} → (x₂ ∈ (x₁ ⟒ x₂))
    [⟒]-containmentᵣ{x₁}{x₂} = [↔]-elimₗ([∃]-proof(pair{x₁}{x₂})) ([∨]-introᵣ([≡]-reflexivity))

  module _ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    filter-dep-containment : ∀{s}{φ}{x} → (x ∈ filter-dep(s)(φ)) ↔ (∃{x ∈ s}(proof ↦ φ(x) ⦃ proof ⦄))
    filter-dep-containment{s} = [∃]-proof(comprehension)

    test : ∀{s}{φ}{x} → (x ∈ filter-dep(s)(φ)) → (∃{x ∈ s}(proof ↦ φ(x) ⦃ proof ⦄))
    test{s} = [↔]-elimᵣ (filter-dep-containment)

    test2 : ∀{s}{φ}{x} → (x ∈ filter-dep(s)(φ)) → (x ∈ s)
    test2(a) = [∃]-witness (test(a))

    -- TODO: ?
    -- test3 : ∀{s}{φ}{x} → (x ∈ filter-dep(s)(φ)) → ⦃ _ : (x ∈ s) ⦄ → φ(x)
    -- test3(a) ⦃ _ ⦄ = [∃]-proof (test(a))

    postulate filter-containment : ∀{s}{φ}{x} → (x ∈ filter(s)(φ)) ↔ ((x ∈ s) ∧ φ(x))
    -- filter-containment{s} = [∃]-proof(comprehension)

    [∩]-containment : ∀{s₁ s₂}{x} → (x ∈ (s₁ ∩ s₂)) ↔ (x ∈ s₁)∧(x ∈ s₂)
    [∩]-containment = filter-containment

  module _ ⦃ _ : UnionExistence ⦄ where
    postulate reduce-[∪]-containment : ∀{ss}{x} → (x ∈ reduce-[∪] (ss)) ↔ ∃(s ↦ (s ∈ ss)∧(x ∈ s))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    [∪]-containment : ∀{s₁ s₂}{x} → (x ∈ (s₁ ∪ s₂)) ↔ (x ∈ s₁)∨(x ∈ s₂)
    [∪]-containment = [↔]-intro [∪]-containmentₗ [∪]-containmentᵣ where
      postulate [∪]-containmentₗ : ∀{s₁ s₂}{x} → (x ∈ (s₁ ∪ s₂)) ← (x ∈ s₁)∨(x ∈ s₂)
      postulate [∪]-containmentᵣ : ∀{s₁ s₂}{x} → (x ∈ (s₁ ∪ s₂)) → (x ∈ s₁)∨(x ∈ s₂)

  module _ ⦃ _ : PowerSetExistence ⦄ where
    [℘]-containment : ∀{s sₛ} → (sₛ ⊆ s) ↔ (sₛ ∈ ℘(s))
    [℘]-containment{s} = [↔]-symmetry([∃]-proof(power{s}))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    postulate reduce-[∩]-containment : ∀{ss}{x} → (x ∈ reduce-[∪] (ss)) ↔ (∀{s} → (s ∈ ss) → (x ∈ s))

  -- -- -- -- -- -- -- -- -- -- -- -- -- --
  -- Other

  module _ ⦃ _ : EmptySetExistence ⦄ where
    [∅]-in-subset : ∀{s} → (∅ ⊆ s)
    [∅]-in-subset = [⊥]-elim ∘ [∅]-containment

  module _ ⦃ _ : EmptySetExistence ⦄ ⦃ _ : PowerSetExistence ⦄ where
    [℘][∅]-containment : ∀{s} → (∅ ∈ ℘(s))
    [℘][∅]-containment = [↔]-elimᵣ([℘]-containment)([∅]-in-subset)

  module _ ⦃ _ : PowerSetExistence ⦄ where
    [℘]-set-containment : ∀{s} → (s ∈ ℘(s))
    [℘]-set-containment = [↔]-elimᵣ([℘]-containment)([⊆]-reflexivity)

  module _ ⦃ _ : InductionProof ⦄ where
    self-noncontainment : ∀{s} → (s ∉ s) -- ¬ ∃(s ↦ s ∈ s)
    self-noncontainment = induction{x ↦ x ∉ x} (proof) where
      proof : ∀{s} → (∀{x} → (x ∈ s) → (x ∉ x)) → (s ∉ s)
      proof{s} (f)(s∈s) = f{s}(s∈s)(s∈s)
      -- ∀{s} → (∀{x} → (x ∈ s) → (x ∉ x)) → (s ∉ s)
      -- ∀{s} → (∀{x} → (x ∈ s) → (x ∈ x) → ⊥) → (s ∈ s) → ⊥

    [𝐔]-nonexistence : ¬ ∃(𝐔 ↦ ∀{x} → (x ∈ 𝐔))
    [𝐔]-nonexistence ([∃]-intro(𝐔) ⦃ proof ⦄) = self-noncontainment {𝐔} (proof{𝐔})

  -- -- -- -- -- -- -- -- -- -- -- -- -- --
  -- Subset

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    postulate reduce-[∪]-subset : ∀{ss}{s} → (s ∈ ss) → (s ⊆ reduce-[∪] (ss))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    [∪]-subsetₗ : ∀{s₁ s₂} → (s₁ ⊆ (s₁ ∪ s₂))
    [∪]-subsetₗ = ([↔]-elimₗ([∪]-containment)) ∘ [∨]-introₗ

    [∪]-subsetᵣ : ∀{s₁ s₂} → (s₂ ⊆ (s₁ ∪ s₂))
    [∪]-subsetᵣ = ([↔]-elimₗ([∪]-containment)) ∘ [∨]-introᵣ

    postulate [∪]-subset-eq : ∀{s₁ s₂ s₃} → ((s₁ ∪ s₂) ⊆ s₃) ↔ ((s₁ ⊆ s₃)∧(s₂ ⊆ s₃))

  module _ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    [∩]-subsetₗ : ∀{s₁ s₂} → ((s₁ ∩ s₂) ⊆ s₁)
    [∩]-subsetₗ = [∧]-elimₗ ∘ ([↔]-elimᵣ([∩]-containment))

    [∩]-subsetᵣ : ∀{s₁ s₂} → ((s₁ ∩ s₂) ⊆ s₂)
    [∩]-subsetᵣ = [∧]-elimᵣ ∘ ([↔]-elimᵣ([∩]-containment))

    filter-dep-subset : ∀{s}{φ} → (filter-dep(s)(φ) ⊆ s)
    filter-dep-subset{s}{φ} {x}(x∈s) = [∃]-witness([↔]-elimᵣ(filter-dep-containment{s}{φ})(x∈s))

    filter-subset : ∀{s}{φ} → (filter(s)(φ) ⊆ s)
    filter-subset{s}{φ} {x}(x∈s) = [∧]-elimₗ([↔]-elimᵣ(filter-containment{s}{φ})(x∈s))

  module _ ⦃ _ : PowerSetExistence ⦄ where
    [℘]-subset : ∀{s₁ s₂} → (s₁ ⊆ s₂) ↔ (℘(s₁) ⊆ ℘(s₂))
    [℘]-subset = [↔]-intro l r where
      l : ∀{s₁ s₂} → (s₁ ⊆ s₂) ← (℘(s₁) ⊆ ℘(s₂))
      l {s₁}{s₂} (p1p2) = ([↔]-elimₗ [℘]-containment) (p1p2{s₁} ([℘]-set-containment))

      r : ∀{s₁ s₂} → (s₁ ⊆ s₂) → (℘(s₁) ⊆ ℘(s₂))
      r {s₁}{s₂} (s12) {a} (aps1) = ([↔]-elimᵣ [℘]-containment) ([⊆]-transitivity (([↔]-elimₗ [℘]-containment) aps1) (s12))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    postulate reduce-[∩]-subset : ∀{ss}{s} → (s ∈ ss) → (reduce-[∩] (ss) ⊆ s)

  -- TODO: Does this hold: Empty(s) ∨ NonEmpty(s) ? Probably not

  -- -- -- -- -- -- -- -- -- -- -- -- -- --
  -- Commutativity

  -- [⟒]-commutativity : ∀{s₁ s₂} → (s₁ ⟒ s₂) ≡ (s₂ ⟒ s₁)
  -- [⟒]-commutativity{s₁}{s₂} {x} = [↔]-intro (f{s₂}{s₁}) (f{s₁}{s₂}) where
  --   f : ∀{s₁ s₂} → (x ∈ (s₁ ⟒ s₂)) → (x ∈ (s₂ ⟒ s₁))
  --   f{s₁}{s₂} = ([↔]-elimₗ([⟒]-containment{s₂}{s₁}{x})) ∘ ([∨]-symmetry) ∘ ([↔]-elimᵣ([∪]-containment{s₁}{s₂}{x}))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    [∪]-commutativity : ∀{s₁ s₂} → (s₁ ∪ s₂) ≡ (s₂ ∪ s₁)
    [∪]-commutativity{s₁}{s₂} {x} = [↔]-intro (f{s₂}{s₁}) (f{s₁}{s₂}) where
      f : ∀{s₁ s₂} → (x ∈ (s₁ ∪ s₂)) → (x ∈ (s₂ ∪ s₁))
      f{s₁}{s₂} =
        ([↔]-elimₗ([∪]-containment{s₂}{s₁}{x}))
        ∘ ([∨]-symmetry)
        ∘ ([↔]-elimᵣ([∪]-containment{s₁}{s₂}{x}))

  module _ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    [∩]-commutativity : ∀{s₁ s₂} → (s₁ ∩ s₂) ≡ (s₂ ∩ s₁)
    [∩]-commutativity{s₁}{s₂} {x} = [↔]-intro (f{s₂}{s₁}) (f{s₁}{s₂}) where
      f : ∀{s₁ s₂} → (x ∈ (s₁ ∩ s₂)) → (x ∈ (s₂ ∩ s₁))
      f{s₁}{s₂} =
        ([↔]-elimₗ([∩]-containment{s₂}{s₁}{x}))
        ∘ ([∧]-symmetry)
        ∘ ([↔]-elimᵣ([∩]-containment{s₁}{s₂}{x}))

  -- -- -- -- -- -- -- -- -- -- -- -- -- --
  -- Associativity

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    [∪]-associativity : ∀{s₁ s₂ s₃} → ((s₁ ∪ s₂) ∪ s₃) ≡ (s₁ ∪ (s₂ ∪ s₃))
    [∪]-associativity{s₁}{s₂}{s₃} {x} = [↔]-intro l r where
      l : (x ∈ ((s₁ ∪ s₂) ∪ s₃)) ← (x ∈ (s₁ ∪ (s₂ ∪ s₃)))
      l = ([↔]-elimₗ([∪]-containment{s₁ ∪ s₂}{s₃}{x}))
        ∘ ([∨]-elim ([∨]-introₗ ∘ ([↔]-elimₗ([∪]-containment{s₁}{s₂}{x}))) ([∨]-introᵣ))
        ∘ ([↔]-elimₗ [∨]-associativity)
        ∘ ([∨]-elim ([∨]-introₗ) ([∨]-introᵣ ∘ ([↔]-elimᵣ([∪]-containment{s₂}{s₃}{x}))))
        ∘ ([↔]-elimᵣ([∪]-containment{s₁}{s₂ ∪ s₃}{x}))

      r : (x ∈ ((s₁ ∪ s₂) ∪ s₃)) → (x ∈ (s₁ ∪ (s₂ ∪ s₃)))
      r = ([↔]-elimₗ([∪]-containment{s₁}{s₂ ∪ s₃}{x}))
        ∘ ([∨]-elim ([∨]-introₗ) ([∨]-introᵣ ∘ ([↔]-elimₗ([∪]-containment{s₂}{s₃}{x}))))
        ∘ ([↔]-elimᵣ [∨]-associativity)
        ∘ ([∨]-elim ([∨]-introₗ ∘ ([↔]-elimᵣ([∪]-containment{s₁}{s₂}{x}))) ([∨]-introᵣ))
        ∘ ([↔]-elimᵣ([∪]-containment{s₁ ∪ s₂}{s₃}{x}))

  module _ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    [∩]-associativity : ∀{s₁ s₂ s₃} → ((s₁ ∩ s₂) ∩ s₃) ≡ (s₁ ∩ (s₂ ∩ s₃))
    [∩]-associativity{s₁}{s₂}{s₃} {x} = [↔]-intro l r where
      l : (x ∈ ((s₁ ∩ s₂) ∩ s₃)) ← (x ∈ (s₁ ∩ (s₂ ∩ s₃)))
      l = (([↔]-elimₗ([∩]-containment{s₁ ∩ s₂}{s₃}{x}))                                                   :of: ((x ∈ ((s₁ ∩ s₂) ∩ s₃)) ← (x ∈ (s₁ ∩ s₂))∧(x ∈ s₃)))
        ∘ ((prop ↦ ([∧]-intro ([↔]-elimₗ([∩]-containment{s₁}{s₂}{x}) ([∧]-elimₗ prop)) ([∧]-elimᵣ prop))) :of: ((x ∈ (s₁ ∩ s₂))∧(x ∈ s₃) ← ((x ∈ s₁)∧(x ∈ s₂))∧(x ∈ s₃)))
        ∘ ([↔]-elimₗ [∧]-associativity)
        ∘ ((prop ↦ ([∧]-intro ([∧]-elimₗ prop) ([↔]-elimᵣ([∩]-containment{s₂}{s₃}{x}) ([∧]-elimᵣ prop)))) :of: ((x ∈ s₁)∧((x ∈ s₂)∧(x ∈ s₃)) ← (x ∈ s₁)∧(x ∈ (s₂ ∩ s₃))))
        ∘ (([↔]-elimᵣ([∩]-containment{s₁}{s₂ ∩ s₃}{x}))                                                   :of: ((x ∈ s₁)∧(x ∈ (s₂ ∩ s₃)) ← (x ∈ (s₁ ∩ (s₂ ∩ s₃)))))

      r : (x ∈ ((s₁ ∩ s₂) ∩ s₃)) → (x ∈ (s₁ ∩ (s₂ ∩ s₃)))
      r = (([↔]-elimₗ([∩]-containment{s₁}{s₂ ∩ s₃}{x}))                                                   :of: ((x ∈ s₁)∧(x ∈ (s₂ ∩ s₃)) → (x ∈ (s₁ ∩ (s₂ ∩ s₃)))))
        ∘ ((prop ↦ ([∧]-intro ([∧]-elimₗ prop) ([↔]-elimₗ([∩]-containment{s₂}{s₃}{x}) ([∧]-elimᵣ prop)))) :of: ((x ∈ s₁)∧((x ∈ s₂)∧(x ∈ s₃)) → (x ∈ s₁)∧(x ∈ (s₂ ∩ s₃))))
        ∘ ([↔]-elimᵣ [∧]-associativity)
        ∘ ((prop ↦ ([∧]-intro ([↔]-elimᵣ([∩]-containment{s₁}{s₂}{x}) ([∧]-elimₗ prop)) ([∧]-elimᵣ prop))) :of: ((x ∈ (s₁ ∩ s₂))∧(x ∈ s₃) → ((x ∈ s₁)∧(x ∈ s₂))∧(x ∈ s₃)))
        ∘ (([↔]-elimᵣ([∩]-containment{s₁ ∩ s₂}{s₃}{x}))                                                   :of: ((x ∈ ((s₁ ∩ s₂) ∩ s₃)) → (x ∈ (s₁ ∩ s₂))∧(x ∈ s₃)))

module NaturalNumbers where
  open Axioms1
  open Operations

  module _ ⦃ _ : EmptySetExistence ⦄ where
    -- Could be interpreted as a set theoretic definition of zero from the natural numbers.
    𝟎 : S
    𝟎 = ∅

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    -- Could be interpreted as a set theoretic definition of the successor function from the natural numbers.
    𝐒 : S → S
    𝐒(x) = (x ∪ •(x))

  module _ ⦃ _ : EmptySetExistence ⦄ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    Inductive : S → Stmt
    Inductive(N) = ((𝟎 ∈ N) ∧ (∀{n} → (n ∈ N) → (𝐒(n) ∈ N)))

module Tuples where
  open Axioms1
  open Operations
  open Relations

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    _,_ : S → S → S
    _,_ x y = (x ∪ (x ⟒ y))

    postulate Tuple-elem-uniqueness : ∀{x₁ x₂ y₁ y₂} → ((x₁ , y₁) ≡ (x₂ , y₂)) → (x₁ ≡ x₂)∧(y₁ ≡ y₂)
    -- Tuple-elem-uniqueness (x1y1x2y2) =

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ ⦃ _ : PowerSetExistence ⦄ where
    _⨯_ : S → S → S
    _⨯_ s₁ s₂ = filter(℘(℘(s₁ ∪ s₂))) (s ↦ ∃(x ↦ ∃(y ↦ (x ∈ s₁) ∧ (y ∈ s₂) ∧ (s ≡ (x , y)))))

module Functions where
  open Axioms1
  open Operations
  open Relations
  open Tuples

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    Function : S → S → S → Stmt
    Function(f) (s₁)(s₂) = (∀{x} → (x ∈ s₁) → ∃(y ↦ (y ∈ s₂) ∧ ((x , y) ∈ f) ∧ (∀{y₂} → ((x , y₂) ∈ f) → (y ≡ y₂))))

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ ⦃ _ : PowerSetExistence ⦄ where
    _^_ : S → S → S
    _^_ s₁ s₂ = filter(℘(s₂ ⨯ s₁)) (f ↦ Function(f)(s₁)(s₂))

module Axioms2 where
  open Axioms1
  open NaturalNumbers
  open Relations

  module _ ⦃ _ : EmptySetExistence ⦄ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    -- Sets can model ℕ.
    -- This can be used to construct a set representing the natural numbers.
    -- In this context, "Model" and "Representing" means a bijection.
    record InfinityAxiom : Set(Lvl.𝟎) where
      field infinity : ∃(N ↦ Inductive(N))
    open InfinityAxiom ⦃ ... ⦄ public

  record ChoiceAxiom : Set(Lvl.𝟎) where
    field choice : ⊤
  open ChoiceAxiom ⦃ ... ⦄ public

module NaturalNumberTheorems where
  open Axioms1
  open Axioms2
  open NaturalNumbers
  open Operations
  open OperationsTheorems
  open Relations
  open RelationsTheorems

  module _ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ where
    [𝐒]-contains-arg : ∀{x} → (x ∈ 𝐒(x))
    [𝐒]-contains-arg = [↔]-elimₗ ([∪]-containment) ([∨]-introᵣ [•]-containment)

    [𝐒]-subset-arg : ∀{x} → (x ⊆ 𝐒(x))
    [𝐒]-subset-arg = [∪]-subsetₗ

  module _ ⦃ _ : EmptySetExistence ⦄ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ ⦃ _ : InfinityAxiom ⦄ where
    Infinity-contains-[𝟎] : (𝟎 ∈ [∃]-witness(infinity))
    Infinity-contains-[𝟎] = [∧]-elimₗ ([∃]-proof(infinity))

    Infinity-contains-[𝐒] : ∀{n} → (n ∈ [∃]-witness(infinity)) → (𝐒(n) ∈ [∃]-witness(infinity))
    Infinity-contains-[𝐒] = [∧]-elimᵣ ([∃]-proof(infinity))

    Infinity-inductive : Inductive([∃]-witness(infinity))
    Infinity-inductive = [∧]-intro (Infinity-contains-[𝟎]) (Infinity-contains-[𝐒])

  module _ ⦃ _ : EmptySetExistence ⦄ ⦃ _ : UnionExistence ⦄ ⦃ _ : PairExistence ⦄ ⦃ _ : InfinityAxiom ⦄ ⦃ _ : RestrictedComprehensionExistence ⦄ where
    ℕ : S
    ℕ = filter([∃]-witness(infinity)) (n ↦ ∀{I} → Inductive(I) → (n ∈ I))

    [ℕ]-subset-of-infinity : (ℕ ⊆ [∃]-witness(infinity))
    [ℕ]-subset-of-infinity = filter-subset

    [ℕ]-contains-[𝟎] : (𝟎 ∈ ℕ)
    [ℕ]-contains-[𝟎] = ([↔]-elimₗ (filter-containment {_}{_}{𝟎})) ([∧]-intro (Infinity-contains-[𝟎]) (\{_} → [∧]-elimₗ))

    [ℕ]-contains-[𝐒] : ∀{n} → (n ∈ ℕ) → (𝐒(n) ∈ ℕ)
    [ℕ]-contains-[𝐒] {n} (n-in) with ([↔]-elimᵣ filter-containment) (n-in)
    ... | ([∧]-intro (n-in-inf) (n-satisfies)) =
      (([↔]-elimₗ (filter-containment {_}{_}{𝐒(n)}))
        ([∧]-intro
          (Sn-in-inf)
          (\{_} → Sn-satisfies)
        )
      )
      where
        Sn-in-inf : (𝐒(n) ∈ [∃]-witness(infinity))
        Sn-in-inf = Infinity-contains-[𝐒] (n-in-inf)

        Sn-satisfies : ∀{I} → Inductive(I) → (𝐒(n) ∈ I)
        Sn-satisfies{I}(I-inductive) = ([∧]-elimᵣ(I-inductive)) (n-satisfies{I}(I-inductive))

    -- TODO: Is this provable without extensionality? The problem is (x∈z ↔ y∈z) when (x≡y).
    module _ ⦃ _ : SetEquality ⦄ where
      [ℕ]-containsₗ : ∀{n} → (n ∈ ℕ) ← (n ≡ 𝟎)∨(∃(x ↦ (x ∈ ℕ)∧(n ≡ 𝐒(x))))
      [ℕ]-containsₗ {_} ([∨]-introₗ n-zero) with equality(n-zero)
      ... | [≡]-intro = [ℕ]-contains-[𝟎]
      [ℕ]-containsₗ {n} ([∨]-introᵣ ([∃]-intro (x) ⦃ [∧]-intro (in-N) (n-succ) ⦄)) with equality(n-succ)
      ... | [≡]-intro = [ℕ]-contains-[𝐒] {x} (in-N)

    [ℕ]-inductive : Inductive(ℕ)
    [ℕ]-inductive = [∧]-intro ([ℕ]-contains-[𝟎]) ([ℕ]-contains-[𝐒])

    [ℕ]-subset : ∀{I} → Inductive(I) → (ℕ ⊆ I)
    [ℕ]-subset{I} (I-inductive) {n} (n-in-ℕ) with ([↔]-elimᵣ filter-containment) (n-in-ℕ)
    ... | ([∧]-intro (n-in-inf) (n-satisfies)) = n-satisfies{I} (I-inductive)

    -- [ℕ]-containsᵣ : ∀{n} → (n ∈ ℕ) → (n ≡ 𝟎)∨(∃(x ↦ (x ∈ ℕ)∧(n ≡ 𝐒(x))))
    -- [ℕ]-containsᵣ{n} (n-in) with ([↔]-elimᵣ filter-containment) (n-in) =

    [ℕ]-set-induction : ∀{Nₛ} → (Nₛ ⊆ ℕ) → Inductive(Nₛ) → (Nₛ ≡ ℕ)
    [ℕ]-set-induction {Nₛ} (Nₛ-subset) (ind) = [↔]-intro ([ℕ]-subset {Nₛ} (ind)) (Nₛ-subset)

    module _ ⦃ _ : (𝟎 ∈ ℕ)⦄ ⦃ _ : ∀{n} → ⦃ _ : (n ∈ ℕ) ⦄ → (𝐒(n) ∈ ℕ) ⦄ where
      postulate [ℕ]-induction : ∀{φ : (n : S) → ⦃ _ : (n ∈ ℕ) ⦄ → Stmt} → φ(𝟎) → (∀{n} → ⦃ n-in : (n ∈ ℕ) ⦄ → φ(n) → φ(𝐒(n))) → (∀{n} → ⦃ _ : n ∈ ℕ ⦄ → φ(n))
      {-[ℕ]-induction {φ} (zero) (succ) {n} ⦃ n-in-ℕ ⦄ =
        ([∧]-elimᵣ
          (([↔]-elimᵣ filter-containment)
            ([ℕ]-subset {set} ([∧]-intro (zero-in) (succ-in)) {n} (n-in-ℕ))
          )
        ) where

        set : S
        set = filter-dep(ℕ)(φ)

        module _ {n} ⦃ n-in-ℕ : (n ∈ ℕ) ⦄ where
          n-inₗ : φ(n) ← (n ∈ set)
          n-inₗ (proof) = [∃]-proof (([↔]-elimᵣ filter-dep-containment) (proof))

          n-inᵣ : φ(n) → (n ∈ set)
          n-inᵣ (proof) = ([↔]-elimₗ filter-containment) ([∧]-intro (n-in-ℕ) (proof))

          -- TODO: Unnecessary
          Sn-inₗ : φ(𝐒(n)) ← (𝐒(n) ∈ set)
          Sn-inₗ (proof) = [∧]-elimᵣ (([↔]-elimᵣ filter-containment) (proof))

          Sn-inᵣ : φ(𝐒(n)) → (𝐒(n) ∈ set)
          Sn-inᵣ (proof) = ([↔]-elimₗ filter-containment) ([∧]-intro ([ℕ]-contains-[𝐒] (n-in-ℕ)) (proof))

        zero-in : 𝟎 ∈ set
        zero-in =
          (([↔]-elimₗ filter-containment)
            ([∧]-intro
              ([ℕ]-contains-[𝟎])
              (zero)
            )
          )

        succ-in : ∀{n} → (n ∈ set) → (𝐒(n) ∈ set)
        succ-in{n} (n-in-filter) with ([↔]-elimᵣ filter-containment) (n-in-filter)
        ... | ([∧]-intro (n-in-ℕ) (φn)) = (Sn-inᵣ ⦃ n-in-ℕ ⦄ (succ ⦃ n-in-ℕ ⦄ (n-inₗ ⦃ n-in-ℕ ⦄ n-in-filter)))
        -}
        {- ... | ([∧]-intro (n-in-ℕ) (φn)) =
          (([↔]-elimₗ filter-containment)
            ([∧]-intro
              ([ℕ]-contains-[𝐒] (n-in-ℕ))
              (?)
            )
          )
        -}
        -- succ-in = (Sn-inᵣ) ∘ (succ {n} (n-in-ℕ)) ∘ (n-inₗ)

      _<_ : (a : S) → ⦃ _ : (a ∈ ℕ) ⦄ → (b : S) → ⦃ _ : (b ∈ ℕ) ⦄ → Stmt
      a < b = (a ∈ b)

      _≤_ : (a : S) → ⦃ _ : (a ∈ ℕ) ⦄ → (b : S) → ⦃ _ : (b ∈ ℕ) ⦄ → Stmt
      a ≤ b = (a < b) ∨ (a ≡ b)

      {- [<]-transitivity : ∀{a b c} → ⦃ _ : (a ∈ ℕ) ⦄ → ⦃ _ : (b ∈ ℕ) ⦄ → ⦃ _ : (c ∈ ℕ) ⦄ → (a < b) → (b < c) → (a < c)
      [<]-transitivity{a}{b}{c} = [ℕ]-induction{n ↦ \ ⦃ _ ⦄ → ((a < b) → (b < n) → (a < n))} φ-zero φ-succ {c} where
        postulate φ-zero : (a < b) → (b < 𝟎) ⦃ _ ⦄ ⦃ [ℕ]-contains-[𝟎] ⦄ → (a < 𝟎) ⦃ _ ⦄ ⦃ [ℕ]-contains-[𝟎] ⦄
        postulate φ-succ : ∀{n} → ⦃ _ : n ∈ ℕ ⦄ → ((a < b) → (b < n) → (a < n)) → ((a < b) → (b < 𝐒(n)) → (a < 𝐒(n)))
      -}

    {--- TODO: I think a filtering like this gives the minimal inductive set? But probably not. (x∈ℕ) is missing, and then the definition is refering to itself.
    ℕ : S
    ℕ = filter([∃]-witness(infinity)) (n ↦ (n ≡ 𝟎) ∨ ∃(x ↦ ∧(n ≡ 𝐒(x)))) -- TODO: Does this potentially include other stuff too? Like 𝐒 ⦃ 𝟎 ⦄ ?

    -- TODO: ∀{n} → (n ∈ ℕ) → (n ≡ 𝟎)∨(∃(x ↦ (x ∈ ℕ)∧(n ≡ 𝐒(x)))). COuld use [ℕ]-contains-[𝐒]-arg to achieve this.
    [ℕ]-contains-only : ∀{n} → (n ∈ ℕ) → (n ≡ 𝟎)∨(∃(x ↦ n ≡ 𝐒(x)))
    [ℕ]-contains-only {n} (n-containment) = [∧]-elimᵣ (([↔]-elimᵣ (filter-containment {_}{_}{n})) (n-containment))

    -- [ℕ]-contains-[𝐒]-arg : ∀{n} → (𝐒(n) ∈ ℕ) → (n ∈ ℕ)
    -- [ℕ]-contains-[𝐒]-arg{n} (sn-in) = [ℕ]-contains-only{𝐒(n)} ([∨]-introᵣ )

    [ℕ]-contains-[𝟎] : (𝟎 ∈ ℕ)
    [ℕ]-contains-[𝟎] = ([↔]-elimₗ (filter-containment {_}{_}{𝟎})) ([∧]-intro Infinity-contains-[𝟎] satisfy-property) where
      satisfy-property : (𝟎 ≡ 𝟎) ∨ ∃(y ↦ 𝟎 ≡ 𝐒(y))
      satisfy-property = [∨]-introₗ [≡]-reflexivity

    [ℕ]-contains-[𝐒] : ∀{n} → (n ∈ ℕ) → (𝐒(n) ∈ ℕ)
    [ℕ]-contains-[𝐒] {n} (n-containment) = ([↔]-elimₗ (filter-containment {_}{_}{𝐒(n)})) ([∧]-intro (Infinity-contains-[𝐒] {n} ([ℕ]-subset-of-infinity {n} (n-containment))) satisfy-property) where
      satisfy-property : (𝐒(n) ≡ 𝟎) ∨ ∃(y ↦ 𝐒(n) ≡ 𝐒(y))
      satisfy-property = [∨]-introᵣ ([∃]-intro n ⦃ [≡]-reflexivity ⦄)

    -- [ℕ]-subset-implies-containment : ∀{n} → (n ⊆ ℕ) → (n ∈ ℕ)
    -- [ℕ]-strict-subset-is-containment : ∀{n} → (n ⊂ ℕ) ↔ (n ∈ ℕ)

    [ℕ]-subset : ∀{Nₛ} → Inductive(Nₛ) → (ℕ ⊆ Nₛ)
    [ℕ]-subset {Nₛ} ([∧]-intro zero-containment successor-containment) {n} ([ℕ]-n-containment) =
      [∨]-elim (zero) (succ) ([ℕ]-contains-only{n} ([ℕ]-n-containment)) where

      zero : (n ≡ 𝟎) → (n ∈ Nₛ)
      zero(n0) with equality(n0)
      ... | [≡]-intro = zero-containment

      succ : (∃(x ↦ n ≡ 𝐒(x))) → (n ∈ Nₛ)
      succ([∃]-intro(x) ⦃ prop ⦄) with equality(prop)
      ... | [≡]-intro = successor-containment(x-in) where
        postulate x-in : (x ∈ Nₛ) -- TODO: Impossible to prove? Something is missing in the definition of ℕ?

    -- TODO: Is it possible to connect this to the ℕ in Numeral.Natural.ℕ?

    -- TODO: Is (∀{s₁ s₂ : S} → (s₁ ≡ s₂) → (s₁ ∈ S) → (s₂ ∈ S)) provable without axiom of extensionality?
-}
record IZF : Set(Lvl.𝐒(Lvl.𝟎)) where
  instance constructor IZFStructure
  open Axioms1
  open Axioms2

  field
   ⦃ extensionality ⦄ : SetEquality
   ⦃ empty ⦄         : EmptySetExistence
   ⦃ pair ⦄          : PairExistence
   ⦃ union ⦄         : UnionExistence
   ⦃ power ⦄         : PowerSetExistence
   ⦃ comprehension ⦄ : RestrictedComprehensionExistence
   ⦃ infinity ⦄      : InfinityAxiom
   ⦃ collection ⦄    : CollectionAxiom
   ⦃ induction ⦄     : InductionProof

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Math.NumberTheory.Product.Generic.Properties where

-- agda-stdlib
open import Algebra

-- agda-misc
open import Math.NumberTheory.Summation.Generic.Properties

-- TODO add renamaings
module CommutativeMonoidProductProperties {c e} (CM : CommutativeMonoid c e) =
  CommutativeMonoidSummationProperties CM
  renaming
  ( Σ<-cong to Π<-cong
  ; Σ<-congˡ to Π<-congˡ
  ; Σ<-congʳ to Π<-congʳ
  ; Σ≤-cong to Π≤-cong
  ; Σ≤-congˡ to Π≤-congˡ
  ; Σ≤-congʳ to Π≤-congʳ
  ; Σ<range-cong to Π<range-cong
  ; Σ<range-cong₃ to Π<range-cong₃
  ; Σ<range-cong₁₂ to Π<range-cong₁₂
  ; Σ<range-cong₁ to Π<range-cong₁
  ; Σ<range-cong₂ to Π<range-cong₂
  ; Σ≤range-cong to Π≤range-cong
  ; Σ<-congˡ-with-< to Π<-congˡ-with-<
  ; Σ≤-congˡ-with-≤ to Π≤-congˡ-with-≤
  ; Σ<-0 to Π<-1
  ; Σ≤-0 to Π≤-1
  ; Σ<[1,f]≈f[0] to Π<[1,f]≈f[0]
  ; Σ≤[0,f]≈f[0] to Π≤[0,f]≈f[0]
  ; n≤m⇒Σ<range[m,n,f]≈0 to n≤m⇒Π<range[m,n,f]≈1
  ; n<m⇒Σ≤range[m,n,f]≈0 to n<m⇒Π≤range[m,n,f]≈1
  ; Σ<range[n,n,f]≈0 to Π<range[n,n,f]≈1
  ; Σ<range-cong₃-with-< to Π<range-cong₃-with-<
  ; Σ≤range-cong₃-with-≤ to Π≤range-cong₃-wiht-≤
  ; Σ<range[n,1+n,f]≈f[n] to Π<range[n,1+n,f]≈f[n]
  ; Σ≤range[n,n,f]≈f[n] to Π≤range[n,n,f]≈f[n]
  ; Σ<-+ to Π<-+
  ; Σ≤-Σ<-+ to Π≤-Π<-+
  ; Σ≤-+ to Π≤-+
  ; Σ<-push-suc to Π<-push-suc
  ; Σ≤-push-suc to Π≤-push-suc
  ; Σ<range[0,n,f]≈Σ<[n,f] to Π<range[0,n,f]≈Π<[n,f]
  ; Σ≤range[0,n,f]≈Σ≤[n,f] to Π≤range[0,n,f]≈Π≤[n,f]
  ; Σ<range[m,m+n+o,f]≈Σ<range[m,m+n,f]+Σ<range[m+n,m+n+o,f] to
      Π<range[m,m+n+o,f]≈Π<range[m,m+n,f]*Π<range[m+n,m+n+o,f]
  ; Σ<range[m,n,f]≈Σ<range[m,o,f]+Σ<range[o,n,f] to
      Π<range[m,n,f]≈Π<range[m,o,f]*Π<range[o,n,f]
  ; Σ<range[m,n,f]≈Σ<range[o+m,o+n,i→f[i∸o]] to
      Π<range[m,n,f]≈Π<range[o+m,o+n,i→f[i∸o]]
  ; Σ<-const to Π<-const
  ; Σ≤-const to Π≤-const
  ; Σ<range-const to Π<range-const
  ; Σ≤range-const to Π≤range-const
  ; Σ<-distrib-+ to Π<-distrib-*
  ; Σ≤-distrib-+ to Π≤-distrib-*
  ; Σ<range-distrib-+ to Π<range-distrib-*
  ; Σ≤range-distrib-+ to Π≤range-distrib-*
  ; Σ<-comm to Π<-comm
  ; Σ≤-comm to Π≤-comm
  ; Σ<range-comm to Π<range-comm
  ; Σ≤range-comm to Π≤range-comm
  ; Σ<-sumₜ-syntax to Π<-sumₜ-syntax
  ; Σ<-reverse to Π<-reverse
  ; Σ≤-reverse to Π≤-reverse
  ; Σ<range-reverse to Π<range-reverse
  ; Σ≤range-reverse to Π≤range-reverse
  ; Σ<-split-even to Π<-split-even
  ; Σ<-split-odd to Π<-split-odd
  )
  using ()


text:
-- Andreas, 2015-10-26, issue reported by Wolfram Kahl
-- {-# OPTIONS -v scope.mod.inst:30 -v tc.mod.check:10 -v tc.mod.apply:80 #-}

module _ where

  module ModParamsRecord (A : Set) where
    record R (B : Set) : Set where
      field F : A → B

  module ModParamsToLoose (A : Set) where
    open ModParamsRecord

    private
      module M (B : Set) (G : A → B) where
        r : R A B
        r = record { F = G }

        module r = R r
    open M public

  module ModParamsLost (A : Set) where
    open ModParamsRecord
    open ModParamsToLoose A

    f : (A → A) → A → A
    f G = S.F
      where
        module S = r A G           -- expected |S.F : A → A|,
                                   -- WAS: but obtained |S.F : (B : Set) (G₁ : A → B) → A → B|
        -- module S = r            -- as expected: |S.F : (B : Set) (G₁ : A → B) → A → B|
        -- module S = R A (r A G)  -- as expected: |S.F : A → A|

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Relation.Binary.Core

module Quasigroup.Definitions
  {a ℓ} {A : Set a}   -- The underlying set
  (_≈_ : Rel A ℓ)     -- The underlying equality
  where

open import Algebra.Core
open import Data.Product

LatinSquareProperty₁ : Op₂ A → Set _
LatinSquareProperty₁ _*_ = ∀ a b x  → (a * x) ≈ b

LatinSquareProperty₂ : Op₂ A → Set _
LatinSquareProperty₂ _*_ = ∀ a b y → (y * a) ≈ b

LatinSquareProperty : Op₂ A → Set _
LatinSquareProperty _*_ = (LatinSquareProperty₁ _*_) × (LatinSquareProperty₂ _*_)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Universe.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence

isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
  → transport p ≡ transport q → p ≡ q
isInjectiveTransport {p = p} {q} α i =
  hcomp
    (λ j → λ
      { (i = i0) → secEq univalence p j
      ; (i = i1) → secEq univalence q j
      })
    (invEq univalence ((λ a → α i a) , t i))
  where
  t : PathP (λ i → isEquiv (λ a → α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→isContrPathP (λ i → isPropIsEquiv (λ a → α i a)) _ _ .fst

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reflexivity {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product

-- Reflexivity of valid types.
reflᵛ : ∀ {A Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ≡ A / [Γ] / [A]
reflᵛ [Γ] [A] ⊢Δ [σ] =
  reflEq (proj₁ ([A] ⊢Δ [σ]))

-- Reflexivity of valid terms.
reflᵗᵛ : ∀ {A t Γ l}
         ([Γ] : ⊩ᵛ Γ)
         ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
         ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A])
       → Γ ⊩ᵛ⟨ l ⟩ t ≡ t ∷ A / [Γ] / [A]
reflᵗᵛ [Γ] [A] [t] ⊢Δ [σ] =
  reflEqTerm (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ]))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.RingSolver.RawRing where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level

record RawRing ℓ : Type (ℓ-suc ℓ) where

  constructor rawring

  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier

  infixl 8 _·_
  infixl 7 -_
  infixl 6 _+_

⟨_⟩ : RawRing ℓ → Type ℓ
⟨_⟩ = RawRing.Carrier

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Issue1760f where

-- Skipping a single record definition in an abstract block.
abstract
  {-# NO_POSITIVITY_CHECK #-}
  record U : Set where
    field ap : U → U

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --verbose=10 #-}

module inorderF where

  open import Data.Nat
  open import Data.Vec
  open import Agda.Builtin.Sigma
  open import Data.Product
  open import Data.Fin using (fromℕ)

  open import trees
  open import optics
  open import lemmas

  inorderTreeF : {A : Set} -> (t : Tree A) -> Vec A (#nodes t) × (Vec A (#nodes t) -> Tree A)
  inorderTreeF empty = ([] , λ _ -> empty)
  inorderTreeF {A} (node t₁ x t₂) with inorderTreeF t₁ | inorderTreeF t₂
  ...                                | (g₁ , p₁)       | (g₂ , p₂) =
    (g₁ ++ (x ∷ g₂) , λ v -> node (p₁ (take n₁ v)) (head (drop n₁ v)) (righttree v))
    where
      n  = #nodes (node t₁ x t₂)
      n₁ = #nodes t₁
      n₂ = #nodes t₂
      righttree :  Vec A n -> Tree A
      righttree v rewrite +-suc n₁ n₂ = p₂ (drop (1 + n₁) v)

  inorderF : {A : Set} -> TraversalF (Tree A) (Tree A) A A
  inorderF = record{ extract = (#nodes , inorderTreeF) }

  module tests where
    tree1 : Tree ℕ
    tree1 = node (node empty 1 empty) 3 empty

    open Traversal

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
open import Common.Prelude
open import Common.Reflection

module TermSplicing1 where

x = unquote (give Set)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties related to Data.Star
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
-- module directly.
------------------------------------------------------------------------

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

module Data.Star.Properties where

open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
  public


text:
------------------------------------------------------------------------------
-- Well-founded induction on the relation _◁_
------------------------------------------------------------------------------

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

-- N.B This module does not contain combined proofs, but it imports
-- modules which contain combined proofs.

module FOTC.Program.McCarthy91.WF-Relation.Induction.Acc.WF-ATP where

open import FOTC.Base
open import FOTC.Data.Nat

import FOTC.Data.Nat.Induction.Acc.WF-ATP
open FOTC.Data.Nat.Induction.Acc.WF-ATP.<-WF using ( <-wf )

open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Induction.WF
open import FOTC.Program.McCarthy91.WF-Relation
open import FOTC.Program.McCarthy91.WF-Relation.PropertiesATP

-- Parametrized modules
open module InvImg =
  FOTC.Induction.WF.InverseImage {N} {N} {_<_} ◁-fn-N

------------------------------------------------------------------------------
-- The relation _◁_ is well-founded (using the inverse image combinator).
◁-wf : WellFounded _◁_
◁-wf Nn = wellFounded <-wf Nn

-- Well-founded induction on the relation _◁_.
◁-wfind : (A : D → Set) →
          (∀ {n} → N n → (∀ {m} → N m → m ◁ n → A m) → A n) →
          ∀ {n} → N n → A n
◁-wfind A = WellFoundedInduction ◁-wf

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists defined in terms of the reflexive-transitive closure, Star
------------------------------------------------------------------------

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

module Data.Star.List where

open import Data.Star.Nat
open import Data.Unit
open import Relation.Binary.Construct.Always using (Always)
open import Relation.Binary.Construct.Constant using (Const)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- Lists.

List : ∀ {a} → Set a → Set a
List A = Star (Const A) tt tt

-- Nil and cons.

[] : ∀ {a} {A : Set a} → List A
[] = ε

infixr 5 _∷_

_∷_ : ∀ {a} {A : Set a} → A → List A → List A
_∷_ = _◅_

-- The sum of the elements in a list containing natural numbers.

sum : List ℕ → ℕ
sum = fold (Star Always) _+_ zero


text: module triple where

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Syntactic kits from Conor McBride's
-- "Type-Preserving Renaming and Substitution"
module Syntax.Substitution.Kits where

open import Syntax.Types
open import Syntax.Context
open import Syntax.Terms

open import CategoryTheory.Categories

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

-- Type of entities that we can traverse
-- (instantiated by variables and types)
Schema : Set₁
Schema = Context -> Judgement -> Set

-- Explicit substitution from term in context Δ to term in context Γ
-- E.g. from Γ ⌊ A ⌋ Γ′ ⊢ N : B to Γ ⌊⌋ Γ′ ⊢ N[σ] : B
-- using substitution Γ ⌊⌋ Γ′ ⊢ σ : Γ ⌊ A ⌋ Γ′
data Subst (𝒮 : Schema) : Context -> Context -> Set where
    -- Empty substitution
    ●   : ∀ {Δ}     -> Subst 𝒮 ∙ Δ
    -- Extending the domain of a substitution
    _▸_ : ∀ {A Γ Δ} -> (σ : Subst 𝒮 Γ Δ) -> (T : 𝒮 Δ A) -> Subst 𝒮 (Γ , A) Δ

-- Syntactic kit grouping together common operations on traversable
-- syntactic entities such as variables and terms
record Kit (𝒮 : Schema) : Set where
    field
        -- Convert a variable to the entity
        𝓋 : ∀ {Γ A} -> A ∈ Γ -> 𝒮 Γ A
        -- Convert the entity to a term
        𝓉 : ∀ {Γ A} -> 𝒮 Γ A -> Γ ⊢ A
        -- Weaken the entity
        𝓌 : ∀ {B Γ A} -> 𝒮 Γ A -> 𝒮 (Γ , B) A
        -- Stabilise the context of the entity
        𝒶 : ∀ {Γ A} -> 𝒮 Γ (A always) -> 𝒮 (Γ ˢ) (A always)

-- Substitutable kit
record SubstKit (𝒮 : Schema) : Set where
    field
        -- Underlying traversable kit
        𝓀 : Kit 𝒮
        -- Apply substitution to a kit
        𝓈 : ∀ {Γ Δ A} -> Subst 𝒮 Γ Δ -> 𝒮 Γ A -> 𝒮 Δ A

open Kit

-- | Combinators
-- | All take a syntactic (substitutable) kit as an argument
-- | which provides the necessary operations

-- Weakening a substitution
-- Δ ⊢ σ : Γ to (Δ , A) ⊢ σ : Γ
_⁺_ : ∀ {A 𝒮 Γ Δ} -> Subst 𝒮 Γ Δ -> Kit 𝒮 -> Subst 𝒮 Γ (Δ , A)
●       ⁺ _ = ●
(σ ▸ T) ⁺ k = (σ ⁺ k) ▸ 𝓌 k T
infixl 40 _⁺_

-- Lifting a substitution
-- Δ ⊢ σ : Γ to (Δ , A) ⊢ σ : (Γ , A)
_↑_ : ∀ {A 𝒮 Γ Δ} -> Subst 𝒮 Γ Δ -> Kit 𝒮 -> Subst 𝒮 (Γ , A) (Δ , A)
σ ↑ k = (σ ⁺ k) ▸ 𝓋 k top
infixl 40 _↑_

-- Stabilising a substitution
-- Δ ⊢ σ : Γ to Δ ˢ ⊢ σ : Γ ˢ
_↓ˢ_ : ∀ {𝒮 Γ Δ} -> Subst 𝒮 Γ Δ -> Kit 𝒮 -> Subst 𝒮 (Γ ˢ) (Δ ˢ)
●                    ↓ˢ _ = ●
(_▸_ {A now} σ T)    ↓ˢ k = σ ↓ˢ k
(_▸_ {A always} σ T) ↓ˢ k = (σ ↓ˢ k) ▸ 𝒶 k T
infixl 40 _↓ˢ_

-- Identity substitution
idₛ : ∀ {Γ 𝒮} -> Kit 𝒮 -> Subst 𝒮 Γ Γ
idₛ {∙}     k = ●
idₛ {Γ , _} k = idₛ k ↑ k

-- Composition of substitutions
_∘[_]ₛ_ : ∀ {𝒮 Γ Δ Ξ} -> Subst 𝒮 Δ Ξ -> SubstKit 𝒮 -> Subst 𝒮 Γ Δ -> Subst 𝒮 Γ Ξ
σ₂ ∘[ k ]ₛ ●        = ●
σ₂ ∘[ k ]ₛ (σ₁ ▸ T) = (σ₂ ∘[ k ]ₛ σ₁) ▸ SubstKit.𝓈 k σ₂ T

-- Substitution from an order-preserving embedding
-- Γ ⊆ Δ to Δ ⊢ σ : Γ
_⊆ₛ_ : ∀ {𝒮 Γ Δ} -> Γ ⊆ Δ -> Kit 𝒮 -> Subst 𝒮 Γ Δ
refl ⊆ₛ k     = idₛ k
(keep s) ⊆ₛ k = (s ⊆ₛ k) ↑ k
(drop s) ⊆ₛ k = (s ⊆ₛ k) ⁺ k

-- Substitution from propositional equality of contexts
_≡ₛ_ : ∀ {𝒮 Γ Δ} -> Γ ≡ Δ -> Kit 𝒮 -> Subst 𝒮 Γ Δ
refl ≡ₛ k = idₛ k

-- Substitution from idempotence of stabilisation
_ˢˢₛ_ : ∀ {𝒮} -> (Γ : Context) -> Kit 𝒮 -> Subst 𝒮 (Γ ˢ) (Γ ˢ ˢ)
∙ ˢˢₛ k = ●
(Γ , A now) ˢˢₛ k = Γ ˢˢₛ k
(Γ , A always) ˢˢₛ k = (Γ ˢˢₛ k) ↑ k

-- | Standard substitutions
-- | Common transformations between contexts

module _ {𝒮 : Schema} (sk : SubstKit 𝒮) where
    open SubstKit sk
    open Kit 𝓀

    -- | Weakening

    -- Weakening the top of the context
    weak-topₛ : ∀{A Γ} -> Subst 𝒮 Γ (Γ , A)
    weak-topₛ = idₛ 𝓀 ⁺ 𝓀

    -- Weakening the middle of the context
    weak-midₛ : ∀{A} Γ Γ′ -> Subst 𝒮 (Γ ⌊⌋ Γ′) (Γ ⌊ A ⌋ Γ′)
    weak-midₛ Γ ∙ = weak-topₛ
    weak-midₛ Γ (Γ′ , B) = weak-midₛ Γ Γ′ ↑ 𝓀

    -- General weakening from an OPE
    weakₛ : ∀{Γ Δ} -> Γ ⊆ Δ -> Subst 𝒮 Γ Δ
    weakₛ = _⊆ₛ 𝓀

    -- | Exchange

    -- Exchange on top
    ex-topₛ : ∀{A B} Γ -> Subst 𝒮 (Γ , A , B) (Γ , B , A)
    ex-topₛ Γ = (idₛ 𝓀 ⁺ 𝓀 ↑ 𝓀) ▸ (𝓋 𝓀 (pop top))

    -- General exchange lemma
    exₛ : ∀{A B} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ⌊ A ⌋ Γ′ ⌊ B ⌋ Γ″) (Γ ⌊ B ⌋ Γ′ ⌊ A ⌋ Γ″)
    exₛ Γ ∙ ∙ = ex-topₛ Γ
    exₛ {A} {B} Γ (Γ′ , C) ∙ =
        (exₛ Γ Γ′ [ A ] ∘[ sk ]ₛ ex-topₛ (Γ , C ⌊⌋ Γ′)) ∘[ sk ]ₛ exₛ Γ Γ′ [ B ]
    exₛ Γ ∙ (Γ″ , D) = exₛ Γ ∙ Γ″ ↑ 𝓀
    exₛ Γ (Γ′ , C) (Γ″ , D) = exₛ Γ (Γ′ , C) Γ″ ↑ 𝓀

    -- | Contraction

    -- Contraction on top
    contr-topₛ : ∀{A Γ} -> Subst 𝒮 (Γ , A , A) (Γ , A)
    contr-topₛ = (idₛ 𝓀) ▸ (𝓋 𝓀 top)

    -- General contraction lemma (left)
    contr-lₛ : ∀{A} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ⌊ A ⌋ Γ′ ⌊ A ⌋ Γ″) (Γ ⌊ A ⌋ Γ′ ⌊⌋ Γ″)
    contr-lₛ Γ ∙ ∙ = contr-topₛ
    contr-lₛ Γ (Γ′ , B) ∙ = (idₛ 𝓀) ▸ (𝓌 𝓀 (𝓈 (contr-lₛ Γ Γ′ ∙) (𝓋 𝓀 top)))
    contr-lₛ Γ ∙ (Γ″ , C) = contr-lₛ Γ ∙ Γ″ ↑ 𝓀
    contr-lₛ Γ (Γ′ , B) (Γ″ , C) = contr-lₛ Γ (Γ′ , B) Γ″ ↑ 𝓀

    -- General contraction lemma (right)
    contr-rₛ : ∀{A} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ⌊ A ⌋ Γ′ ⌊ A ⌋ Γ″) (Γ ⌊⌋ Γ′ ⌊ A ⌋ Γ″)
    contr-rₛ Γ ∙ ∙ = contr-topₛ
    contr-rₛ {A} Γ (Γ′ , B) ∙ =
        (ex-topₛ (Γ ⌊⌋ Γ′) ∘[ sk ]ₛ contr-rₛ Γ Γ′ [ B ]) ∘[ sk ]ₛ ex-topₛ (Γ , A ⌊⌋ Γ′)
    contr-rₛ Γ ∙ (Γ″ , C) = contr-rₛ Γ ∙ Γ″ ↑ 𝓀
    contr-rₛ Γ (Γ′ , B) (Γ″ , C) = contr-rₛ Γ (Γ′ , B) Γ″ ↑ 𝓀

    -- | Movement

    -- Moving a variable to the right in the context
    move-rₛ : ∀{A} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ⌊ A ⌋ Γ′ ⌊⌋ Γ″) (Γ ⌊⌋ Γ′ ⌊ A ⌋ Γ″)
    move-rₛ {A} Γ Γ′ Γ″ = contr-rₛ Γ Γ′ Γ″ ∘[ sk ]ₛ weak-midₛ (Γ ⌊ A ⌋ Γ′) Γ″

    -- Moving a variable to the left in the context
    -- Bit verbose as we have to deal with associativity
    move-lₛ : ∀{A} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ⌊⌋ Γ′ ⌊ A ⌋ Γ″) (Γ ⌊ A ⌋ Γ′ ⌊⌋ Γ″)
    move-lₛ {A} Γ Γ′ Γ″
        =        contr-lₛ Γ Γ′ Γ″
        ∘[ sk ]ₛ ((sym (⌊A⌋-assoc Γ Γ′ Γ″ A A) ≡ₛ 𝓀)
        ∘[ sk ]ₛ ((weak-midₛ {A} Γ (Γ′ ⌊ A ⌋ Γ″))
        ∘[ sk ]ₛ (⌊⌋-assoc Γ (Γ′ , A) Γ″ ≡ₛ 𝓀)))

    -- Moving a variable to the right in the stabilised context context
    moveˢ-rₛ : ∀{A} Γ Γ′ Γ″ -> Subst 𝒮 (Γ ˢ ⌊ A ⌋ (Γ′ ⌊⌋ Γ″) ˢ) ((Γ ⌊⌋ Γ′) ˢ ⌊ A ⌋ Γ″ ˢ)
    moveˢ-rₛ {A} Γ Γ′ Γ″
        rewrite ˢ-pres-⌊⌋ Γ Γ′
              | ˢ-pres-⌊⌋ Γ′ Γ″
              | sym (⌊⌋-assoc (Γ ˢ , A) (Γ′ ˢ) (Γ″ ˢ))
        = move-rₛ (Γ ˢ) (Γ′ ˢ) (Γ″ ˢ)

    -- | Substitution

    -- Substitution for the top of the context
    sub-topₛ : ∀{A Γ} -> 𝒮 Γ A -> Subst 𝒮 (Γ , A) Γ
    sub-topₛ T = (idₛ 𝓀) ▸ T

    -- Substitution for the top of a stabilised context
    sub-topˢₛ : ∀{Γ A} -> 𝒮 Γ A -> Subst 𝒮 (Γ ˢ , A) Γ
    sub-topˢₛ {Γ} T = (Γˢ⊆Γ Γ ⊆ₛ 𝓀) ▸ T

    -- Substitution for the middle of the context
    sub-midₛ : ∀{A} Γ Γ′ -> 𝒮 (Γ ⌊⌋ Γ′) A -> Subst 𝒮 (Γ ⌊ A ⌋ Γ′) (Γ ⌊⌋ Γ′)
    sub-midₛ Γ Γ′ T = sub-topₛ T ∘[ sk ]ₛ move-rₛ Γ Γ′ ∙

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module constructs the zero R-module, and similar for weaker
-- module-like structures.
-- The intended universal property is that, given any R-module M, there
-- is a unique map into and a unique map out of the zero R-module
-- from/to M.
------------------------------------------------------------------------

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

module Algebra.Module.Construct.Zero where

open import Algebra.Bundles
open import Algebra.Module.Bundles
open import Data.Unit
open import Level

private
  variable
    r s ℓr ℓs : Level

leftSemimodule : {R : Semiring r ℓr} → LeftSemimodule R 0ℓ 0ℓ
leftSemimodule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

rightSemimodule : {S : Semiring s ℓs} → RightSemimodule S 0ℓ 0ℓ
rightSemimodule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

bisemimodule :
  {R : Semiring r ℓr} {S : Semiring s ℓs} → Bisemimodule R S 0ℓ 0ℓ
bisemimodule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

semimodule : {R : CommutativeSemiring r ℓr} → Semimodule R 0ℓ 0ℓ
semimodule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

leftModule : {R : Ring r ℓr} → LeftModule R 0ℓ 0ℓ
leftModule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

rightModule : {S : Ring s ℓs} → RightModule S 0ℓ 0ℓ
rightModule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

bimodule : {R : Ring r ℓr} {S : Ring s ℓs} → Bimodule R S 0ℓ 0ℓ
bimodule = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }

⟨module⟩ : {R : CommutativeRing r ℓr} → Module R 0ℓ 0ℓ
⟨module⟩ = record
  { Carrierᴹ = ⊤
  ; _≈ᴹ_ = λ _ _ → ⊤
  }


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

module Stream.Iterable where

open import Data
open import Data.Boolean
open import Functional
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Relator.Equals
open import Stream as Stream
open import Structure.Container.Iterable
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

instance
  Stream-iterable : Iterable(Stream(T))
  Iterable.Element  (Stream-iterable {T = T}) = T
  Iterable.isEmpty   Stream-iterable = const 𝐹
  Iterable.current   Stream-iterable = Stream.head
  Iterable.indexStep Stream-iterable = const <>
  Iterable.step      Stream-iterable = Stream.tail

instance
  Stream-prepend : Iterable.PrependConstruction(Stream-iterable{T = T})(_⊰_)
  ∃.witness Stream-prepend = [≡]-intro
  ∃.proof (Stream-prepend) = [∧]-intro [≡]-intro [≡]-intro


text:
open import Mockingbird.Forest using (Forest)

-- To Mock a Mockingbird
module Mockingbird.Problems.Chapter09 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_,_; proj₁; proj₂; ∃-syntax)
open import Function using (_$_)
open import Level using (_⊔_)
open import Relation.Nullary using (¬_)

open import Mockingbird.Forest.Birds forest

open Forest forest

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
  problem₁ : ∀ A → ∃[ B ] A IsFondOf B
  problem₁ A =
    let C = A ∘ M

        isFond : A IsFondOf (C ∙ C)
        isFond = sym $ begin
          C ∙ C        ≈⟨ isComposition A M C ⟩
          A ∙ (M ∙ C)  ≈⟨ congˡ (isMockingbird C) ⟩
          A ∙ (C ∙ C)  ∎

    in (C ∙ C , isFond)

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
  problem₂ : ∃[ E ] IsEgocentric E
  problem₂ =
    let (E , isFond) = problem₁ M

        isEgocentric : IsEgocentric E
        isEgocentric = begin
          E ∙ E  ≈˘⟨ isMockingbird E ⟩
          M ∙ E  ≈⟨ isFond ⟩
          E      ∎

    in (E , isEgocentric)

module _ ⦃ _ : HasComposition ⦄ (hasAgreeable : ∃[ A ] IsAgreeable A) where
  A = proj₁ hasAgreeable
  isAgreeable = proj₂ hasAgreeable

  problem₃ : ∀ B → ∃[ C ] B IsFondOf C
  problem₃ B =
    let D = B ∘ A
        (x , Ax≈Dx) = isAgreeable D

        isFond : B IsFondOf (A ∙ x)
        isFond = begin
          B ∙ (A ∙ x)  ≈˘⟨ isComposition B A x ⟩
          D ∙ x        ≈˘⟨ Ax≈Dx ⟩
          A ∙ x        ∎

    in (A ∙ x , isFond)

-- Bonus question of Problem 3.
C₂→HasAgreeable : ⦃ _ : HasMockingbird ⦄ → ∃[ A ] IsAgreeable A
C₂→HasAgreeable = (M , λ B → (B , isMockingbird B))

module _ ⦃ _ : HasComposition ⦄ (A B C : Bird) (Cx≈A[Bx] : IsComposition A B C) where
  problem₄ : IsAgreeable C → IsAgreeable A
  problem₄ C-isAgreeable D =
    let E = D ∘ B
        (x , Cx≈Ex) = C-isAgreeable E

        agree : Agree A D (B ∙ x)
        agree = begin
          A ∙ (B ∙ x)  ≈˘⟨ Cx≈A[Bx] x ⟩
          C ∙ x        ≈⟨ Cx≈Ex ⟩
          E ∙ x        ≈⟨ isComposition D B x ⟩
          D ∙ (B ∙ x)  ∎

    in (B ∙ x , agree)

module _ ⦃ _ : HasComposition ⦄ where
  problem₅ : ∀ A B C → ∃[ D ] (∀ x → D ∙ x ≈ A ∙ (B ∙ (C ∙ x)))
  problem₅ A B C =
    let E = B ∘ C
        D = A ∘ E
    in (D , λ x → trans (isComposition A E x) $ congˡ (isComposition B C x))

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ where
  problem₆ : ∀ A B → Compatible A B
  problem₆ A B =
    let C = A ∘ B
        (y , Cy≈y) = problem₁ C
        x = B ∙ y
    in (x , y , trans (sym (isComposition A B y)) Cy≈y , refl)

problem₇ : ∀ A → ∃[ B ] A IsFondOf B → IsHappy A
problem₇ A (B , AB≈B) = (B , B , AB≈B , AB≈B)
-- problem₇ : ∀ A → IsNormal A → IsHappy A

module _ ⦃ _ : HasComposition ⦄ where
  problem₈ : ∃[ H ] IsHappy H → ∃[ N ] IsNormal N
  problem₈ (H , x , y , Hx≈y , Hy≈x) =
    let N = H ∘ H

        isFond : N IsFondOf x
        isFond = begin
          N ∙ x        ≈⟨ isComposition H H x ⟩
          H ∙ (H ∙ x)  ≈⟨ congˡ Hx≈y ⟩
          H ∙ y        ≈⟨ Hy≈x ⟩
          x            ∎

    in (N , x , isFond)

module _ ⦃ _ : HasComposition ⦄ ⦃ _ : HasMockingbird ⦄ ⦃ _ : HasKestrel ⦄ where
  problem₉ : ∃[ A ] IsHopelesslyEgocentric A
  problem₉ =
    let (A , KA≈A) = problem₁ K

        isHopelesslyEgocentric : IsHopelesslyEgocentric A
        isHopelesslyEgocentric x = begin
          A ∙ x        ≈˘⟨ congʳ KA≈A ⟩
          (K ∙ A) ∙ x  ≈⟨ isKestrel A x ⟩
          A            ∎

    in (A , isHopelesslyEgocentric)

problem₁₀ : ∀ x y → x IsFixatedOn y → x IsFondOf y
problem₁₀ x y xz≈y = xz≈y y

problem₁₁ : ∀ K → IsKestrel K → IsEgocentric K → IsHopelesslyEgocentric K
problem₁₁ K isKestrel KK≈K x = begin
  K ∙ x        ≈˘⟨ congʳ KK≈K ⟩
  (K ∙ K) ∙ x  ≈⟨ isKestrel K x ⟩
  K            ∎

problem₁₂ : ⦃ _ : HasKestrel ⦄ → ∀ x → IsEgocentric (K ∙ x) → K IsFondOf x
problem₁₂ x [Kx][Kx]≈Kx = begin
  K ∙ x              ≈˘⟨ [Kx][Kx]≈Kx ⟩
  (K ∙ x) ∙ (K ∙ x)  ≈⟨ isKestrel x (K ∙ x) ⟩
  x                  ∎

problem₁₃ : ∀ A x y → IsHopelesslyEgocentric A → A ∙ x ≈ A ∙ y
problem₁₃ A x y Az≈A = begin
  A ∙ x  ≈⟨ Az≈A x ⟩
  A      ≈˘⟨ Az≈A y ⟩
  A ∙ y  ∎

problem₁₄ : ∀ A x y → IsHopelesslyEgocentric A → (A ∙ x) ∙ y ≈ A
problem₁₄ A x y Az≈A = begin
  (A ∙ x) ∙ y  ≈⟨ congʳ (Az≈A x) ⟩
  A ∙ y        ≈⟨ Az≈A y ⟩
  A            ∎

problem₁₅ : ∀ A x → IsHopelesslyEgocentric A → IsHopelesslyEgocentric (A ∙ x)
problem₁₅ A x Az≈A y = begin
  (A ∙ x) ∙ y  ≈⟨ congʳ (Az≈A x) ⟩
  A ∙ y        ≈⟨ Az≈A y ⟩
  A            ≈˘⟨ Az≈A x ⟩
  A ∙ x        ∎

problem₁₆ : ∀ K → IsKestrel K → ∀ x y → K ∙ x ≈ K ∙ y → x ≈ y
problem₁₆ K isKestrel x y Kx≈Ky = begin
  x            ≈˘⟨ isKestrel x K ⟩
  -- NOTE: for the right-most kestrel, we can choose any bird. (Since we know
  -- only of three birds to exist here, the only option is a combination of
  -- {K, x, y}).
  (K ∙ x) ∙ K  ≈⟨ congʳ Kx≈Ky ⟩
  (K ∙ y) ∙ K  ≈⟨ isKestrel y K ⟩
  y            ∎

problem₁₇ : ∀ A x y → A IsFixatedOn x → A IsFixatedOn y → x ≈ y
problem₁₇ A x y Az≈x Az≈y = begin
  x      ≈˘⟨ Az≈x A ⟩
  -- NOTE: for the right-most A, we can choose any bird. (In this case a
  -- combination of {A, B, C}).
  A ∙ A  ≈⟨ Az≈y A ⟩
  y      ∎

problem₁₈ : ⦃ _ : HasKestrel ⦄ → ∀ x → K IsFondOf K ∙ x → K IsFondOf x
problem₁₈ x K[Kx]≈Kx = begin
  K ∙ x              ≈˘⟨ isKestrel (K ∙ x) x ⟩
  -- NOTE: for the right-most x, we can choose any bird.
  (K ∙ (K ∙ x)) ∙ x  ≈⟨ congʳ K[Kx]≈Kx ⟩
  (K ∙ x) ∙ x        ≈⟨ isKestrel x x ⟩
  x                  ∎

-- In the circumstances of Problem 19, the only bird in the forest is the
-- kestrel.
problem₁₉ : ∀ K → IsKestrel K → IsEgocentric K → ∀ x → x ≈ K
problem₁₉ K isKestrel KK≈K x = begin
  x            ≈⟨ lemma x x ⟩
  K ∙ x        ≈˘⟨ congʳ KK≈K ⟩
  (K ∙ K) ∙ x  ≈⟨ isKestrel K x ⟩
  K            ∎
  where
    lemma : ∀ y z → y ≈ K ∙ z
    lemma y z = begin
      y                  ≈˘⟨ isKestrel y z ⟩
      (K ∙ y) ∙ z        ≈˘⟨ congʳ (congʳ KK≈K) ⟩
      ((K ∙ K) ∙ y) ∙ z  ≈⟨ congʳ (isKestrel K y) ⟩
      K ∙ z              ∎

module _ ⦃ _ : HasIdentity ⦄ where
  problem₂₀ : IsAgreeable I → ∀ A → ∃[ B ] A IsFondOf B
  problem₂₀ isAgreeable A =
    let (B , IB≈AB) = isAgreeable A

        isFond : A IsFondOf B
        isFond = begin
          A ∙ B  ≈˘⟨ IB≈AB ⟩
          I ∙ B  ≈⟨ isIdentity B ⟩
          B      ∎

    in (B , isFond)

  problem₂₁ : (∀ A → ∃[ B ] A IsFondOf B) → IsAgreeable I
  problem₂₁ isFond A =
    let (B , AB≈B) = isFond A

        agree : I ∙ B ≈ A ∙ B
        agree = begin
          I ∙ B  ≈⟨ isIdentity B ⟩
          B      ≈˘⟨ AB≈B ⟩
          A ∙ B  ∎

    in (B , agree)

  problem₂₂-1 : (∀ A B → Compatible A B) → ∀ A → IsNormal A
  problem₂₂-1 compatible A =
    let (x , y , Ix≈y , Ay≈x) = compatible I A

        isFond : A IsFondOf y
        isFond = begin
          A ∙ y  ≈⟨ Ay≈x ⟩
          x      ≈˘⟨ isIdentity x ⟩
          I ∙ x  ≈⟨ Ix≈y ⟩
          y      ∎
    in (y , isFond)

  problem₂₂-2 : (∀ A B → Compatible A B) → IsAgreeable I
  problem₂₂-2 compatible A =
    let (x , y , Ix≈y , Ay≈x) = compatible I A

        agree : Agree I A y
        agree = begin
          I ∙ y  ≈⟨ isIdentity y ⟩
          y      ≈˘⟨ Ix≈y ⟩
          I ∙ x  ≈⟨ isIdentity x ⟩
          x      ≈˘⟨ Ay≈x ⟩
          A ∙ y  ∎

    in (y , agree)

  problem₂₃ : IsHopelesslyEgocentric I → ∀ x → I ≈ x
  problem₂₃ isHopelesslyEgocentric x = begin
    I      ≈˘⟨ isHopelesslyEgocentric x ⟩
    I ∙ x  ≈⟨ isIdentity x ⟩
    x      ∎

module _ ⦃ _ : HasLark ⦄ ⦃ _ : HasIdentity ⦄ where
  problem₂₄ : HasMockingbird
  problem₂₄ = record
    { M = L ∙ I
    ; isMockingbird = λ x → begin
        (L ∙ I) ∙ x  ≈⟨ isLark I x ⟩
        I ∙ (x ∙ x)  ≈⟨ isIdentity (x ∙ x) ⟩
        x ∙ x        ∎
    }

module _ ⦃ _ : HasLark ⦄ where
  problem₂₅ : ∀ x → IsNormal x
  problem₂₅ x =
    let isFond : x IsFondOf (L ∙ x) ∙ (L ∙ x)
        isFond = begin
          x ∙ ((L ∙ x) ∙ (L ∙ x))  ≈˘⟨ isLark x (L ∙ x) ⟩
          (L ∙ x) ∙ (L ∙ x)        ∎
    in ((L ∙ x) ∙ (L ∙ x) , isFond)

  problem₂₆ : IsHopelesslyEgocentric L → ∀ x → x IsFondOf L
  problem₂₆ isHopelesslyEgocentric x = begin
    x ∙ L        ≈˘⟨ congˡ $ isHopelesslyEgocentric L ⟩
    x ∙ (L ∙ L)  ≈˘⟨ isLark x L ⟩
    (L ∙ x) ∙ L  ≈⟨ congʳ $ isHopelesslyEgocentric x ⟩
    L ∙ L        ≈⟨ isHopelesslyEgocentric L ⟩
    L            ∎

module _ ⦃ _ : HasLark ⦄ ⦃ _ : HasKestrel ⦄ where
  problem₂₇ : L ≉ K → ¬ L IsFondOf K
  problem₂₇ L≉K isFond =
    let K-fondOf-KK : K IsFondOf K ∙ K
        K-fondOf-KK = begin
          K ∙ (K ∙ K)              ≈˘⟨ congʳ isFond ⟩
          (L ∙ K) ∙ (K ∙ K)        ≈⟨ isLark K (K ∙ K) ⟩
          K ∙ ((K ∙ K) ∙ (K ∙ K))  ≈⟨ congˡ $ isKestrel K (K ∙ K) ⟩
          K ∙ K                    ∎

        isEgocentric : IsEgocentric K
        isEgocentric = problem₁₈ K K-fondOf-KK

        L≈K : L ≈ K
        L≈K = problem₁₉ K isKestrel isEgocentric L

    in L≉K L≈K

  problem₂₈ : K IsFondOf L → ∀ x → x IsFondOf L
  problem₂₈ KL≈L =
    let isHopelesslyEgocentric : IsHopelesslyEgocentric L
        isHopelesslyEgocentric y = begin
          L ∙ y        ≈˘⟨ congʳ KL≈L ⟩
          (K ∙ L) ∙ y  ≈⟨ isKestrel L y ⟩
          L            ∎
    in problem₂₆ isHopelesslyEgocentric

module _ ⦃ _ : HasLark ⦄ where
  problem₂₉ : ∃[ x ] IsEgocentric x
  problem₂₉ =
    let (y , [LL]y≈y) = problem₂₅ (L ∙ L)

        isEgocentric : IsEgocentric (y ∙ y)
        isEgocentric = begin
          (y ∙ y) ∙ (y ∙ y)  ≈˘⟨ isLark (y ∙ y) y ⟩
          (L ∙ (y ∙ y)) ∙ y  ≈˘⟨ congʳ (isLark L y) ⟩
          ((L ∙ L) ∙ y) ∙ y  ≈⟨ congʳ [LL]y≈y ⟩
          y ∙ y              ∎

        -- The expression of yy in terms of L and brackets.
        _  : y ∙ y ≈ ((L ∙ (L ∙ L)) ∙ (L ∙ (L ∙ L))) ∙ ((L ∙ (L ∙ L)) ∙ (L ∙ (L ∙ L)))
        _ = refl

    in (y ∙ y , isEgocentric)

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
module Web.URI.Scheme.Primitive where

postulate Scheme? : Set
{-# COMPILED_TYPE Scheme? String #-}

postulate http: : Scheme?
{-# COMPILED http: "http:" #-}

postulate https: : Scheme?
{-# COMPILED https: "https:" #-}

postulate ε : Scheme?
{-# COMPILED ε "" #-}

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Util.Util
import      LibraBFT.Yasm.Types as LYT
open import Optics.All

-- This module provides some scaffolding to define the handlers for our fake/simple
-- "implementation" and connect them to the interface of the SystemModel.

module LibraBFT.Impl.Handle where
 open import LibraBFT.Impl.Consensus.RoundManager
 open RWST-do

 open EpochConfig

 record GenesisInfo : Set where
   constructor mkGenInfo
   field
     -- TODO-1 : Nodes, PKs for initial epoch
     -- TODO-1 : Faults to tolerate (or quorum size?)
     genQC      : QuorumCert            -- We use the same genesis QC for both highestQC and
                                        -- highestCommitCert.
 open GenesisInfo

 postulate -- valid assumption
   -- We postulate the existence of GenesisInfo known to all
   -- TODO: construct one or write a function that generates one from some parameters.
   genInfo : GenesisInfo

 postulate -- TODO-2: define GenesisInfo to match implementation and write these functions
   initVV  : GenesisInfo → ValidatorVerifier
   init-EC : GenesisInfo → EpochConfig

 data ∈GenInfo : Signature → Set where
  inGenQC : ∀ {vs} → vs ∈ qcVotes (genQC genInfo) → ∈GenInfo (proj₂ vs)

 open import LibraBFT.Abstract.Records UID _≟UID_ NodeId
                                       (init-EC genInfo)
                                       (ConcreteVoteEvidence (init-EC genInfo))
                                       as Abs using ()

 postulate -- TODO-1 : prove
   ∈GenInfo? : (sig : Signature) → Dec (∈GenInfo sig)

 postulate -- TODO-1: prove after defining genInfo
   genVotesRound≡0     : ∀ {pk v}
                      → (wvs : WithVerSig pk v)
                      → ∈GenInfo (ver-signature wvs)
                      → v ^∙ vRound ≡ 0
   genVotesConsistent : (v1 v2 : Vote)
                      → ∈GenInfo (₋vSignature v1) → ∈GenInfo (₋vSignature v2)
                      → v1 ^∙ vProposedId ≡ v2 ^∙ vProposedId

 postulate -- TODO-1: reasonable assumption that some RoundManager exists, though we could prove
           -- it by construction; eventually we will construct an entire RoundManager, so
           -- this won't be needed

 -- This represents an uninitialised RoundManager, about which we know nothing, which we use as
 -- the initial RoundManager for every peer until it is initialised.
   fakeRM : RoundManager

 initSR : SafetyRules
 initSR =  over (srPersistentStorage ∙ pssSafetyData ∙ sdEpoch) (const 1)
                (over (srPersistentStorage ∙ pssSafetyData ∙ sdLastVotedRound) (const 0)
                      (₋rmSafetyRules (₋rmEC fakeRM)))

 initRMEC : RoundManagerEC
 initRMEC = RoundManagerEC∙new (EpochState∙new 1 (initVV genInfo)) initSR

 postulate -- TODO-2 : prove these once initRMEC is defined directly
   init-EC-epoch-1  : epoch (init-EC genInfo) ≡ 1
   initRMEC-correct : RoundManagerEC-correct initRMEC

 initRM : RoundManager
 initRM = fakeRM

 -- Eventually, the initialization should establish some properties we care about, but for now we
 -- just initialise again to fakeRM, which means we cannot prove the base case for various
 -- properties, e.g., in Impl.Properties.VotesOnce
 -- TODO: create real RoundManager using GenesisInfo
 initialRoundManagerAndMessages
     : (a : Author) → GenesisInfo
     → RoundManager × List NetworkMsg
 initialRoundManagerAndMessages a _ = initRM , []

 handle : NodeId → NetworkMsg → Instant → LBFT Unit
 handle _self msg now
    with msg
 ...| P p = processProposalMsg now p
 ...| V v = processVote now v
 ...| C c = return unit            -- We don't do anything with commit messages, they are just for defining Correctness.

 initWrapper : NodeId → GenesisInfo → RoundManager × List (LYT.Action NetworkMsg)
 initWrapper nid g = ×-map₂ (List-map LYT.send) (initialRoundManagerAndMessages nid g)

 -- Note: the SystemModel allows anyone to receive any message sent, so intended recipient is ignored;
 -- it is included in the model only to facilitate future work on liveness properties, when we will need
 -- assumptions about message delivery between honest peers.
 outputToActions : RoundManager → Output → List (LYT.Action NetworkMsg)
 outputToActions rm (BroadcastProposal p) = List-map (const (LYT.send (P p)))
                                                     (List-map proj₁
                                                               (kvm-toList (:vvAddressToValidatorInfo (₋esVerifier (₋rmEpochState (₋rmEC rm))))))
 outputToActions _  (LogErr x)            = []
 outputToActions _  (SendVote v toList)   = List-map (const (LYT.send (V v))) toList

 outputsToActions : ∀ {State} → List Output → List (LYT.Action NetworkMsg)
 outputsToActions {st} = concat ∘ List-map (outputToActions st)

 runHandler : RoundManager → LBFT Unit → RoundManager × List (LYT.Action NetworkMsg)
 runHandler st handler = ×-map₂ (outputsToActions {st}) (proj₂ (LBFT-run handler st))

 -- And ultimately, the all-knowing system layer only cares about the
 -- step function.
 --
 -- Note that we currently do not do anything non-trivial with the timestamp.
 -- Here, we just pass 0 to `handle`.
 peerStep : NodeId → NetworkMsg → RoundManager → RoundManager × List (LYT.Action NetworkMsg)
 peerStep nid msg st = runHandler st (handle nid msg 0)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --no-positivity-check --no-termination-check #-}
module Homogenous.Base where
-- module Homogenous.Base(Arity, Sig, T, Intro) where

import TYPE
import PolyDepPrelude

open PolyDepPrelude using
  ( Absurd
  ; Unit; unit
  ; Nat; zero; suc
  ; List; nil; _::_
  ; Either; left; right
  ; Pair; pair)

-- A homogenous algebra can be represented by a list of arities
--   (natural numbers)

Arity : Set
Arity = Nat

Sig   : Set
Sig   = List Arity

-- Many definitions below come in pairs - one for Arity and one for
-- Sig - where name of the first one ends in a (as in Arity) :
--   funa : Arity -> ...
--   fun  : Sig -> ...

-- (Fa n,Fa1 n) is the functor "n-tuple of same type" or
--                 "vector of length n" or "(^n)"

Fa : (n : Arity) -> Set -> Set
Fa (zero)  X = Unit
Fa (suc m) X = Pair X (Fa m X)

 ----------------------------------------------------------------
Fa1 : (n : Arity) -> {a b : Set} -> (a -> b) -> Fa n a -> Fa n b
Fa1 (zero)  f (unit)         = unit
Fa1 (suc m) f (pair fst snd) = pair (f fst) (Fa1 m f snd)

-- (F fi, F1 fi) is the pattern functor for a homogenous algebra

F : (fi : Sig)(X : Set) -> Set
F (nil)      X = Absurd
F (n :: fi') X = Either (Fa n X) (F fi' X)

F1 : (fi : Sig){a b : Set}(f : a -> b)(x : F fi a) -> F fi b
F1 (nil)      f ()        -- empty
F1 (n :: ns)  f (left  t) = left  (Fa1 n f t)
F1 (n :: ns)  f (right y) = right (F1 ns f y)

-- For the definition of the recursor R we need family-level
-- variants of F and F1 : FIH and Fmap. As usual we define these first
-- for arities (with a postfix 'a' in the name) and then for signatures.

FIHa : (n : Arity){X : Set}(C : X -> Set)(x : Fa n X) -> Set
FIHa (zero)  C unit           = Unit
FIHa (suc m) C (pair fst snd) = Pair (C fst) (FIHa m C snd)

FIH : (fi : Sig){X : Set}(C : X -> Set)(x : F fi X) -> Set
FIH (nil)      C ()      -- empty
FIH (n :: ns)  C (left  t) = FIHa n C t
FIH (n :: ns)  C (right y) = FIH ns C y

Fmapa : (n : Arity){X : Set}{C : X -> Set}(h : (x : X) -> C x)(u : Fa n X)
      -> FIHa n C u
Fmapa (zero)  h (unit)         = unit
Fmapa (suc m) h (pair fst snd) = pair (h fst) (Fmapa m h snd)

Fmap : (fi : Sig){X : Set}{C : X -> Set}(h : (x : X) -> C x)(u : F fi X)
     -> FIH fi C u
Fmap (nil)      h () -- empty
Fmap (n :: ns)  h (left  x) = Fmapa n h x
Fmap (n :: ns)  h (right y) = Fmap ns h y

-- Finally the homogenous algebra construction itself - for each code
-- fi there is a datatype T fi and an iterator It fi

data T (fi : Sig) : Set where
  Intro : F fi (T fi) -> T fi

It : (fi : Sig){C : Set}(d : F fi C -> C) -> T fi -> C
It fi d (Intro i) = d (F1 fi (It fi d) i)

-- Mendler style iterator is also straight forward

MIt : (fi : Sig){C : Set}(s : {X : Set} -> (X -> C) -> F fi X -> C)
    -> T fi -> C
MIt fi s (Intro i) = s (MIt fi s) i

R : (fi : Sig)
    {C : T fi -> Set}
    (d : (y : F fi (T fi)) -> FIH fi C y -> C (Intro y))
    (x : T fi) -> C x
R fi d (Intro i) = d i (Fmap fi (R fi d) i)

-- Special case of FIH

FIHs : (fi : Sig) -> (T fi -> Set) -> F fi (T fi) -> Set
FIHs fi = FIH fi

-- A simple example : the inverse of Intro

out : (fi : Sig) -> T fi -> F fi (T fi)
out fi = R fi (\y p -> y)

----------------------------------------------------------------
-- Now for the Type level : define FIHa, FIH, Fmapa, Fmap again
--   (universe polymorphism, please!)

FIHaT : (n : Arity)(X : Set)(C : X -> Set1)(x : Fa n X) -> Set1
FIHaT (zero)  X C (unit)         = TYPE.Unit
FIHaT (suc m) X C (pair fst snd) = TYPE.Pair (C fst) (FIHaT m X C snd)

FIHT : (fi : Sig)(X : Set)(C : X -> Set1)(x : F fi X) -> Set1
FIHT (nil)      X C () -- empty
FIHT (n :: ns)  X C (left  t) = FIHaT n X C t
FIHT (n :: ns)  X C (right y) = FIHT ns X C y

FIHsT : (fi : Sig)(C : T fi -> Set1)(x : F fi (T fi)) -> Set1
FIHsT fi C x = FIHT fi (T fi) C x

FmapaT : (n : Arity){X : Set}{C : X -> Set1}(h : (x : X) -> C x)(u : Fa n X)
  -> FIHaT n X C u
FmapaT (zero)  h (unit)         = TYPE.unit
FmapaT (suc m) h (pair fst snd) = TYPE.pair (h fst) (FmapaT m h snd)

FmapT : (fi : Sig){X : Set}{C : X -> Set1}(h : (x : X) -> C x)(u : F fi X)
      -> FIHT fi X C u
FmapT (nil)      h () -- empty
FmapT (n :: ns)  h (left  x') = FmapaT n h x'
FmapT (n :: ns)  h (right y)  = FmapT ns h y

RT : (fi : Sig)
     {C : T fi -> Set1}
     (d : (y : F fi (T fi)) -> FIHT fi (T fi) C y -> C (Intro y))
     (x : T fi) -> C x
RT fi d (Intro i) = d i (FmapT fi (RT fi d) i)


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Naturals | Nat

type
  N : 0-ary

term
  ze   : N
  su   : N  ->  N
  nrec : N  α  (α,N).α  ->  α

theory
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
-}

module Naturals.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Naturals.Signature

private
  variable
    Γ Δ Π : Ctx
    α : NatT
    𝔛 : Familyₛ

-- Inductive term declaration
module Nat:Terms (𝔛 : Familyₛ) where

  data Nat : Familyₛ where
    var  : ℐ ⇾̣ Nat
    mvar : 𝔛 α Π → Sub Nat Π Γ → Nat α Γ

    ze   : Nat N Γ
    su   : Nat N Γ → Nat N Γ
    nrec : Nat N Γ → Nat α Γ → Nat α (α ∙ N ∙ Γ) → Nat α Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Natᵃ : MetaAlg Nat
  Natᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (zeₒ   ⋮ _)         → ze
      (suₒ   ⋮ a)         → su   a
      (nrecₒ ⋮ a , b , c) → nrec a b c
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Natᵃ = MetaAlg Natᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : Nat ⇾̣ 𝒜
    𝕊 : Sub Nat Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞  ze          = 𝑎𝑙𝑔 (zeₒ   ⋮ tt)
    𝕤𝕖𝕞 (su   a)     = 𝑎𝑙𝑔 (suₒ   ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (nrec a b c) = 𝑎𝑙𝑔 (nrecₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Natᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ Nat α Γ) → 𝕤𝕖𝕞 (Natᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (zeₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (suₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (nrecₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ Nat ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : Nat ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Natᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : Nat α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub Nat Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! ze = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (su a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (nrec a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
Nat:Syn : Syntax
Nat:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = Nat:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open Nat:Terms 𝔛 in record
    { ⊥ = Nat ⋉ Natᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax Nat:Syn public
open Nat:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Natᵃ public
open import SOAS.Metatheory Nat:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Data.Option.Iterable where

open import Data
open import Data.Option
import      Data.Option.Functions as Option
open import Functional
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Relator.Equals
open import Structure.Container.Iterable
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

instance
  Option-iterable : Iterable(Option(T))
  Iterable.Element  (Option-iterable {T = T}) = T
  Iterable.isEmpty   Option-iterable = Option.isNone
  Iterable.current   Option-iterable None     = <>
  Iterable.current   Option-iterable (Some x) = x
  Iterable.indexStep Option-iterable None     = <>
  Iterable.indexStep Option-iterable (Some _) = <>
  Iterable.step      Option-iterable None     = <>
  Iterable.step      Option-iterable (Some x) = None

instance
  Option-finite-iterable : Iterable.Finite(Option-iterable{T = T})
  ∃.witness Option-finite-iterable(_▫_) id None     = id
  ∃.witness Option-finite-iterable(_▫_) id (Some x) = x ▫ id
  ∃.proof Option-finite-iterable {iter = None}   = [≡]-intro
  ∃.proof Option-finite-iterable {iter = Some x} = [≡]-intro

instance
  Option-empty : Iterable.EmptyConstruction(Option-iterable{T = T})(None)
  Option-empty = <>