text:
module HelpDefs where

-- open import Relation.Binary.PropositionalEquality

open import StdLibStuff

open import Syntax
open import FSC
open import STT
open import DerivedProps

m-weak-h : ∀ {n} Γ₁ Γ₂ {t} → {Γ₃ : Ctx n} → Form (Γ₃ ++ Γ₁) t → Form (Γ₃ ++ (Γ₂ r++ Γ₁)) t
m-weak-h {n} Γ₁ ε = λ f → f
m-weak-h {n} Γ₁ (t' ∷ Γ₂) {t} {Γ₃} = λ f → m-weak-h {n} (t' ∷ Γ₁) Γ₂ {t} {Γ₃} (weak-i Γ₃ Γ₁ f)

m-weak2 : ∀ {n Γ₁} Γ₂ → {t : Type n} → Form Γ₁ t → Form (Γ₂ ++ Γ₁) t
m-weak2 {n} {Γ₁} ε f = f
m-weak2 {n} {Γ₁} (t' ∷ Γ₂) f = weak (m-weak2 {n} {Γ₁} Γ₂ f)

hypos-i-h : ∀ {n Γ-t₁ Γ-t₂ Γ-t₃} → FSC-Ctx n Γ-t₁ → Form (Γ-t₃ ++ (Γ-t₂ r++ Γ-t₁)) $o → Form (Γ-t₃ ++ (Γ-t₂ r++ Γ-t₁)) $o
hypos-i-h ε = λ f → f
hypos-i-h {n} {Γ-t₁} {Γ-t₂} {Γ-t₃} (h ∷h Γ) = λ f → hypos-i-h {n} {Γ-t₁} {Γ-t₂} {Γ-t₃} Γ (m-weak-h Γ-t₁ Γ-t₂ {$o} {Γ-t₃} (m-weak2 Γ-t₃ h) => f)
hypos-i-h {n} {.(t ∷ _)} {Γ-t₂} {Γ-t₃} (t ∷ Γ) = hypos-i-h {n} {_} {t ∷ Γ-t₂} {Γ-t₃} Γ

m-weak : ∀ {n Γ₁ Γ₂ t} → Form Γ₁ t → Form (Γ₂ r++ Γ₁) t
m-weak {n} {Γ₁} {Γ₂} {t} = m-weak-h {n} Γ₁ Γ₂ {t} {ε}

hypos-i : ∀ {n Γ-t₁ Γ-t₂} → FSC-Ctx n Γ-t₁ → Form (Γ-t₂ r++ Γ-t₁) $o → Form (Γ-t₂ r++ Γ-t₁) $o
hypos-i {n} {Γ-t₁} {Γ-t₂} = hypos-i-h {n} {Γ-t₁} {Γ-t₂} {ε}

hypos : ∀ {n Γ-t} → FSC-Ctx n Γ-t → Form Γ-t $o → Form Γ-t $o
hypos {n} {Γ-t} = hypos-i {n} {Γ-t} {ε}

-- Props

eq-1-i : ∀ {n} Γ₁ Γ₂ → (t : Type n) (X₁ : Form (t ∷ Γ₁) $o) (X₂ : Form Γ₁ $o) →
         X₁ ≡ weak-i {n} {$o} {t} ε Γ₁ X₂ →
         m-weak-h Γ₁ Γ₂ {$o} {t ∷ ε} X₁ ≡ weak-i {n} {$o} {t} ε (Γ₂ r++ Γ₁) (m-weak-h Γ₁ Γ₂ {$o} {ε} X₂)
eq-1-i Γ₁ ε t X₁ X₂ = λ h → h
eq-1-i Γ₁ (u ∷ Γ₂) t X₁ X₂ = λ h → eq-1-i (u ∷ Γ₁) Γ₂ t (weak-i {_} {$o} {u} (t ∷ ε) Γ₁ X₁) (weak-i {_} {$o} {u} ε Γ₁ X₂) (trans (cong (weak-i {_} {$o} {u} (t ∷ ε) Γ₁) h) (weak-weak-p-1 Γ₁ t u $o X₂))

eq-1 : ∀ {n} Γ₁ Γ₂ → (t : Type n) (X : Form Γ₁ $o) →
       m-weak-h Γ₁ Γ₂ {$o} {t ∷ ε} (weak-i {n} {$o} {t} ε Γ₁ X) ≡ weak-i {n} {$o} {t} ε (Γ₂ r++ Γ₁) (m-weak-h Γ₁ Γ₂ {$o} {ε} X)
eq-1 Γ₁ Γ₂ t X = eq-1-i Γ₁ Γ₂ t (weak-i {_} {$o} {t} ε Γ₁ X) X refl

eq-2-2 : ∀ n → (Γ-t Γ' : Ctx n) → (t : Type n) (X₁ : Form (t ∷ Γ-t) $o) (X₂ : Form Γ-t $o) →
 weak-i {n} {$o} {t} ε Γ-t X₂ ≡ X₁ →
 (h₂ : t ∷ (Γ' r++ Γ-t) ≡ (Γ' ++ (t ∷ ε)) r++ Γ-t) →
 m-weak-h Γ-t (Γ' ++ (t ∷ ε)) {$o} {ε} X₂ ≡
 subst (λ z → Form z $o) h₂ (m-weak-h Γ-t Γ' {$o} {t ∷ ε} X₁)
eq-2-2 n Γ-t ε t X₁ X₂ h refl = h
eq-2-2 n Γ-t (u ∷ Γ') t X₁ X₂ h h₂ = eq-2-2 n (u ∷ Γ-t) Γ' t (weak-i {_} {$o} {u} (t ∷ ε) Γ-t X₁) (weak-i {_} {$o} {u} ε Γ-t X₂) (
 trans (sym (weak-weak-p-1 Γ-t t u $o X₂)) (cong (weak-i {_} {$o} {u} (t ∷ ε) Γ-t) h))
 h₂

eq-2-1 : ∀ n → (Γ-t Γ' : Ctx n) → (t : Type n) (h : Form Γ-t $o) (F : Form (t ∷ (Γ' r++ Γ-t)) $o) →
         (Γ'' : Ctx n)
         (h₁₁ : Γ'' ≡ (Γ' ++ (t ∷ ε)) r++ Γ-t) →
         (h₁₂ : t ∷ (Γ' r++ Γ-t) ≡  Γ'') →
         app (app A (app N (m-weak-h Γ-t (Γ' ++ (t ∷ ε)) {$o} {ε} h))) (subst (λ z → Form z $o) h₁₁ (subst (λ z → Form z $o) h₁₂ F)) ≡
         subst (λ z → Form z $o) h₁₁ (app (app A (app N (subst (λ z → Form z $o) h₁₂ (m-weak-h Γ-t Γ' {$o} {t ∷ ε} (weak-i ε Γ-t h))))) (subst (λ z → Form z $o) h₁₂ F))
eq-2-1 n Γ-t Γ' t h F .((Γ' ++ (t ∷ ε)) r++ Γ-t) refl h₁₂ = cong (λ z → app (app A (app N z)) (subst (λ z → Form z $o) h₁₂ F)) (eq-2-2 n Γ-t Γ' t (weak-i {_} {$o} {t} ε Γ-t h) h refl h₁₂)

eq-2-i : ∀ {n} Γ-t → (t : Type n) (Γ : FSC-Ctx n Γ-t) (Γ' : Ctx n) (F : Form (t ∷ (Γ' r++ Γ-t)) $o) →
       (h₁ : t ∷ (ε ++ (Γ' r++ Γ-t)) ≡ (Γ' ++ (t ∷ ε)) r++ Γ-t) →
       hypos-i-h {n} {Γ-t} {Γ' ++ (t ∷ ε)} {ε} Γ (subst (λ z → Form z $o) h₁ F) ≡ subst (λ z → Form z $o) h₁ (hypos-i-h {n} {Γ-t} {Γ'} {t ∷ ε} Γ F)
eq-2-i .ε t ε Γ' F h₁ = refl
eq-2-i .(u ∷ _) t (u ∷ Γ) Γ' F h₁ = eq-2-i _ t Γ (u ∷ Γ') F h₁
eq-2-i Γ-t t (h ∷h Γ) Γ' F h₁ = trans (cong (hypos-i-h {_} {Γ-t} {Γ' ++ (t ∷ ε)} {ε} Γ) (eq-2-1 _ Γ-t Γ' t h F _ h₁ refl)) (eq-2-i Γ-t t Γ Γ' (app (app A (app N (m-weak-h Γ-t Γ' {$o} {t ∷ ε} (weak-i ε Γ-t h)))) F) h₁)

eq-2 : ∀ {n Γ-t} → (t : Type n) (Γ : FSC-Ctx n Γ-t) (F : Form (t ∷ Γ-t) $o) →
       hypos-i-h {n} {Γ-t} {t ∷ ε} {ε} Γ F ≡ hypos-i-h {n} {Γ-t} {ε} {t ∷ ε} Γ F
eq-2 {_} {Γ-t} t Γ F = eq-2-i {_} Γ-t t Γ ε F refl

traverse-hypos-i : ∀ {n Γ-t₁ Γ-t₂} → (F G : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → (⊢ (F => G)) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F => hypos-i {n} {Γ-t₁} {Γ-t₂} Γ G)
traverse-hypos-i F G ε h = h
traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} F G (X ∷h Γ) h = traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} X => F) (m-weak {n} {Γ-t₁} {Γ-t₂} X => G) Γ (inf-V ax-4-s h)
traverse-hypos-i {n} {.(t ∷ _)} {Γ-t₂} F G (t ∷ Γ) h = traverse-hypos-i {n} {_} {t ∷ Γ-t₂} F G Γ h

traverse-hypos : ∀ {n Γ-t} → (F G : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) → (⊢ (F => G)) → ⊢ (hypos Γ F => hypos Γ G)
traverse-hypos {n} {Γ-t} = traverse-hypos-i {n} {Γ-t} {ε}

traverse-hypos-pair-I-i : ∀ {n Γ-t₁ Γ-t₂} → (F G : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F => (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ G => hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (F & G)))
traverse-hypos-pair-I-i F G ε = lemb1 F G
traverse-hypos-pair-I-i {n} {Γ-t₁} {Γ-t₂} F G (x ∷h Γ) = inf-V (inf-V (ax-4-s {_} {_} {(hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (m-weak {n} {Γ-t₁} {Γ-t₂} x => G) => (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ ((m-weak {n} {Γ-t₁} {Γ-t₂} x => F) & (m-weak {n} {Γ-t₁} {Γ-t₂} x => G))))})
 (inf-V (ax-4-s {_} {_} {(hypos-i {n} {Γ-t₁} {Γ-t₂} Γ ((m-weak {n} {Γ-t₁} {Γ-t₂} x => F) & (m-weak {n} {Γ-t₁} {Γ-t₂} x => G)))}) (traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} ((m-weak {n} {Γ-t₁} {Γ-t₂} x => F) & (m-weak {n} {Γ-t₁} {Γ-t₂} x => G)) (m-weak {n} {Γ-t₁} {Γ-t₂} x => (F & G)) Γ (lem2 (m-weak {n} {Γ-t₁} {Γ-t₂} x) F G))))
 (traverse-hypos-pair-I-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} x => F) (m-weak {n} {Γ-t₁} {Γ-t₂} x => G) Γ)
traverse-hypos-pair-I-i {n} {.(t ∷ _)} {Γ-t₂} F G (t ∷ Γ) = traverse-hypos-pair-I-i {n} {_} {t ∷ Γ-t₂} F G Γ

traverse-hypos-pair-I : ∀ {n Γ-t} → (F G : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) → ⊢ (hypos Γ F => (hypos Γ G => hypos Γ (F & G)))
traverse-hypos-pair-I {n} {Γ-t} = traverse-hypos-pair-I-i {n} {Γ-t} {ε}

traverse-hypos-elim-i : ∀ {n Γ-t₁ Γ-t₂} → (F : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) (x : HVar Γ) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => F) => hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F)
traverse-hypos-elim-i {n} {Γ-t₁} {Γ-t₂} F .(h ∷h Γ) (zero {._} {h} {Γ}) = traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} h => (m-weak {n} {Γ-t₁} {Γ-t₂} h => F)) (m-weak {n} {Γ-t₁} {Γ-t₂} h => F) Γ (lem3 (m-weak {n} {Γ-t₁} {Γ-t₂} h) F)
traverse-hypos-elim-i {n} {Γ-t₁} {Γ-t₂} F .(h ∷h Γ) (succ {._} {h} {Γ} x) = inf-V ax-3-s (inf-V (inf-V (ax-4-s {_} {_} {~ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => (m-weak {n} {Γ-t₁} {Γ-t₂} h => F)))}) (inf-V (lem5 (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (m-weak {n} {Γ-t₁} {Γ-t₂} h => (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => F))) (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => (m-weak {n} {Γ-t₁} {Γ-t₂} h => F)))) (traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} h => (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => F)) (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x) => (m-weak {n} {Γ-t₁} {Γ-t₂} h => F)) Γ (lem4 (m-weak {n} {Γ-t₁} {Γ-t₂} h) (m-weak {n} {Γ-t₁} {Γ-t₂} (lookup-hyp Γ x)) F)))) (inf-V ax-3-s (traverse-hypos-elim-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} h => F) Γ x)))
traverse-hypos-elim-i {n} {.(t ∷ _)} {Γ-t₂} F (t ∷ Γ) (skip x) = traverse-hypos-elim-i {n} {_} {t ∷ Γ-t₂} F Γ x

traverse-hypos-elim : ∀ {n Γ-t} → (F : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) (x : HVar Γ) → ⊢ (hypos Γ (lookup-hyp Γ x => F) => hypos Γ F)
traverse-hypos-elim {n} {Γ-t} = traverse-hypos-elim-i {n} {Γ-t} {ε}

traverse-hypos-use-i : ∀ {n Γ-t₁ Γ-t₂} → (F : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → ⊢ (F) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F)
traverse-hypos-use-i F ε h = h
traverse-hypos-use-i {n} {Γ-t₁} {Γ-t₂} F (X ∷h Γ) h = traverse-hypos-use-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} X => F) Γ (inf-V ax-3-s (inf-V ax-2-s h))
traverse-hypos-use-i {n} {.(t ∷ _)} {Γ-t₂} F (t ∷ Γ) h = traverse-hypos-use-i {n} {_} {t ∷ Γ-t₂} F Γ h

traverse-hypos-use : ∀ {n Γ-t} → (F : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) → ⊢ (F) → ⊢ (hypos Γ F)
traverse-hypos-use {n} {Γ-t} = traverse-hypos-use-i {n} {Γ-t} {ε}

traverse-hypos2-i : ∀ {n Γ-t₁ Γ-t₂} → (F G H : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → (⊢ (F => (G => H))) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F => (hypos-i {n} {Γ-t₁} {Γ-t₂}Γ G => hypos-i {n} {Γ-t₁} {Γ-t₂} Γ H))
traverse-hypos2-i F G H ε imp = imp
traverse-hypos2-i {n} {Γ-t₁} {Γ-t₂} F G H (X ∷h Γ) imp = traverse-hypos2-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} X => F) (m-weak {n} {Γ-t₁} {Γ-t₂} X => G) (m-weak {n} {Γ-t₁} {Γ-t₂} X => H) Γ (inf-V (lem8 (m-weak {n} {Γ-t₁} {Γ-t₂} X) F G H) imp)
traverse-hypos2-i {n} {.(t ∷ _)} {Γ-t₂} F G H (t ∷ Γ) imp = traverse-hypos2-i {n} {_} {t ∷ Γ-t₂} F G H Γ imp

traverse-hypos2 : ∀ {n Γ-t} → (F G H : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) → (⊢ (F => (G => H))) → ⊢ (hypos Γ F => (hypos Γ G => hypos Γ H))
traverse-hypos2 {n} {Γ-t} = traverse-hypos2-i {n} {Γ-t} {ε}

traverse-hypos3-i : ∀ {n Γ-t₁ Γ-t₂} → (F G H I : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → (⊢ (F => (G => (H => I)))) → ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ F => (hypos-i {n} {Γ-t₁} {Γ-t₂}Γ G => (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ H => hypos-i {n} {Γ-t₁} {Γ-t₂} Γ I)))
traverse-hypos3-i F G H I ε imp = imp
traverse-hypos3-i {n} {Γ-t₁} {Γ-t₂} F G H I (X ∷h Γ) imp = traverse-hypos3-i {n} {Γ-t₁} {Γ-t₂} (m-weak {n} {Γ-t₁} {Γ-t₂} X => F) (m-weak {n} {Γ-t₁} {Γ-t₂} X => G) (m-weak {n} {Γ-t₁} {Γ-t₂} X => H) (m-weak {n} {Γ-t₁} {Γ-t₂} X => I) Γ (inf-V (lem8-3 (m-weak {n} {Γ-t₁} {Γ-t₂} X) F G H I) imp)
traverse-hypos3-i {n} {.(t ∷ _)} {Γ-t₂} F G H I (t ∷ Γ) imp = traverse-hypos3-i {n} {_} {t ∷ Γ-t₂} F G H I Γ imp

traverse-hypos3 : ∀ {n Γ-t} → (F G H I : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) → (⊢ (F => (G => (H => I)))) → ⊢ (hypos Γ F => (hypos Γ G => (hypos Γ H => hypos Γ I)))
traverse-hypos3 {n} {Γ-t} = traverse-hypos3-i {n} {Γ-t} {ε}

traverse-=>-I-dep-i : ∀ {n Γ-t₁ Γ-t₂} → (t : Type n) (F : Form (t ∷ (Γ-t₂ r++ Γ-t₁)) $o) (Γ : FSC-Ctx n Γ-t₁) →
                      ⊢ (![ t ] hypos-i-h {n} {Γ-t₁} {Γ-t₂} {t ∷ ε} Γ F) →
                      ⊢ (hypos-i {n} {Γ-t₁} {Γ-t₂} Γ (![ t ] F))
traverse-=>-I-dep-i t F ε h = h
traverse-=>-I-dep-i {n} {Γ-t₁} {Γ-t₂} t F (X ∷h Γ) h = inf-V (traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} (![ t ] (weak (m-weak {n} {Γ-t₁} {Γ-t₂} X) => F)) (m-weak {n} {Γ-t₁} {Γ-t₂} X => (![ t ] F)) Γ (ax-6-s {_} {_} {_} {~ (m-weak {n} {Γ-t₁} {Γ-t₂} X)} {F})) (traverse-=>-I-dep-i {n} {Γ-t₁} {Γ-t₂} t (weak (m-weak {n} {Γ-t₁} {Γ-t₂} X) => F) Γ
 (subst (λ z → ⊢_ {n} {_r++_ {n} Γ-t₂ Γ-t₁} (app {n} {_>_ {_} t ($o {_})} {$o {_}} {_r++_ {n} Γ-t₂ Γ-t₁} (Π {n} {t} {_r++_ {n} Γ-t₂ Γ-t₁}) (lam {n} {$o {_}} {_r++_ {n} Γ-t₂ Γ-t₁} t  ((hypos-i-h {n} {Γ-t₁} {Γ-t₂} {_∷_ {_} t (ε {_})} Γ (_=>_ {_} {_∷_ {_} t (_r++_ {n} Γ-t₂ Γ-t₁)} z F))))))
        (eq-1 {n} Γ-t₁ Γ-t₂ t X) h))
traverse-=>-I-dep-i {n} {.(t' ∷ _)} {Γ-t₂} t F (t' ∷ Γ) h = traverse-=>-I-dep-i {n} {_} {t' ∷ Γ-t₂} t F Γ h

traverse-=>-I-dep : ∀ {n Γ-t} → (t : Type n) (F : Form (t ∷ Γ-t) $o) (Γ : FSC-Ctx n Γ-t) →
                    ⊢ (![ t ] hypos (t ∷ Γ) F) → ⊢ (hypos Γ (![ t ] F))
traverse-=>-I-dep {n} {Γ-t} t F Γ h = traverse-=>-I-dep-i {n} {Γ-t} {ε} t F Γ (subst (λ z → ⊢ app Π (lam t (z))) (eq-2 t Γ F) h)

traverse-=>-I-dep'-I2 : ∀ {n Γ-t₁ Γ-t₂} → (t : Type n) (F : Form (t ∷ (Γ-t₂ r++ Γ-t₁)) $o) (G : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) →
                        (⊢ (F => weak-i ε (Γ-t₂ r++ Γ-t₁) G)) →
                        ⊢ (hypos-i-h {n} {Γ-t₁} {Γ-t₂} {t ∷ ε} Γ F => weak-i ε (Γ-t₂ r++ Γ-t₁) (hypos-i-h {n} {Γ-t₁} {Γ-t₂} {ε} Γ G))
traverse-=>-I-dep'-I2 t F G ε h = h
traverse-=>-I-dep'-I2 {n} {t' ∷ Γ-t₁} {Γ-t₂} t F G (.t' ∷ Γ) h = traverse-=>-I-dep'-I2 {n} {Γ-t₁} {t' ∷ Γ-t₂} t F G Γ h
traverse-=>-I-dep'-I2 {n} {Γ-t₁} {Γ-t₂} t F G (X ∷h Γ) h = traverse-=>-I-dep'-I2 {n} {Γ-t₁} {Γ-t₂} t (m-weak-h Γ-t₁ Γ-t₂ {$o} {t ∷ ε} (weak-i ε Γ-t₁ X) => F) (m-weak-h Γ-t₁ Γ-t₂ {$o} {ε} X => G) Γ (
 subst (λ z → ⊢ ((m-weak-h Γ-t₁ Γ-t₂ {$o} {t ∷ ε} (weak-i ε Γ-t₁ X) => F) => (z => weak-i ε (Γ-t₂ r++ Γ-t₁) G))) (eq-1 Γ-t₁ Γ-t₂ t X) (inf-V ax-4-s h))

traverse-=>-I-dep'-I : ∀ {n Γ-t} → (t : Type n) (F : Form (t ∷ Γ-t) $o) (G : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) →
                       (⊢ (F => weak-i ε Γ-t G)) →
                       ⊢ (hypos (t ∷ Γ) F => weak-i ε Γ-t (hypos Γ G))
traverse-=>-I-dep'-I {n} {Γ-t} t F G Γ h = subst (λ z → ⊢ (z => weak-i ε Γ-t (hypos Γ G))) (sym (eq-2 t Γ F)) (traverse-=>-I-dep'-I2 {n} {Γ-t} {ε} t F G Γ h)

traverse-=>-I-dep' : ∀ {n Γ-t} → (t : Type n) (F : Form Γ-t (t > $o)) (Γ : FSC-Ctx n Γ-t) →
                     ⊢ hypos (t ∷ Γ) (weak F · $ this {refl}) → ⊢ (hypos Γ (!'[ t ] F))
traverse-=>-I-dep' t F Γ h = extend-context t (inf-V (traverse-=>-I-dep'-I t (weak F · $ this {refl}) (!'[ t ] F) Γ (inf-VI this (occurs-p-2 F) refl)) h)

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

traverse-hypos-eq-=>-I-i : ∀ {n Γ-t₁ Γ-t₂} → {t : Type n} → (F : Form (t ∷ (Γ-t₂ r++ Γ-t₁)) $o) (G : Form (Γ-t₂ r++ Γ-t₁) $o) (Γ : FSC-Ctx n Γ-t₁) → (⊢ (F => weak G)) → ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂} {t ∷ ε} Γ F → ⊢ hypos-i {n} {Γ-t₁} {Γ-t₂} Γ G
traverse-hypos-eq-=>-I-i {n} {.ε} {Γ-t₂} {t} F G ε = λ z z' → extend-context t (inf-V z z')
traverse-hypos-eq-=>-I-i {n} {Γ-t₁} {Γ-t₂} {t} F G (X ∷h Γ) = λ h → traverse-hypos-eq-=>-I-i {n} {Γ-t₁} {Γ-t₂} {t} (m-weak-h {_} Γ-t₁ Γ-t₂ {_} {t ∷ ε} (m-weak2 (t ∷ ε) X) => F) (m-weak-h {_} Γ-t₁ Γ-t₂ {_} {ε} (m-weak2 ε X) => G) Γ (subst (λ z → ⊢ ((m-weak-h {_} Γ-t₁ Γ-t₂ {_} {t ∷ ε} (m-weak2 (t ∷ ε) X) => F) => (z => weak G))) (eq-1 Γ-t₁ Γ-t₂ t X) (inf-V ax-4-s h))
traverse-hypos-eq-=>-I-i {n} {t₁ ∷ Γ-t₁} {Γ-t₂} {t} F G ((.t₁) ∷ Γ) = traverse-hypos-eq-=>-I-i {n} {Γ-t₁} {t₁ ∷ Γ-t₂} {t} F G Γ

traverse-hypos-eq-=>-I'' : ∀ {n Γ-t} → {t : Type n} (F : Form (t ∷ Γ-t) $o) (G : Form Γ-t $o) (Γ : FSC-Ctx n Γ-t) →
 ⊢ (F => weak G) →
 ⊢ hypos (t ∷ Γ) F → ⊢ hypos Γ G
traverse-hypos-eq-=>-I'' {n} {Γ-t} F G Γ = λ h₁ h₂ → traverse-hypos-eq-=>-I-i {n} {Γ-t} {ε} F G Γ h₁ (subst (λ z → ⊢ z) (eq-2 _ Γ F) h₂)

tst3-ε : ∀ {n} → (Γ₁ Γ₂ : Ctx n) (F : Form Γ₁ $o)
 (eq : Γ₁ ≡ Γ₂) →
 ⊢_ {n} {Γ₂} (subst (λ z → Form z $o) eq F) →
 ⊢_ {n} {Γ₁} F
tst3-ε .Γ₂ Γ₂ F refl p = p  -- rewrite eq = p

tst3b : ∀ {n} → {t u : Type n} → (Γ-t₁ Γ-t₂ : Ctx n) (X : Form Γ-t₁ u) →
 (eq2 : t ∷ (Γ-t₂ r++ Γ-t₁) ≡ (Γ-t₂ ++ (t ∷ ε)) r++ Γ-t₁) →
 m-weak-h Γ-t₁ (Γ-t₂ ++ (t ∷ ε)) {_} {ε} X ≡
 subst (λ z → Form z u) eq2 (weak-i ε (Γ-t₂ r++ Γ-t₁) (m-weak-h Γ-t₁ Γ-t₂ {_} {ε} X))
tst3b Γ-t₁ ε X refl = refl
tst3b Γ-t₁ (v ∷ Γ-t₂) X eq2 = tst3b (v ∷ Γ-t₁) Γ-t₂ (weak-i ε Γ-t₁ X) eq2

tst3'-∷h : ∀ {n Γ-t₁ Γ-t₂} → {t : Type n} (F : Form (t ∷ (Γ-t₂ r++ Γ-t₁)) $o) (Γ : FSC-Ctx n Γ-t₁) →
 (X : Form Γ-t₁ $o)
 (Γ1 : Ctx n)
 (eq1 : Γ1 ≡ (Γ-t₂ ++ (t ∷ ε)) r++ Γ-t₁)
 (eq2 : t ∷ (Γ-t₂ r++ Γ-t₁) ≡ Γ1)
 (p : ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂ ++ (t ∷ ε)} {ε} Γ (app (app A (app N (m-weak-h {n} Γ-t₁ (Γ-t₂ ++ (t ∷ ε)) {$o} {ε} X))) (subst (λ z → Form z $o) eq1 (subst (λ z → Form z $o) eq2 F)))) →
 ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂ ++ (t ∷ ε)} {ε} Γ (subst (λ z → Form z $o) eq1 (app (app A (app N (subst (λ z → Form z $o) eq2 (weak-i ε (Γ-t₂ r++ Γ-t₁) (m-weak-h Γ-t₁ Γ-t₂ {$o} {ε} X))))) (subst (λ z → Form z $o) eq2 F)))
tst3'-∷h {n} {Γ-t₁} {Γ-t₂} {t} F Γ X .((Γ-t₂ ++ (t ∷ ε)) r++ Γ-t₁) refl eq2 p = subst (λ z → ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂ ++ (t ∷ ε)} {ε} Γ (app (app A (app N z)) (subst (λ z → Form z $o) eq2 F))) (tst3b {n} {t} Γ-t₁ Γ-t₂ X eq2) p

tst3' : ∀ {n Γ-t₁ Γ-t₂} → {t : Type n} (F : Form (t ∷ (Γ-t₂ r++ Γ-t₁)) $o) (Γ : FSC-Ctx n Γ-t₁) →
 (eq : t ∷ (Γ-t₂ r++ Γ-t₁) ≡ (Γ-t₂ ++ (t ∷ ε)) r++ Γ-t₁) →
 ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂ ++ (t ∷ ε)} {ε} Γ (subst (λ z → Form z $o) eq F) →
 ⊢ hypos-i-h {n} {Γ-t₁} {Γ-t₂} {ε} Γ (![ t ] F)
tst3' {n} {ε} {Γ-t₂} {t} F ε eq = λ p → inf-VI-s (tst3-ε {n} (t ∷ (Γ-t₂ r++ ε)) ((Γ-t₂ ++ (t ∷ ε)) r++ ε) F eq p)
tst3' {n} {t' ∷ Γ-t₁} {Γ-t₂} F ((.t') ∷ Γ) eq = tst3' {n} {Γ-t₁} {t' ∷ Γ-t₂} F Γ eq
tst3' {n} {Γ-t₁} {Γ-t₂} {t} F (X ∷h Γ) eq = λ p → inf-V (traverse-hypos-i {n} {Γ-t₁} {Γ-t₂} (![ t ] (weak (~ (m-weak-h Γ-t₁ Γ-t₂ {_} {ε} X)) || F)) (m-weak-h {n} Γ-t₁ Γ-t₂ {$o} {ε} X => ![ t ] F) Γ (inf-V (inf-V ax-4-s ax-6-s) (lem2h2hb _))) (tst3' {n} {Γ-t₁} {Γ-t₂} {t} (weak (~ (m-weak-h Γ-t₁ Γ-t₂ {_} {ε} X)) || F) Γ eq (tst3'-∷h {n} {Γ-t₁} {Γ-t₂} {t} F Γ X (t ∷ (Γ-t₂ r++ Γ-t₁)) eq refl p))

traverse-hypos-eq-=>-I : ∀ {n Γ-t} → {t₁ t₂ : Type n} (F₁ F₂ : Form (t₁ ∷ Γ-t) t₂) (Γ : FSC-Ctx n Γ-t) →
 ⊢ hypos (t₁ ∷ Γ) (F₁ == F₂) →
 ⊢ hypos Γ (lam t₁ F₁ == lam t₁ F₂)
traverse-hypos-eq-=>-I {_} {Γ-t} {t₁} {t₂} F₁ F₂ Γ p = inf-V (traverse-hypos (![ t₁ ] (F₁ == F₂)) (lam t₁ F₁ == lam t₁ F₂) Γ ax-10-b-s) (tst3' {_} {Γ-t} {ε} (F₁ == F₂) Γ refl p)

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
module Bool where

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Rational.Base where

open import Cubical.Relation.Nullary
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.HITs.Ints.QuoInt
open import Cubical.Data.Nat
open import Cubical.Data.Empty
open import Cubical.Data.Unit

data ℚ : Type₀ where
  con : (u : ℤ) (a : ℤ) → ¬ (a ≡ pos 0) → ℚ
  path : ∀ u a v b {p q} → (u *ℤ b) ≡ (v *ℤ a) → con u a p ≡ con v b q
  trunc : isSet ℚ

int : ℤ → ℚ
int z = con z (pos 1) \ p → snotz (cong abs p)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import lib.Basics

module lib.types.Paths where

{- ! is an equivalence and works on ≠ -}
module _ {i} {A : Type i} {x y : A} where

  !-equiv : (x == y) ≃ (y == x)
  !-equiv = equiv ! ! !-! !-!

  ≠-inv : (x ≠ y) → (y ≠ x)
  ≠-inv x≠y y=x = x≠y (! y=x)

{- Pre- and post- concatenation are equivalences -}
module _ {i} {A : Type i} {x y z : A} where

  pre∙-is-equiv : (p : x == y) → is-equiv (λ (q : y == z) → p ∙ q)
  pre∙-is-equiv p = is-eq (λ q → p ∙ q) (λ r → ! p ∙ r) f-g g-f
    where f-g : ∀ r → p ∙ ! p ∙ r == r
          f-g r = ! (∙-assoc p (! p) r) ∙ ap (λ s → s ∙ r) (!-inv-r p)

          g-f : ∀ q → ! p ∙ p ∙ q == q
          g-f q = ! (∙-assoc (! p) p q) ∙ ap (λ s → s ∙ q) (!-inv-l p)

  pre∙-equiv : (p : x == y) → (y == z) ≃ (x == z)
  pre∙-equiv p = ((λ q → p ∙ q) , pre∙-is-equiv p)

  post∙-is-equiv : (p : y == z) → is-equiv (λ (q : x == y) → q ∙ p)
  post∙-is-equiv p = is-eq (λ q → q ∙ p) (λ r → r ∙ ! p) f-g g-f
    where f-g : ∀ r → (r ∙ ! p) ∙ p == r
          f-g r = ∙-assoc r (! p) p ∙ ap (λ s → r ∙ s) (!-inv-l p) ∙ ∙-unit-r r

          g-f : ∀ q → (q ∙ p) ∙ ! p == q
          g-f q = ∙-assoc q p (! p) ∙ ap (λ s → q ∙ s) (!-inv-r p) ∙ ∙-unit-r q

  post∙-equiv : (p : y == z) → (x == y) ≃ (x == z)
  post∙-equiv p = ((λ q → q ∙ p) , post∙-is-equiv p)

  pre∙'-is-equiv : (p : x == y) → is-equiv (λ (q : y == z) → p ∙' q)
  pre∙'-is-equiv p = is-eq (λ q → p ∙' q) (λ r → ! p ∙' r) f-g g-f
    where f-g : ∀ r → p ∙' ! p ∙' r == r
          f-g r = ! (∙'-assoc p (! p) r) ∙ ap (λ s → s ∙' r) (!-inv'-r p)
                  ∙ ∙'-unit-l r

          g-f : ∀ q → ! p ∙' p ∙' q == q
          g-f q = ! (∙'-assoc (! p) p q) ∙ ap (λ s → s ∙' q) (!-inv'-l p)
                  ∙ ∙'-unit-l q

  pre∙'-equiv : (p : x == y) → (y == z) ≃ (x == z)
  pre∙'-equiv p = ((λ q → p ∙' q) , pre∙'-is-equiv p)

  post∙'-is-equiv : (p : y == z) → is-equiv (λ (q : x == y) → q ∙' p)
  post∙'-is-equiv p = is-eq (λ q → q ∙' p) (λ r → r ∙' ! p) f-g g-f
    where f-g : ∀ r → (r ∙' ! p) ∙' p == r
          f-g r = ∙'-assoc r (! p) p ∙ ap (λ s → r ∙' s) (!-inv'-l p)

          g-f : ∀ q → (q ∙' p) ∙' ! p == q
          g-f q = ∙'-assoc q p (! p) ∙ ap (λ s → q ∙' s) (!-inv'-r p)

  post∙'-equiv : (p : y == z) → (x == y) ≃ (x == z)
  post∙'-equiv p = ((λ q → q ∙' p) , post∙'-is-equiv p)

module _ {i j} {A : Type i} {B : Type j}
  {f : A → B} {x y : A} {b : B} where

  ↓-app=cst-in : {p : x == y} {u : f x == b} {v : f y == b}
    → u == (ap f p ∙ v)
    → (u == v [ (λ x → f x == b) ↓ p ])
  ↓-app=cst-in {p = idp} q = q

  ↓-app=cst-out : {p : x == y} {u : f x == b} {v : f y == b}
    → (u == v [ (λ x → f x == b) ↓ p ])
    → u == (ap f p ∙ v)
  ↓-app=cst-out {p = idp} r = r

  ↓-app=cst-β : {p : x == y} {u : f x == b} {v : f y == b}
    → (q : u == (ap f p ∙ v))
    → ↓-app=cst-out {p = p} (↓-app=cst-in q) == q
  ↓-app=cst-β {p = idp} q = idp

  ↓-app=cst-η : {p : x == y} {u : f x == b} {v : f y == b}
    → (q : u == v [ (λ x → f x == b) ↓ p ])
    → ↓-app=cst-in (↓-app=cst-out q) == q
  ↓-app=cst-η {p = idp} q = idp

  ↓-app=cst-econv : {p : x == y} {u : f x == b} {v : f y == b}
    → (u == (ap f p ∙ v)) ≃ (u == v [ (λ x → f x == b) ↓ p ])
  ↓-app=cst-econv {p = p} = equiv ↓-app=cst-in ↓-app=cst-out
    (↓-app=cst-η {p = p}) (↓-app=cst-β {p = p})

  ↓-cst=app-in : {p : x == y} {u : b == f x} {v : b == f y}
    → (u ∙' ap f p) == v
    → (u == v [ (λ x → b == f x) ↓ p ])
  ↓-cst=app-in {p = idp} q = q

  ↓-cst=app-out : {p : x == y} {u : b == f x} {v : b == f y}
    → (u == v [ (λ x → b == f x) ↓ p ])
    → (u ∙' ap f p) == v
  ↓-cst=app-out {p = idp} r = r

  ↓-cst=app-econv : {p : x == y} {u : b == f x} {v : b == f y}
    → ((u ∙' ap f p) == v) ≃ (u == v [ (λ x → b == f x) ↓ p ])
  ↓-cst=app-econv {p = idp} = equiv ↓-cst=app-in ↓-cst=app-out
     (λ _ → idp) (λ _ → idp)

{- alternative versions -}

module _ {i j} {A : Type i} {B : Type j}
  {f : A → B} {x y : A} {b : B} where

  ↓-app=cst-in' : {p : x == y} {u : f x == b} {v : f y == b}
    → u == (ap f p ∙' v)
    → (u == v [ (λ x → f x == b) ↓ p ])
  ↓-app=cst-in' {p = idp} {v = idp} q = q

  ↓-app=cst-out' : {p : x == y} {u : f x == b} {v : f y == b}
    → (u == v [ (λ x → f x == b) ↓ p ])
    → u == (ap f p ∙' v)
  ↓-app=cst-out' {p = idp} {v = idp} r = r

  ↓-app=cst-β' : {p : x == y} {u : f x == b} {v : f y == b}
    → (q : u == (ap f p ∙' v))
    → ↓-app=cst-out' {p = p} {v = v} (↓-app=cst-in' q) == q
  ↓-app=cst-β' {p = idp} {v = idp} q = idp

  ↓-app=cst-η' : {p : x == y} {u : f x == b} {v : f y == b}
    → (q : u == v [ (λ x → f x == b) ↓ p ])
    → ↓-app=cst-in' (↓-app=cst-out' q) == q
  ↓-app=cst-η' {p = idp} {v = idp} q = idp

  ↓-cst=app-in' : {p : x == y} {u : b == f x} {v : b == f y}
    → (u ∙ ap f p) == v
    → (u == v [ (λ x → b == f x) ↓ p ])
  ↓-cst=app-in' {p = idp} {u = idp} q = q

  ↓-cst=app-out' : {p : x == y} {u : b == f x} {v : b == f y}
    → (u == v [ (λ x → b == f x) ↓ p ])
    → (u ∙ ap f p) == v
  ↓-cst=app-out' {p = idp} {u = idp} r = r

module _ {i} {A : Type i} where

  ↓-app=idf-in : {f : A → A} {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → u ∙' p == ap f p ∙ v
    → u == v [ (λ z → f z == z) ↓ p ]
  ↓-app=idf-in {p = idp} q = q

  ↓-app=idf-out : {f : A → A} {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → u == v [ (λ z → f z == z) ↓ p ]
    → u ∙' p == ap f p ∙ v
  ↓-app=idf-out {p = idp} q = q

  ↓-cst=idf-in : {a : A} {x y : A} {p : x == y} {u : a == x} {v : a == y}
    → (u ∙' p) == v
    → (u == v [ (λ x → a == x) ↓ p ])
  ↓-cst=idf-in {p = idp} q = q

  ↓-cst=idf-in' : {a : A} {x y : A} {p : x == y} {u : a == x} {v : a == y}
    → (u ∙ p) == v
    → (u == v [ (λ x → a == x) ↓ p ])
  ↓-cst=idf-in' {p = idp} q = ! (∙-unit-r _) ∙ q

  ↓-idf=cst-in : {a : A} {x y : A} {p : x == y} {u : x == a} {v : y == a}
    → u == p ∙ v
    → (u == v [ (λ x → x == a) ↓ p ])
  ↓-idf=cst-in {p = idp} q = q

  ↓-idf=cst-out : {a : A} {x y : A} {p : x == y} {u : x == a} {v : y == a}
    → (u == v [ (λ x → x == a) ↓ p ])
    → u == p ∙ v
  ↓-idf=cst-out {p = idp} q = q

  ↓-idf=cst-in' : {a : A} {x y : A} {p : x == y} {u : x == a} {v : y == a}
    → u == p ∙' v
    → (u == v [ (λ x → x == a) ↓ p ])
  ↓-idf=cst-in' {p = idp} q = q ∙ ∙'-unit-l _

  ↓-idf=idf-in' : {x y : A} {p : x == y} {u : x == x} {v : y == y}
    → u ∙ p == p ∙' v
    → (u == v [ (λ x → x == x) ↓ p ])
  ↓-idf=idf-in' {p = idp} q = ! (∙-unit-r _) ∙ q ∙ ∙'-unit-l _

  ↓-idf=idf-out' : {x y : A} {p : x == y} {u : x == x} {v : y == y}
    → (u == v [ (λ x → x == x) ↓ p ])
    → u ∙ p == p ∙' v
  ↓-idf=idf-out' {p = idp} q = ∙-unit-r _ ∙ q ∙ ! (∙'-unit-l _)

{- Nondependent identity type -}

↓-='-in : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (u ∙' ap g p) == (ap f p ∙ v)
  → (u == v [ (λ x → f x == g x) ↓ p ])
↓-='-in {p = idp} q = q

↓-='-out : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (u == v [ (λ x → f x == g x) ↓ p ])
  → (u ∙' ap g p) == (ap f p ∙ v)
↓-='-out {p = idp} q = q

↓-='-in' : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (u ∙ ap g p) == (ap f p ∙' v)
  → (u == v [ (λ x → f x == g x) ↓ p ])
↓-='-in' {p = idp} q = ! (∙-unit-r _) ∙ q ∙ (∙'-unit-l _)

↓-='-out' : ∀ {i j} {A : Type i} {B : Type j} {f g : A → B}
  {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
  → (u == v [ (λ x → f x == g x) ↓ p ])
  → (u ∙ ap g p) == (ap f p ∙' v)
↓-='-out' {p = idp} q = (∙-unit-r _) ∙ q ∙ ! (∙'-unit-l _)

{- Identity type where the type is dependent -}

↓-=-in : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u ◃ apd f p) == (apd g p ▹ v)
  → (u == v [ (λ x → g x == f x) ↓ p ])
↓-=-in {B = B} {p = idp} {u} {v} q = ! (◃idp {B = B} u) ∙ q ∙ idp▹ {B = B} v

↓-=-out : ∀ {i j} {A : Type i} {B : A → Type j} {f g : Π A B}
  {x y : A} {p : x == y} {u : g x == f x} {v : g y == f y}
  → (u == v [ (λ x → g x == f x) ↓ p ])
  → (u ◃ apd f p) == (apd g p ▹ v)
↓-=-out {B = B} {p = idp} {u} {v} q = (◃idp {B = B} u) ∙ q ∙ ! (idp▹ {B = B} v)

-- Dependent path in a type of the form [λ x → g (f x) == x]
module _ {i j} {A : Type i} {B : Type j} (g : B → A) (f : A → B) where
  ↓-∘=idf-in' : {x y : A} {p : x == y} {u : g (f x) == x} {v : g (f y) == y}
    → ((ap g (ap f p) ∙' v) == (u ∙ p))
    → (u == v [ (λ x → g (f x) == x) ↓ p ])
  ↓-∘=idf-in' {p = idp} q = ! (∙-unit-r _) ∙ (! q) ∙ (∙'-unit-l _)

-- WIP, derive it from more primitive principles
-- ↓-∘=id-in f g {p = p} {u} {v} q =
--   ↓-=-in (u ◃ apd (λ x → g (f x)) p =⟨ apd-∘ f g p |in-ctx (λ t → u ◃ t) ⟩
--         u ◃ ↓-apd-out _ f p (apdd g p (apd f p)) =⟨ apdd-cst (λ _ b → g b) p (ap f p) (! (apd-nd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
--         u ◃ ↓-apd-out _ f p (apd (λ t → g (π₂ t)) (pair= p (apd f p))) =⟨ apd-∘ π₂ g (pair= p (apd f p)) |in-ctx (λ t → u ◃ ↓-apd-out _ f p t) ⟩
--         u ◃ ↓-apd-out _ f p (↓-apd-out _ π₂ (pair= p (apd f p)) (apdd g (pair= p (apd f p)) (apd π₂ (pair= p (apd f p))))) =⟨ {!!} ⟩
--         apd (λ x → x) p ▹ v ∎)

-- module _ {i j} {A : Type i} {B : Type j} {x y z : A → B} where

--   lhs :
--     {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
--     {r : y a == z a} {r' : y a' == z a'}
--     (α : q == q'            [ (λ a → x a == y a) ↓ p ])
--     (β : r ∙ ap z p == ap y p ∙' r')
--     → (q ∙' r) ∙ ap z p == ap x p ∙' q' ∙' r'
--   lhs =
--     (q ∙' r) ∙ ap z p     =⟨ ? ⟩  -- assoc
--     q ∙' (r ∙ ap z p)     =⟨ ? ⟩  -- β
--     q ∙' (ap y p ∙' r')   =⟨ ? ⟩  -- assoc
--     (q ∙' ap y p) ∙' r'   =⟨ ? ⟩  -- ∙ = ∙'
--     (q ∙ ap y p) ∙' r'    =⟨ ? ⟩  -- α
--     (ap x p ∙' q') ∙' r'  =⟨ ? ⟩  -- assoc
--     ap x p ∙' q' ∙' r' ∎

--   thing :
--     {a a' : A} {p : a == a'} {q : x a == y a} {q' : x a' == y a'}
--     {r : y a == z a} {r' : y a' == z a'}
--     (α : q == q'            [ (λ a → x a == y a) ↓ p ])
--     (β : r ∙ ap z p == ap y p ∙' r')
--     → (_∙'2ᵈ_ {r = r} {r' = r'} α (↓-='-in' β) == ↓-='-in' {!!})
--   thing = {!!}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- {-# OPTIONS -v impossible:100 #-}
-- 2013-06-15 Andreas, reported by evancavallo
module Issue870 where

{- The following fails with

  An internal error has occurred. Please report this as a bug.
  Location of the error: src/full/Agda/TypeChecking/Rules/Term.hs:421

in Agda 2.3.3 on Ubuntu. Works fine using Set instead of Type or after tweaking the definition of test into a more sensible form. -}

Type = Set

data ⊤ : Type where
  tt : ⊤

record R : Type
  where
  field
    a : ⊤

test : ⊤ → R
test t = (λ a → record {a = a}) t

-- There was a possible __IMPOSSIBLE__ in the code for
-- guessing the record type of record{a = a}.
-- The problem was that a defined sort like Type, needs to be
-- reduced.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

open import utility
open import sn-calculus
  using (all-ready ; bound-ready)

open import Data.Product using (∃ ; Σ ; _,_ ; _×_ ; _,′_ ; proj₁ ; proj₂)
open import Relation.Binary.PropositionalEquality using (sym ; inspect ; Reveal_·_is_ ; trans)
open import Data.Empty
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Context
open import Esterel.Environment as Env
open import Esterel.Lang.CanFunction
  using (Canₖ ; module CodeSet ; Canₛ ; Canₛₕ ; Canθₛ ; Canθₛₕ)
open import Esterel.Lang.CanFunction.Base
  using (can-shr-var-irr)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ) renaming (_≟ₛₜ_ to _≟ₛₜₛ_)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ) renaming (_≟ₛₜ_ to _≟ₛₜₛₕ_)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Esterel.Lang.CanFunction using (Canₖ)

open import Data.Product using (_,_)
open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; trans ; sym)
import Data.FiniteMap
open import Data.List
  using (List ; [] ; _∷_ ; [_] ; _++_ ; map ; concatMap ; filter)
open import Data.List.Any using (Any ; any ; here ; there)
open import Data.List.All using (All ; [] ; _∷_)
open import Data.OrderedListMap

open all-ready
open bound-ready

data blocked-s : Env → s/l → Set where
   bbshr-old : ∀{θ s} →
     (s∈ : Env.isShr∈ s θ) →
     Env.shr-stats{s} θ s∈ ≡ SharedVar.old →
     blocked-s θ (shr-ref s)
   bbshr-new : ∀{θ s} →
     (s∈ : Env.isShr∈ s θ) →
     Env.shr-stats{s} θ s∈ ≡ SharedVar.new →
     blocked-s θ (shr-ref s)

-- Note: θ and e are in the opposite order of all-ready definition.
-- We directly used Any here as a synonym. Should all-ready be the same?
blocked-e : Env → Expr → Set
blocked-e θ (plus operators) = Any (blocked-s θ) operators

data blocked : Env → Ctrl → Term → Set where
  bsig-exists : ∀{θ p q A} S S∈ → (sig-stats{S} θ S∈ ≡ Signal.unknown) →
                ------------------------
                blocked θ A (present S ∣⇒ p ∣⇒ q)
  bpar-both  : ∀{θ p q A} → blocked θ A p → blocked θ A q → blocked θ A (p ∥ q)
  bpar-left  : ∀{θ p q A} → blocked θ A p → done q → blocked θ A (p ∥ q)
  bpar-right : ∀{θ p q A} → done p → blocked θ A q → blocked θ A (p ∥ q)
  bseq       : ∀{θ p q A} → blocked θ A p → blocked θ A (p >> q)
  bloopˢ     : ∀{θ p q A} → blocked θ A p → blocked θ A (loopˢ p q)
  bsusp      : ∀{θ p S A} → blocked θ A p → blocked θ A (suspend p S)
  btrap      : ∀{θ p A}   → blocked θ A p → blocked θ A (trap p)
  bwset      : ∀{θ s e} → blocked θ WAIT (s ⇐ e)
  bwemit      : ∀{θ S} → blocked θ WAIT (emit S)
  bshared    : ∀{θ s e p A} → blocked-e θ e → blocked θ A (shared s ≔ e in: p)
  bsset      : ∀{θ s e A} → blocked-e θ e → blocked θ A (s ⇐ e)
  bvar       : ∀{θ x e p A} → blocked-e θ e → blocked θ A (var x ≔ e in: p)
  bxset      : ∀{θ x e A} → blocked-e θ e → blocked θ A (x ≔ e)

data manifests-as-non-constructive : Env → Ctrl → Term → Set where
  mnc : ∀{p θ A} → (blocked-p : blocked θ A p)
              -- absent rule cannot fire: unknown signals might be emitted at some point
              → (θS≡unknown→S∈can-p-θ :
                 ∀ S →
                  (S∈Domθ        : Signal.unwrap S ∈ fst (Dom θ)) →
                  (θS≡unknown    : sig-stats {S} θ S∈Domθ ≡ Signal.unknown) →
                  Signal.unwrap S ∈ Canθₛ (sig θ) 0 p []env)
              -- readyness rule cannot fire: unready variables might become ready
              → (θs≡old⊎θs≡new→s∈can-p-θ :
                 ∀ s →
                  (s∈Domθ        : SharedVar.unwrap s ∈ snd (Dom θ)) →
                  (θs≡old⊎θs≡new : shr-stats {s} θ s∈Domθ ≡ SharedVar.old ⊎
                                   shr-stats {s} θ s∈Domθ ≡ SharedVar.new) →
                  SharedVar.unwrap s ∈ Canθₛₕ (sig θ) 0 p []env)
              → manifests-as-non-constructive θ A p

halted-blocked-disjoint : ∀ {θ p A} → halted p → blocked θ A p → ⊥
halted-blocked-disjoint hnothin   ()
halted-blocked-disjoint (hexit n) ()

paused-blocked-disjoint : ∀ {θ A p} → paused p → blocked θ A p → ⊥
paused-blocked-disjoint ppause ()
paused-blocked-disjoint (pseq p/paused) (bseq p/blocked) =
  paused-blocked-disjoint p/paused p/blocked
paused-blocked-disjoint (ploopˢ p/paused) (bloopˢ p/blocked) =
  paused-blocked-disjoint p/paused p/blocked
paused-blocked-disjoint (ppar p/paused q/paused) (bpar-both  p/blocked q/blocked) =
  paused-blocked-disjoint q/paused q/blocked
paused-blocked-disjoint (ppar p/paused q/paused) (bpar-left  p/blocked q/done) =
  paused-blocked-disjoint p/paused p/blocked
paused-blocked-disjoint (ppar p/paused q/paused) (bpar-right p/done q/blocked) =
  paused-blocked-disjoint q/paused q/blocked
paused-blocked-disjoint (psuspend p/paused) (bsusp p/blocked) =
  paused-blocked-disjoint p/paused p/blocked
paused-blocked-disjoint (ptrap p/paused) (btrap p/blocked) =
  paused-blocked-disjoint p/paused p/blocked

done-blocked-disjoint : ∀ {θ A p} → done p → blocked θ A p → ⊥
done-blocked-disjoint (dhalted p/halted) p/blocked = halted-blocked-disjoint p/halted p/blocked
done-blocked-disjoint (dpaused p/paused) p/blocked = paused-blocked-disjoint p/paused p/blocked

-- An expression cannot be both all-ready and blocked-e, i.e.
-- all-ready and blocked-e characterize disjoint subsets of e.
all-ready-blocked-disjoint : ∀ {e θ} → ¬ (all-ready e θ × blocked-e θ e)
all-ready-blocked-disjoint {θ = θ}
  (aplus (brshr {s = s} s∈ θs≡ready ∷ e/all-ready) ,
   here (bbshr-old {s = .s} s∈' θs≡old))
  with trans (sym θs≡ready) (trans (Env.shr-stats-∈-irr {s} {θ} s∈ s∈') θs≡old)
... | ()
all-ready-blocked-disjoint {θ = θ}
  (aplus (brshr {s = s} s∈ θs≡ready ∷ e/all-ready) ,
   here (bbshr-new {s = .s} s∈' θs≡new))
  with trans (sym θs≡ready) (trans (Env.shr-stats-∈-irr {s} {θ} s∈ s∈') θs≡new)
... | ()
all-ready-blocked-disjoint {θ = θ}
  (aplus (px ∷ e/all-ready) ,
   there e/blocked) =
  all-ready-blocked-disjoint (aplus e/all-ready ,′ e/blocked)

-- A subexpression in the hole in a blocked program must be either blocked or done.
blocked-⟦⟧e : ∀ {θ p p' E A} → blocked θ A p → p ≐ E ⟦ p' ⟧e → blocked θ A p' ⊎ done p'
blocked-⟦⟧e p/blocked dehole = inj₁ p/blocked
blocked-⟦⟧e (bseq p/blocked)  (deseq p≐E⟦p'⟧)     = blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (bloopˢ p/blocked) (deloopˢ p≐E⟦p'⟧)    = blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (bsusp p/blocked) (desuspend p≐E⟦p'⟧) = blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (btrap p/blocked) (detrap p≐E⟦p'⟧)    = blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (bpar-both  p/blocked q/blocked) (depar₁ p≐E⟦p'⟧) =
  blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (bpar-left  p/blocked q/done)    (depar₁ p≐E⟦p'⟧) =
  blocked-⟦⟧e p/blocked p≐E⟦p'⟧
blocked-⟦⟧e (bpar-right p/done    q/blocked) (depar₁ p≐E⟦p'⟧) =
  inj₂ (done-⟦⟧e p/done p≐E⟦p'⟧)
blocked-⟦⟧e (bpar-both  p/blocked q/blocked) (depar₂ q≐E⟦p'⟧) =
  blocked-⟦⟧e q/blocked q≐E⟦p'⟧
blocked-⟦⟧e (bpar-left  p/blocked q/done)    (depar₂ q≐E⟦p'⟧) =
  inj₂ (done-⟦⟧e q/done q≐E⟦p'⟧)
blocked-⟦⟧e (bpar-right p/done    q/blocked) (depar₂ q≐E⟦p'⟧) =
  blocked-⟦⟧e q/blocked q≐E⟦p'⟧

blocked-el-dec : ∀ θ l -> Dec (Any (blocked-s θ) l)
blocked-el-dec θ [] = no (λ ())
blocked-el-dec θ (num n ∷ l) with blocked-el-dec θ l
blocked-el-dec θ (num n ∷ l) | yes p = yes (there p)
blocked-el-dec θ (num n ∷ l) | no ¬p = no (λ { (here ()) ; (there x) → ¬p x } )
blocked-el-dec θ (seq-ref x ∷ l) with blocked-el-dec θ l
blocked-el-dec θ (seq-ref x ∷ l) | yes p = yes (there p)
blocked-el-dec θ (seq-ref x ∷ l) | no ¬p = no (λ { (here ()) ; (there x) → ¬p x })
blocked-el-dec θ (shr-ref s ∷ l) with blocked-el-dec θ l
blocked-el-dec θ (shr-ref s ∷ l) | yes p = yes (there p)
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p with Env.Shr∈ s θ
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p | yes s∈θ with Env.shr-stats{s} θ s∈θ | inspect (Env.shr-stats {s} θ) s∈θ
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p | yes s∈θ | SharedVar.ready | Reveal_·_is_.[ eq ] =
  no (λ { (here (bbshr-old s∈θ₂ eq₂)) → lookup-s-eq θ s s∈θ s∈θ₂ eq eq₂ (λ ()) ;
          (here (bbshr-new s∈θ₂ eq₂)) → lookup-s-eq θ s s∈θ s∈θ₂ eq eq₂ (λ ()) ;
          (there x) → ¬p x })
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p | yes s∈θ | SharedVar.new   | Reveal_·_is_.[ eq ] = yes (here (bbshr-new s∈θ eq))
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p | yes s∈θ | SharedVar.old   | Reveal_·_is_.[ eq ] = yes (here (bbshr-old s∈θ eq))
blocked-el-dec θ (shr-ref s ∷ l) | no ¬p | no ¬s∈θ =
  no (λ { (here (bbshr-old s∈ x)) → ¬s∈θ s∈ ;
          (here (bbshr-new s∈ x)) → ¬s∈θ s∈ ;
          (there x) → ¬p x })

blocked-e-dec : ∀ θ e -> Dec (blocked-e θ e)
blocked-e-dec θ (plus l) = blocked-el-dec θ l

blocked-dec : ∀ θ A p -> Dec (blocked θ A p)
blocked-dec θ A nothin = no (λ ())
blocked-dec θ A pause = no (λ ())
blocked-dec θ A (signl S p) = no (λ ())
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) with Sig∈ S θ
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) | yes SigS∈θ
   with Env.sig-stats{S} θ SigS∈θ | inspect (Env.sig-stats{S} θ) SigS∈θ
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) | yes SigS∈θ₁ | Signal.present | Reveal_·_is_.[ eq₁ ] =
  no (λ { (bsig-exists .S SigS∈θ₂ eq₂) → lookup-S-eq θ S SigS∈θ₁ SigS∈θ₂ eq₁ eq₂ (λ ()) })
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) | yes SigS∈θ₁ | Signal.absent | Reveal_·_is_.[ eq₁ ] =
  no (λ { (bsig-exists .S SigS∈θ₂ eq₂) → lookup-S-eq θ S SigS∈θ₁ SigS∈θ₂ eq₁ eq₂ (λ ()) } )
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) | yes SigS∈θ | Signal.unknown | Reveal_·_is_.[ eq ] =
  yes (bsig-exists S SigS∈θ eq)
blocked-dec θ A (present S ∣⇒ p ∣⇒ q) | no ¬SigS∈θ =
  no (λ { (bsig-exists .S S∈ _) → ¬SigS∈θ S∈ })
blocked-dec θ GO (emit S) = no (λ ())
blocked-dec θ WAIT (emit S) = yes bwemit
blocked-dec θ A (p ∥ q) with blocked-dec θ A p | blocked-dec θ A q
blocked-dec θ A (p ∥ q) | yes blockedp | yes blockedq =
  yes (bpar-both blockedp blockedq)
blocked-dec θ A (p ∥ q) | yes blockedp | no ¬blockedq with done-dec q
blocked-dec θ A (p ∥ q) | yes blockedp | no ¬blockedq | yes donep =
  yes (bpar-left blockedp donep)
blocked-dec θ A (p ∥ q) | yes blockedp | no ¬blockedq | no ¬donep =
  no (λ { (bpar-both  _ x) → ¬blockedq x ;
          (bpar-left  _ x) → ¬donep x ;
          (bpar-right _ x) → ¬blockedq x })
blocked-dec θ A (p ∥ q) | no ¬blockedp | yes blockedq with done-dec p
blocked-dec θ A (p ∥ q) | no ¬blockedp | yes blockedq | yes donep =
  yes (bpar-right donep blockedq)
blocked-dec θ A (p ∥ q) | no ¬blockedp | yes blockedq | no ¬donep =
  no (λ { (bpar-both  x _) → ¬blockedp x ;
          (bpar-left  x _) → ¬blockedp x ;
          (bpar-right x _) → ¬donep x })
blocked-dec θ A (p ∥ q) | no ¬blockedp | no ¬blockedq =
  no (λ { (bpar-both  _ x) → ¬blockedq x ;
          (bpar-left  x _) → ¬blockedp x ;
          (bpar-right _ x) → ¬blockedq x })
blocked-dec θ A (loop p) = no (λ ())
blocked-dec θ A (p >> q) with blocked-dec θ A p
blocked-dec θ A (p >> q) | yes blockedp = yes (bseq blockedp)
blocked-dec θ A (p >> q) | no ¬blockedp = no (λ { (bseq x) → ¬blockedp x })
blocked-dec θ A (loopˢ p q) with blocked-dec θ A p
blocked-dec θ A (loopˢ p q) | yes blockedp = yes (bloopˢ blockedp)
blocked-dec θ A (loopˢ p q) | no ¬blockedp = no (λ { (bloopˢ x) → ¬blockedp x })
blocked-dec θ A (suspend p S) with blocked-dec θ A p
blocked-dec θ A (suspend p S) | yes blockedp = yes (bsusp blockedp)
blocked-dec θ A (suspend p S) | no ¬blockedp = no (λ { (bsusp x) → ¬blockedp x })
blocked-dec θ A (trap p) with blocked-dec θ A p
blocked-dec θ A (trap p) | yes blockedp = yes (btrap blockedp)
blocked-dec θ A (trap p) | no ¬blockedp = no (λ { (btrap x) → ¬blockedp x })
blocked-dec θ A (exit x) = no (λ ())
blocked-dec θ A (shared s ≔ e in: p) with blocked-e-dec θ e
blocked-dec θ A (shared s ≔ e in: p) | yes blockede = yes (bshared blockede)
blocked-dec θ A (shared s ≔ e in: p) | no ¬blockede = no (λ { (bshared x) → ¬blockede x })
blocked-dec θ A (s ⇐ e) with blocked-e-dec θ e
blocked-dec θ A (s ⇐ e) | yes p = yes (bsset p)
blocked-dec θ GO (s ⇐ e) | no ¬p = no (λ { (bsset x) → ¬p x })
blocked-dec θ WAIT (s ⇐ e) | no ¬p = yes bwset
blocked-dec θ A (var x ≔ e in: p) with blocked-e-dec θ e
blocked-dec θ A (var x ≔ e in: p₁) | yes p = yes (bvar p)
blocked-dec θ A (var x ≔ e in: p) | no ¬p = no (λ { (bvar x₁) → ¬p x₁ })
blocked-dec θ A (x ≔ e) with blocked-e-dec θ e
blocked-dec θ A (x ≔ e) | yes p = yes (bxset p)
blocked-dec θ A (x ≔ e) | no ¬p = no (λ { (bxset x₁) → ¬p x₁ })
blocked-dec θ A (if x ∣⇒ p ∣⇒ p₁) = no (λ ())
blocked-dec θ A (ρ⟨ θ₁ , A₁ ⟩· p) = no (λ ())

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Properties.Functions where

infixr 5 _∘_

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
module Numeral.Natural.Relation.Divisibility where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Type

-- Divisibility relation of natural numbers.
-- `(y ∣ x)` means that `y` is divisible by `x`.
-- In other words: `x/y` is an integer.
-- Or: `∃(c: ℕ). x = c⋅y`.
-- Note on the definition of Div𝐒:
--   The order (y + x) works and depends on rewriting rules of ℕ at the moment (Specifically on the commuted identity and successor rules, I think).
--   Without rewriting rules, deconstruction of Div𝐒 seems not working.
--   Example:
--     div23 : ¬(2 ∣ 3)
--     div23(Div𝐒())
--     This is a "valid" proof, but would not type-check because deconstruction from (2 ∣ 3) to (2 ∣ 1) is impossible.
--     Seems like the compiler would see (3 = 2+x), but because of definition of (_+_), only (3 = x+2) can be found.
--   Defining Div𝐒 with (x + y) inside would work, but then the definition of DivN becomes more complicated because (_⋅_) is defined in this order.
-- Note on zero divisors:
--   (0 ∣ 0) is true, and it is the only number divisible by 0.
-- Example definitions of special cases of the divisibility relation and the divisibility with remainder relation:
--   data Even : ℕ → Stmt{Lvl.𝟎} where
--     Even0 : Even(𝟎)
--     Even𝐒 : ∀{x : ℕ} → Even(x) → Even(𝐒(𝐒(x)))
--   data Odd : ℕ → Stmt{Lvl.𝟎} where
--     Odd0 : Odd(𝐒(𝟎))
--     Odd𝐒 : ∀{x : ℕ} → Odd(x) → Odd(𝐒(𝐒(x)))
data _∣_ : ℕ → ℕ → Stmt{Lvl.𝟎} where
  Div𝟎 : ∀{y}   → (y ∣ 𝟎)
  Div𝐒 : ∀{y x} → (y ∣ x) → (y ∣ (y + x))

_∤_ : ℕ → ℕ → Stmt
y ∤ x = ¬(y ∣ x)

-- `Divisor(n)(d)` means that `d` is a divisor of `n`.
Divisor = swap(_∣_)

-- `Multiple(n)(m)` means that `m` is a multiple of `n`.
Multiple = _∣_

-- Elimination rule for (_∣_).
divides-elim : ∀{ℓ}{P : ∀{y x} → (y ∣ x) → Type{ℓ}} → (∀{y} → P(Div𝟎{y})) → (∀{y x}{p : y ∣ x} → P(p) → P(Div𝐒 p)) → (∀{y x} → (p : y ∣ x) → P(p))
divides-elim        z s Div𝟎     = z
divides-elim{P = P} z s (Div𝐒 p) = s(divides-elim{P = P} z s p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- 2010-10-01 Issue 342
module NonDependentConstructorType where

data Wrap : Set1 where
  wrap : Set -> Wrap

bla : Set
bla = wrap
-- 2010-10-01 error is printed as (_ : Set) -> Wrap !=< Set
-- error should be printed as Set -> Wrap !=< Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.types.Bool

open import Sec2preliminaries
open import Sec4hasConstToSplit

module Sec6hasConstToDecEq where

-- Lemma 6.1
hasConst-family-dec : {X : Type} → (x₁ x₂ : X) → ((x : X) → hasConst ((x₁ == x) + (x₂ == x))) → (x₁ == x₂) + ¬(x₁ == x₂)
hasConst-family-dec {X} x₁ x₂ hasConst-fam = solution where
  f₋ : (x : X) → (x₁ == x) + (x₂ == x) → (x₁ == x) + (x₂ == x)
  f₋ x = fst (hasConst-fam x)

  E₋ : X → Type
  E₋ x = fix (f₋ x)

  E : Type
  E = Σ X λ x → (E₋ x)

  E-fst-determines-eq : (e₁ e₂ : E) → (fst e₁ == fst e₂) → e₁ == e₂
  E-fst-determines-eq e₁ e₂ p = second-comp-triv (λ x → fixed-point (f₋ x) (snd (hasConst-fam x))) _ _ p

  r : Bool → E
  r true = x₁ , to-fix (f₋ x₁) (snd (hasConst-fam x₁)) (inl idp)
  r false = x₂ , to-fix (f₋ x₂) (snd (hasConst-fam x₂)) (inr idp)

  about-r : (r true == r false) ↔ (x₁ == x₂)
  about-r = (λ p → ap fst p) , (λ p → E-fst-determines-eq _ _ p)

  s : E → Bool
  s (_ , inl _ , _) = true
  s (_ , inr _ , _) = false

  s-section-of-r : (e : E) → r(s e) == e
  s-section-of-r (x , inl p , q) = E-fst-determines-eq _ _ p
  s-section-of-r (x , inr p , q) = E-fst-determines-eq _ _ p

  about-s : (e₁ e₂ : E) → (s e₁ == s e₂) ↔ (e₁ == e₂)
  about-s e₁ e₂ = one , two where
    one : (s e₁ == s e₂) → (e₁ == e₂)
    one p =
      e₁       =⟨ ! (s-section-of-r e₁) ⟩
      r(s(e₁)) =⟨ ap r p ⟩
      r(s(e₂)) =⟨ s-section-of-r e₂ ⟩
      e₂       ∎
    two : (e₁ == e₂) → (s e₁ == s e₂)
    two p = ap s p

  combine : (s (r true) == s (r false)) ↔ (x₁ == x₂)
  combine = (about-s _ _) ◎ about-r

  check-bool : (s (r true) == s (r false)) + ¬(s (r true) == s (r false))
  check-bool = Bool-has-dec-eq _ _

  solution : (x₁ == x₂) + ¬(x₁ == x₂)
  solution with check-bool
  solution | inl p = inl (fst combine p)
  solution | inr np = inr (λ p → np (snd combine p))

-- Theorem 6.2
all-hasConst→dec-eq : ((X : Type) → hasConst X) → (X : Type) → has-dec-eq X
all-hasConst→dec-eq all-hasConst X x₁ x₂ = hasConst-family-dec x₁ x₂ (λ x → all-hasConst _)

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Empty where

open import Cubical.Data.Empty.Base public

open import Cubical.Data.Empty.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
data D : Set where
  c_c_ : D → D

test : D → D
test c x c_ = x


text:
-- Andreas, 2017-07-28, issue #657 is fixed
-- WAS: display form problem

postulate
  A : Set
  x : A

record R (A : Set) : Set₁ where
  field
    P : A → Set

module M (r : ∀ A → R A) where

  open module R′ {A} = R (r A) public

postulate
  r : ∀ A → R A

open M r

p : P x
p = {!!}

-- WAS: goal displayed as  R.P (r A) x

-- Expected: P x


text:
module UselessPrivateImport where

private
  open import Common.Prelude


text:
module Oscar.Data.Substitunction {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Equality
open import Oscar.Data.Equality.properties
open import Oscar.Data.Fin
open import Oscar.Data.Nat
open import Oscar.Data.Term FunctionName
open import Oscar.Data.Vec
open import Oscar.Function
open import Oscar.Level
open import Oscar.Relation

-- Substitunction
_⊸_ : (m n : Nat) → Set 𝔣
m ⊸ n = Fin m → Term n

▸ : ∀ {m n} → m ⟨ Fin ⟩→ n → m ⊸ n
▸ r = i ∘ r

infix 19 _◂_ _◂s_

mutual

  _◂_ : ∀ {m n} → m ⊸ n → m ⟨ Term ⟩→ n
  σ̇ ◂ i 𝑥 = σ̇ 𝑥
  _ ◂ leaf = leaf
  σ̇ ◂ (τl fork τr) = (σ̇ ◂ τl) fork (σ̇ ◂ τr)
  σ̇ ◂ (function fn τs) = function fn (σ̇ ◂s τs) where

  _◂s_ : ∀ {m n} → m ⊸ n → ∀ {N} → m ⟨ Terms N ⟩→ n  -- Vec (Term m) N → Vec (Term n) N
  f ◂s [] = []
  f ◂s (t ∷ ts) = f ◂ t ∷ f ◂s ts

_∙_ : ∀ {m n} → m ⊸ n → ∀ {l} → l ⊸ m → l ⊸ n
_∙_ f g = (f ◂_) ∘ g

mutual

  ◂-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → f ◂_ ≡̇ g ◂_
  ◂-extensionality p (i x) = p x
  ◂-extensionality p leaf = refl
  ◂-extensionality p (s fork t) = cong₂ _fork_ (◂-extensionality p s) (◂-extensionality p t)
  ◂-extensionality p (function fn ts) = cong (function fn) (◂s-extensionality p ts)

  ◂s-extensionality : ∀ {m n} {f g : m ⊸ n} → f ≡̇ g → ∀ {N} → _◂s_ f {N} ≡̇ _◂s_ g
  ◂s-extensionality p [] = refl
  ◂s-extensionality p (t ∷ ts) = cong₂ _∷_ (◂-extensionality p t) (◂s-extensionality p ts)

mutual

  ◂-associativity : ∀ {l m} (f : l ⊸ m) {n} (g : m ⊸ n) → (g ∙ f) ◂_ ≡̇ (g ◂_) ∘ (f ◂_)
  ◂-associativity _ _ (i _) = refl
  ◂-associativity _ _ leaf = refl
  ◂-associativity _ _ (τ₁ fork τ₂) = cong₂ _fork_ (◂-associativity _ _ τ₁) (◂-associativity _ _ τ₂)
  ◂-associativity f g (function fn ts) = cong (function fn) (◂s-associativity f g ts)

  ◂s-associativity : ∀ {l m n} (f : l ⊸ m) (g : m ⊸ n) → ∀ {N} → (_◂s_ (g ∙ f) {N}) ≡̇ (g ◂s_) ∘ (f ◂s_)
  ◂s-associativity _ _ [] = refl
  ◂s-associativity _ _ (τ ∷ τs) = cong₂ _∷_ (◂-associativity _ _ τ) (◂s-associativity _ _ τs)

∙-associativity : ∀ {k l} (f : k ⊸ l) {m} (g : l ⊸ m) {n} (h : m ⊸ n) → (h ∙ g) ∙ f ≡̇ h ∙ (g ∙ f)
∙-associativity f g h x rewrite ◂-associativity g h (f x) = refl

∙-extensionality : ∀ {l m} {f₁ f₂ : l ⊸ m} → f₁ ≡̇ f₂ → ∀ {n} {g₁ g₂ : m ⊸ n} → g₁ ≡̇ g₂ → g₁ ∙ f₁ ≡̇ g₂ ∙ f₂
∙-extensionality {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = ◂-extensionality g₁≡̇g₂ (f₂ x)

ε : ∀ {m} → m ⊸ m
ε = i

mutual

  ◂-identity : ∀ {m} (t : Term m) → ε ◂ t ≡ t
  ◂-identity (i x) = refl
  ◂-identity leaf = refl
  ◂-identity (s fork t) = cong₂ _fork_ (◂-identity s) (◂-identity t)
  ◂-identity (function fn ts) = cong (function fn) (◂s-identity ts)

  ◂s-identity : ∀ {N m} (t : Vec (Term m) N) → ε ◂s t ≡ t
  ◂s-identity [] = refl
  ◂s-identity (t ∷ ts) = cong₂ _∷_ (◂-identity t) (◂s-identity ts)

∙-left-identity : ∀ {m n} (f : m ⊸ n) → ε ∙ f ≡̇ f
∙-left-identity f = ◂-identity ∘ f

∙-right-identity : ∀ {m n} (f : m ⊸ n) → f ∙ ε ≡̇ f
∙-right-identity _ _ = refl

open import Oscar.Category

semigroupoidSubstitunction : Semigroupoid _⊸_ (λ {m n} → ≡̇-setoid (λ _ → Term n))
Semigroupoid._∙_ semigroupoidSubstitunction = _∙_
Semigroupoid.∙-extensionality semigroupoidSubstitunction = ∙-extensionality
Semigroupoid.∙-associativity semigroupoidSubstitunction = ∙-associativity

semigroupoidExtensionTerm : Semigroupoid (_⟨ Term ⟩→_) (λ {m n} → ≡̇-setoid (λ _ → Term n))
Semigroupoid._∙_ semigroupoidExtensionTerm g = g ∘_
Semigroupoid.∙-extensionality semigroupoidExtensionTerm {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = g₁≡̇g₂ (f₂ x)
Semigroupoid.∙-associativity semigroupoidExtensionTerm _ _ _ _ = refl

semigroupoidExtensionTerms : ∀ N → Semigroupoid (_⟨ Terms N ⟩→_) (λ {m n} → ≡̇-setoid (λ _ → Terms N n))
Semigroupoid._∙_ (semigroupoidExtensionTerms _) g = g ∘_
Semigroupoid.∙-extensionality (semigroupoidExtensionTerms _) {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = g₁≡̇g₂ (f₂ x)
Semigroupoid.∙-associativity (semigroupoidExtensionTerms _) _ _ _ _ = refl

semifunctorSubstitute : Semifunctor semigroupoidSubstitunction semigroupoidExtensionTerm
Semifunctor.μ semifunctorSubstitute = id
Semifunctor.𝔣 semifunctorSubstitute = _◂_
Semifunctor.𝔣-extensionality semifunctorSubstitute = ◂-extensionality
Semifunctor.𝔣-commutativity semifunctorSubstitute {f = f} {g = g} = ◂-associativity f g

semifunctorSubstitutes : ∀ N → Semifunctor semigroupoidSubstitunction (semigroupoidExtensionTerms N)
Semifunctor.μ (semifunctorSubstitutes _) = id
Semifunctor.𝔣 (semifunctorSubstitutes N) f τs = f ◂s τs
Semifunctor.𝔣-extensionality (semifunctorSubstitutes _) f≡̇g = ◂s-extensionality f≡̇g
Semifunctor.𝔣-commutativity (semifunctorSubstitutes _) {f = f} {g = g} = ◂s-associativity f g

------------ subfact3 : ∀ {l m n} (f : m ⊸ n) (r : l ⟨ Fin ⟩→ m) → f ◇ (▸ r) ≡ f ∘ r
------------ subfact3 f r = refl

-- -- -- -- prop-id : ∀ {m n} {f : _ ⊸ n} {ℓ} {P : ⊸-ExtentionalProperty {ℓ} m} → proj₁ P f → proj₁ P (i ◇ f)
-- -- -- -- prop-id {_} {_} {f} {_} {P'} Pf = proj₂ P' (λ x → sym (◃-identity (f x))) Pf

-- -- -- -- ≐-cong : ∀ {m n o} {f : m ⊸ n} {g} (h : _ ⊸ o) → f ≐ g → (h ◇ f) ≐ (h ◇ g)
-- -- -- -- ≐-cong h f≐g t = cong (h ◃_) (f≐g t)

-- -- -- -- -- data AList : ℕ -> ℕ -> Set 𝔣 where
-- -- -- -- --   anil : ∀ {n} -> AList n n
-- -- -- -- --   _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
-- -- -- -- --                -> AList (suc m) n

-- -- -- -- -- sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
-- -- -- -- -- sub anil = i
-- -- -- -- -- sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

-- -- -- -- -- _++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
-- -- -- -- -- ρ ++ anil = ρ
-- -- -- -- -- ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

-- -- -- -- -- ++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
-- -- -- -- -- ++-assoc ρ σ anil = refl
-- -- -- -- -- ++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

-- -- -- -- -- module SubList where
-- -- -- -- --   anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
-- -- -- -- --   anil-id-l anil = refl
-- -- -- -- --   anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

-- -- -- -- --   fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
-- -- -- -- --   fact1 ρ anil v = refl
-- -- -- -- --   fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
-- -- -- -- --     where
-- -- -- -- --       t = (t' for x) v
-- -- -- -- --       hyp-on-terms = ◃-extentionality (fact1 r s) t
-- -- -- -- --       ◃-assoc = ◃-associativity t

-- -- -- -- -- _∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
-- -- -- -- --   -> ∃ (AList (suc m))
-- -- -- -- -- (n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

-- -- -- -- -- open import Data.Maybe using (Maybe; nothing; just)

-- -- -- -- -- flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
-- -- -- -- -- flexFlex {suc m} x y with check x y
-- -- -- -- -- ...              | just y' = m , anil asnoc i y' / x
-- -- -- -- -- ...              | nothing = suc m , anil
-- -- -- -- -- flexFlex {zero} () _

-- -- -- -- -- open import Oscar.Class.ThickAndThin

-- -- -- -- -- flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
-- -- -- -- -- flexRigid {suc m} x t with check x t
-- -- -- -- -- ...                   | just t' = just (m , anil asnoc t' / x)
-- -- -- -- -- ...                   | nothing = nothing
-- -- -- -- -- flexRigid {zero} () _

-- -- -- -- -- -- open import Oscar.Data.Fin using (Fin; zero; suc; thick?; Check; check; thin; module Thick)

-- -- -- -- -- -- open import Data.Fin using (Fin; suc; zero)
-- -- -- -- -- -- open import Data.Nat hiding (_≤_)
-- -- -- -- -- -- open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
-- -- -- -- -- -- open import Function using (_∘_; id; case_of_; _$_; flip)
-- -- -- -- -- -- open import Relation.Nullary
-- -- -- -- -- -- open import Data.Product renaming (map to _***_)
-- -- -- -- -- -- open import Data.Empty
-- -- -- -- -- -- open import Data.Maybe
-- -- -- -- -- -- open import Category.Functor
-- -- -- -- -- -- open import Category.Monad
-- -- -- -- -- -- import Level
-- -- -- -- -- -- open RawMonad (Data.Maybe.monad {Level.zero})
-- -- -- -- -- -- open import Data.Sum
-- -- -- -- -- -- open import Data.Maybe using (maybe; maybe′; nothing; just; monad; Maybe)
-- -- -- -- -- -- open import Data.List renaming (_++_ to _++L_)
-- -- -- -- -- -- open ≡-Reasoning
-- -- -- -- -- -- open import Data.Vec using (Vec; []; _∷_) renaming (_++_ to _++V_; map to mapV)

-- -- -- -- -- -- open import Data.Nat using (ℕ; suc; zero)
-- -- -- -- -- -- open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
-- -- -- -- -- -- open import Function using (_∘_; flip)
-- -- -- -- -- -- open import Relation.Nullary using (¬_; Dec; yes; no)
-- -- -- -- -- -- open import Data.Product using (∃; _,_; _×_)
-- -- -- -- -- -- open import Data.Empty using (⊥-elim)
-- -- -- -- -- -- open import Data.Vec using (Vec; []; _∷_)

-- -- -- -- -- -- Term-function-inj-FunctionName : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → fn₁ ≡ fn₂
-- -- -- -- -- -- Term-function-inj-FunctionName refl = refl

-- -- -- -- -- -- Term-function-inj-VecSize : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → N₁ ≡ N₂
-- -- -- -- -- -- Term-function-inj-VecSize refl = refl

-- -- -- -- -- -- Term-function-inj-Vector : ∀ {fn₁ fn₂} {n N} {ts₁ : Vec (Term n) N} {ts₂ : Vec (Term n) N} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≡ ts₂
-- -- -- -- -- -- Term-function-inj-Vector refl = refl

-- -- -- -- -- -- Term-fork-inj-left : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → l₁ ≡ l₂
-- -- -- -- -- -- Term-fork-inj-left refl = refl

-- -- -- -- -- -- Term-fork-inj-right : ∀ {n} {l₁ r₁ l₂ r₂ : Term n} → l₁ fork r₁ ≡ l₂ fork r₂ → r₁ ≡ r₂
-- -- -- -- -- -- Term-fork-inj-right refl = refl

-- -- -- -- -- -- open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)

-- -- -- -- -- -- Term-function-inj-HetVector : ∀ {fn₁ fn₂} {n N₁ N₂} {ts₁ : Vec (Term n) N₁} {ts₂ : Vec (Term n) N₂} → Term.function fn₁ ts₁ ≡ Term.function fn₂ ts₂ → ts₁ ≅ ts₂
-- -- -- -- -- -- Term-function-inj-HetVector refl = refl

-- -- -- -- -- -- _⊸_ : (m n : ℕ) → Set
-- -- -- -- -- -- m ⊸ n = Fin m → Term n

-- -- -- -- -- -- ▸ : ∀ {m n} → (r : Fin m → Fin n) → Fin m → Term n
-- -- -- -- -- -- ▸ r = i ∘ r

-- -- -- -- -- -- record Substitution (T : ℕ → Set) : Set where
-- -- -- -- -- --   field
-- -- -- -- -- --     _◃_ : ∀ {m n} → (f : m ⊸ n) → T m → T n

-- -- -- -- -- -- open Substitution ⦃ … ⦄ public

-- -- -- -- -- -- {-# DISPLAY Substitution._◃_ _ = _◃_ #-}

-- -- -- -- -- -- mutual

-- -- -- -- -- --   instance SubstitutionTerm : Substitution Term
-- -- -- -- -- --   Substitution._◃_ SubstitutionTerm = _◃′_ where
-- -- -- -- -- --     _◃′_ : ∀ {m n} → (f : m ⊸ n) → Term m → Term n
-- -- -- -- -- --     f ◃′ i x = f x
-- -- -- -- -- --     f ◃′ leaf = leaf
-- -- -- -- -- --     f ◃′ (s fork t) = (f ◃ s) fork (f ◃ t)
-- -- -- -- -- --     f ◃′ (function fn ts) = function fn (f ◃ ts)

-- -- -- -- -- --   instance SubstitutionVecTerm : ∀ {N} → Substitution (flip Vec N ∘ Term )
-- -- -- -- -- --   Substitution._◃_ (SubstitutionVecTerm {N}) = _◃′_ where
-- -- -- -- -- --     _◃′_ : ∀ {m n} → (f : m ⊸ n) → Vec (Term m) N → Vec (Term n) N
-- -- -- -- -- --     f ◃′ [] = []
-- -- -- -- -- --     f ◃′ (t ∷ ts) = f ◃ t ∷ f ◃ ts

-- -- -- -- -- -- _≐_ : {m n : ℕ} → (Fin m → Term n) → (Fin m → Term n) → Set
-- -- -- -- -- -- f ≐ g = ∀ x → f x ≡ g x

-- -- -- -- -- -- record SubstitutionExtensionality (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set₁ where
-- -- -- -- -- --   field
-- -- -- -- -- --     ◃ext : ∀ {m n} {f g : Fin m → Term n} → f ≐ g → (t : T m) → f ◃ t ≡ g ◃ t

-- -- -- -- -- -- open SubstitutionExtensionality ⦃ … ⦄ public

-- -- -- -- -- -- mutual

-- -- -- -- -- --   instance SubstitutionExtensionalityTerm : SubstitutionExtensionality Term
-- -- -- -- -- --   SubstitutionExtensionality.◃ext SubstitutionExtensionalityTerm = ◃ext′ where
-- -- -- -- -- --     ◃ext′ : ∀ {m n} {f g : Fin m → Term n} → f ≐ g → ∀ t → f ◃ t ≡ g ◃ t
-- -- -- -- -- --     ◃ext′ p (i x) = p x
-- -- -- -- -- --     ◃ext′ p leaf = refl
-- -- -- -- -- --     ◃ext′ p (s fork t) = cong₂ _fork_ (◃ext p s) (◃ext p t)
-- -- -- -- -- --     ◃ext′ p (function fn ts) = cong (function fn) (◃ext p ts)

-- -- -- -- -- --   instance SubstitutionExtensionalityVecTerm : ∀ {N} → SubstitutionExtensionality (flip Vec N ∘ Term)
-- -- -- -- -- --   SubstitutionExtensionality.◃ext (SubstitutionExtensionalityVecTerm {N}) = λ x → ◃ext′ x where
-- -- -- -- -- --     ◃ext′ : ∀ {m n} {f g : Fin m → Term n} → f ≐ g → ∀ {N} (t : Vec (Term m) N) → f ◃ t ≡ g ◃ t
-- -- -- -- -- --     ◃ext′ p [] = refl
-- -- -- -- -- --     ◃ext′ p (t ∷ ts) = cong₂ _∷_ (◃ext p t) (◃ext p ts)

-- -- -- -- -- -- _◇_ : ∀ {l m n : ℕ } → (f : Fin m → Term n) (g : Fin l → Term m) → Fin l → Term n
-- -- -- -- -- -- f ◇ g = (f ◃_) ∘ g

-- -- -- -- -- -- ≐-cong : ∀ {m n o} {f : m ⊸ n} {g} (h : _ ⊸ o) → f ≐ g → (h ◇ f) ≐ (h ◇ g)
-- -- -- -- -- -- ≐-cong h f≐g t = cong (h ◃_) (f≐g t)

-- -- -- -- -- -- ≐-sym : ∀ {m n} {f : m ⊸ n} {g} → f ≐ g → g ≐ f
-- -- -- -- -- -- ≐-sym f≐g = sym ∘ f≐g

-- -- -- -- -- -- module Sub where
-- -- -- -- -- --   record Fact1 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
-- -- -- -- -- --     field
-- -- -- -- -- --       fact1 : ∀ {n} → (t : T n) → i ◃ t ≡ t

-- -- -- -- -- --   open Fact1 ⦃ … ⦄ public

-- -- -- -- -- --   mutual

-- -- -- -- -- --     instance Fact1Term : Fact1 Term
-- -- -- -- -- --     Fact1.fact1 Fact1Term (i x) = refl
-- -- -- -- -- --     Fact1.fact1 Fact1Term leaf = refl
-- -- -- -- -- --     Fact1.fact1 Fact1Term (s fork t) = cong₂ _fork_ (fact1 s) (fact1 t)
-- -- -- -- -- --     Fact1.fact1 Fact1Term (function fn ts) = cong (function fn) (fact1 ts)

-- -- -- -- -- --     instance Fact1TermVec : ∀ {N} → Fact1 (flip Vec N ∘ Term)
-- -- -- -- -- --     Fact1.fact1 Fact1TermVec [] = refl
-- -- -- -- -- --     Fact1.fact1 Fact1TermVec (t ∷ ts) = cong₂ _∷_ (fact1 t) (fact1 ts)

-- -- -- -- -- --   record Fact2 (T : ℕ → Set) ⦃ _ : Substitution T ⦄ : Set where
-- -- -- -- -- --     field
-- -- -- -- -- --       -- ⦃ s ⦄ : Substitution T
-- -- -- -- -- --       fact2 : ∀ {l m n} → {f : Fin m → Term n} {g : _} (t : T l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)

-- -- -- -- -- --   open Fact2 ⦃ … ⦄ public

-- -- -- -- -- --   mutual

-- -- -- -- -- --     instance Fact2Term : Fact2 Term
-- -- -- -- -- --     -- Fact2.s Fact2Term = SubstitutionTerm
-- -- -- -- -- --     Fact2.fact2 Fact2Term (i x) = refl
-- -- -- -- -- --     Fact2.fact2 Fact2Term leaf = refl
-- -- -- -- -- --     Fact2.fact2 Fact2Term (s fork t) = cong₂ _fork_ (fact2 s) (fact2 t)
-- -- -- -- -- --     Fact2.fact2 Fact2Term {f = f} {g = g} (function fn ts) = cong (function fn) (fact2 {f = f} {g = g} ts) -- fact2 ts

-- -- -- -- -- --     instance Fact2TermVec : ∀ {N} → Fact2 (flip Vec N ∘ Term)
-- -- -- -- -- --     -- Fact2.s Fact2TermVec = SubstitutionVecTerm
-- -- -- -- -- --     Fact2.fact2 Fact2TermVec [] = refl
-- -- -- -- -- --     Fact2.fact2 Fact2TermVec (t ∷ ts) = cong₂ _∷_ (fact2 t) (fact2 ts)

-- -- -- -- -- --   fact3 : ∀ {l m n} (f : Fin m → Term n) (r : Fin l → Fin m) → (f ◇ (▸ r)) ≡ (f ∘ r)
-- -- -- -- -- --   fact3 f r = refl

-- -- -- -- -- -- ◃ext' : ∀ {m n o} {f : Fin m → Term n}{g : Fin m → Term o}{h} → f ≐ (h ◇ g) → ∀ (t : Term _) → f ◃ t ≡ h ◃ (g ◃ t)
-- -- -- -- -- -- ◃ext' p t = trans (◃ext p t) (Sub.fact2 t)

-- -- -- -- -- -- open import Data.Maybe using (Maybe; nothing; just; functor; maybe′; maybe)
-- -- -- -- -- -- open import Category.Monad
-- -- -- -- -- -- import Level
-- -- -- -- -- -- --open RawMonad (Data.Maybe.monad {Level.zero})
-- -- -- -- -- -- open import Data.Nat using (ℕ)

-- -- -- -- -- -- _<*>_ = _⊛_

-- -- -- -- -- -- mutual

-- -- -- -- -- --   instance CheckTerm : Check Term
-- -- -- -- -- --   Check.check CheckTerm x (i y) = i <$> thick? x y
-- -- -- -- -- --   Check.check CheckTerm x leaf = just leaf
-- -- -- -- -- --   Check.check CheckTerm x (s fork t) = _fork_ <$> check x s ⊛ check x t
-- -- -- -- -- --   Check.check CheckTerm x (function fn ts) = ⦇ (function fn) (check x ts) ⦈

-- -- -- -- -- --   instance CheckTermVec : ∀ {N} → Check (flip Vec N ∘ Term)
-- -- -- -- -- --   Check.check CheckTermVec x [] = just []
-- -- -- -- -- --   Check.check CheckTermVec x (t ∷ ts) = ⦇ check x t ∷ check x ts ⦈

-- -- -- -- -- -- _for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) → Fin (suc n) → Term n
-- -- -- -- -- -- (t' for x) y = maybe′ i t' (thick? x y)

-- -- -- -- -- -- open import Data.Product using () renaming (Σ to Σ₁)
-- -- -- -- -- -- open Σ₁ renaming (proj₁ to π₁; proj₂ to π₂)

-- -- -- -- -- -- Property⋆ : (m : ℕ) → Set1
-- -- -- -- -- -- Property⋆ m = ∀ {n} → (Fin m → Term n) → Set

-- -- -- -- -- -- Extensional : {m : ℕ} → Property⋆ m → Set
-- -- -- -- -- -- Extensional P = ∀ {m f g} → f ≐ g → P {m} f → P g

-- -- -- -- -- -- Property : (m : ℕ) → Set1
-- -- -- -- -- -- Property m = Σ₁ (Property⋆ m) Extensional

-- -- -- -- -- -- prop-id : ∀ {m n} {f : _ ⊸ n} {P : Property m} → π₁ P f → π₁ P (i ◇ f)
-- -- -- -- -- -- prop-id {_} {_} {f} {P'} Pf = π₂ P' (λ x → sym (Sub.fact1 (f x))) Pf

-- -- -- -- -- -- Unifies⋆ : ∀ {m} (s t : Term m) → Property⋆ m
-- -- -- -- -- -- Unifies⋆ s t f = f ◃ s ≡ f ◃ t

-- -- -- -- -- -- Unifies⋆V : ∀ {m N} (ss ts : Vec (Term m) N) → Property⋆ m
-- -- -- -- -- -- Unifies⋆V ss ts f = f ◃ ss ≡ f ◃ ts

-- -- -- -- -- -- open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
-- -- -- -- -- -- open ≡-Reasoning

-- -- -- -- -- -- Unifies : ∀ {m} (s t : Term m) → Property m
-- -- -- -- -- -- Unifies s t = (λ {_} → Unifies⋆ s t) , λ {_} {f} {g} f≐g f◃s=f◃t →
-- -- -- -- -- --   begin
-- -- -- -- -- --     g ◃ s
-- -- -- -- -- --   ≡⟨ sym (◃ext f≐g s) ⟩
-- -- -- -- -- --     f ◃ s
-- -- -- -- -- --   ≡⟨ f◃s=f◃t ⟩
-- -- -- -- -- --     f ◃ t
-- -- -- -- -- --   ≡⟨ ◃ext f≐g t ⟩
-- -- -- -- -- --     g ◃ t
-- -- -- -- -- --   ∎

-- -- -- -- -- -- UnifiesV : ∀ {m} {N} (s t : Vec (Term m) N) → Property m
-- -- -- -- -- -- UnifiesV s t = (λ {_} → Unifies⋆V s t) , λ {_} {f} {g} f≐g f◃s=f◃t →
-- -- -- -- -- --   begin
-- -- -- -- -- --     g ◃ s
-- -- -- -- -- --   ≡⟨ sym (◃ext f≐g s) ⟩
-- -- -- -- -- --     f ◃ s
-- -- -- -- -- --   ≡⟨ f◃s=f◃t ⟩
-- -- -- -- -- --     f ◃ t
-- -- -- -- -- --   ≡⟨ ◃ext f≐g t ⟩
-- -- -- -- -- --     g ◃ t
-- -- -- -- -- --   ∎

-- -- -- -- -- -- _∧⋆_ : ∀{m} → (P Q : Property⋆ m) → Property⋆ m
-- -- -- -- -- -- P ∧⋆ Q = (λ f → P f × Q f)

-- -- -- -- -- -- -- open import Data.Product renaming (map to _***_)
-- -- -- -- -- -- open import Data.Product using (Σ)
-- -- -- -- -- -- open Σ

-- -- -- -- -- -- _∧_ : ∀{m} → (P Q : Property m) → Property m
-- -- -- -- -- -- P ∧ Q = (λ {_} f → π₁ P f × π₁ Q f) , λ {_} {_} {_} f≐g Pf×Qf → π₂ P f≐g (proj₁ Pf×Qf) , π₂ Q f≐g (proj₂ Pf×Qf)

-- -- -- -- -- -- _⇔⋆_ : ∀{m} → (P Q : Property⋆ m) → Set
-- -- -- -- -- -- P ⇔⋆ Q = ∀ {n} f → (P {n} f → Q f) × (Q f → P f)

-- -- -- -- -- -- _⇔_ : ∀{m} → (P Q : Property m) → Set
-- -- -- -- -- -- P ⇔ Q = ∀ {n} f → (π₁ P {n} f → π₁ Q f) × (π₁ Q f → π₁ P f)

-- -- -- -- -- -- switch⋆ : ∀ {m} (P Q : Property⋆ m) → P ⇔⋆ Q → Q ⇔⋆ P
-- -- -- -- -- -- switch⋆ _ _ P⇔Q f = proj₂ (P⇔Q f) , proj₁ (P⇔Q f)

-- -- -- -- -- -- switch : ∀ {m} (P Q : Property m) → P ⇔ Q → Q ⇔ P
-- -- -- -- -- -- switch _ _ P⇔Q f = proj₂ (P⇔Q f) , proj₁ (P⇔Q f)

-- -- -- -- -- -- open import Data.Empty

-- -- -- -- -- -- Nothing⋆ : ∀{m} → (P : Property⋆ m) → Set
-- -- -- -- -- -- Nothing⋆ P = ∀{n} f → P {n} f → ⊥

-- -- -- -- -- -- Nothing : ∀{m} → (P : Property m) → Set
-- -- -- -- -- -- Nothing P = ∀{n} f → π₁ P {n} f → ⊥

-- -- -- -- -- -- _[-◇⋆_] : ∀{m n} (P : Property⋆ m) (f : Fin m → Term n) → Property⋆ n
-- -- -- -- -- -- (P [-◇⋆ f ]) g = P (g ◇ f)

-- -- -- -- -- -- _[-◇_] : ∀{m n} (P : Property m) (f : Fin m → Term n) → Property n
-- -- -- -- -- -- P [-◇ f ] = (λ {_} g → π₁ P (g ◇ f)) , λ {_} {f'} {g'} f'≐g' Pf'◇f → π₂ P (◃ext f'≐g' ∘ f)  Pf'◇f

-- -- -- -- -- -- open import Function using (_∘_; id; case_of_; _$_; flip)
-- -- -- -- -- -- open import Data.Product using (curry; uncurry)

-- -- -- -- -- -- module Properties where
-- -- -- -- -- --   fact1 : ∀ {m} {s t : Term m} → (Unifies s t) ⇔ (Unifies t s)
-- -- -- -- -- --   fact1 _ = sym , sym

-- -- -- -- -- --   fact1'⋆ : ∀ {m} {s1 s2 t1 t2 : Term m}
-- -- -- -- -- --          → Unifies⋆ (s1 fork s2) (t1 fork t2) ⇔⋆ (Unifies⋆ s1 t1 ∧⋆ Unifies⋆ s2 t2)
-- -- -- -- -- --   fact1'⋆ f = deconstr _ _ _ _ , uncurry (cong₂ _fork_)
-- -- -- -- -- --     where deconstr : ∀ {m} (s1 s2 t1 t2 : Term m)
-- -- -- -- -- --                    → (s1 fork s2) ≡ (t1 fork t2)
-- -- -- -- -- --                    → (s1 ≡ t1) × (s2 ≡ t2)
-- -- -- -- -- --           deconstr s1 s2 .s1 .s2 refl = refl , refl

-- -- -- -- -- --   fact1' : ∀ {m} {s1 s2 t1 t2 : Term m}
-- -- -- -- -- --          → Unifies (s1 fork s2) (t1 fork t2) ⇔ (Unifies s1 t1 ∧ Unifies s2 t2)
-- -- -- -- -- --   fact1' f = deconstr _ _ _ _ , uncurry (cong₂ _fork_)
-- -- -- -- -- --     where deconstr : ∀ {m} (s1 s2 t1 t2 : Term m)
-- -- -- -- -- --                    → (s1 fork s2) ≡ (t1 fork t2)
-- -- -- -- -- --                    → (s1 ≡ t1) × (s2 ≡ t2)
-- -- -- -- -- --           deconstr s1 s2 .s1 .s2 refl = refl , refl

-- -- -- -- -- --   fact1'V : ∀ {m} {t₁ t₂ : Term m} {N} {ts₁ ts₂ : Vec (Term m) N}
-- -- -- -- -- --          → UnifiesV (t₁ ∷ ts₁) (t₂ ∷ ts₂) ⇔ (Unifies t₁ t₂ ∧ UnifiesV ts₁ ts₂)
-- -- -- -- -- --   fact1'V f = deconstr _ _ _ _ , uncurry (cong₂ _∷_)
-- -- -- -- -- --     where deconstr : ∀ {m} (t₁ t₂ : Term m) {N} (ts₁ ts₂ : Vec (Term m) N)
-- -- -- -- -- --                    → (t₁ Vec.∷ ts₁) ≡ (t₂ ∷ ts₂)
-- -- -- -- -- --                    → (t₁ ≡ t₂) × (ts₁ ≡ ts₂)
-- -- -- -- -- --           deconstr s1 _ s2! _ refl = refl , refl -- refl , refl

-- -- -- -- -- --   fact2⋆ : ∀ {m} (P Q : Property⋆ m) → P ⇔⋆ Q → Nothing⋆ P → Nothing⋆ Q
-- -- -- -- -- --   fact2⋆ P Q iff notp f q with iff f
-- -- -- -- -- --   ...                        | (p2q , q2p) = notp f (q2p q)

-- -- -- -- -- --   fact2 : ∀ {m} (P Q : Property m) → P ⇔ Q → Nothing P → Nothing Q
-- -- -- -- -- --   fact2 P Q iff notp f q with iff f
-- -- -- -- -- --   ...                       | (p2q , q2p) = notp f (q2p q)

-- -- -- -- -- --   fact3 : ∀ {m} {P : Property m} → P ⇔ (P [-◇ i ])
-- -- -- -- -- --   fact3 f = id , id

-- -- -- -- -- --   fact4 : ∀{m n} {P : Property m} (f : _ → Term n)
-- -- -- -- -- --           → Nothing P → Nothing (P [-◇ f ])
-- -- -- -- -- --   fact4 f nop g = nop (g ◇ f)

-- -- -- -- -- --   fact5⋆ : ∀{m n} (P Q : Property⋆ _) (f : m ⊸ n) → P ⇔⋆ Q → (P [-◇⋆ f ]) ⇔⋆ (Q [-◇⋆ f ])
-- -- -- -- -- --   fact5⋆ _ _ f P⇔Q f' = P⇔Q (f' ◇ f)

-- -- -- -- -- --   fact5 : ∀{m n} (P Q : Property _) (f : m ⊸ n) → P ⇔ Q → (P [-◇ f ]) ⇔ (Q [-◇ f ])
-- -- -- -- -- --   fact5 _ _ f P⇔Q f' = P⇔Q (f' ◇ f)

-- -- -- -- -- --   fact6 : ∀{m n} P {f g : m ⊸ n} → f ≐ g → (P [-◇ f ]) ⇔ (P [-◇ g ])
-- -- -- -- -- --   fact6 P f≐g h = π₂ P (≐-cong h f≐g) , π₂ P (≐-sym (≐-cong h f≐g))

-- -- -- -- -- -- _≤_ : ∀ {m n n'} (f : Fin m → Term n) (g : Fin m → Term n') → Set
-- -- -- -- -- -- f ≤ g = ∃ λ f' → f ≐ (f' ◇ g)

-- -- -- -- -- -- module Order where

-- -- -- -- -- --   reflex : ∀ {m n} {f : Fin m → Term n} → f ≤ f
-- -- -- -- -- --   reflex = i  , λ _ → sym (Sub.fact1 _)

-- -- -- -- -- --   transitivity : ∀ {l m n o} {f : Fin l → Term m}{g : _ → Term n}
-- -- -- -- -- --                              {h : _ → Term o}
-- -- -- -- -- --                    → f ≤ g → g ≤ h → f ≤ h
-- -- -- -- -- --   transitivity {l} {_} {_} {_} {f} {g} {h} (fg , pfg) (gh , pgh) =
-- -- -- -- -- --                    fg ◇ gh , proof
-- -- -- -- -- --     where
-- -- -- -- -- --       proof : (x : Fin l) → f x ≡ (λ x' → fg ◃ (gh x')) ◃ (h x)
-- -- -- -- -- --       proof x = trans z (sym (Sub.fact2 (h x)))
-- -- -- -- -- --         where z = trans (pfg x) (cong (fg ◃_) (pgh x))

-- -- -- -- -- --   i-max : ∀ {m n} (f : Fin m → Term n) → f ≤ i
-- -- -- -- -- --   i-max f = f , λ _ → refl

-- -- -- -- -- --   dist : ∀{l m n o}{f : Fin l → Term m}{g : _ → Term n}(h : Fin o → _) → f ≤ g → (f ◇ h) ≤ (g ◇ h)
-- -- -- -- -- --   dist h (fg , pfg) = fg  , λ x → trans (◃ext pfg (h x)) (Sub.fact2 (h x))

-- -- -- -- -- -- Max⋆ : ∀ {m} (P : Property⋆ m) → Property⋆ m
-- -- -- -- -- -- Max⋆ P f = P f × (∀ {n} f' → P {n} f' → f' ≤ f)

-- -- -- -- -- -- Max : ∀ {m} (P : Property m) → Property m
-- -- -- -- -- -- Max P' = (λ {_} → Max⋆ P) , λ {_} {_} {_} → lemma1
-- -- -- -- -- --   where
-- -- -- -- -- --     open Σ₁ P' renaming (proj₁ to P; proj₂ to Peq)
-- -- -- -- -- --     lemma1 : {m : ℕ} {f : Fin _ → Term m} {g : Fin _ → Term m} →
-- -- -- -- -- --              f ≐ g →
-- -- -- -- -- --              P f × ({n : ℕ} (f' : Fin _ → Term n) → P f' → f' ≤ f) →
-- -- -- -- -- --              P g × ({n : ℕ} (f' : Fin _ → Term n) → P f' → f' ≤ g)
-- -- -- -- -- --     lemma1 {_} {f} {g} f≐g (Pf , MaxPf) = Peq f≐g Pf , λ {_} → lemma2
-- -- -- -- -- --       where
-- -- -- -- -- --         lemma2 : ∀ {n} f' → P {n} f' → ∃ λ f0 → f' ≐ (f0 ◇ g)
-- -- -- -- -- --         lemma2 f' Pf' = f0 , λ x → trans (f'≐f0◇f x) (cong (f0 ◃_) (f≐g x))
-- -- -- -- -- --               where
-- -- -- -- -- --                 f0 = proj₁ (MaxPf f' Pf')
-- -- -- -- -- --                 f'≐f0◇f = proj₂ (MaxPf f' Pf')

-- -- -- -- -- -- module Max where
-- -- -- -- -- --   fact : ∀{m}(P Q : Property m) → P ⇔ Q → Max P ⇔ Max Q
-- -- -- -- -- --   fact {m} P Q a f =
-- -- -- -- -- --    (λ maxp → pq (proj₁ maxp) , λ f' → proj₂ maxp f' ∘ qp)
-- -- -- -- -- --     , λ maxq → qp (proj₁ maxq) , λ f'  → proj₂ maxq f' ∘ pq
-- -- -- -- -- --     where
-- -- -- -- -- --       pq : {n : ℕ} {f0 : Fin m → Term n} → (π₁ P f0 → π₁ Q f0)
-- -- -- -- -- --       pq {_} {f} =  proj₁ (a f)
-- -- -- -- -- --       qp : {n : ℕ} {f0 : Fin m → Term n} → (π₁ Q f0 → π₁ P f0)
-- -- -- -- -- --       qp {_} {f} = proj₂ (a f)

-- -- -- -- -- -- DClosed : ∀{m} (P : Property m) → Set
-- -- -- -- -- -- DClosed P = ∀ {n} f {o} g → f ≤ g → π₁ P {o} g → π₁ P {n} f

-- -- -- -- -- -- module DClosed where

-- -- -- -- -- --   fact1 : ∀ {m} s t → DClosed {m} (Unifies s t)
-- -- -- -- -- --   fact1 s t f g (f≤g , p) gs=gt =
-- -- -- -- -- --          begin
-- -- -- -- -- --          f ◃ s
-- -- -- -- -- --          ≡⟨ ◃ext' p s ⟩
-- -- -- -- -- --          f≤g ◃ (g ◃ s)
-- -- -- -- -- --          ≡⟨ cong (f≤g ◃_) gs=gt ⟩
-- -- -- -- -- --          f≤g ◃ (g ◃ t)
-- -- -- -- -- --          ≡⟨ sym (◃ext' p t) ⟩
-- -- -- -- -- --          f ◃ t
-- -- -- -- -- --          ∎

-- -- -- -- -- -- optimist : ∀ {l m n o} (a : Fin _ → Term n) (p : Fin _ → Term o)
-- -- -- -- -- --                  (q : Fin _ → Term l) (P Q : Property m)
-- -- -- -- -- --            → DClosed P → π₁ (Max (P [-◇ a ])) p
-- -- -- -- -- --            → π₁ (Max (Q [-◇ (p ◇ a) ])) q
-- -- -- -- -- --            → π₁ (Max ((P ∧ Q) [-◇ a ])) (q ◇ p)
-- -- -- -- -- -- optimist a p q P' Q' DCP (Ppa , pMax) (Qqpa , qMax) =
-- -- -- -- -- --      (Peq (sym ∘ Sub.fact2 ∘ a) (DCP (q ◇ (p ◇ a)) (p ◇ a) (q , λ _ → refl) Ppa)
-- -- -- -- -- --       , Qeq (sym ∘ Sub.fact2 ∘ a) Qqpa )
-- -- -- -- -- --      , λ {_} → aux
-- -- -- -- -- --   where
-- -- -- -- -- --     open Σ₁ P' renaming (proj₁ to P; proj₂ to Peq)
-- -- -- -- -- --     open Σ₁ Q' renaming (proj₁ to Q; proj₂ to Qeq)
-- -- -- -- -- --     aux : ∀ {n} (f : _ → Term n) → P (f ◇ a) × Q (f ◇ a) → f ≤ (q ◇ p)
-- -- -- -- -- --     aux f (Pfa , Qfa) = h ,
-- -- -- -- -- --                         λ x → trans (f≐g◇p x) (◃ext' g≐h◇q (p x))
-- -- -- -- -- --       where
-- -- -- -- -- --         one = pMax f Pfa
-- -- -- -- -- --         g = proj₁ one
-- -- -- -- -- --         f≐g◇p = proj₂ one
-- -- -- -- -- --         Qgpa : Q (g ◇ (p ◇ a))
-- -- -- -- -- --         Qgpa = Qeq (λ x → ◃ext' f≐g◇p (a x)) Qfa
-- -- -- -- -- --         g≤q = qMax g Qgpa
-- -- -- -- -- --         h = proj₁ g≤q
-- -- -- -- -- --         g≐h◇q = proj₂ g≤q

-- -- -- -- -- -- module failure-propagation where

-- -- -- -- -- --   first⋆ : ∀ {m n} (a : _ ⊸ n) (P Q : Property⋆ m) →
-- -- -- -- -- --          Nothing⋆ (P [-◇⋆ a ]) → Nothing⋆ ((P ∧⋆ Q) [-◇⋆ a ])
-- -- -- -- -- --   first⋆ a P' Q' noP-a f (Pfa , Qfa) = noP-a f Pfa

-- -- -- -- -- --   first : ∀ {m n} (a : _ ⊸ n) (P Q : Property m) →
-- -- -- -- -- --          Nothing (P [-◇ a ]) → Nothing ((P ∧ Q) [-◇ a ])
-- -- -- -- -- --   first a P' Q' noP-a f (Pfa , Qfa) = noP-a f Pfa

-- -- -- -- -- --   second⋆ : ∀ {m n o} (a : _ ⊸ n) (p : _ ⊸ o)(P : Property⋆ m)(Q : Property m) →
-- -- -- -- -- --              (Max⋆ (P [-◇⋆ a ])) p → Nothing⋆ (π₁ Q [-◇⋆ (p ◇ a)])
-- -- -- -- -- --              → Nothing⋆ ((P ∧⋆ π₁ Q) [-◇⋆ a ])
-- -- -- -- -- --   second⋆ a p P' Q' (Ppa , pMax) noQ-p◇a f (Pfa , Qfa) = noQ-p◇a g Qgpa
-- -- -- -- -- --        where
-- -- -- -- -- --          f≤p = pMax f Pfa
-- -- -- -- -- --          g = proj₁ f≤p
-- -- -- -- -- --          f≐g◇p = proj₂ f≤p
-- -- -- -- -- --          Qgpa : π₁ Q' (g ◇ (p ◇ a))
-- -- -- -- -- --          Qgpa = π₂ Q' (◃ext' f≐g◇p ∘ a)  Qfa

-- -- -- -- -- --   second : ∀ {m n o} (a : _ ⊸ n) (p : _ ⊸ o)(P Q : Property m) →
-- -- -- -- -- --              π₁ (Max (P [-◇ a ])) p → Nothing (Q [-◇ (p ◇ a)])
-- -- -- -- -- --              → Nothing ((P ∧ Q) [-◇ a ])
-- -- -- -- -- --   second a p P' Q' (Ppa , pMax) noQ-p◇a f (Pfa , Qfa) = noQ-p◇a g Qgpa
-- -- -- -- -- --        where
-- -- -- -- -- --          f≤p = pMax f Pfa
-- -- -- -- -- --          g = proj₁ f≤p
-- -- -- -- -- --          f≐g◇p = proj₂ f≤p
-- -- -- -- -- --          Qgpa : π₁ Q' (g ◇ (p ◇ a))
-- -- -- -- -- --          Qgpa = π₂ Q' (◃ext' f≐g◇p ∘ a)  Qfa

-- -- -- -- -- -- trivial-problem : ∀ {m n t} {f : m ⊸ n} → (Max⋆ ((Unifies⋆ t t) [-◇⋆ f ])) i
-- -- -- -- -- -- trivial-problem = refl , λ f' _ → f' , λ _ → refl

-- -- -- -- -- -- trivial-problemV : ∀ {m n N} {t : Vec (Term _) N} {f : m ⊸ n} → (Max⋆ ((Unifies⋆V t t) [-◇⋆ f ])) i
-- -- -- -- -- -- trivial-problemV = refl , λ f' _ → f' , λ _ → refl

-- -- -- -- -- -- open import Data.Sum

-- -- -- -- -- -- var-elim : ∀ {m} (x : Fin (suc m)) (t' : Term _)
-- -- -- -- -- --               → π₁ (Max ((Unifies (i x) ((▸ (thin x) ◃_) t')))) (t' for x)
-- -- -- -- -- -- var-elim x t' = first , \{_} → second
-- -- -- -- -- --   where
-- -- -- -- -- --     lemma : ∀{m}(x : Fin (suc m)) t → i ≐ ((t for x) ◇ (▸ (thin x)))
-- -- -- -- -- --     lemma x t x' = sym (cong (maybe i t) (Thick.half2 x _ x' refl))
-- -- -- -- -- --     first = begin
-- -- -- -- -- --              (t' for x) ◃ (i x) ≡⟨ cong (maybe i t') (Thick.half1 x) ⟩
-- -- -- -- -- --              t'                 ≡⟨ sym (Sub.fact1 t') ⟩
-- -- -- -- -- --              i ◃ t'             ≡⟨ ◃ext' (lemma x t') t' ⟩
-- -- -- -- -- --              (t' for x) ◃ ((▸ (thin x) ◃_) t') ∎

-- -- -- -- -- --     second : ∀ {n} (f : _ ⊸ n) → f x ≡ f ◃ ((▸ (thin x) ◃_) t') → f ≤ (t' for x)
-- -- -- -- -- --     second f Unifiesf = (f ∘ thin x) , third
-- -- -- -- -- --         where
-- -- -- -- -- --           third : ((x' : Fin _) →  f x' ≡ (f ∘ thin x) ◃ (maybe′ i t' (thick? x x')))
-- -- -- -- -- --           third x' with thick? x x' | Thick.fact1 x x' (thick? x x') refl
-- -- -- -- -- --           third .x | .nothing | inj₁ (refl , refl)  =
-- -- -- -- -- --                                        sym (begin
-- -- -- -- -- --                                            (f ∘ thin x) ◃ t'  ≡⟨ cong (λ g → (g ◃_) t') (sym (Sub.fact3 f (thin x))) ⟩
-- -- -- -- -- --                                            (f ◇ (▸ (thin x))) ◃ t' ≡⟨ Sub.fact2 {-f (▸ (thin x))-} t' ⟩
-- -- -- -- -- --                                            f ◃ ((▸ (thin x) ◃_) t') ≡⟨ sym Unifiesf ⟩
-- -- -- -- -- --                                            f x ∎)
-- -- -- -- -- --           third x' | .(just y) | inj₂ (y , ( thinxy≡x' , refl))  = sym (cong f thinxy≡x')

-- -- -- -- -- -- var-elim-i : ∀ {m} (x : Fin (suc m)) (t' : Term _)
-- -- -- -- -- --               → π₁ (Max ((Unifies (i x) ((▸ (thin x) ◃_) t')))) (i ◇ (t' for x))
-- -- -- -- -- -- var-elim-i {m} x t = prop-id {_} {_} {t for x} {Max (Unifies (i x) ((▸ (thin x) ◃_) t))} (var-elim {m} x t)

-- -- -- -- -- -- var-elim-i-≡ : ∀ {m} {t'} (x : Fin (suc m)) t1  → t1 ≡ (i ∘ thin x) ◃ t' → π₁ (Max (Unifies (i x) t1)) (i ◇ (t' for x))
-- -- -- -- -- -- var-elim-i-≡ {_} {t'} x .((i ∘ thin x) ◃ t') refl = var-elim-i x t'

-- -- -- -- -- -- ◇-assoc : ∀ {l m n o} (f : l ⊸ m) (g : n ⊸ _) (h : o ⊸ _) →
-- -- -- -- -- --                (f ◇ (g ◇ h)) ≐ ((f ◇ g) ◇ h)
-- -- -- -- -- -- ◇-assoc f g h x = sym (Sub.fact2 (h x))

-- -- -- -- -- -- bind-assoc : ∀ {l m n o} (f : l ⊸ m) (g : n ⊸ _) (h : o ⊸ _) t → (f ◇ g) ◃ (h ◃ t) ≡ (f ◇ (g ◇ h)) ◃ t
-- -- -- -- -- -- bind-assoc f g h t = sym (begin
-- -- -- -- -- --            (f ◇ (g ◇ h)) ◃ t  ≡⟨ ◃ext (◇-assoc f g h) t ⟩
-- -- -- -- -- --            ((f ◇ g) ◇ h) ◃ t  ≡⟨ Sub.fact2 ⦃ SubstitutionTerm ⦄ ⦃ Sub.Fact2Term ⦄ {f = (f ◇ g)} {g = h} {-(f ◇ g) h-} t ⟩
-- -- -- -- -- --            (f ◇ g) ◃ (h  ◃ t)
-- -- -- -- -- --                               ∎)


text:
{-# OPTIONS --no-auto-inline #-}
module Haskell.Prelude where

open import Agda.Builtin.Unit         public
open import Agda.Builtin.Nat as Nat   public hiding (_==_; _<_; _+_; _*_; _-_)
open import Agda.Builtin.List         public
open import Agda.Builtin.Bool         public
open import Agda.Builtin.Char         public
open import Agda.Builtin.FromString   public
import Agda.Builtin.String as Str
open import Agda.Builtin.Strict
open import Agda.Builtin.Equality     public
open import Agda.Builtin.Int using (pos; negsuc)

open import Haskell.Prim
open Haskell.Prim public using ( TypeError; ⊥; iNumberNat; IsTrue; IsFalse;
                                 All; allNil; allCons; NonEmpty; lengthNat;
                                 id; _∘_; _$_; flip; const;
                                 if_then_else_; case_of_;
                                 Number; fromNat; Negative; fromNeg;
                                 a; b; c; d; e; f; m; s; t )

open import Haskell.Prim.Absurd      public
open import Haskell.Prim.Applicative public
open import Haskell.Prim.Bool        public
open import Haskell.Prim.Char        public
open import Haskell.Prim.Bounded     public
open import Haskell.RangedSets.Boundaries  public
open import Haskell.RangedSets.Ranges      public
open import Haskell.RangedSets.RangedSet   public
open import Haskell.Prim.Double      public
open import Haskell.Prim.Either      public
open import Haskell.Prim.Enum        public
open import Haskell.Prim.Eq          public
open import Haskell.Prim.Foldable    public
open import Haskell.Prim.Functor     public
open import Haskell.Prim.Int         public
open import Haskell.Prim.Integer     public
open import Haskell.Prim.Real        public
open import Haskell.Prim.List        public
open import Haskell.Prim.Maybe       public
open import Haskell.Prim.Monad       public
open import Haskell.Prim.Monoid      public
open import Haskell.Prim.Num         public
open import Haskell.Prim.Ord         public
open import Haskell.Prim.Show        public
open import Haskell.Prim.String      public
open import Haskell.Prim.Traversable public
open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
open import Haskell.Prim.Word        public

-- Problematic features
--  - [Partial]:  Could pass implicit/instance arguments to prove totality.
--  - [Float]:    Or Float (Agda floats are Doubles)
--  - [Infinite]: Define colists and map to Haskell lists?

-- Missing from the Haskell Prelude:
--
--     Float        [Float]
--     Rational
--
--     Real(toRational),
--     Integral(quot, rem, div, mod, quotRem, divMod, toInteger),
--     Fractional((/), recip, fromRational),
--     Floating(pi, exp, log, sqrt, (**), logBase, sin, cos, tan,
--              asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh),
--     RealFrac(properFraction, truncate, round, ceiling, floor),
--     RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
--               encodeFloat, exponent, significand, scaleFloat, isNaN,
--               isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
--
--     subtract, even, odd, gcd, lcm, (^), (^^),
--     fromIntegral, realToFrac,
--
--     foldr1, foldl1, maximum, minimum      [Partial]
--
--     until [Partial]
--
--     iterate, repeat, cycle          [Infinite]
--
--     ReadS, Read(readsPrec, readList),
--     reads, readParen, read, lex,
--
--     IO, putChar, putStr, putStrLn, print,
--     getChar, getLine, getContents, interact,
--     FilePath, readFile, writeFile, appendFile, readIO, readLn,
--     IOError, ioError, userError,

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

infixr 0 _$!_
_$!_ : (a → b) → a → b
f $! x = primForce x f

seq : a → b → b
seq x y = const y $! x

asTypeOf : a → a → a
asTypeOf x _ = x

undefined : {@(tactic absurd) i : ⊥} → a
undefined {i = ()}

error : {@(tactic absurd) i : ⊥} → String → a
error {i = ()} err

errorWithoutStackTrace : {@(tactic absurd) i : ⊥} → String → a
errorWithoutStackTrace {i = ()} err

-------------------------------------------------
-- More List functions
--   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
--   turning those dependencies around.

reverse : List a → List a
reverse = foldl (flip _∷_) []

infixl 9 _!!_ _!!ᴺ_

_!!ᴺ_ : (xs : List a) (n : Nat) → ⦃ IsTrue (n < lengthNat xs) ⦄ → a
(x ∷ xs) !!ᴺ zero  = x
(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n

_!!_ : (xs : List a) (n : Int) ⦃ nn : IsNonNegativeInt n ⦄ → ⦃ IsTrue (intToNat n < lengthNat xs) ⦄ → a
xs !! n = xs !!ᴺ intToNat n

lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
lookup x []              = Nothing
lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs