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

F : Bool → Set
F false = Bool
F true  = Nat

f : ∀ b → F b → Nat
f false false = 0
f false true  = 1
f true  x     = 2

data D : Nat → Set where
  mkD : (b : Bool) (x : F b) → D (f b x)

mutual
  ?X : Nat → Set
  ?X = _

  ?b : Nat → Bool
  ?b = _

  -- Here we should check
  --    (n : Nat) → ?X n == (x : F (?b 0)) → D (f (?b 0) x)
  -- and get stuck on comparing the domains, but special inference
  -- for constructors is overeager and compares the target types,
  -- solving
  --    ?X : Nat → Set
  --    ?X x := D (f (?b 0) x)
  -- Note that the call to f is not well-typed unless we solve the
  -- (as yet unsolved) constraint Nat == F (?b 0).
  constr₁ : (n : Nat) → ?X n
  constr₁ = mkD (?b 0)

  -- Now we can form other constraints on ?X. This one simplifies to
  --   f (?b 0) 1 ≡ 0      (*)
  constr₂ : ?X 1 ≡ D 0
  constr₂ = refl

  -- Finally, we pick the wrong solution for ?b, causing (*) to become
  --   f false 1 ≡ 0
  -- which crashes with an impossible when we try to reduce the call to f.
  solve-b : ?b ≡ λ _ → false
  solve-b = refl


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Prelims
open import Cubical.ZCohomology.KcompPrelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Algebra.Group

open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2) hiding (map)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim2 to pElim2 ; ∣_∣ to ∣_∣₁) hiding (map)
open import Cubical.HITs.Nullification
open import Cubical.HITs.Truncation renaming (elim to trElim ; elim2 to trElim2 ; map to trMap ; rec to trRec)

open GroupHom
open GroupIso

private
  module congLemma (key : Unit') where
    module K = lockedCohom key

    main : (n : ℕ) (p : Path (coHomK n) (0ₖ n) (0ₖ n))
              → Path (K.+K n (0ₖ n) (0ₖ n) ≡ K.+K n (0ₖ n) (0ₖ n))
                      (cong (K.+K n (0ₖ n)) p) (cong (λ x → K.+K n x (0ₖ n)) p)
    main n = congIdLeft≡congIdRight (K.+K n) (K.-K n) (0ₖ n) (K.rUnitK n) (K.lUnitK n) (rUnitlUnit0K key n)

--------- H⁰(T²) ------------
H⁰-T²≅ℤ : GroupIso (coHomGr 0 (S₊ 1 × S₊ 1)) intGroup
H⁰-T²≅ℤ =
  H⁰-connected (base , base)
    λ (a , b) → pRec propTruncIsProp
                     (λ id1 → pRec propTruncIsProp
                                   (λ id2 → ∣ ΣPathP (id1 , id2) ∣₁)
                                   (Sn-connected 0 b) )
                     (Sn-connected 0 a)

--------- H¹(T²) -------------------------------

H¹-T²≅ℤ×ℤ : GroupIso (coHomGr 1 ((S₊ 1) × (S₊ 1))) (dirProd intGroup intGroup)
H¹-T²≅ℤ×ℤ = theIso □ dirProdGroupIso (invGroupIso (Hⁿ-Sⁿ≅ℤ 0)) (H⁰-Sⁿ≅ℤ 0)
  where
  helper : (x : hLevelTrunc 3 (S₊ 1)) → ∣ (S¹map x) ∣ ≡ x
  helper = trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
                  λ a → refl

  typIso : Iso _ _
  typIso = setTruncIso (curryIso ⋄ codomainIso S1→K₁≡S1×Int ⋄ toProdIso)
                      ⋄ setTruncOfProdIso

  theIso : GroupIso _ _
  fun (map theIso) = Iso.fun (typIso)
  isHom (map theIso) =
    sElim2 (λ _ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet)) _ _)
            λ f g → ΣPathP ((cong ∣_∣₂
                             (funExt (λ x → helper (f (x , base) +ₖ g (x , base))
                                           ∙ sym (cong₂ (λ x y → x +ₖ y)
                                                        (helper (f (x , base)))
                                                        (helper (g (x , base))))))) ,
                           (cong ∣_∣₂
                              (funExt
                                (toPropElim
                                   (λ _ → isSetInt _ _)
                                   (cong winding
                                         (basechange-lemma2
                                           (λ x → f (base , x))
                                           (λ x → g (base , x))
                                           λ x → S¹map x)
                                  ∙∙ winding-hom
                                      (basechange2⁻
                                          (S¹map (f (base , base)))
                                          (λ i → S¹map (f (base , (loop i)))))
                                      (basechange2⁻
                                          (S¹map (g (base , base)))
                                          (λ i → S¹map (g (base , (loop i)))))
                                  ∙∙ sym (addLemma
                                          (winding
                                            (basechange2⁻
                                              (S¹map (f (base , base)))
                                              (λ i → S¹map (f (base , (loop i))))))
                                          (winding
                                            (basechange2⁻
                                              (S¹map  (g (base , base)))
                                              (λ i → S¹map (g (base , (loop i))))))))))))
  inv theIso = Iso.inv typIso
  rightInv theIso = Iso.rightInv typIso
  leftInv theIso = Iso.leftInv typIso

----------------------- H²(T²) ------------------------------
open import Cubical.Foundations.Equiv
H²-T²≅ℤ : GroupIso (coHomGr 2 (S₊ 1 × S₊ 1)) intGroup
H²-T²≅ℤ = invGroupIso (ℤ≅H²-T² unlock)
  where
    module _ (key : Unit') where
      module K = lockedCohom key
      private
        _+K_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
        _+K_ {n = n} = K.+K n

        -K_ : {n : ℕ} → coHomK n → coHomK n
        -K_ {n = n} = K.-K n

        -H_ : {A : Type₀} {n : ℕ} → coHom n A → coHom n A
        -H_ {n = n} = K.-H n

        _+H_ : {A : Type₀} {n : ℕ} → coHom n A → coHom n A → coHom n A
        _+H_ {n = n} = K.+H n

      typIso : Iso _ _
      typIso = helper
            ⋄ (invIso (prodIso (GroupIso→Iso (Hⁿ-S¹≅0 0))
                               (invIso (GroupIso→Iso (Hⁿ-Sⁿ≅ℤ 0))))
            ⋄ ((invIso setTruncOfProdIso)
            ⋄ (invIso (setTruncIso (curryIso
                                  ⋄ codomainIso (S1→K2≡K2×K1' key)
                                  ⋄ toProdIso)))))
        where
        helper : Iso Int (Unit × Int)
        Iso.inv helper = snd
        Iso.fun helper x = tt , x
        Iso.leftInv helper _ = refl
        Iso.rightInv helper _ = refl

      mapIsHom : (x y : Int)
              → Iso.fun typIso (x +ℤ y) ≡ ((Iso.fun typIso x) +H Iso.fun typIso y)
      mapIsHom a b =
          (cong f ((GroupHom.isHom (GroupIso.map (invGroupIso (dirProdGroupIso (Hⁿ-S¹≅0 0) (invGroupIso (Hⁿ-Sⁿ≅ℤ 0)))))
                                                              (_ , a) (_ , b))
                ∙ λ i → guyId i , +H≡+ₕ key _ (~ i) (g a) (g b)))
        ∙∙ helper (g a) (g b)
        ∙∙ cong₂ (_+H_) (λ i → f (guyId2 (~ i) , g a)) λ i → f (guyId2 (~ i) , g b)
        where
        f = Iso.fun (((invIso setTruncOfProdIso ⋄ invIso (setTruncIso (curryIso ⋄ codomainIso (S1→K2≡K2×K1' key) ⋄ toProdIso)))))
        g = GroupIso.inv (invGroupIso (Hⁿ-Sⁿ≅ℤ 0))

        isPropH²-S¹ : isProp (coHom 2 (S₊ 1))
        isPropH²-S¹ = isPropRetract (fun (map (Hⁿ-S¹≅0 0)))
                                    (inv (Hⁿ-S¹≅0 0))
                                    (leftInv (Hⁿ-S¹≅0 0))
                                    isPropUnit

        guyId : ∣ _ ∣₂ ≡ 0ₕ 2
        guyId = isPropH²-S¹ _ _

        guyId2 : ∣ _ ∣₂ ≡ 0ₕ 2
        guyId2 = isPropH²-S¹ _ _

        helper : (x y : ∥ ((S₊ 1) → (hLevelTrunc 3 (S₊ 1) )) ∥₂) →
                  f ((0ₕ 2) , (x +H y)) ≡ f ((0ₕ 2) , x) +H f (0ₕ 2 , y)
        helper =
          sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                 λ f g i → ∣ (λ x → helper2 (f (fst x)) (g (fst x)) (snd x) i) ∣₂
          where
          helper2 : (x y : coHomK 1) (s : S₊ 1)
                 → Iso.inv (S1→K2≡K2×K1' key) (0ₖ 2 , x +K y) s ≡ (Iso.inv (S1→K2≡K2×K1' key) (0ₖ 2 , x)) s +K (Iso.inv (S1→K2≡K2×K1' key) (0ₖ 2 , y)) s
          helper2 =
            trElim2 (λ _ _ → isOfHLevelΠ 3 λ _ → isOfHLevelTrunc 4 _ _)
                    λ a b → λ {base → cong₂ (_+K_) (sym (K.lUnitK _ 0₂)) (sym (K.lUnitK _ 0₂))
                            ; (loop i) j → hcomp (λ k → λ{ (i = i0) → cong₂ (_+K_) (sym (K.lUnitK _ 0₂)) (sym (K.lUnitK _ 0₂)) (j ∧ k)
                                                         ; (i = i1) → cong₂ (_+K_) (sym (K.lUnitK _ 0₂)) (sym (K.lUnitK _ 0₂)) (j ∧ k)
                                                         ; (j = i0) → 0₂ +K (Kn→ΩKn+1 1 (∣ a ∣ +K ∣ b ∣) i)
                                                         ; (j = i1) → cong₂ (_+K_) (sym (K.lUnitK _ (Kn→ΩKn+1 1 ∣ a ∣ i)))
                                                                            (sym (K.lUnitK _ (Kn→ΩKn+1 1 ∣ b ∣ i))) k})
                                               (helper3 ∣ a ∣ ∣ b ∣ j i)}
            where
            helper3 : (a b : coHomK 1) → cong (0₂ +K_) (Kn→ΩKn+1 1 (a +K b)) ≡ cong₂ (_+K_) (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b)
            helper3 a b = cong (cong (0₂ +K_)) (+K→∙ key 1 a b)
                        ∙ (congFunct (0₂ +K_) (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b)
                        ∙∙ (λ i → congLemma.main key 2 (Kn→ΩKn+1 1 a) i ∙ cong (_+K_ ∣ north ∣) (λ i → Kn→ΩKn+1 1 b i))
                        ∙∙ sym (cong₂Funct (_+K_) (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b)))

      ℤ≅H²-T² : GroupIso intGroup (coHomGr 2 (S₊ 1 × S₊ 1))
      fun (map ℤ≅H²-T²) = Iso.fun typIso
      isHom (map ℤ≅H²-T²) = pm key mapIsHom
        where
        pm : (t : Unit')
          → ((x y : Int)
                → Iso.fun typIso (x +ℤ y) ≡ (lockedCohom.+H t _ (Iso.fun typIso x) (Iso.fun typIso y)))
          → isGroupHom intGroup (coHomGr 2 (S₊ 1 × S₊ 1)) (Iso.fun typIso)
        pm unlock p = p
      inv ℤ≅H²-T² = Iso.inv typIso
      rightInv ℤ≅H²-T² = Iso.rightInv typIso
      leftInv ℤ≅H²-T² = Iso.leftInv typIso

private
  to₂ : coHom 2 (S₊ 1 × S₊ 1) → Int
  to₂ = fun (map H²-T²≅ℤ)

  from₂ : Int → coHom 2 (S₊ 1 × S₊ 1)
  from₂ = inv H²-T²≅ℤ

  to₁ : coHom 1 (S₊ 1 × S₊ 1) → Int × Int
  to₁ = fun (map H¹-T²≅ℤ×ℤ)

  from₁ : Int × Int → coHom 1 (S₊ 1 × S₊ 1)
  from₁ = inv H¹-T²≅ℤ×ℤ

  to₀ : coHom 0 (S₊ 1 × S₊ 1) → Int
  to₀ = fun (map H⁰-T²≅ℤ)

  from₀ : Int → coHom 0 (S₊ 1 × S₊ 1)
  from₀ = inv H⁰-T²≅ℤ

{-
-- Compute fast:
test : to₁ (from₁ (0 , 1) +ₕ from₁ (1 , 0)) ≡ (1 , 1)
test = refl

test2 : to₁ (from₁ (5 , 1) +ₕ from₁ (-2 , 3)) ≡ (3 , 4)
test2 = refl

-- Will not compute:

test3 : to₂ (from₂ 0) ≡ 0
test3 = refl

-}

ext: agda

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
------------------------------------------------------------------------------
-- Properties related with lists
------------------------------------------------------------------------------

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

module FOTC.Data.List.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Base.PropertiesI
open import FOTC.Data.Conat
open import FOTC.Data.List
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Congruence properties

++-leftCong : ∀ {xs ys zs} → xs ≡ ys → xs ++ zs ≡ ys ++ zs
++-leftCong refl = refl

++-rightCong : ∀ {xs ys zs} → ys ≡ zs → xs ++ ys ≡ xs ++ zs
++-rightCong refl = refl

mapCong₂ : ∀ {f xs ys} → xs ≡ ys → map f xs ≡ map f ys
mapCong₂ refl = refl

revCong₁ : ∀ {xs ys zs} → xs ≡ ys → rev xs zs ≡ rev ys zs
revCong₁ refl = refl

revCong₂ : ∀ {xs ys zs} → ys ≡ zs → rev xs ys ≡ rev xs zs
revCong₂ refl = refl

reverseCong : ∀ {xs ys} → xs ≡ ys → reverse xs ≡ reverse ys
reverseCong refl = refl

reverse'Cong : ∀ {xs ys} → xs ≡ ys → reverse' xs ≡ reverse' ys
reverse'Cong refl = refl

lengthCong : ∀ {xs ys} → xs ≡ ys → length xs ≡ length ys
lengthCong refl = refl

------------------------------------------------------------------------------
-- Totality properties

lengthList-N : ∀ {xs} → List xs → N (length xs)
lengthList-N lnil               = subst N (sym length-[]) nzero
lengthList-N (lcons x {xs} Lxs) =
  subst N (sym (length-∷ x xs)) (nsucc (lengthList-N Lxs))

++-List : ∀ {xs ys} → List xs → List ys → List (xs ++ ys)
++-List {ys = ys} lnil               Lys = subst List (sym (++-[] ys)) Lys
++-List {ys = ys} (lcons x {xs} Lxs) Lys =
  subst List (sym (++-∷ x xs ys)) (lcons x (++-List Lxs Lys))

map-List : ∀ f {xs} → List xs → List (map f xs)
map-List f lnil               = subst List (sym (map-[] f)) lnil
map-List f (lcons x {xs} Lxs) =
  subst List (sym (map-∷ f x xs)) (lcons (f · x) (map-List f Lxs))

rev-List : ∀ {xs ys} → List xs → List ys → List (rev xs ys)
rev-List {ys = ys} lnil               Lys = subst List (sym (rev-[] ys)) Lys
rev-List {ys = ys} (lcons x {xs} Lxs) Lys =
  subst List (sym (rev-∷ x xs ys)) (rev-List Lxs (lcons x Lys))

reverse-List : ∀ {xs} → List xs → List (reverse xs)
reverse-List Lxs = rev-List Lxs lnil

reverse'-List : ∀ {xs} → List xs → List (reverse' xs)
reverse'-List lnil = subst List (sym reverse'-[]) lnil
reverse'-List (lcons x {xs} Lxs) =
  subst List (sym (reverse'-∷ x xs)) (++-List (reverse'-List Lxs) (lcons x lnil))

-- Length properties

lg-x<lg-x∷xs : ∀ x {xs} → List xs → length xs < length (x ∷ xs)
lg-x<lg-x∷xs x lnil =
  lt (length []) (length (x ∷ []))
    ≡⟨ subst₂ (λ t t' → lt (length []) (length (x ∷ [])) ≡ lt t t')
              length-[]
              (length-∷ x [])
              refl
    ⟩
  lt zero (succ₁ (length []))
    ≡⟨ lt-0S (length []) ⟩
  true ∎

lg-x<lg-x∷xs x (lcons y {xs} Lxs) =
  lt (length (y ∷ xs)) (length (x ∷ y ∷ xs))
    ≡⟨ subst₂ (λ t t' → lt (length (y ∷ xs)) (length (x ∷ y ∷ xs)) ≡ lt t t')
              (length-∷ y xs)
              (length-∷ x (y ∷ xs))
              refl
    ⟩
  lt (succ₁ (length xs)) (succ₁ (length (y ∷ xs)))
    ≡⟨ lt-SS (length xs) (length (y ∷ xs)) ⟩
  lt (length xs) (length (y ∷ xs))
    ≡⟨ lg-x<lg-x∷xs y Lxs ⟩
  true ∎

lg-xs<lg-[]→⊥ : ∀ {xs} → List xs → ¬ (length xs < length [])
lg-xs<lg-[]→⊥ lnil lg-[]<lg-[] = ⊥-elim (0<0→⊥ helper)
  where
  helper : zero < zero
  helper =
    lt zero zero
      ≡⟨ subst₂ (λ t t' → lt zero zero ≡ lt t t')
                (sym length-[])
                (sym length-[])
                refl
      ⟩
    lt (length []) (length [])
      ≡⟨ lg-[]<lg-[] ⟩
    true ∎

lg-xs<lg-[]→⊥ (lcons x {xs} Lxs) lg-x∷xs<lg-[] = ⊥-elim (S<0→⊥ helper)
  where
  helper : succ₁ (length xs) < zero
  helper =
    lt (succ₁ (length xs)) zero
      ≡⟨ subst₂ (λ t t' → lt (succ₁ (length xs)) zero ≡ lt t t')
                (sym (length-∷ x xs))
                (sym length-[])
                refl
      ⟩
    lt (length (x ∷ xs)) (length [])
      ≡⟨ lg-x∷xs<lg-[] ⟩
    true ∎

lg-xs≡∞→lg-x∷xs≡∞ : ∀ x xs → length xs ≡ ∞ → length (x ∷ xs) ≡ ∞
lg-xs≡∞→lg-x∷xs≡∞ x xs h =
  length (x ∷ xs)   ≡⟨ length-∷ x xs ⟩
  succ₁ (length xs) ≡⟨ succCong h ⟩
  succ₁ ∞           ≡⟨ sym ∞-eq ⟩
  ∞                 ∎

-- Append properties

++-leftIdentity : ∀ xs → [] ++ xs ≡ xs
++-leftIdentity = ++-[]

++-rightIdentity : ∀ {xs} → List xs → xs ++ [] ≡ xs
++-rightIdentity lnil               = ++-leftIdentity []
++-rightIdentity (lcons x {xs} Lxs) =
  (x ∷ xs) ++ [] ≡⟨ ++-∷ x xs [] ⟩
  x ∷ (xs ++ []) ≡⟨ ∷-rightCong (++-rightIdentity Lxs) ⟩
  x ∷ xs         ∎

++-assoc : ∀ {xs} → List xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc lnil ys zs =
  ([] ++ ys) ++ zs ≡⟨ ++-leftCong (++-leftIdentity ys) ⟩
  ys ++ zs         ≡⟨ sym (++-leftIdentity (ys ++ zs)) ⟩
  [] ++ ys ++ zs   ∎

++-assoc (lcons x {xs} Lxs) ys zs =
  ((x ∷ xs) ++ ys) ++ zs ≡⟨ ++-leftCong (++-∷ x xs ys) ⟩
  (x ∷ (xs ++ ys)) ++ zs ≡⟨ ++-∷ x (xs ++ ys) zs ⟩
  x ∷ ((xs ++ ys) ++ zs) ≡⟨ ∷-rightCong (++-assoc Lxs ys zs) ⟩
  x ∷ (xs ++ ys ++ zs)   ≡⟨ sym (++-∷ x xs (ys ++ zs)) ⟩
  (x ∷ xs) ++ ys ++ zs   ∎

-- Map properties

map-++ : ∀ f {xs} → List xs → ∀ ys → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f lnil ys =
  map f ([] ++ ys)     ≡⟨ mapCong₂ (++-leftIdentity ys) ⟩
  map f ys             ≡⟨ sym (++-leftIdentity (map f ys)) ⟩
  [] ++ map f ys       ≡⟨ ++-leftCong (sym (map-[] f)) ⟩
  map f [] ++ map f ys ∎

map-++ f (lcons x {xs} Lxs) ys =
  map f ((x ∷ xs) ++ ys)         ≡⟨ mapCong₂ (++-∷ x xs ys) ⟩
  map f (x ∷ xs ++ ys)           ≡⟨ map-∷ f x (xs ++ ys) ⟩
  f · x ∷ map f (xs ++ ys)       ≡⟨ ∷-rightCong (map-++ f Lxs ys) ⟩
  f · x ∷ (map f xs ++ map f ys) ≡⟨ sym (++-∷ (f · x) (map f xs) (map f ys)) ⟩
  (f · x ∷ map f xs) ++ map f ys ≡⟨ ++-leftCong (sym (map-∷ f x xs)) ⟩
  map f (x ∷ xs) ++ map f ys     ∎

map≡[] : ∀ {f xs} → List xs → map f xs ≡ [] → xs ≡ []
map≡[] lnil                   h = refl
map≡[] {f} (lcons x {xs} Lxs) h = ⊥-elim ([]≢cons (trans (sym h) (map-∷ f x xs)))

-- Reverse properties

reverse-[x]≡[x] : ∀ x → reverse (x ∷ []) ≡ x ∷ []
reverse-[x]≡[x] x =
  rev (x ∷ []) [] ≡⟨ rev-∷ x [] [] ⟩
  rev [] (x ∷ []) ≡⟨ rev-[] (x ∷ []) ⟩
  x ∷ []          ∎

rev-++ : ∀ {xs} → List xs → ∀ ys → rev xs ys ≡ rev xs [] ++ ys
rev-++ lnil ys =
  rev [] ys       ≡⟨ rev-[] ys ⟩
  ys              ≡⟨ sym (++-leftIdentity ys) ⟩
  [] ++ ys        ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  rev [] [] ++ ys ∎

rev-++ (lcons x {xs} Lxs) ys =
  rev (x ∷ xs) ys
    ≡⟨ rev-∷ x xs ys ⟩
  rev xs (x ∷ ys)
    ≡⟨ rev-++ Lxs (x ∷ ys) ⟩
  rev xs [] ++ x ∷ ys
    ≡⟨ subst (λ t → rev xs [] ++ x ∷ ys ≡ rev xs [] ++ t)
             (sym (
               (x ∷ []) ++ ys  ≡⟨ ++-∷ x [] ys ⟩
                x ∷ ([] ++ ys) ≡⟨ ∷-rightCong (++-leftIdentity ys) ⟩
                x ∷ ys         ∎
               )
             )
             refl
    ⟩
  rev xs [] ++ (x ∷ []) ++ ys
    ≡⟨ sym (++-assoc (rev-List Lxs lnil) (x ∷ []) ys) ⟩
  (rev xs [] ++ (x ∷ [])) ++ ys
    ≡⟨ ++-leftCong (sym (rev-++ Lxs (x ∷ []))) ⟩
  rev xs (x ∷ []) ++ ys
    ≡⟨ ++-leftCong (sym (rev-∷ x xs [])) ⟩
  rev (x ∷ xs) [] ++ ys ∎

reverse-++ : ∀ {xs ys} → List xs → List ys →
             reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ {ys = ys} lnil Lys =
  reverse ([] ++ ys)       ≡⟨ reverseCong (++-leftIdentity ys) ⟩
  reverse ys               ≡⟨ sym (++-rightIdentity (reverse-List Lys)) ⟩
  reverse ys ++ []         ≡⟨ ++-rightCong (sym (rev-[] [])) ⟩
  reverse ys ++ reverse [] ∎

reverse-++ (lcons x {xs} Lxs) lnil =
  reverse ((x ∷ xs) ++ [])
    ≡⟨ reverseCong (++-rightIdentity (lcons x Lxs)) ⟩
  reverse (x ∷ xs)
    ≡⟨ sym (++-leftIdentity (reverse (x ∷ xs))) ⟩
  [] ++ reverse (x ∷ xs)
     ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  reverse [] ++ reverse (x ∷ xs) ∎

reverse-++ (lcons x {xs} Lxs) (lcons y {ys} Lys) =
  reverse ((x ∷ xs) ++ y ∷ ys)
    ≡⟨ refl ⟩
  rev ((x ∷ xs) ++ y ∷ ys) []
    ≡⟨ revCong₁ (++-∷ x xs (y ∷ ys)) ⟩
  rev (x ∷ (xs ++ y ∷ ys)) []
    ≡⟨ rev-∷ x (xs ++ y ∷ ys) [] ⟩
  rev (xs ++ y ∷ ys) (x ∷ [])
    ≡⟨ rev-++ (++-List Lxs (lcons y Lys)) (x ∷ []) ⟩
  rev (xs ++ y ∷ ys) [] ++ (x ∷ [])
    ≡⟨ refl ⟩
  reverse (xs ++ y ∷ ys) ++ (x ∷ [])
    ≡⟨ ++-leftCong (reverse-++ Lxs (lcons y Lys)) ⟩
  (reverse (y ∷ ys) ++ reverse xs) ++ x ∷ []
    ≡⟨ ++-assoc (reverse-List (lcons y Lys)) (reverse xs) (x ∷ []) ⟩
  reverse (y ∷ ys) ++ reverse xs ++ x ∷ []
    ≡⟨ refl ⟩
  reverse (y ∷ ys) ++ rev xs [] ++ x ∷ []
    ≡⟨ ++-rightCong (sym (rev-++ Lxs (x ∷ []))) ⟩
  reverse (y ∷ ys) ++ rev xs (x ∷ [])
    ≡⟨ ++-rightCong (sym (rev-∷ x xs [])) ⟩
  reverse (y ∷ ys) ++ rev (x ∷ xs) []
    ≡⟨ refl ⟩
  reverse (y ∷ ys) ++ reverse (x ∷ xs) ∎

reverse-∷ : ∀ x {ys} → List ys →
            reverse (x ∷ ys) ≡ reverse ys ++ (x ∷ [])
reverse-∷ x lnil =
  rev (x ∷ []) []     ≡⟨ rev-∷ x [] [] ⟩
  rev [] (x ∷ [])     ≡⟨ rev-[] (x ∷ []) ⟩
  x ∷ []              ≡⟨ sym (++-leftIdentity (x ∷ [])) ⟩
  [] ++ x ∷ []        ≡⟨ ++-leftCong (sym (rev-[] [])) ⟩
  rev [] [] ++ x ∷ [] ∎

reverse-∷ x (lcons y {ys} Lys) = sym prf
  where
  prf : reverse (y ∷ ys) ++ x ∷ [] ≡ reverse (x ∷ y ∷ ys)
  prf =
    reverse (y ∷ ys) ++ x ∷ []
      ≡⟨ ++-rightCong (sym (reverse-[x]≡[x] x)) ⟩
    (reverse (y ∷ ys) ++ reverse (x ∷ []))
      ≡⟨ sym (reverse-++ (lcons x lnil) (lcons y Lys)) ⟩
    reverse ((x ∷ []) ++ (y ∷ ys))
      ≡⟨ reverseCong (++-∷ x [] (y ∷ ys)) ⟩
    reverse (x ∷ ([] ++ (y ∷ ys)))
      ≡⟨ reverseCong (∷-rightCong (++-leftIdentity (y ∷ ys))) ⟩
    reverse (x ∷ y ∷ ys) ∎

reverse'-involutive-helper : ∀ x {ys} → List ys →
                             reverse' (ys ++ x ∷ []) ≡ x ∷ reverse' ys
reverse'-involutive-helper x lnil =
  reverse' ([] ++ x ∷ []) ≡⟨ reverse'Cong (++-[] (x ∷ [])) ⟩
  reverse' (x ∷ [])       ≡⟨ reverse'-∷ x [] ⟩
  reverse' [] ++ x ∷ []   ≡⟨ ++-leftCong reverse'-[] ⟩
  [] ++ x ∷ []            ≡⟨ ++-[] (x ∷ []) ⟩
  x ∷ []                  ≡⟨ ∷-rightCong (sym reverse'-[]) ⟩
  x ∷ reverse' []         ∎

reverse'-involutive-helper x (lcons y {ys} Lys) =
  reverse' ((y ∷ ys) ++ x ∷ [])
    ≡⟨ reverse'Cong (++-∷ y ys (x ∷ [])) ⟩
  reverse' (y ∷ ys ++ x ∷ [])
    ≡⟨ reverse'-∷ y (ys ++ x ∷ []) ⟩
  reverse' (ys ++ x ∷ []) ++ y ∷ []
    ≡⟨ ++-leftCong (reverse'-involutive-helper x Lys) ⟩
  (x ∷ reverse' ys) ++ (y ∷ [])
    ≡⟨ ++-∷ x (reverse' ys) (y ∷ []) ⟩
  x ∷ (reverse' ys ++ y ∷ [])
    ≡⟨ ∷-rightCong (sym (reverse'-∷ y ys)) ⟩
  x ∷ reverse' (y ∷ ys) ∎

-- Adapted from (Bird and Wadler, 1988 §5.4.2).
reverse'-involutive : ∀ {xs} → List xs → reverse' (reverse' xs) ≡ xs
reverse'-involutive lnil =
  reverse' (reverse' []) ≡⟨ reverse'Cong reverse'-[] ⟩
  reverse' []            ≡⟨ reverse'-[] ⟩
  []                     ∎

reverse'-involutive (lcons x {xs} Lxs) =
  reverse' (reverse' (x ∷ xs))
    ≡⟨ reverse'Cong (reverse'-∷ x xs) ⟩
  reverse' (reverse' xs ++ (x ∷ []))
    ≡⟨ reverse'-involutive-helper x (reverse'-List Lxs) ⟩
  x ∷ reverse' (reverse' xs)
    ≡⟨ ∷-rightCong (reverse'-involutive Lxs) ⟩
  x ∷ xs ∎

------------------------------------------------------------------------------
-- References

-- Bird, R. and Wadler, P. (1988). Introduction to Functional
-- Programming. Prentice Hall International.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Vec where

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

data Vec (A : Set) : Nat -> Set where
  ε   : Vec A zero
  _►_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

vec : {A : Set}{n : Nat} -> A -> Vec A n
vec {n = zero}  x = ε
vec {n = suc n} x = x ► vec x

_<*>_ : {A B : Set}{n : Nat} -> Vec (A -> B) n -> Vec A n -> Vec B n
ε        <*> ε        = ε
(f ► fs) <*> (x ► xs) = f x ► (fs <*> xs)

-- map
-- zip

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module MisformedTypeSignature where

postulate A : Set

(f g) : A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined as functions from a finite set to a type.
------------------------------------------------------------------------

-- This implementation is designed for reasoning about fixed-size
-- vectors where ease of retrieval of elements is prioritised.

-- See `Data.Vec` for an alternative implementation using inductive
-- data-types, which is more suitable for reasoning about vectors that
-- will grow or shrink in size.

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

module Data.Vec.Functional where

open import Data.Fin.Base using (Fin; zero; suc; splitAt; punchIn)
open import Data.List.Base as L using (List)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec.Base as V using (Vec)
open import Function
open import Level using (Level)

infixr 5 _∷_ _++_
infixl 4 _⊛_

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Definition

Vector : Set a → ℕ → Set a
Vector A n = Fin n → A

------------------------------------------------------------------------
-- Conversion

toVec : ∀ {n} → Vector A n → Vec A n
toVec = V.tabulate

fromVec : ∀ {n} → Vec A n → Vector A n
fromVec = V.lookup

toList : ∀ {n} → Vector A n → List A
toList = L.tabulate

fromList : ∀ (xs : List A) → Vector A (L.length xs)
fromList = L.lookup

------------------------------------------------------------------------
-- Construction and deconstruction

[] : Vector A zero
[] ()

_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
(x ∷ xs) zero    = x
(x ∷ xs) (suc i) = xs i

head : ∀ {n} → Vector A (suc n) → A
head xs = xs zero

tail : ∀ {n} → Vector A (suc n) → Vector A n
tail xs = xs ∘ suc

uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
uncons xs = head xs , tail xs

replicate : ∀ {n} → A → Vector A n
replicate = const

remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
remove i t = t ∘ punchIn i

------------------------------------------------------------------------
-- Transformations

map : (A → B) → ∀ {n} → Vector A n → Vector B n
map f xs = f ∘ xs

_++_ : ∀ {m n} → Vector A m → Vector A n → Vector A (m + n)
_++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)

foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
foldr f z {n = zero}  xs = z
foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))

foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
foldl f z {n = zero}  xs = z
foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)

rearrange : ∀ {m n} → (Fin m → Fin n) → Vector A n → Vector A m
rearrange r xs = xs ∘ r

_⊛_ : ∀ {n} → Vector (A → B) n → Vector A n → Vector B n
_⊛_ = _ˢ_

zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
zipWith f xs ys i = f (xs i) (ys i)

zip : ∀ {n} → Vector A n → Vector B n → Vector (A × B) n
zip = zipWith _,_


text:
open import Type
open import Logic.Classical as Logic using (Classical)
open import Logic.Predicate as Logic using ()

module Formalization.ClassicalPropositionalLogic ⦃ classical : ∀{ℓ} → Logic.∀ₗ(Classical{ℓ}) ⦄ where

import      Lvl
open import Data
open import Data.Boolean
import      Data.Boolean.Operators
open import Data.Boolean.Stmt
open import Data.Either as Either using (_‖_ ; Left ; Right)
open import Data.Tuple as Tuple using ()
private module BoolOp = Data.Boolean.Operators.Logic
open import Functional
open import Function.Names using (_⊜_)
open import Logic
open import Logic.Propositional as Logic using (_←_)
open import Logic.Propositional.Theorems as Logic using ()
open import Logic.Predicate.Theorems as Logic using ()
open import Relator.Equals
open import Relator.Equals.Proofs
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)
open        Sets.PredicateSet.BoundedQuantifiers
open import Structure.Relator.Properties
open import Syntax.Function
open import Type.Properties.Decidable.Proofs
open import Type.Properties.Decidable
open import Type.Size.Countable

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level

open import Formalization.ClassicalPropositionalLogic.NaturalDeduction
open import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Proofs
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Formalization.ClassicalPropositionalLogic.Syntax.Proofs
open import Formalization.ClassicalPropositionalLogic.Semantics
open import Formalization.ClassicalPropositionalLogic.Semantics.Proofs
import      Formalization.ClassicalPropositionalLogic.TruthTable as TruthTable

instance _ = classical-to-decidable
instance _ = classical-to-decider

module NaturalDeduction where
  private variable P : Type{ℓₚ}
  private variable Γ Γ₁ Γ₂ : Formulas(P){ℓ}
  private variable φ ψ : Formula(P)

  [⊢]-functionₗ : (Γ₁ ≡ₛ Γ₂) → ((Γ₁ ⊢_) ≡ₛ (Γ₂ ⊢_))
  [⊢]-functionₗ Γ₁Γ₂ = Logic.[↔]-intro (weaken (Logic.[↔]-to-[←] Γ₁Γ₂)) (weaken (Logic.[↔]-to-[→] Γ₁Γ₂))

  [⊢]-compose : (Γ ⊢ φ) → ((Γ ∪ singleton(φ)) ⊢ ψ) → (Γ ⊢ ψ)
  [⊢]-compose Γφ Γφψ = [∨]-elim Γφψ Γφψ ([∨]-introₗ Γφ)

  -- TODO: Is this provable? Does one need to include it in the definition of (_⊢_)? Is it even possible to include it?
  -- [⊢]-hypothesis : ((Γ ⊢ φ) → (Γ ⊢ ψ)) → ((Γ ∪ singleton(φ)) ⊢ ψ)
  -- [⊢]-hypothesis hyp = {!!}

  [⊢][→]-intro-from-[∨] : (Γ ⊢ ¬ φ) Logic.∨ (Γ ⊢ ψ) → (Γ ⊢ (φ ⟶ ψ))
  [⊢][→]-intro-from-[∨] {Γ = Γ}{φ}{ψ} (Left x) = [⟶]-intro ([⊥]-elim ([⊥]-intro (direct (Right [≡]-intro)) (weaken-union {Γ₂ = singleton φ} x)))
  [⊢][→]-intro-from-[∨] (Right x) = [⟶]-intro (weaken-union x)

  -- A smallest finite set of assumptions that is able to derive a formula.
  finiteAssumptions : ∀{φ : Formula(P)} → (Γ ⊢ φ) → Formulas(P){Lvl.of(P)}
  finiteAssumptions {φ = φ}        (direct _)                  = singleton(φ)
  finiteAssumptions {φ = .⊤}       [⊤]-intro                   = ∅
  finiteAssumptions {φ = .⊥}       ([⊥]-intro           p q)   = finiteAssumptions p ∪ finiteAssumptions q
  finiteAssumptions {φ = φ}        ([⊥]-elim            p)     = finiteAssumptions p
  finiteAssumptions {φ = ¬ φ}      ([¬]-intro{φ = φ}    p)     = finiteAssumptions p ∖ singleton(φ)
  finiteAssumptions {φ = φ}        ([¬]-elim {φ = φ}    p)     = finiteAssumptions p ∖ singleton(¬ φ)
  finiteAssumptions {φ = .(_ ∧ _)} ([∧]-intro           p q)   = finiteAssumptions p ∪ finiteAssumptions q
  finiteAssumptions {φ = φ}        ([∧]-elimₗ           p)     = finiteAssumptions p
  finiteAssumptions {φ = φ}        ([∧]-elimᵣ           p)     = finiteAssumptions p
  finiteAssumptions {φ = .(_ ∨ _)} ([∨]-introₗ          p)     = finiteAssumptions p
  finiteAssumptions {φ = .(_ ∨ _)} ([∨]-introᵣ          p)     = finiteAssumptions p
  finiteAssumptions {φ = _}        ([∨]-elim {φ = φ}{ψ} p q r) = ((finiteAssumptions p ∖ singleton(φ)) ∪ (finiteAssumptions q ∖ singleton(ψ))) ∪ finiteAssumptions r
  finiteAssumptions {φ = .(_ ⟶ _)} ([⟶]-intro{φ = φ}    p)     = finiteAssumptions p ∖ singleton(φ)
  finiteAssumptions {φ = φ}        ([⟶]-elim            p q)   = finiteAssumptions p ∪ finiteAssumptions q
  finiteAssumptions {φ = .(_ ⟷ _)} ([⟷]-intro{φ = φ}{ψ} p q)   = (finiteAssumptions p ∖ singleton(ψ)) ∪ (finiteAssumptions q ∖ singleton(φ))
  finiteAssumptions {φ = φ}        ([⟷]-elimₗ           p q)   = finiteAssumptions p ∪ finiteAssumptions q
  finiteAssumptions {φ = φ}        ([⟷]-elimᵣ           p q)   = finiteAssumptions p ∪ finiteAssumptions q

  finiteAssumptions-correctness : (p : (Γ ⊢ φ)) → (finiteAssumptions p ⊢ φ)
  finiteAssumptions-correctness (direct x)         = direct [≡]-intro
  finiteAssumptions-correctness [⊤]-intro          = [⊤]-intro
  finiteAssumptions-correctness ([⊥]-intro  p q)   = [⊥]-intro (weaken Left (finiteAssumptions-correctness p)) (weaken Right (finiteAssumptions-correctness q))
  finiteAssumptions-correctness ([⊥]-elim   p)     = [⊥]-elim (finiteAssumptions-correctness p)
  finiteAssumptions-correctness ([¬]-intro  p)     = [¬]-intro (weaken (Logic.[↔]-to-[←] ([∖][∪]-is-[∪] {A = finiteAssumptions p}{B = singleton _}) ∘ Logic.[∨]-introₗ) (finiteAssumptions-correctness p))
  finiteAssumptions-correctness ([¬]-elim   p)     = [¬]-elim (weaken (Logic.[↔]-to-[←] ([∖][∪]-is-[∪] {A = finiteAssumptions p}{B = singleton _}) ∘ Logic.[∨]-introₗ) (finiteAssumptions-correctness p))
  finiteAssumptions-correctness ([∧]-intro  p q)   = [∧]-intro (weaken Left (finiteAssumptions-correctness p)) (weaken Right (finiteAssumptions-correctness q))
  finiteAssumptions-correctness ([∧]-elimₗ  p)     = [∧]-elimₗ (finiteAssumptions-correctness p)
  finiteAssumptions-correctness ([∧]-elimᵣ  p)     = [∧]-elimᵣ (finiteAssumptions-correctness p)
  finiteAssumptions-correctness ([∨]-introₗ p)     = [∨]-introₗ (finiteAssumptions-correctness p)
  finiteAssumptions-correctness ([∨]-introᵣ p)     = [∨]-introᵣ (finiteAssumptions-correctness p)
  finiteAssumptions-correctness ([∨]-elim{φ = φ}{ψ} p q r) = [∨]-elim (weaken (sl ∘ Left) (finiteAssumptions-correctness p)) (weaken (sr ∘ Left) (finiteAssumptions-correctness q)) (weaken Right (finiteAssumptions-correctness r)) where
    postulate sl : (finiteAssumptions p ∪ singleton(φ)) ⊆ ((((finiteAssumptions p ∖ singleton(φ)) ∪ (finiteAssumptions q ∖ singleton(ψ))) ∪ finiteAssumptions r) ∪ singleton(φ))
    postulate sr : (finiteAssumptions q ∪ singleton(ψ)) ⊆ ((((finiteAssumptions p ∖ singleton(φ)) ∪ (finiteAssumptions q ∖ singleton(ψ))) ∪ finiteAssumptions r) ∪ singleton(ψ))
  finiteAssumptions-correctness ([⟶]-intro  p)     = [⟶]-intro (weaken (Logic.[↔]-to-[←] ([∖][∪]-is-[∪] {A = finiteAssumptions p}{B = singleton _}) ∘ Logic.[∨]-introₗ) (finiteAssumptions-correctness p))
  finiteAssumptions-correctness ([⟶]-elim   p q)   = [⟶]-elim (weaken Left (finiteAssumptions-correctness p)) (weaken Right (finiteAssumptions-correctness q))
  finiteAssumptions-correctness ([⟷]-intro  p q)   = [⟷]-intro (weaken (sl ∘ Left) (finiteAssumptions-correctness p)) (weaken (sr ∘ Left) (finiteAssumptions-correctness q)) where
    postulate sl : (finiteAssumptions p ∪ singleton(φ)) ⊆ (((finiteAssumptions p ∖ singleton(φ)) ∪ (finiteAssumptions q ∖ singleton(ψ))) ∪ singleton(φ))
    postulate sr : (finiteAssumptions q ∪ singleton(ψ)) ⊆ (((finiteAssumptions p ∖ singleton(φ)) ∪ (finiteAssumptions q ∖ singleton(ψ))) ∪ singleton(ψ))
  finiteAssumptions-correctness ([⟷]-elimₗ  p q)   = [⟷]-elimₗ (weaken Left (finiteAssumptions-correctness p)) (weaken Right (finiteAssumptions-correctness q))
  finiteAssumptions-correctness ([⟷]-elimᵣ  p q)   = [⟷]-elimᵣ (weaken Left (finiteAssumptions-correctness p)) (weaken Right (finiteAssumptions-correctness q))

  finiteAssumptions-subset : (p : (Γ ⊢ φ)) → (finiteAssumptions p ⊆ Γ)
  finiteAssumptions-subset        (direct x)         = \{[≡]-intro → x}
  finiteAssumptions-subset        [⊤]-intro          = empty
  finiteAssumptions-subset        ([⊥]-intro  p q)   = [∪]-subset (\{x} → finiteAssumptions-subset p {x}) (\{x} → finiteAssumptions-subset q {x})
  finiteAssumptions-subset        ([⊥]-elim   p)     = finiteAssumptions-subset p
  finiteAssumptions-subset        ([¬]-intro  p)     = [∪][∖]-invertᵣ-[⊆] {A = finiteAssumptions p} (finiteAssumptions-subset p)
  finiteAssumptions-subset        ([¬]-elim   p)     = [∪][∖]-invertᵣ-[⊆] {A = finiteAssumptions p} (finiteAssumptions-subset p)
  finiteAssumptions-subset        ([∧]-intro  p q)   = [∪]-subset (\{x} → finiteAssumptions-subset p {x}) (\{x} → finiteAssumptions-subset q {x})
  finiteAssumptions-subset        ([∧]-elimₗ  p)     = finiteAssumptions-subset p
  finiteAssumptions-subset        ([∧]-elimᵣ  p)     = finiteAssumptions-subset p
  finiteAssumptions-subset        ([∨]-introₗ p)     = finiteAssumptions-subset p
  finiteAssumptions-subset        ([∨]-introᵣ p)     = finiteAssumptions-subset p
  finiteAssumptions-subset{Γ = Γ} ([∨]-elim   p q r) = [∪]-subset (\{x} → [∪]-subset{C = Γ} ([∪][∖]-invertᵣ-[⊆] {B = Γ} (finiteAssumptions-subset p)) ([∪][∖]-invertᵣ-[⊆] {B = Γ} (finiteAssumptions-subset q)) {x}) (finiteAssumptions-subset r)
  finiteAssumptions-subset        ([⟶]-intro  p)     = \{(Logic.[∧]-intro fpx φx) → Logic.[∨]-elim id (Logic.[⊥]-elim ∘ φx) (finiteAssumptions-subset p fpx)}
  finiteAssumptions-subset        ([⟶]-elim   p q)   = [∪]-subset (\{x} → finiteAssumptions-subset p {x}) (\{x} → finiteAssumptions-subset q {x})
  finiteAssumptions-subset        ([⟷]-intro  p q)   = Logic.[∨]-elim ([∪][∖]-invertᵣ-[⊆] {A = finiteAssumptions p} (finiteAssumptions-subset p)) ([∪][∖]-invertᵣ-[⊆] {A = finiteAssumptions q} (finiteAssumptions-subset q))
  finiteAssumptions-subset        ([⟷]-elimₗ  p q)   = [∪]-subset (\{x} → finiteAssumptions-subset p {x}) (\{x} → finiteAssumptions-subset q {x})
  finiteAssumptions-subset        ([⟷]-elimᵣ  p q)   = [∪]-subset (\{x} → finiteAssumptions-subset p {x}) (\{x} → finiteAssumptions-subset q {x})

  {-
  module _ where
    open import Numeral.Natural

    finiteAssumptions-index : (p : (Γ ⊢ φ)) → ∀{x} → (x ∈ finiteAssumptions p) → ℕ
    finiteAssumptions-index (direct x) [≡]-intro = {!!}
    finiteAssumptions-index [⊤]-intro ()
    finiteAssumptions-index ([⊥]-intro p q) (Left x) = {!!}
    finiteAssumptions-index ([⊥]-intro p q) (Right x) = {!!}
    finiteAssumptions-index ([⊥]-elim p) = {!!}
    finiteAssumptions-index ([¬]-intro p) = {!!}
    finiteAssumptions-index ([¬]-elim p) = {!!}
    finiteAssumptions-index ([∧]-intro p p₁) = {!!}
    finiteAssumptions-index ([∧]-elimₗ p) = {!!}
    finiteAssumptions-index ([∧]-elimᵣ p) = {!!}
    finiteAssumptions-index ([∨]-introₗ p) = {!!}
    finiteAssumptions-index ([∨]-introᵣ p) = {!!}
    finiteAssumptions-index ([∨]-elim p p₁ p₂) = {!!}
    finiteAssumptions-index ([⟶]-intro p) = {!!}
    finiteAssumptions-index ([⟶]-elim p p₁) = {!!}
    finiteAssumptions-index ([⟷]-intro p p₁) = {!!}
    finiteAssumptions-index ([⟷]-elimₗ p p₁) = {!!}
    finiteAssumptions-index ([⟷]-elimᵣ p p₁) = {!!}
  -}

  module _ (Γ : Formulas(P){ℓ}) where
    ConsistentSubsetMaximality  = ∀{Δ : Formulas(P){Lvl.of(P) Lvl.⊔ ℓ}} → Consistent(Δ) → (Γ ⊆ Δ) → (Δ ⊆ Γ)
    ConsistentElementMaximality = ∀{φ} → Consistent(Γ ∪ singleton(φ)) → (φ ∈ Γ)
    CompleteDerivability        = ∀{φ} → (Γ ⊢ φ) Logic.∨ (Γ ⊢ (¬ φ))
    CompleteMembership          = ∀{φ} → (φ ∈ Γ) Logic.∨ ((¬ φ) ∈ Γ)

    -- Equivalences when `Γ` is consistent. Used in the definition of `MaximallyConsistent`.
    data ConsistentlyComplete : Stmt{Lvl.𝐒(Lvl.of(P) Lvl.⊔ ℓ)} where
      subset-intro          : ConsistentSubsetMaximality  → ConsistentlyComplete
      element-intro         : ConsistentElementMaximality → ConsistentlyComplete
      complete-deriv-intro  : CompleteDerivability        → ConsistentlyComplete
      complete-member-intro : CompleteMembership          → ConsistentlyComplete

    module CompleteMembership(p : CompleteMembership) where
      consistentSubsetMaximality : ConsistentSubsetMaximality
      consistentSubsetMaximality conΔ ΓΔ {φ} φΔ = Logic.[∨]-not-right (p{φ}) (¬φΓ ↦ conΔ([⊥]-intro (direct φΔ) (direct(ΓΔ ¬φΓ))))

    module ConsistentElementMaximality(element-maximal : ConsistentElementMaximality) where
      consistentSubsetMaximality : ConsistentSubsetMaximality
      consistentSubsetMaximality conΔ ΓΔ {φ} φΔ = element-maximal ([⊢]-subset-consistency (Logic.[∨]-elim ΓΔ (\{([≡]-intro) → φΔ})) conΔ)

      element-maximal-contra : (φ ∉ Γ) → Inconsistent(Γ ∪ singleton(φ))
      element-maximal-contra = Logic.[↔]-to-[←] Logic.contrapositive-variant2 element-maximal

      [⊢]-derivability-consistencyₗ : ((Γ ⊢ φ) ← Consistent(Γ ∪ singleton(φ)))
      [⊢]-derivability-consistencyₗ = direct ∘ element-maximal

      module Consistent(consistent : Consistent(Γ)) where
        [⊢]-to-[∈] : (Γ ⊢ φ) → (φ ∈ Γ)
        [⊢]-to-[∈] = Logic.[→]-from-contrary (\Γφ φ∉Γ → consistent ([⊢]-compose-inconsistency Γφ (element-maximal-contra φ∉Γ)))

        [⊢][∈]-equivalence : (Γ ⊢ φ) Logic.↔ (φ ∈ Γ)
        [⊢][∈]-equivalence = Logic.[↔]-intro direct [⊢]-to-[∈]

        -- [•]-maximal-membership : ((• p) ∈ Γ) Logic.↔ ?
        -- [•]-maximal-membership =

        [⊤]-maximal-membership : (⊤ ∈ Γ) Logic.↔ Logic.⊤
        [⊤]-maximal-membership = Logic.[↔]-intro l r where
          l = const (element-maximal (Γ⊤-incons ↦ consistent([⊢]-compose-inconsistency [⊤]-intro Γ⊤-incons)))
          r = const Logic.[⊤]-intro

        [⊥]-maximal-membership : (⊥ ∈ Γ) Logic.↔ Logic.⊥
        [⊥]-maximal-membership = Logic.[↔]-intro l r where
          l = Logic.[⊥]-elim
          r = consistent ∘ direct

        [¬]-maximal-membership : ((¬ φ) ∈ Γ) Logic.↔ (φ ∉ Γ)
        [¬]-maximal-membership = Logic.[↔]-intro l r where
          l = [⊢]-to-[∈] ∘ [¬]-intro ∘ element-maximal-contra
          r = [⊢]-consistent-noncontradicting-membership consistent

        [∧]-maximal-membership : ((φ ∧ ψ) ∈ Γ) Logic.↔ ((φ ∈ Γ) Logic.∧ (ψ ∈ Γ))
        [∧]-maximal-membership = Logic.[↔]-intro l r where
          l = \{(Logic.[∧]-intro φΓ ψΓ) → [⊢]-to-[∈] ([∧]-intro (direct φΓ) (direct ψΓ))}
          r = φψΓ ↦ Logic.[∧]-intro ([⊢]-to-[∈] ([∧]-elimₗ(direct φψΓ))) ([⊢]-to-[∈] ([∧]-elimᵣ(direct φψΓ)))

        [∨]-maximal-membership : ((φ ∨ ψ) ∈ Γ) Logic.↔ ((φ ∈ Γ) Logic.∨ (ψ ∈ Γ))
        [∨]-maximal-membership = Logic.[↔]-intro l r where
          l = Logic.[∨]-elim ([⊢]-to-[∈] ∘ [∨]-introₗ ∘ direct) ([⊢]-to-[∈] ∘ [∨]-introᵣ ∘ direct)
          r = Logic.contrapositiveₗ ⦃ classical ⦄ ((\{(Logic.[∧]-intro ¬φΓ ¬ψΓ) → φψΓ ↦ consistent([∨]-elim (element-maximal-contra ¬φΓ) (element-maximal-contra ¬ψΓ) (direct φψΓ))}) ∘ Logic.[↔]-to-[→] Logic.[¬]-preserves-[∨][∧])

        [⟶]-maximal-membership : ((φ ⟶ ψ) ∈ Γ) Logic.↔ ((φ ∉ Γ) Logic.∨ (ψ ∈ Γ))
        [⟶]-maximal-membership =
          Logic.[↔]-symmetry [⊢][∈]-equivalence ⦗ Logic.[↔]-transitivity ⦘ₗ
          [→]-disjunctive-form                  ⦗ Logic.[↔]-transitivity ⦘ₗ
          [⊢][∈]-equivalence                    ⦗ Logic.[↔]-transitivity ⦘ₗ
          [∨]-maximal-membership                ⦗ Logic.[↔]-transitivity ⦘ₗ
          Logic.[↔]-intro
            (Either.mapLeft (Logic.[↔]-to-[←] [¬]-maximal-membership))
            (Either.mapLeft ((Logic.[↔]-to-[→] [¬]-maximal-membership)))

        [⟷]-maximal-membership : ((φ ⟷ ψ) ∈ Γ) Logic.↔ (((φ ∈ Γ) Logic.∧ (ψ ∈ Γ)) Logic.∨ ((φ ∉ Γ) Logic.∧ (ψ ∉ Γ)))
        [⟷]-maximal-membership =
          Logic.[↔]-symmetry [⊢][∈]-equivalence ⦗ Logic.[↔]-transitivity ⦘ₗ
          [⟷]-conjunction-disjunction-negation  ⦗ Logic.[↔]-transitivity ⦘ₗ
          [⊢][∈]-equivalence                    ⦗ Logic.[↔]-transitivity ⦘ₗ
          [∨]-maximal-membership                ⦗ Logic.[↔]-transitivity ⦘ₗ
          Logic.[↔]-intro
            (Either.map (Logic.[↔]-to-[←] [∧]-maximal-membership) (Logic.[↔]-to-[←] [∧]-maximal-membership))
            (Either.map (Logic.[↔]-to-[→] [∧]-maximal-membership) (Logic.[↔]-to-[→] [∧]-maximal-membership))
                                                ⦗ Logic.[↔]-transitivity ⦘ₗ
          Logic.[↔]-intro
            (Either.mapRight (Tuple.map (Logic.[↔]-to-[←] [¬]-maximal-membership) (Logic.[↔]-to-[←] [¬]-maximal-membership)))
            (Either.mapRight (Tuple.map (Logic.[↔]-to-[→] [¬]-maximal-membership) (Logic.[↔]-to-[→] [¬]-maximal-membership)))

        complete-membership : CompleteMembership
        complete-membership = Logic.[¬→]-disjunctive-formᵣ (Logic.[↔]-to-[←] [¬]-maximal-membership)

        equal-model-existence : Logic.∃(𝔐 ↦ (Γ ≡ₛ (𝔐 ⊧_)))
        equal-model-existence = Logic.[∃]-intro witness ⦃ Logic.[↔]-intro l r ⦄ where
          witness = (p ↦ decide(0)((• p) ∈ Γ))

          l : (witness ⊧ φ) → (φ ∈ Γ)
          r : witness ⊧₊ Γ

          r {• x}   = Logic.[↔]-to-[→] decider-true
          r {⊤}     = Logic.[↔]-to-[→] [⊤]-maximal-membership
          r {⊥}     = Logic.[↔]-to-[→] [⊥]-maximal-membership
          r {¬ φ}   = Logic.contrapositiveᵣ l ∘ Logic.[↔]-to-[→] [¬]-maximal-membership
          r {φ ∧ ψ} = Tuple.map r r ∘ Logic.[↔]-to-[→] [∧]-maximal-membership
          r {φ ∨ ψ} = Either.map r r ∘ Logic.[↔]-to-[→] [∨]-maximal-membership
          r {φ ⟶ ψ} = Either.map (Logic.contrapositiveᵣ l) r ∘ Logic.[↔]-to-[→] [⟶]-maximal-membership
          r {φ ⟷ ψ} = Either.map (Tuple.map r r) (Tuple.map (Logic.contrapositiveᵣ l) (Logic.contrapositiveᵣ l)) ∘ Logic.[↔]-to-[→] [⟷]-maximal-membership

          l {• x}   = Logic.[↔]-to-[←] decider-true
          l {⊤}     = Logic.[↔]-to-[←] [⊤]-maximal-membership
          l {¬ φ}   = Logic.[↔]-to-[←] [¬]-maximal-membership ∘ Logic.contrapositiveᵣ r
          l {φ ∧ ψ} = Logic.[↔]-to-[←] [∧]-maximal-membership ∘ Tuple.map l l
          l {φ ∨ ψ} = Logic.[↔]-to-[←] [∨]-maximal-membership ∘ Either.map l l
          l {φ ⟶ ψ} = Logic.[↔]-to-[←] [⟶]-maximal-membership ∘ Either.map (Logic.contrapositiveᵣ r) l
          l {φ ⟷ ψ} = Logic.[↔]-to-[←] [⟷]-maximal-membership ∘ Either.map (Tuple.map l l) (Tuple.map (Logic.contrapositiveᵣ r) (Logic.contrapositiveᵣ r))

        satisfiable : Satisfiable(Γ)
        satisfiable = Logic.[∃]-map-proof (\eq {φ} → Logic.[↔]-to-[→] (eq{φ})) equal-model-existence

    module ConsistentSubsetMaximality(p : ConsistentSubsetMaximality) where
      consistentElementMaximality : ConsistentElementMaximality
      consistentElementMaximality con = p con Left (Right [≡]-intro)

    module CompleteDerivability(p : CompleteDerivability) where
      module Consistent(consistent : Consistent(Γ)) where
        [⊢]-to-[∈]' : (Γ ⊢ φ) → (φ ∈ Γ)
        [⊢]-to-[∈]' {φ = φ} = Logic.[→]-disjunctive-formₗ {!!}

        consistentSubsetMaximality : ConsistentSubsetMaximality
        consistentSubsetMaximality {Δ} conΔ ΓΔ {φ} φΔ = {!Logic.[¬→]-disjunctive-formₗ (Either.map (weaken ΓΔ) (weaken ΓΔ) (p{φ}))!}
        {-with p{φ} | Logic.excluded-middle((¬ φ) ∈ Δ)
        ... | Left  q | Left  r = {!!}
        ... | Left  q | Right r with () ← Logic.contrapositiveᵣ(weaken ΓΔ) {!!} {!!}
        ... | Right q | _       with () ← conΔ([⊥]-intro (direct φΔ) (weaken ΓΔ q))-}
        -- conΔ([⊥]-intro (direct φΔ) (direct(ΓΔ ¬φΓ)))
        -- Logic.[∨]-not-right (p{φ}) (¬φΓ ↦ ?)

        consistentElementMaximality : ConsistentElementMaximality
        consistentElementMaximality {φ} conΓφ with p{φ} | Logic.excluded-middle((¬ φ) ∈ Γ)
        ... | Left  q | Left  r with () ← consistent([⊥]-intro q (direct r))
        ... | Left  q | Right r = Logic.[¬¬]-elim (¬Γφ ↦ {![⊢]-consistent-noncontradicting-membership consistent !})
        ... | Right q | _       with () ← conΓφ([¬]-intro-converse q)
        -- ConsistentSubsetMaximality.consistentElementMaximality {!!}
        -- [⊢]-derivability-consistencyᵣ consistent q
        -- [¬]-intro(Logic.[↔]-to-[→] [⊢]-derivability-inconsistency q)
        -- Logic.contrapositiveᵣ direct conΓφ
        -- (¬φΓ ↦ Logic.contrapositiveᵣ direct (conΓφ ∘ [¬]-intro-converse) {!r ∘ direct!})
        -- [⊢]-consistent-noncontradicting-membership consistent
        -- (r ∘ direct)

        completeMembership : CompleteMembership
        completeMembership = Either.map [⊢]-to-[∈] [⊢]-to-[∈] p where
          [⊢]-to-[∈] = (ConsistentElementMaximality.Consistent.[⊢]-to-[∈] consistentElementMaximality consistent)

  record MaximallyConsistent (Γ : Formulas(P){ℓ}) : Stmt{Lvl.𝐒(Lvl.of(P) Lvl.⊔ ℓ)} where
    field
      consistent : Consistent(Γ)
      maximal    : ConsistentlyComplete(Γ)

    subset-maximal  : ConsistentSubsetMaximality(Γ)
    element-maximal : ConsistentElementMaximality(Γ)

    element-maximal with maximal
    ... | subset-intro          p = ConsistentSubsetMaximality.consistentElementMaximality Γ p
    ... | element-intro         p = p
    ... | complete-deriv-intro  p = ConsistentSubsetMaximality.consistentElementMaximality Γ subset-maximal where
    ... | complete-member-intro p = ConsistentSubsetMaximality.consistentElementMaximality Γ (CompleteMembership.consistentSubsetMaximality Γ p)

    open ConsistentElementMaximality Γ element-maximal using
      ( element-maximal-contra
      ; [⊢]-derivability-consistencyₗ
      ) public

    open ConsistentElementMaximality.Consistent Γ element-maximal consistent using
      ( [⊢]-to-[∈]
      ; equal-model-existence
      ) public

    subset-maximal with maximal
    ... | subset-intro          p = p
    ... | element-intro         p = ConsistentElementMaximality.consistentSubsetMaximality Γ p
    ... | complete-deriv-intro  p = CompleteMembership.consistentSubsetMaximality Γ (Either.map [⊢]-to-[∈] [⊢]-to-[∈] p)
    ... | complete-member-intro p = CompleteMembership.consistentSubsetMaximality Γ p

    {-r : (term-model(max Γ con) ⊧ φ) → (φ ∈ max Γ con)
    r {• x}   modelsφ Γφ-incons = Logic.[↔]-to-[←] Logic.decide-is-true modelsφ Γφ-incons
    r {⊤}     modelsφ Γφ-incons = con([⊢]-compose-inconsistency [⊤]-intro Γφ-incons)-}

  open MaximallyConsistent ⦃ … ⦄ using
    ( [⊢]-derivability-consistencyₗ
    ; [⊤]-maximal-membership
    ; [⊥]-maximal-membership
    ; [¬]-maximal-membership
    ; [∧]-maximal-membership
    ; [∨]-maximal-membership
    ; [⟶]-maximal-membership
    ; [⟷]-maximal-membership
    ) public

  module _ ⦃ countable-P : CountablyInfinite P ⦄ where
    -- Also called: Lindenbaums' lemma
    open import Numeral.Natural
    private variable n : ℕ
    {-
    data maxi (Γ : Formulas(P){ℓ}) : ℕ → Formulas(P){Lvl.of(P) Lvl.⊔ ℓ} where
      base : Γ        ⊆ maxi Γ 𝟎
      step : maxi Γ n ⊆ maxi Γ (𝐒(n))
      form : let ψ = Logic.[∃]-witness (Formula-is-countably-infinite {P = P}) n
             in  maxi Γ (𝐒(n)) (if Logic.decide(maxi Γ n ⊢ ψ) then ψ else (¬ ψ))

    maxi-zero : (Γ ≡ₛ maxi Γ 𝟎)
    maxi-zero = Logic.[↔]-intro (\{(base p) → p}) base

    maxi-succ : let ψ = Logic.[∃]-witness (Formula-is-countably-infinite {P = P}) n in (((maxi Γ n) ∪ singleton(if Logic.decide(maxi Γ n ⊢ ψ) then ψ else (¬ ψ))) ≡ₛ maxi Γ (𝐒(n)))
    maxi-succ {n = n}{Γ = Γ} = Logic.[↔]-intro l r where
      p = Logic.[∃]-witness (Formula-is-countably-infinite {P = P}) n

      l : ((maxi Γ n) ∪ singleton(if Logic.decide(maxi Γ n ⊢ p) then p else (¬ p))) ⊇ maxi Γ (𝐒(n))
      l (step x) = Left x
      l form     = Right [≡]-intro

      r : ((maxi Γ n) ∪ singleton(if Logic.decide(maxi Γ n ⊢ p) then p else (¬ p))) ⊆ maxi Γ (𝐒(n))
      r (Left x)          = step x
      r (Right [≡]-intro) = form

    maxi-superset : Consistent(Γ) → (∀{n} → (Γ ⊆ maxi Γ n))
    maxi-superset {Γ = Γ} con {𝟎} = Logic.[↔]-to-[→] maxi-zero
    maxi-superset {Γ = Γ} con {𝐒 n} {φ} Γφ = {!!}

    instance
      maxi-consistent : Consistent(Γ) → (∀{n} → Consistent(maxi Γ n))
      maxi-consistent         con {n = 𝟎}   = [⊢]-subset-consistency (Logic.[↔]-to-[←] maxi-zero) con
      maxi-consistent {Γ = Γ} con {n = 𝐒 n} = [⊢]-subset-consistency (Logic.[↔]-to-[←] maxi-succ) con-eq where
        p = Logic.[∃]-witness (Formula-is-countably-infinite {P = P}) n
        con-eq : Consistent((maxi Γ n) ∪ singleton(if Logic.decide(maxi Γ n ⊢ p) then p else (¬ p)))
        con-eq with Logic.excluded-middle(maxi Γ n ⊢ p) | Logic.decide(maxi Γ n ⊢ p)
        ... | Left  derp  | _ = [⊢]-compose-consistency derp (maxi-consistent con {n = n})
        ... | Right dernp | _ = [⊬]-negation-consistency(dernp ∘ [¬¬]-elim)
    -}

    maxi2 : Formulas(P){ℓ} → ℕ → Formulas(P){Lvl.of(P) Lvl.⊔ ℓ}
    maxi2 Γ 𝟎      = Lvl.Up{Lvl.of(P)} ∘ Γ
    maxi2 Γ (𝐒(n)) = let ψ = CountablyInfinite.index(Formula P) n
                     in  (maxi2 Γ n) ∪ singleton(if decide(0)(maxi2 Γ n ⊢ ψ) then ψ else (¬ ψ))

    maxi2-succ : let ψ = CountablyInfinite.index(Formula P) n in (((maxi2 Γ n) ∪ singleton(if decide(0)(maxi2 Γ n ⊢ ψ) then ψ else (¬ ψ))) ≡ₛ maxi2 Γ (𝐒(n)))
    -- maxi2-succ {n = n}{Γ = Γ} = Logic.[↔]-intro {!!} {!!}

    maxi2-zero : (Γ ≡ₛ maxi2 Γ 𝟎)
    maxi2-zero {Γ = Γ} = Logic.[↔]-symmetry (Sets.PredicateSet.LvlUp-set-equality {S = Γ})

    maxi2-superset : ∀{n} → (Γ ⊆ maxi2 Γ n)
    maxi2-superset {Γ = Γ} {𝟎}   = Logic.[↔]-to-[→] (maxi2-zero {Γ = Γ})
    maxi2-superset {Γ = Γ} {𝐒 n} = Left ∘ maxi2-superset {Γ = Γ} {n}

    instance
      maxi2-consistent : Consistent(Γ) → (∀{n} → Consistent(maxi2 Γ n))
      maxi2-consistent {Γ = Γ} con {n = 𝟎}   = [⊢]-subset-consistency (Logic.[↔]-to-[←] (maxi2-zero {Γ = Γ})) con
      maxi2-consistent {Γ = Γ} con {n = 𝐒 n} = [⊢]-subset-consistency (Logic.[↔]-to-[←] (maxi2-succ {Γ = Γ})) con-eq where
        p = CountablyInfinite.index(Formula P) n
        con-eq : Consistent((maxi2 Γ n) ∪ singleton(if decide(0)(maxi2 Γ n ⊢ p) then p else (¬ p)))
        con-eq with Logic.excluded-middle(maxi2 Γ n ⊢ p) | decide(0)(maxi2 Γ n ⊢ p)
        ... | Left  derp  | _ = [⊢]-compose-consistency derp (maxi2-consistent con {n = n})
        ... | Right dernp | _ = [⊬]-negation-consistency(dernp ∘ [¬¬]-elim)

    max : (Γ : Formulas(P){ℓ}) → Formulas(P){Lvl.of(P) Lvl.⊔ ℓ}
    max(Γ) φ = Logic.∃(n ↦ φ ∈ maxi2 Γ n)

    maxi2-subset-max : (maxi2 Γ n ⊆ max Γ)
    maxi2-subset-max {Γ = Γ} {n} p = Logic.[∃]-intro n ⦃ p ⦄

    open import Lang.Inspect
    max-maximal : (φ ∈ max Γ) Logic.∨ ((¬ φ) ∈ max Γ)
    max-maximal {φ = φ}{Γ = Γ}
      with n ← CountablyInfinite.indexing(Formula P) φ
      with Logic.excluded-middle(maxi2 Γ n ⊢ CountablyInfinite.index(Formula P) n) | inspect(maxi2 Γ) (𝐒 n)
    ... | Left  p | intro q with r ← [≡]-with(_$ CountablyInfinite.index(Formula P) n) q = Left  (Logic.[∃]-intro (𝐒(n)) ⦃ Right {!!} ⦄)
    ... | Right p | intro q = Right (Logic.[∃]-intro (𝐒(n)) ⦃ Right {!q!} ⦄)

    instance
      max-consistent : Consistent(Γ) → Consistent(max Γ)
      max-consistent {Γ = Γ} con = [⊢]-subset-consistency (Logic.[∃]-proof test5) (maxi2-consistent con {Logic.[∃]-witness test5}) where
        open import Numeral.Natural.Relation.Order
        open import Type.Properties.Inhabited

        test2 : (φ ∈ max Γ) → Logic.∃(n ↦ (φ ∈ maxi2 Γ n))
        test2 p = p

        test3a : ∀{φ} → Logic.∃(n ↦ ((φ ∈ max Γ) → (φ ∈ maxi2 Γ n)))
        test3a = Logic.[∃]-unrelatedᵣ-[→]ₗ ⦃ pos = intro ⦃ 𝟎 ⦄ ⦄ test2

        test3b : Logic.∃{Obj = Formula(P) → ℕ}(n ↦ (max Γ) ⊆ (φ ↦ φ ∈ maxi2 Γ (n(φ))))
        test3b = Logic.[∀][∃]-to-function-existence test3a

        test4 : ∀{a b} → (a ≤ b) → ∀{Γ : Formulas(P){ℓ}} → ((maxi2 Γ a) ⊆ (maxi2 Γ b))
        test4 {a = 𝟎}   {𝟎}   [≤]-minimum                  p = p
        test4 {a = 𝟎}   {𝐒 b} [≤]-minimum           {Γ}    p = Left(test4 {a = 𝟎}{b} [≤]-minimum {Γ} p)
        test4 {a = 𝐒 a} {𝐒 b} ([≤]-with-[𝐒] ⦃ ab ⦄) {Γ}    (Left p)  = Left (test4 {a = a}{b} ab p)
        test4 {a = 𝐒 a} {𝐒 b} ([≤]-with-[𝐒] ⦃ ab ⦄) {Γ}{φ} (Right p) = {!test4 {a = a}{b = b} ab {Γ ∪ singleton(if Logic.decide(maxi2 Γ b ⊢ β) then β else (¬ β))}{φ} ? !} where
          β = CountablyInfinite.index(Formula P) b
        {-with Logic.excluded-middle(maxi2 Γ a ⊢ Logic.[∃]-witness Formula-is-countably-infinite a) | p
        ... | Left x | [≡]-intro = {!!}
        ... | Right x | q = test4 {a} {𝐒 b} {!!} {!!}-}

        -- TODO: Because test3 and test4
        test5 : Logic.∃(n ↦ (max Γ) ⊆ (maxi2 Γ n))

      -- with [∃]-intro n ⦃ pn ⦄ ← max Γ = {!!}
      -- [⊢]-subset-consistency (\{φ} → {!maxi2-consistent con {n = 𝟎}!}) {!con!}

    instance
      max-maximally-consistent : Consistent(Γ) → MaximallyConsistent(max Γ)
      MaximallyConsistent.consistent (max-maximally-consistent         con) = max-consistent con
      MaximallyConsistent.maximal    (max-maximally-consistent {Γ = Γ} con) = {!!}
      -- {φ} conm with n ← CountablyInfinite.indexing(Formula P) φ = {!!}

    max-superset : Γ ⊆ max Γ
    max-superset {Γ = Γ} Γφ = Logic.[∃]-intro 𝟎 ⦃ maxi2-superset {Γ = Γ}{n = 𝟎} Γφ ⦄

{-

  {-
  max : (Γ : Formulas(P){ℓ}) → Consistent(Γ) → Formulas(P){Lvl.𝐒(Lvl.of(P) Lvl.⊔ ℓ)}
  max Γ con φ = Consistent(Γ ∪ singleton(φ)) -- TODO: Probably not like this. The problem with this definition is that (Consistent(Γ ∪ singleton(φ)) → (Γ ⊢ φ)) is impossible to prove, and it is neccessary for proving that (max Γ con) for any Γ is a consistent set of formulas. This is related to the issue that if both (Γ ∪ singleton(φ)) and (Γ ∪ singleton(¬ φ)) is consistent, then both of them will be included. But this would lead to (max Γ cons) not necccesarily consistent.
  -- if decide(Consistent(Γ ∪ singleton(φ))) then (Γ ∪ singleton(φ)) else (Γ ∪ singleton(¬ φ))
  {-data max2 (Γ : Formulas(P){ℓ}) (con : Consistent(Γ)) : Formulas(P){Lvl.𝐒(Lvl.of(P) Lvl.⊔ ℓ)} where
    Positive : Consistent  (Γ ∪ singleton(φ)) → Inconsistent(Γ ∪ singleton(¬ φ)) → max2 Γ con φ
    Negative : Inconsistent(Γ ∪ singleton(φ)) → Consistent  (Γ ∪ singleton(¬ φ)) → max2 Γ con φ
  -}
  max2 : (Γ : Formulas(P){ℓ}) → Consistent(Γ) → Formulas(P){Lvl.𝐒(Lvl.of(P) Lvl.⊔ ℓ)}
  max2 Γ con φ = Consistent(Γ ∪ singleton(φ)) Logic.∧ Inconsistent(Γ ∪ singleton(¬ φ))

  max-maximal : ∀{con : Consistent(Γ)} → (φ ∈ max Γ con) Logic.∨ ((¬ φ) ∈ max Γ con)
  max-maximal {Γ = Γ}{φ = φ}{con = con} with Logic.excluded-middle(Inconsistent(Γ ∪ singleton(φ))) ⦃ classical ⦄
  ... | Logic.[∨]-introₗ  Γφ⊥ = Logic.[∨]-introᵣ (Γ¬φ⊥ ↦ Logic.[⊥]-elim(con ([⊥]-intro ([¬]-elim Γ¬φ⊥) ([¬]-intro Γφ⊥))))
  ... | Logic.[∨]-introᵣ ¬Γφ⊥ = Logic.[∨]-introₗ ¬Γφ⊥

  max-no-bottom : ∀{con : Consistent(Γ)} → (⊥ ∉ max Γ con)
  max-no-bottom = apply(direct(Right [≡]-intro))

  max-consistent-containment : ∀{con : Consistent(Γ)} → (φ ∈ max Γ con) → ((¬ φ) ∈ max Γ con) → Logic.⊥
  max-consistent-containment {Γ = Γ}{φ = φ}{con = con} ¬Γφ⊥ ¬Γ¬φ⊥ = ¬Γφ⊥ ([⊥]-intro (direct (Right [≡]-intro)) {!!})

  max-consistency-membership : ∀{con} → Consistent(Γ ∪ singleton(φ)) Logic.↔ (φ ∈ max Γ con)
  max-consistency-membership = Logic.[↔]-intro id id

  max-inconsistency-membership2 : ∀{con} → Inconsistent(Γ ∪ singleton(φ)) Logic.↔ (φ ∉ max Γ con)
  max-inconsistency-membership2 = Logic.[↔]-intro Logic.[¬¬]-elim apply

  test : ∀{con} → (φ ∉ max Γ con) → ((¬ φ) ∈ max Γ con)
  test {con = con} p = [⊢]-compose-consistency ([¬]-intro(Logic.[¬¬]-elim p)) con

  max-consistent : ∀{con : Consistent(Γ)} → Consistent(max Γ con)
  max-consistent {Γ = Γ} {con = con} = Logic.contrapositiveᵣ {!!} con
  {-max-consistent {Γ = Γ} {con = con} (direct x)        = max-no-bottom{con = con} x
  max-consistent {Γ = Γ} {con = con} ([⊥]-intro p q)   = {!max-consistent q!}
  max-consistent {Γ = Γ} {con = con} ([⊥]-elim  p)     = max-consistent{con = con} p
  max-consistent {Γ = Γ} {con = con} ([¬]-elim  p)     = {!!}
  max-consistent {Γ = Γ} {con = con} ([∧]-elimₗ p)     = {!max-consistent !}
  max-consistent {Γ = Γ} {con = con} ([∧]-elimᵣ p)     = {!!}
  max-consistent {Γ = Γ} {con = con} ([∨]-elim  p q r) = {!!}
  max-consistent {Γ = Γ} {con = con} ([⟶]-elim  p q)   = {!!}
  max-consistent {Γ = Γ} {con = con} ([⟷]-elimₗ p q)   = {!!}
  max-consistent {Γ = Γ} {con = con} ([⟷]-elimᵣ p q)   = {!!}-}

  {-
  test2 : ∀{con} → ((¬ φ) ∈ max Γ con) → (φ ∉ max Γ con)
  test2 {con = con} p q = {!!}

  test3 : ∀{con} → (max Γ con ⊢ φ) → (Γ ⊢ φ)
  test3 {Γ = Γ} {φ} {con = con} (direct x) = {!!}
  test3 {Γ = Γ} {.⊤} {con = con} [⊤]-intro = {!!}
  test3 {Γ = Γ} {.⊥} {con = con} ([⊥]-intro p p₁) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([⊥]-elim p) = {!!}
  test3 {Γ = Γ} {.(¬ _)} {con = con} ([¬]-intro p) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([¬]-elim p) = {!!}
  test3 {Γ = Γ} {.(_ ∧ _)} {con = con} ([∧]-intro p p₁) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([∧]-elimₗ p) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([∧]-elimᵣ p) = {!!}
  test3 {Γ = Γ} {.(_ ∨ _)} {con = con} ([∨]-introₗ p) = {!!}
  test3 {Γ = Γ} {.(_ ∨ _)} {con = con} ([∨]-introᵣ p) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([∨]-elim p p₁ p₂) = {!!}
  test3 {Γ = Γ} {.(_ ⟶ _)} {con = con} ([⟶]-intro p) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([⟶]-elim p p₁) = {!!}
  test3 {Γ = Γ} {.(_ ⟷ _)} {con = con} ([⟷]-intro p p₁) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([⟷]-elimₗ p p₁) = {!!}
  test3 {Γ = Γ} {φ} {con = con} ([⟷]-elimᵣ p p₁) = {!!}
  -}

  max-inconsistency-membership : ∀{con} → Inconsistent(Γ ∪ singleton(φ)) Logic.↔ ((¬ φ) ∈ max Γ con)
  max-inconsistency-membership {Γ = Γ}{φ = φ}{con = con} =
    Logic.double-negation ⦗ Logic.[↔]-transitivity ⦘ₗ
    Logic.[¬]-unaryOperator max-consistency-membership ⦗ Logic.[↔]-transitivity ⦘ₗ
    Logic.[↔]-intro
      ll
      (Γ¬φ-incons ↦ Γφ-incons ↦ con([⊥]-intro ([¬]-elim Γφ-incons) ([¬]-intro (Logic.[¬¬]-elim Γ¬φ-incons))))
    where
      ll : Logic.¬((Γ ∪ singleton(¬ φ)) ⊢ ⊥) → Logic.¬((Γ ∪ singleton(φ)) ⊢ ⊥) → Empty
      ll ¬φin φin = {!!}
      -- () ← ¬φin([⊥]-intro {!!} (direct (Right [≡]-intro)))
      -- con([⊥]-intro {!!} {!!})
      --
      -- {![⊥]-intro (direct φin) (direct ¬φin)!})
  -- Logic.contrapositiveₗ ⦃ classical ⦄ (Γ¬φ-incons ↦ Γφ-incons ↦ con([⊥]-intro ([¬]-elim (Logic.[¬¬]-elim Γ¬φ-incons)) ([¬]-intro Γφ-incons)))

  max-superset : ∀{con : Consistent(Γ)} → (Γ ⊆ max Γ con)
  max-superset {con = con} {x = φ} φΓ Γφ⊥ = con ([⊥]-intro (direct φΓ) ([¬]-intro Γφ⊥))

  -- TODO: Are there any easy ways to prove this?
  instance
    max-maximally-consistent : ∀{con : Consistent(Γ)} → MaximallyConsistent(max Γ con)
    MaximallyConsistent.consistent (max-maximally-consistent {con = con}) = max-consistent{con = con}
    MaximallyConsistent.element-maximal max-maximally-consistent p = {!!} -- max-consistency-membership {!Logic.contrapositive-variant2ₗ weaken-union-singleton!} -- max-consistency-membership {!p!}

  -- max-[⊢]-subset : ∀{con : Consistent(Γ)} → ((max Γ con ⊢_) ⊆ (Γ ⊢_))
  -- max-[⊢]-subset {con = con} p = {!!}
-}
-}

module _ where
  open NaturalDeduction

  private variable P : Type{ℓₚ}
  private variable φ ψ : Formula(P)

  module _ where
    private variable Γ Γ₁ Γ₂ : Formulas(P){ℓₚ}

    soundness : (Γ ⊢ φ) → (Γ ⊨ φ)
    soundness (direct Γφ) 𝔐Γ            = 𝔐Γ(Γφ)
    soundness [⊤]-intro                 = const(Logic.[⊤]-intro)
    soundness ([⊥]-intro Γφ Γ¬φ) 𝔐Γ     = (soundness Γ¬φ 𝔐Γ) (soundness Γφ 𝔐Γ)
    soundness ([⊥]-elim Γ⊥) 𝔐Γ          = Logic.[⊥]-elim(soundness Γ⊥ 𝔐Γ)
    soundness {Γ = Γ}{φ = φ} ([¬]-intro Γφ⊥) 𝔐Γ 𝔐φ = soundness Γφ⊥ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton _} (𝔐Γ) (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] 𝔐φ))
    soundness {Γ = Γ}{φ = φ} ([¬]-elim Γ¬φ⊥) {𝔐} 𝔐Γ = Logic.[¬¬]-elim {P = (𝔐 ⊧ φ)} (¬𝔐φ ↦ soundness Γ¬φ⊥ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton _} 𝔐Γ (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] ¬𝔐φ)))
    soundness ([∧]-intro Γφ Γψ) 𝔐Γ = (Logic.[∧]-intro (soundness Γφ 𝔐Γ) (soundness Γψ 𝔐Γ))
    soundness ([∧]-elimₗ Γφψ) = Logic.[∧]-elimₗ ∘ (soundness Γφψ)
    soundness ([∧]-elimᵣ Γφψ) = Logic.[∧]-elimᵣ ∘ (soundness Γφψ)
    soundness ([∨]-introₗ Γφ) = Logic.[∨]-introₗ ∘ (soundness Γφ)
    soundness ([∨]-introᵣ Γψ) = Logic.[∨]-introᵣ ∘ (soundness Γψ)
    soundness {Γ = Γ}{φ = φ} ([∨]-elim {φ = ψ₁} {ψ₂} Γψ₁φ Γψ₂φ Γψ₁ψ₂) {𝔐} 𝔐Γ =
      (Logic.[∨]-elim
        (𝔐ψ₁ ↦ soundness Γψ₁φ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton _} (𝔐Γ) (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] 𝔐ψ₁)))
        (𝔐ψ₂ ↦ soundness Γψ₂φ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton _} (𝔐Γ) (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] 𝔐ψ₂)))
        (soundness Γψ₁ψ₂ 𝔐Γ)
      )
    soundness {Γ = Γ} ([⟶]-intro Γφψ) 𝔐Γ = Logic.[→]-disjunctive-formᵣ (𝔐φ ↦ soundness Γφψ ([⊧₊]-strengthen {Γ₁ = Γ}{Γ₂ = singleton _} (𝔐Γ) (Logic.[↔]-to-[→] [⊧]-to-[⊧₊] 𝔐φ)))
    soundness ([⟶]-elim Γφ Γφψ) 𝔐Γ = Logic.[→]-disjunctive-formₗ((soundness Γφψ) 𝔐Γ) (soundness Γφ 𝔐Γ)
    soundness {Γ = Γ} ([⟷]-intro {φ = φ} {ψ = ψ} Γψφ Γφψ) {𝔐} 𝔐Γ with Logic.excluded-middle(𝔐 ⊧ φ) | Logic.excluded-middle(𝔐 ⊧ ψ)
    ... | Logic.[∨]-introₗ 𝔐φ  | Logic.[∨]-introₗ 𝔐ψ  = Logic.[∨]-introₗ (Logic.[∧]-intro 𝔐φ 𝔐ψ)
    ... | Logic.[∨]-introₗ 𝔐φ  | Logic.[∨]-introᵣ ¬𝔐ψ = (Logic.[⊥]-elim ∘ ¬𝔐ψ ∘ soundness Γφψ) (Logic.[∨]-elim 𝔐Γ \{[≡]-intro → 𝔐φ})
    ... | Logic.[∨]-introᵣ ¬𝔐φ | Logic.[∨]-introₗ 𝔐ψ  = (Logic.[⊥]-elim ∘ ¬𝔐φ ∘ soundness Γψφ) (Logic.[∨]-elim 𝔐Γ \{[≡]-intro → 𝔐ψ})
    ... | Logic.[∨]-introᵣ ¬𝔐φ | Logic.[∨]-introᵣ ¬𝔐ψ = Logic.[∨]-introᵣ (Logic.[∧]-intro ¬𝔐φ ¬𝔐ψ)
    soundness {Γ = Γ} ([⟷]-elimₗ {φ = φ} {ψ = ψ} Γψ Γφψ) 𝔐Γ with soundness Γφψ 𝔐Γ
    ... | Logic.[∨]-introₗ(Logic.[∧]-intro 𝔐φ  𝔐ψ ) = 𝔐φ
    ... | Logic.[∨]-introᵣ(Logic.[∧]-intro ¬𝔐φ ¬𝔐ψ) = Logic.[⊥]-elim(¬𝔐ψ(soundness Γψ 𝔐Γ))
    soundness {Γ = Γ} ([⟷]-elimᵣ {φ = φ} {ψ = ψ} Γφ Γφψ) 𝔐Γ with soundness Γφψ 𝔐Γ
    ... | Logic.[∨]-introₗ(Logic.[∧]-intro 𝔐φ  𝔐ψ ) = 𝔐ψ
    ... | Logic.[∨]-introᵣ(Logic.[∧]-intro ¬𝔐φ ¬𝔐ψ) = Logic.[⊥]-elim(¬𝔐φ(soundness Γφ 𝔐Γ))

    satisfiable-consistent : Satisfiable(Γ) → Consistent(Γ)
    satisfiable-consistent sat = Logic.contrapositiveᵣ soundness (\p → Logic.[↔]-to-[→] [⊨]-unsatisfiability p sat)

    consistency-of-∅ : Consistent{P = P}{ℓ = ℓ}(∅)
    consistency-of-∅ = satisfiable-consistent [∅]-satisfiable

  module _ where
    open import Data.Boolean.Stmt.Proofs
    open import Lang.Inspect

    modelSet : Model(P) → Formulas(P)
    modelSet(𝔐) = 𝔐 ⊧_

    module _ {𝔐 : Model(P)} where
      modelSet-satisfiable : Satisfiable(modelSet(𝔐))
      modelSet-satisfiable = Logic.[∃]-intro 𝔐 ⦃ id ⦄

      modelSet-maximally-consistent : MaximallyConsistent(modelSet(𝔐))
      MaximallyConsistent.consistent modelSet-maximally-consistent = satisfiable-consistent modelSet-satisfiable
      MaximallyConsistent.maximal    modelSet-maximally-consistent = element-intro p where
        p : ConsistentElementMaximality(modelSet(𝔐))
        p {φ} cons with TruthTable.eval 𝔐 φ | inspect (TruthTable.eval 𝔐) φ
        ... | 𝑇 | intro eval-𝑇 = TruthTable.eval-to-models {φ = φ} (Logic.[↔]-to-[←] IsTrue.is-𝑇 eval-𝑇)
        ... | 𝐹 | intro eval-𝐹 = Logic.[⊥]-elim (cons ([⊥]-intro (direct (Right [≡]-intro)) (weaken Left (direct (TruthTable.eval-to-models {φ = ¬ φ} (Logic.[↔]-to-[←] IsTrue.is-𝑇 ([≡]-with(BoolOp.¬) eval-𝐹)))))))

      {-maximally-consistent-is-modelSet : MaximallyConsistent(Γ) → (Γ ≡ₛ modelSet(𝔐))
      maximally-consistent-is-modelSet maxCon {• x} = Logic.[↔]-intro {!Logic.[↔]-to-[←] Logic.decide-is-true!} {!Logic.[↔]-to-[→] Logic.decide-is-true!}
      maximally-consistent-is-modelSet maxCon {⊤} = [⊤]-maximal-membership ⦃ maxCon ⦄
      maximally-consistent-is-modelSet maxCon {⊥} = [⊥]-maximal-membership ⦃ maxCon ⦄
      maximally-consistent-is-modelSet maxCon {¬ φ} = Logic.[↔]-transitivity ([¬]-maximal-membership ⦃ maxCon ⦄) (Logic.[¬]-unaryOperator (maximally-consistent-is-modelSet maxCon))
      maximally-consistent-is-modelSet maxCon {φ ∧ ψ} = Logic.[↔]-transitivity ([∧]-maximal-membership ⦃ maxCon ⦄) (Logic.[∧]-binaryOperator (maximally-consistent-is-modelSet maxCon) (maximally-consistent-is-modelSet maxCon))
      maximally-consistent-is-modelSet maxCon {φ ∨ ψ} = Logic.[↔]-transitivity ([∨]-maximal-membership ⦃ maxCon ⦄) (Logic.[∨]-binaryOperator (maximally-consistent-is-modelSet maxCon) (maximally-consistent-is-modelSet maxCon))
      maximally-consistent-is-modelSet maxCon {φ ⟶ ψ} = {!!}
      maximally-consistent-is-modelSet maxCon {φ ⟷ ψ} = {!!}-}

    term-model : Formulas(P){ℓ} → Model(P)
    term-model(Γ) p = decide(0)((• p) ∈ Γ)

  module _ ⦃ countable-P : CountablyInfinite(P) ⦄ where
    private variable Γ Γ₁ Γ₂ : Formulas(P){ℓₚ}

    term-model-of-max-proof : (con : Consistent(Γ)) → (max Γ ≡ₛ (term-model(max Γ) ⊧_))
    term-model-of-max-proof {Γ = Γ} con = Logic.[∃]-proof(MaximallyConsistent.equal-model-existence (max-maximally-consistent con))

    consistent-satisfiable : Consistent(Γ) → Satisfiable(Γ)
    Logic.∃.witness (consistent-satisfiable {Γ = Γ} con)     = term-model(max Γ)
    Logic.∃.proof   (consistent-satisfiable {Γ = Γ} con) {γ} = (Logic.[↔]-to-[→] (term-model-of-max-proof {Γ = Γ} con {γ})) ∘ max-superset

    completeness : (Γ ⊨ φ) → (Γ ⊢ φ)
    completeness {Γ = Γ}{φ = φ} =
      (Logic.[↔]-to-[←] [⊢]-derivability-inconsistency)
      ∘ (Logic.[↔]-to-[←] Logic.contrapositive-variant2 consistent-satisfiable)
      ∘ (Logic.[↔]-to-[→] [⊨]-entailment-unsatisfiability)

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:
open import Agda.Builtin.Nat

[_] :  (Nat → Set) → Set
[ T ] = ∀ {i} → T i

data D : Nat → Nat → Set where
  c : ∀ {i} → [ D i ]


text:
open import Haskell.Prelude

mutual

  data Map (k : Set) (a : Set) : Set where
    Bin : (sz : Nat) → (kx : k) → (x : a)
          → (l : Map k a) → (r : Map k a)
          → {{szVal : sz ≡ (size l) + (size r) + 1}}
          → Map k a
    Tip : Map k a
  {-# COMPILE AGDA2HS Map #-}

  size : {k a : Set} → Map k a → Nat
  size Tip = 0
  size (Bin sz _ _ _ _) = sz
  {-# COMPILE AGDA2HS size #-}


text:
{-# OPTIONS --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.Coalg.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function using ( _∘_ )
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Sigma

open import Cubical.Codata.M.AsLimit.Container
open import Cubical.Codata.M.AsLimit.helper

-------------------------------
-- Definition of a Coalgebra --
-------------------------------

Coalg₀ : ∀ {ℓ} {S : Container ℓ} -> Type (ℓ-suc ℓ)
Coalg₀ {ℓ} {S = S} = Σ[ C ∈ Type ℓ ] (C → P₀ S C)

--------------------------
-- Definition of a Cone --
--------------------------

Cone₀ : ∀ {ℓ} {S : Container ℓ} {C,γ : Coalg₀ {S = S}} -> Type ℓ
Cone₀ {S = S} {C , _} = (n : ℕ) → C → X (sequence S) n

Cone₁ : ∀ {ℓ} {S : Container ℓ} {C,γ : Coalg₀ {S = S}} -> (f : Cone₀ {C,γ = C,γ}) -> Type ℓ
Cone₁ {S = S} {C , _} f = (n : ℕ) → π (sequence S) ∘ (f (suc n)) ≡ f n

Cone : ∀ {ℓ} {S : Container ℓ} (C,γ : Coalg₀ {S = S}) -> Type ℓ
Cone {S = S} C,γ = Σ[ Cone ∈ (Cone₀ {C,γ = C,γ}) ] (Cone₁{C,γ = C,γ} Cone)

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:
module Contexts where

open import Prelude
open import T
open import SubstTheory

module Contexts where

  infix 60 _e$_ _$e_
  -- Has a hole of type (Γ ⊢ A), produces a term of type (Γ' ⊢ A')
  data TCtx (Γ : Ctx) (A : TTp) : (Γ' : Ctx) → (A' : TTp) → Set where
    ∘ : TCtx Γ A Γ A
    _e$_ : ∀{Γ' A' B} (e₁ : TExp Γ' (A' ⇒ B)) (C₂ : TCtx Γ A Γ' A') → TCtx Γ A Γ' B
    _$e_ : ∀{Γ' A' B} (C₁ : TCtx Γ A Γ' (A' ⇒ B)) (e₂ : TExp Γ' A') → TCtx Γ A Γ' B

    Λ : ∀{A₁ A₂ Γ'} (C : TCtx Γ A (A₁ :: Γ') A₂) → TCtx Γ A Γ' (A₁ ⇒ A₂)
    suc : ∀{Γ'} (C : TCtx Γ A Γ' nat) → TCtx Γ A Γ' nat

    rec1 : ∀{Γ' B} → (C : TCtx Γ A Γ' nat) → (e₀ : TExp Γ' B) → (es : TExp (B :: Γ') B) →
                     TCtx Γ A Γ' B
    rec2 : ∀{Γ' B} → (e : TExp Γ' nat) → (C₀ : TCtx Γ A Γ' B) → (es : TExp (B :: Γ') B) →
                     TCtx Γ A Γ' B
    rec3 : ∀{Γ' B} → (e : TExp Γ' nat) → (e₀ : TExp Γ' B) → (Cs : TCtx Γ A (B :: Γ') B) →
                     TCtx Γ A Γ' B

  _<_> : ∀{Γ A Γ' A'} → TCtx Γ A Γ' A' → TExp Γ A → TExp Γ' A'
  ∘ < e' > = e'
  (e₁ e$ C₂) < e' > = e₁ $ C₂ < e' >
  (C₁ $e e₂) < e' > = C₁ < e' > $ e₂
  Λ C < e' > = Λ (C < e' >)
  suc C < e' > = suc (C < e' >)
  rec1 C e₀ es < e' > = rec (C < e' >) e₀ es
  rec2 e C₀ es < e' > = rec e (C₀ < e' >) es
  rec3 e e₀ Cs < e' > = rec e e₀ (Cs < e' >)

  infix 70 _<<_>> _<_>
  _<<_>> : ∀{Γ A Γ' A' Γ'' A''} → TCtx Γ' A' Γ'' A'' → TCtx Γ A Γ' A' →
            TCtx Γ A Γ'' A''
  ∘ << C' >> = C'
  (e₁ e$ C₂) << C' >> = e₁ e$ C₂ << C' >>
  (C₁ $e e₂) << C' >> = C₁ << C' >> $e e₂
  Λ C << C' >> = Λ (C << C' >>)
  suc C << C' >> = suc (C << C' >>)
  rec1 C e₀ es << C' >> = rec1 (C << C' >>) e₀ es
  rec2 e C₀ es << C' >> = rec2 e (C₀ << C' >>) es
  rec3 e e₀ Cs << C' >> = rec3 e e₀ (Cs << C' >>)

  -- I hate having to prove this sort of theorem.
  composing-commutes : ∀{Γ A Γ' A' Γ'' A''} →
                       (C : TCtx Γ' A' Γ'' A'') →
                       (C' : TCtx Γ A Γ' A') →
                       (e : TExp Γ A) →
                       ((C << C' >>) < e >) ≡ C < C' < e > >
  composing-commutes ∘ C' e = Refl
  composing-commutes (e₁ e$ C) C' e = resp (_$_ e₁) (composing-commutes C C' e)
  composing-commutes (C $e e₂) C' e = resp (λ x → x $ e₂) (composing-commutes C C' e)
  composing-commutes (Λ C) C' e = resp Λ (composing-commutes C C' e)
  composing-commutes (suc C) C' e = resp suc (composing-commutes C C' e)
  composing-commutes (rec1 C e₀ es) C' e = resp (λ x → rec x e₀ es) (composing-commutes C C' e)
  composing-commutes (rec2 e' C es) C' e = resp (λ x → rec e' x es) (composing-commutes C C' e)
  composing-commutes (rec3 e' e₀ C) C' e = resp (λ x → rec e' e₀ x) (composing-commutes C C' e)

  -- If the hole is closed, then the rest needs to be too.
  tctx-empty-thing : ∀{F : Set} {Γ A A' B} → TCtx [] A (B :: Γ) A' → F
  tctx-empty-thing (e₁ e$ C) = tctx-empty-thing C
  tctx-empty-thing (C $e e₂) = tctx-empty-thing C
  tctx-empty-thing (Λ C) = tctx-empty-thing C
  tctx-empty-thing (suc C) = tctx-empty-thing C
  tctx-empty-thing (rec1 C e₀ es) = tctx-empty-thing C
  tctx-empty-thing (rec2 e C es) = tctx-empty-thing C
  tctx-empty-thing (rec3 e e₀ C) = tctx-empty-thing C

  -- Very restricted function for weakening a program context where
  -- the hole also occurs under no free variables.
  weaken-closed-tctx : ∀{Γ A A'} → TCtx [] A [] A' → TCtx Γ A Γ A'
  weaken-closed-tctx ∘ = ∘
  weaken-closed-tctx (e₁ e$ C) = weaken-closed e₁ e$ weaken-closed-tctx C
  weaken-closed-tctx (C $e e₂) = weaken-closed-tctx C $e weaken-closed e₂
  weaken-closed-tctx (Λ C) = tctx-empty-thing C
  weaken-closed-tctx (suc C) = suc (weaken-closed-tctx C)
  weaken-closed-tctx (rec1 C e₀ es) =
    rec1 (weaken-closed-tctx C) (weaken-closed e₀) (ren (wk closed-wkγ) es)
  weaken-closed-tctx (rec2 e C es) =
    rec2 (weaken-closed e) (weaken-closed-tctx C) (ren (wk closed-wkγ) es)
  weaken-closed-tctx (rec3 e e₀ C) = tctx-empty-thing C

  -- Substitution commutes with a closed context
  subst-commutes-w-closed-tctx : ∀{Γ A A'} → (γ : TSubst Γ []) → (C : TCtx [] A [] A') → (e : TExp Γ A) →
                                 C < ssubst γ e > ≡ ssubst γ ((weaken-closed-tctx C) < e >)
  subst-commutes-w-closed-tctx γ ∘ e = Refl
  subst-commutes-w-closed-tctx γ (e₁ e$ C) e =
    resp2 _$_
    (symm (closed-subst _ e₁) ≡≡ symm (subren γ closed-wkγ e₁))
    (subst-commutes-w-closed-tctx γ C e)
  subst-commutes-w-closed-tctx γ (C $e e₂) e =
    resp2 _$_
    (subst-commutes-w-closed-tctx γ C e)
    (symm (closed-subst _ e₂) ≡≡ symm (subren γ closed-wkγ e₂))
  subst-commutes-w-closed-tctx γ (Λ C) e = tctx-empty-thing C
  subst-commutes-w-closed-tctx γ (suc C) e =
    resp suc (subst-commutes-w-closed-tctx γ C e)
  subst-commutes-w-closed-tctx γ (rec1 C e₀ es) e with subren (liftγ γ) (wk closed-wkγ) es
  ... | lol1 with subeq (liftwk γ closed-wkγ) es
  ... | lol2 with lift-closed-subst (γ o closed-wkγ) es
  ... | lol3 with symm lol3 ≡≡ symm lol2 ≡≡ symm lol1
  ... | lol = resp3 rec
              (subst-commutes-w-closed-tctx γ C e)
              (symm (closed-subst _ e₀) ≡≡ symm (subren γ closed-wkγ e₀))
              lol
  subst-commutes-w-closed-tctx γ (rec2 en C es) e with subren (liftγ γ) (wk closed-wkγ) es
  ... | lol1 with subeq (liftwk γ closed-wkγ) es
  ... | lol2 with lift-closed-subst (γ o closed-wkγ) es
  ... | lol3 with symm lol3 ≡≡ symm lol2 ≡≡ symm lol1
  ... | lol = resp3 rec
              (symm (closed-subst _ en) ≡≡ symm (subren γ closed-wkγ en))
              (subst-commutes-w-closed-tctx γ C e)
              lol
  subst-commutes-w-closed-tctx γ (rec3 e e₀ C) e₁ = tctx-empty-thing C

open Contexts public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
------------------------------------------------------------------------
-- Specialised eliminators
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Partiality-monad.Inductive.Eliminators where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)

open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Nat equality-with-J as Nat

open import Partiality-monad.Inductive

------------------------------------------------------------------------
-- Non-dependent eliminators

Inc-nd : ∀ {a p q}
         (A : Type a) (P : Type p)
         (Q : P → P → Type q) → Type (p ⊔ q)
Inc-nd A P Q = ∃ λ (p : ℕ → P) → ∀ n → Q (p n) (p (suc n))

record Arguments-nd {a} p q (A : Type a) : Type (a ⊔ lsuc (p ⊔ q)) where
  field
    P  : Type p
    Q  : P → P → Type q
    pe : P
    po : (x : A) → P
    pl : (s : Increasing-sequence A) (pq : Inc-nd A P Q) → P
    pa : (p₁ p₂ : P) (q₁ : Q p₁ p₂) (q₂ : Q p₂ p₁) → p₁ ≡ p₂
    ps : Is-set P
    qr : (x : A ⊥) (p : P) → Q p p
    qt : {x y z : A ⊥} → x ⊑ y → y ⊑ z →
         (px py pz : P) → Q px py → Q py pz → Q px pz
    qe : (x : A ⊥) (p : P) → Q pe p
    qu : (s : Increasing-sequence A) (pq : Inc-nd A P Q) (n : ℕ) →
         Q (proj₁ pq n) (pl s pq)
    ql : ∀ s (ub : A ⊥) (is-ub : Is-upper-bound s ub) pq (pu : P)
         (qu : ∀ n → Q (proj₁ pq n) pu) →
         Q (pl s pq) pu
    qp : (p₁ p₂ : P) → Is-proposition (Q p₁ p₂)

module _ {a p q} {A : Type a} (args : Arguments-nd p q A) where

  open Arguments-nd args

  private

    args′ : Arguments p q A
    args′ = record
      { P  = λ _ → P
      ; Q  = λ p-x p-y _ → Q p-x p-y
      ; pe = pe
      ; po = po
      ; pl = pl
      ; pa = λ x⊑y x⊒y p₁ p₂ q₁ q₂ →
               subst (const P) (antisymmetry x⊑y x⊒y) p₁  ≡⟨ subst-const (antisymmetry x⊑y x⊒y) ⟩
               p₁                                         ≡⟨ pa p₁ p₂ q₁ q₂ ⟩∎
               p₂                                         ∎
      ; pp = ps
      ; qr = qr
      ; qt = qt
      ; qe = qe
      ; qu = qu
      ; ql = ql
      ; qp = λ p-x p-y _ → qp p-x p-y
      }

  ⊥-rec-nd : A ⊥ → P
  ⊥-rec-nd = ⊥-rec args′

  ⊑-rec-nd : ∀ {x y} → x ⊑ y → Q (⊥-rec-nd x) (⊥-rec-nd y)
  ⊑-rec-nd = ⊑-rec args′

  inc-rec-nd : Increasing-sequence A → Inc-nd A P Q
  inc-rec-nd = inc-rec args′

  ⊥-rec-nd-never : ⊥-rec-nd never ≡ pe
  ⊥-rec-nd-never = ⊥-rec-never _

  ⊥-rec-nd-now : ∀ x → ⊥-rec-nd (now x) ≡ po x
  ⊥-rec-nd-now = ⊥-rec-now _

  ⊥-rec-nd-⨆ : ∀ s → ⊥-rec-nd (⨆ s) ≡ pl s (inc-rec-nd s)
  ⊥-rec-nd-⨆ = ⊥-rec-⨆ _

------------------------------------------------------------------------
-- Eliminators which are trivial for _⊑_

record Arguments-⊥ {a} p (A : Type a) : Type (a ⊔ lsuc p) where
  field
    P  : A ⊥ → Type p
    pe : P never
    po : ∀ x → P (now x)
    pl : ∀ s (p : ∀ n → P (s [ n ])) → P (⨆ s)
    pp : ∀ x → Is-proposition (P x)

module _ {a p} {A : Type a} (args : Arguments-⊥ p A) where

  open Arguments-⊥ args

  ⊥-rec-⊥ : (x : A ⊥) → P x
  ⊥-rec-⊥ = ⊥-rec (record
    { Q  = λ _ _ _ → ⊤
    ; pe = pe
    ; po = po
    ; pl = λ s pq → pl s (proj₁ pq)
    ; pa = λ _ _ _ _ _ _ → pp _ _ _
    ; pp = mono₁ 1 (pp _)
    ; qp = λ _ _ _ _ _ → refl
    })

  inc-rec-⊥ : (s : ℕ → A ⊥) → ∀ n → P (s n)
  inc-rec-⊥ s = ⊥-rec-⊥ ∘ s

  ⊥-rec-⊥-never : ⊥-rec-⊥ never ≡ pe
  ⊥-rec-⊥-never = ⊥-rec-never _

  ⊥-rec-⊥-now : ∀ x → ⊥-rec-⊥ (now x) ≡ po x
  ⊥-rec-⊥-now = ⊥-rec-now _

  ⊥-rec-⊥-⨆ : ∀ s → ⊥-rec-⊥ (⨆ s) ≡ pl s (λ n → ⊥-rec-⊥ (s [ n ]))
  ⊥-rec-⊥-⨆ = ⊥-rec-⨆ _

------------------------------------------------------------------------
-- Eliminators which are trivial for _⊥

record Arguments-⊑ {a} q (A : Type a) : Type (a ⊔ lsuc q) where
  field
    Q  : {x y : A ⊥} → x ⊑ y → Type q
    qr : ∀ x → Q (⊑-refl x)
    qt : ∀ {x y z} (x⊑y : x ⊑ y) (y⊑z : y ⊑ z) →
         Q x⊑y → Q y⊑z → Q (⊑-trans x⊑y y⊑z)
    qe : ∀ x → Q (never⊑ x)
    qu : ∀ s (q : ∀ n → Q (increasing s n)) n →
         Q (upper-bound s n)
    ql : ∀ s ub is-ub (q : ∀ n → Q (increasing s n))
         (qu : ∀ n → Q (is-ub n)) →
         Q (least-upper-bound s ub is-ub)
    qp : ∀ {x y} (x⊑y : x ⊑ y) →
         Is-proposition (Q x⊑y)

module _ {a q} {A : Type a} (args : Arguments-⊑ q A) where

  open Arguments-⊑ args

  ⊑-rec-⊑ : ∀ {x y} (x⊑y : x ⊑ y) → Q x⊑y
  ⊑-rec-⊑ = ⊑-rec (record
    { P  = λ _ → ⊤
    ; Q  = λ _ _ → Q
    ; pa = λ _ _ _ _ _ _ → refl
    ; pp = mono (Nat.zero≤ 2) ⊤-contractible
    ; qr = λ x _ → qr x
    ; qt = λ x⊑y y⊑z _ _ _ → qt x⊑y y⊑z
    ; qe = λ x _ → qe x
    ; qu = λ s pq → qu s (proj₂ pq)
    ; ql = λ s ub is-ub pq _ → ql s ub is-ub (proj₂ pq)
    ; qp = λ _ _ → qp
    })

  inc-rec-⊑ : (s : Increasing-sequence A) → ∀ n → Q (increasing s n)
  inc-rec-⊑ (_ , inc) = ⊑-rec-⊑ ∘ inc

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module x01naturals where

{-
------------------------------------------------------------------------------
naturals : inductive datatype

definition as a pair of inference rules:
                 -- no assumptions
    ---------
    zero  : ℕ    -- base case

    m     : ℕ    -- assuming m is Natural
    ---------
    suc m : ℕ    -- inductive case : then suc m is also a Natural

in Agda:
-}

data ℕ : Set where
  zero :     ℕ -- base case
  suc  : ℕ → ℕ -- inductive case

-- #### Exercise Write out `7` in longhand.

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

{-
inference rules consists of
- zero or more _judgments_ written above a horizontal line, called the _hypotheses_
- single judgment written below, called the _conclusion_

`Set` : the way in Agda of saying that it is a type

Inductive case defines natural numbers in terms of natural numbers.
Base case jump starts the process of induction.

## Philosophy and history

inductive def of nats is relatively recent
- 1888
  Richard Dedekind's paper "_Was sind und was sollen die Zahlen?_"
  (What are and what should be the numbers?)
- 1889
  Giuseppe Peano's book "_Arithmetices principia, nova methodo exposita_"
  (The principles of arithmetic presented by a new method)

------------------------------------------------------------------------------
## PRAGMA

the line
-}
{-# BUILTIN NATURAL ℕ #-}
{-
tells Agda that `ℕ` corresponds to the natural numbers
- pragma must be given a previously declared type (in this case `ℕ`)
- enables 0, 1, 2, ... shorthand
- enables efficient internal Haskell representation

## IMPORTS

To write equations that hold between terms involving natural numbers
import the definition of equality and notations for reasoning about equality
from the Agda standard library:
-}

import Relation.Binary.PropositionalEquality as Eq
open Eq             using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

{-
1st line : brings equality module into scope and gives it the name `Eq`.
2nd line : opens that module and adds names in `using` clause into scope.
3rd line : opens module that specifies operators to support reasoning about equivalence
           and adds names in `using` clause into scope.

later will see their definitions in Chapter Equality

underbars indicate where terms appear
- `_≡_` and `_≡⟨⟩_`  : terms on each side
- `begin_` is prefix : terms after
- : `_∎`             : terms before

------------------------------------------------------------------------------
## operations on naturals are recursive functions
-}

-- ADDITION
_+_ : ℕ → ℕ → ℕ
zero    + n =          n  -- base case      :  0      + n  ≡  n
(suc m) + n = suc (m + n) -- inductive case : (1 + m) + n  ≡  1 + (m + n) : associativity

{-
Inductive definition works because addition of larger numbers is defined
in terms of addition of smaller numbers : WELL FOUNDED
-}

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3                                       ≡⟨⟩ -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))   ≡⟨⟩ -- inductive case
    suc ((suc zero)  + (suc (suc (suc zero))))  ≡⟨⟩ -- inductive case
    suc (suc (zero   + (suc (suc (suc zero))))) ≡⟨⟩ -- base case
    suc (suc           (suc (suc (suc zero))))  ≡⟨⟩ -- is longhand for
    5
  ∎ -- ∎ is QED

-- equivalent

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3             ≡⟨⟩
    suc      (1 + 3)  ≡⟨⟩
    suc (suc (0 + 3)) ≡⟨⟩
    suc (suc      3)  ≡⟨⟩
    5
  ∎

-- A binary relation is said to be REFLEXIVE if every value relates to itself.
-- Evidence that a value is equal to itself is written `refl`

_ : 2 + 3 ≡ 5
_ = refl

{-
above derivations consist of
- a signature (written with a colon, `:`), giving a type
- a binding (written with an equal sign, `=`), giving a term of the given type.

the dummy name `_` can be reused
consists of a series of terms separated by `≡⟨⟩`.

duality of interpretation
- type as a proposition
- term as evidence (aka proof)

#### Exercise `+-example` Compute `3 + 4`
-}

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4                   ≡⟨⟩
    suc           (2 + 4)   ≡⟨⟩
    suc (suc      (1 + 4))  ≡⟨⟩
    suc (suc (suc (0 + 4))) ≡⟨⟩
    suc (suc (suc      4))  ≡⟨⟩
    7
  ∎

_ : 3 + 4 ≡ 7
_ = refl

{-
------------------------------------------------------------------------------
## MULTIPLICATION
-}

_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero        --  0      * n  ≡  0
(suc m) * n  =  n + (m * n) -- (1 + m) * n  ≡  n + (m * n)

{-
computing `m * n` returns the sum of `m` copies of `n`.

2nd line because multiplication distributes over addition:

    (m + n) * p  ≡  (m * p) + (n * p)

We get the second equation from the third by
- taking `m` to be `1`
- `n` to be `m`
- `p` to be `n`
- then use fact that one is identity for multiplication, so
- `1 * n ≡ n`

WELL FOUNDED : _*_ of larger numbers is defined in terms of _*_ of smaller numbers
-}

_ : 2 * 3 ≡ 6
_ =
  begin
    2 * 3             ≡⟨⟩ -- inductive case
    3 + (1 * 3)       ≡⟨⟩ -- inductive case
    3 + (3 + (0 * 3)) ≡⟨⟩ -- base case
    3 + (3 + 0)       ≡⟨⟩ -- simplify
    6
  ∎

{-
#### Exercise `*-example` Compute `3 * 4`
-}

_ : 3 * 4 ≡ 12
_ =
  begin
    3 * 4                   ≡⟨⟩
    4 + (2 * 4)             ≡⟨⟩
    4 + (4 + (1 * 4))       ≡⟨⟩
    4 + (4 + (4 + (0 * 4))) ≡⟨⟩ -- base case
    4 + (4 + (4 +  0))      ≡⟨⟩ -- addition
    12
  ∎

-- HC

_*hc_ : ℕ → ℕ → ℕ
n *hc zero    =  zero
n *hc (suc m) =  (n *hc m) + n

_ : 2 *hc 3 ≡ 6
_ =
  begin
       2 *hc 3                  ≡⟨⟩
      (2 *hc 2)             + 2 ≡⟨⟩
     ((2 *hc 1)        + 2) + 2 ≡⟨⟩
    (((2 *hc 0)  + 2)  + 2) + 2 ≡⟨⟩
     ((      0   + 2)  + 2) + 2 ≡⟨⟩
     (             2   + 2) + 2 ≡⟨⟩
    6
  ∎

{-
------------------------------------------------------------------------------
#### Exercise (recommended) Define EXPONENTIATION
-}

_^_ : ℕ → ℕ → ℕ
m ^ 0       = 1            -- m ^ 0       = 1
m ^ (suc n) = m * (m ^ n)  -- m ^ (1 + n) = m * (m ^ n)

-- Check that `3 ^ 4` is `81`.
_ : 3 ^ 4 ≡ 81
_ = refl

_ : 2 ^ 3 ≡ 8
_ = refl

{-
------------------------------------------------------------------------------
## MONUS SUBTRACTION

uses pattern matching against both arguments:
-}

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

-- WELL FOUNDED : monus on bigger numbers is defined in terms of monus on smaller numbers.

_ =
  begin
    3 ∸ 2 ≡⟨⟩
    2 ∸ 1 ≡⟨⟩
    1 ∸ 0 ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3 ≡⟨⟩
    1 ∸ 2 ≡⟨⟩
    0 ∸ 1 ≡⟨⟩
    0
  ∎

{-
#### Exercise Compute `5 ∸ 3` and `3 ∸ 5`, reasoning as a chain of equations.
-}

_ =
  begin
    5 ∸ 3 ≡⟨⟩
    4 ∸ 2 ≡⟨⟩
    3 ∸ 1 ≡⟨⟩
    2 ∸ 0 ≡⟨⟩
    2
  ∎

_ =
  begin
    3 ∸ 5 ≡⟨⟩
    2 ∸ 4 ≡⟨⟩
    1 ∸ 3 ≡⟨⟩
    0 ∸ 2 ≡⟨⟩
    0
  ∎

{-
------------------------------------------------------------------------------
## PRECEDENCE

Application higher than operators   : `suc m + n` means `(suc m) + n`

multiplication higher than addition : `n + m * n` means `n + (m * n)`

addition _associates to the left_   : `m + n + p` means `(m + n) + p`

declare precedence and associativity of infix operators
-}

infixl 6  _+_  _∸_
infixl 7  _*_

{-
`infixl` : associate to the left
`infixr` : associate to the right
`infix`  : indicates that parentheses are required to disambiguate

------------------------------------------------------------------------------
## CURRYING

a function of two arguments in terms of
- a function of the first argument
- that returns a function of the second argument

Function arrows associate to the right : `ℕ → ℕ → ℕ` stands for `ℕ → (ℕ → ℕ)`
Application associates to the left     : `_+_ 2 3` stands for `(_+_ 2) 3`

Named for Haskell Curry.

The idea actually appears in the _Begriffsschrift_ of Gottlob Frege, published in 1879.

------------------------------------------------------------------------------
## The story of creation, revisited

inductive definition defines naturals in terms of naturals
recursive definition defines addition in terms of addition

           n : ℕ
    --------------
    zero + n  =  n

         m  + n  =      p
    ---------------------
    (suc m) + n  =  suc p

------------------------------------------------------------------------------
## The story of creation, finitely {name=finite-creation}
SKIPPED

------------------------------------------------------------------------------
## Writing definitions interactively

    _+_ : ℕ → ℕ → ℕ
    m + n = ?

? : ask Agda to fill in
`C-c C-l`
? replaced:

    _+_ : ℕ → ℕ → ℕ
    m + n = { }0

empty braces : a "numbered" *hole*
Emacs will also create a window displaying the text

    ?0 : ℕ

to indicate that hole 0 is to be filled in with a term of type `ℕ`.

`C-c C-f` (for **f**orward) will move you into the next hole.

To define addition by recursion on the first argument:
cursor in hole : `C-c C-c` (for **c**ase).
prompt:

    pattern variables to case (empty for split on result):

Type `m` : case split on `m`:

    _+_ : ℕ → ℕ → ℕ
    zero + n = { }0
    suc m + n = { }1

window at the bottom type of each:

    ?0 : ℕ
    ?1 : ℕ

in hole 0 : `C-c C-,`
displays info on required type of hole, and what free variables are available:

    Goal: ℕ
    ————————————————————————————————————————————————————————————
    n : ℕ

suggests filling the hole with `n`
after hole filled in : `C-c C-space` : removes hole:

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    suc m + n = { }1

in hole 1 : `C-c C-,`
displays info

    Goal: ℕ
    ————————————————————————————————————————————————————————————
    n : ℕ
    m : ℕ

in hole : `C-c C-r` (for **r**efine)
will fill in with a constructor (if there is a unique choice)
or tell you what constructors you might use, if there is a choice

    Don't know which constructor to introduce of zero or suc

fill in hole with `suc ?` : `C-c C-space`

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    suc m + n = suc { }1

in new hole : `C-c C-,`

    Goal: ℕ
    ————————————————————————————————————————————————————————————
    n : ℕ
    m : ℕ

fill hole with `m + n` : `C-c C-space`
complete the program:

    _+_ : ℕ → ℕ → ℕ
    zero + n = n
    suc m + n = suc (m + n)

------------------------------------------------------------------------------
## More pragmas
-}

{-# BUILTIN NATPLUS  _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

{-
tells Agda correspondance between operators correspond and the usual ones.
Enables using corresponding Haskell operators on arbitrary-precision integer type.

------------------------------------------------------------------------------
#### Exercise `Bin` (stretch) {name=Bin} represent nat as bitstring
-}

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

{-
bitstring 1011 (eleven) encoded as ⟨⟩ I O I I
or, with leading zeros,        ⟨⟩ O O I O I I

define

    inc : Bin → Bin

converts bitstring to bitstring for next higher number
-}

-- this definition has TWO forms of ZERO: '⟨⟩' and '⟨⟩ O'
-- will probably cause problems later on
inc : Bin → Bin
inc  ⟨⟩    = ⟨⟩      I
inc (⟨⟩ O) = ⟨⟩      I
inc (⟨⟩ I) = ⟨⟩   I  O
inc (b  O) =      b  I
inc (b  I) = (inc b) O

-- `IOII` eleven to `1100` twelve
_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl

-- Confirm correct answer for the bitstrings encoding zero through four.

_ : inc (⟨⟩     O) ≡ ⟨⟩     I
_ = refl
_ : inc (⟨⟩     I) ≡ ⟨⟩   I O
_ = refl
_ : inc (⟨⟩   I O) ≡ ⟨⟩   I I
_ = refl
_ : inc (⟨⟩   I I) ≡ ⟨⟩ I O O
_ = refl
_ : inc (⟨⟩ I O O) ≡ ⟨⟩ I O I
_ = refl

{-
using above, define

    to   : ℕ → Bin
    from : Bin → ℕ

`to` should not have leading zeros, except represent zero as `⟨⟩ O`

confirm for zero through four
-}

to : ℕ → Bin
to   zero  = ⟨⟩ O
to (suc m) = inc (to m)

from : Bin → ℕ
from     ⟨⟩ = 0
from (b  O) = 2 * from b
from (b  I) = 2 * from b + 1

_ : from (⟨⟩     O) ≡ 0
_ = refl
_ : from (⟨⟩     I) ≡ 1
_ = refl
_ : from (⟨⟩   I O) ≡ 2
_ = refl
_ : from (⟨⟩   I I) ≡ 3
_ = refl
_ : from (⟨⟩ I O O) ≡ 4
_ = refl
_ : from (⟨⟩ I I O) ≡ 6
_ = refl

_ : to 0 ≡ (⟨⟩     O)
_ = refl
_ : to 1 ≡ (⟨⟩     I)
_ = refl
_ : to 2 ≡ (⟨⟩   I O)
_ = refl
_ : to 3 ≡ (⟨⟩   I I)
_ = refl
_ : to 4 ≡ (⟨⟩ I O O)
_ = refl
_ : to 6 ≡ (⟨⟩ I I O)
_ = refl

_ : from (to 12) ≡ 12
_ = refl

_ : to (from (⟨⟩ I I O O)) ≡ ⟨⟩ I I O O
_ = refl

-- 842 exercise : bin-+

_bin-+_ : Bin → Bin → Bin
⟨⟩     bin-+ ⟨⟩     = ⟨⟩
⟨⟩     bin-+ b      = b
b      bin-+ ⟨⟩     = b
(bl O) bin-+ (br O) = let r = bl bin-+ br in      r  O
(bl O) bin-+ (br I) = let r = bl bin-+ br in      r  I
(bl I) bin-+ (br O) = let r = bl bin-+ br in      r  I
(bl I) bin-+ (br I) = let r = bl bin-+ br in (inc r) O

_ : (⟨⟩)       bin-+ (⟨⟩)     ≡ (⟨⟩)
_ = refl
_ : (⟨⟩)       bin-+ (⟨⟩   O) ≡ (⟨⟩       O)
_ = refl
_ : (⟨⟩     O) bin-+ (⟨⟩)     ≡ (⟨⟩       O)
_ = refl
_ : (⟨⟩     O) bin-+ (⟨⟩   O) ≡ (⟨⟩       O)
_ = refl
_ : (⟨⟩     O) bin-+ (⟨⟩   I) ≡ (⟨⟩       I)
_ = refl
_ : (⟨⟩     I) bin-+ (⟨⟩   I) ≡ (⟨⟩     I O)
_ = refl
_ : (⟨⟩   I O) bin-+ (⟨⟩ I O) ≡ (⟨⟩   I O O)
_ = refl
_ : (⟨⟩   I I) bin-+ (⟨⟩ I I) ≡ (⟨⟩   I I O)
_ = refl
_ : (⟨⟩ I O I) bin-+ (⟨⟩   I) ≡ (⟨⟩   I I O)
_ = refl
_ : (⟨⟩ I I I) bin-+ (⟨⟩   I) ≡ (⟨⟩ I O O O)
_ = refl

------------------------------------------------------------------------------
-- hc exercise : explore two representation of ZERO

z1-bin-+ : ∀ (b1 b2 : Bin)
        → b1          ≡ ⟨⟩
        → b1 bin-+ b2 ≡ b2
z1-bin-+ b1 ⟨⟩ p     -- (b1 bin-+  ⟨⟩)    ≡ ⟨⟩
  rewrite
    p                -- (⟨⟩ bin-+  ⟨⟩)    ≡ ⟨⟩
                     --            ⟨⟩     ≡ ⟨⟩
  = refl
z1-bin-+ b1 (⟨⟩ O) p -- (b1 bin-+ (⟨⟩ O)) ≡ (⟨⟩ O)
  rewrite
    p                -- (⟨⟩ bin-+ (⟨⟩ O)) ≡ (⟨⟩ O)
                     --           (⟨⟩ O)  ≡ (⟨⟩ O)
  = refl
z1-bin-+ b1 (b O) p  -- (b1 bin-+ (b  O)) ≡ (b  O)
  rewrite
    p                -- (⟨⟩ bin-+  (b O)) ≡ (b  O)
                     --            (b O)  ≡ (b  O)
  = refl
z1-bin-+ b1 (b I) p  -- (b1 bin-+  (b I)) ≡ (b  I)
  rewrite
    p                -- (⟨⟩ bin-+  (b I)) ≡ (b  I)
                     --            (b I)  ≡ (b  I)
  = refl

z-bin-+ : ∀ (b1 b2 : Bin)
        → b1          ≡ (⟨⟩ O)
        → b1 bin-+ b2 ≡ b2
z-bin-+ b1 ⟨⟩ p     -- (b1     bin-+ ⟨⟩)     ≡ ⟨⟩
  rewrite
    p               -- ((⟨⟩ O) bin-+ ⟨⟩)     ≡ ⟨⟩
                    --  (⟨⟩ O)               ≡ ⟨⟩
  = {!!}
z-bin-+ b1 (⟨⟩ O) p -- (b1     bin-+ (⟨⟩ O)) ≡ (⟨⟩ O)
  rewrite
    p               -- ((⟨⟩ O) bin-+ (⟨⟩ O)) ≡ (⟨⟩ O)
                    --               (⟨⟩ O)  ≡ (⟨⟩ O)
  = refl
z-bin-+ b1 (b O) p  -- (b1     bin-+ (b  O)) ≡ (b  O)
  rewrite
    p               -- ((⟨⟩ O) bin-+ (b  O)) ≡ (b  O)
                    -- ((⟨⟩    bin-+ b)  O)  ≡ (b  O)
  = {!!}
z-bin-+ b1 (b I) p  -- (b1     bin-+ (b  I)) ≡ (b  I)
  rewrite
    p               -- ((⟨⟩ O) bin-+ (b  I)) ≡ (b  I)
                    -- ((⟨⟩    bin-+ b)  I)  ≡ (b  I)
  = {!!}

hc : ∀ (m n : ℕ) →  from (to m bin-+ to n) ≡ m + n
hc  zero   n     -- from (to zero bin-+ to n) ≡ zero + n
  = {!!}         -- from ( (⟨⟩ O) bin-+ to n) ≡        n
hc (suc m) n = {!!}

{-
------------------------------------------------------------------------------
## Standard library

where to find relevant definitions in the standard library

Naturals, constructors, operators :

import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

https://agda.readthedocs.io/en/v2.6.1/language/pragmas.html

------------------------------------------------------------------------------
## Unicode

This chapter uses the following unicode:

 char  code    name                             emacs
------------------------------------------------------
    ℕ  U+2115  DOUBLE-STRUCK CAPITAL N          (\bN)
    →  U+2192  RIGHTWARDS ARROW                 (\to, \r, \->)
    ∸  U+2238  DOT MINUS                        (\.-)
    ≡  U+2261  IDENTICAL TO                     (\==)
    ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET  (\<)
    ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
    ∎  U+220E  END OF PROOF                     (\qed)

`\r` : variety of right arrows

`\l` : variety of left arrows

All the characters supported by `agda-mode`:

    M-x agda-input-show-translations

To see how to input an existing specific Unicode character in an agda file,
move cursor to character

    M-x quail-show-key
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Unit

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Nullification

open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (rec to trRec)
open import Cubical.Algebra.Group

open import Cubical.Homotopy.Connected
open import Cubical.Foundations.Equiv

private
  H⁰-connected-type : ∀ {ℓ} {A : Type ℓ} (a : A) → isConnected 2 A → Iso (coHom 0 A) Int
  Iso.fun (H⁰-connected-type a con) = sRec isSetInt λ f → f a
  Iso.inv (H⁰-connected-type a con) b = ∣ (λ x → b) ∣₂
  Iso.rightInv (H⁰-connected-type a con) b = refl
  Iso.leftInv (H⁰-connected-type a con) =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
           λ f → cong ∣_∣₂ (funExt λ x → trRec (isSetInt _ _) (cong f) (isConnectedPath 1 con a x .fst))

H⁰-connected : ∀ {ℓ} {A : Type ℓ} (a : A) → ((x : A) → ∥ a ≡ x ∥₁) → GroupIso (coHomGr 0 A) intGroup
GroupHom.fun (GroupIso.map (H⁰-connected a con)) = sRec isSetInt (λ f → f a)
GroupHom.isHom (GroupIso.map (H⁰-connected a con)) =
  sElim2 (λ _ _ → isProp→isSet (isSetInt _ _)) λ x y → addLemma (x a) (y a)
GroupIso.inv (H⁰-connected a con) b = ∣ (λ _ → b) ∣₂
GroupIso.rightInv (H⁰-connected a con) _ = refl
GroupIso.leftInv (H⁰-connected a con) =
  sElim (λ _ → isProp→isSet (setTruncIsSet _ _))
        (λ f → cong ∣_∣₂ (funExt λ x → pRec (isSetInt _ _) (cong f) (con x)))