text:
{-

This file contains:

Properties of FreeGroupoid:
- Induction principle for the FreeGroupoid on hProps
- ∥freeGroupoid∥₂ is a Group
- FreeGroup A ≡ ∥ FreeGroupoid A ∥₂

-}
{-# OPTIONS --safe #-}

module Cubical.HITs.FreeGroupoid.Properties where

open import Cubical.HITs.FreeGroupoid.Base
open import Cubical.HITs.FreeGroup renaming (elimProp to freeGroupElimProp)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.BiInvertible
open import Cubical.Foundations.Univalence using (ua)
open import Cubical.HITs.SetTruncation renaming (rec to recTrunc)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup.Base

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- The induction principle for the FreeGroupoid for hProps
elimProp : ∀ {B : FreeGroupoid A → Type ℓ'}
         → ((x : FreeGroupoid A) → isProp (B x))
         → ((a : A) → B (η a))
         → ((g1 g2 : FreeGroupoid A) → B g1 → B g2 → B (g1 · g2))
         → (B ε)
         → ((g : FreeGroupoid A) → B g → B (inv g))
         → (x : FreeGroupoid A)
         → B x
elimProp {B = B} Bprop η-ind ·-ind ε-ind inv-ind = induction where
  induction : ∀ g → B g
  induction (η a) = η-ind a
  induction (g1 · g2) = ·-ind g1 g2 (induction g1) (induction g2)
  induction ε = ε-ind
  induction (inv g) = inv-ind g (induction g)
  induction (assoc g1 g2 g3 i) = path i where
    p1 : B g1
    p1 = induction g1
    p2 : B g2
    p2 = induction g2
    p3 : B g3
    p3 = induction g3
    path : PathP (λ i → B (assoc g1 g2 g3 i)) (·-ind g1 (g2 · g3) p1 (·-ind g2 g3 p2 p3))
                                              (·-ind (g1 · g2) g3 (·-ind g1 g2 p1 p2) p3)
    path = isProp→PathP (λ i → Bprop (assoc g1 g2 g3 i)) (·-ind g1 (g2 · g3) p1 (·-ind g2 g3 p2 p3))
                                                         (·-ind (g1 · g2) g3 (·-ind g1 g2 p1 p2) p3)
  induction (idr g i) = path i where
    p : B g
    p = induction g
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (idr g i)) p (·-ind g ε p pε)
    path = isProp→PathP (λ i → Bprop (idr g i)) p (·-ind g ε p pε)
  induction (idl g i) = path i where
    p : B g
    p = induction g
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (idl g i)) p (·-ind ε g pε p)
    path = isProp→PathP (λ i → Bprop (idl g i)) p (·-ind ε g pε p)
  induction (invr g i) = path i where
    p : B g
    p = induction g
    pinv : B (inv g)
    pinv = inv-ind g p
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (invr g i)) (·-ind g (inv g) p pinv) pε
    path = isProp→PathP (λ i → Bprop (invr g i)) (·-ind g (inv g) p pinv) pε
  induction (invl g i) = path i where
    p : B g
    p = induction g
    pinv : B (inv g)
    pinv = inv-ind g p
    pε : B ε
    pε = induction ε
    path : PathP (λ i → B (invl g i)) (·-ind (inv g) g pinv p) pε
    path = isProp→PathP (λ i → Bprop (invl g i)) (·-ind (inv g) g pinv p) pε

-- The truncation of the FreeGroupoid is a group and is equal to FreeGroup

∥freeGroupoid∥₂IsSet : isSet ∥ FreeGroupoid A ∥₂
∥freeGroupoid∥₂IsSet = squash₂

_∣·∣₂_ : ∥ FreeGroupoid A ∥₂ → ∥ FreeGroupoid A ∥₂ → ∥ FreeGroupoid A ∥₂
_∣·∣₂_ = rec2 ∥freeGroupoid∥₂IsSet (λ g1 g2 → ∣ g1 · g2 ∣₂)

∥freeGroupoid∥₂IsSemiGroup : ∀ {ℓ}{A : Type ℓ} → IsSemigroup _∣·∣₂_
∥freeGroupoid∥₂IsSemiGroup {A = A} = issemigroup ∥freeGroupoid∥₂IsSet |assoc∣₂ where
  inuctionBase : ∀ g1 g2 g3 → ∣ g1 ∣₂ ∣·∣₂ (∣ g2 ∣₂ ∣·∣₂ ∣ g3 ∣₂) ≡ (∣ g1 ∣₂ ∣·∣₂ ∣ g2 ∣₂) ∣·∣₂ ∣ g3 ∣₂
  inuctionBase g1 g2 g3 = cong (λ x → ∣ x ∣₂) (assoc g1 g2 g3)
  Bset : ∀ x y z → isSet (x ∣·∣₂ (y ∣·∣₂ z) ≡ (x ∣·∣₂ y) ∣·∣₂ z)
  Bset x y z = isProp→isSet (squash₂ (x ∣·∣₂ (y ∣·∣₂ z)) ((x ∣·∣₂ y) ∣·∣₂ z))
  |assoc∣₂ : (x y z : ∥ FreeGroupoid A ∥₂) → x ∣·∣₂ (y ∣·∣₂ z) ≡ (x ∣·∣₂ y) ∣·∣₂ z
  |assoc∣₂ = elim3 Bset inuctionBase

∣ε∣₂ : ∥ FreeGroupoid A ∥₂
∣ε∣₂ = ∣ ε ∣₂

∥freeGroupoid∥₂IsMonoid : IsMonoid {A = ∥ FreeGroupoid A ∥₂} ∣ε∣₂ _∣·∣₂_
∥freeGroupoid∥₂IsMonoid = ismonoid ∥freeGroupoid∥₂IsSemiGroup
  (λ x → elim (λ g → isProp→isSet (squash₂ (g ∣·∣₂ ∣ε∣₂) g)) (λ g → cong (λ g' → ∣ g' ∣₂) (sym (idr g))) x)
  (λ x → elim (λ g → isProp→isSet (squash₂ (∣ε∣₂ ∣·∣₂ g) g)) (λ g → cong (λ g' → ∣ g' ∣₂) (sym (idl g))) x)

∣inv∣₂ : ∥ FreeGroupoid A ∥₂ → ∥ FreeGroupoid A ∥₂
∣inv∣₂ = map inv

∥freeGroupoid∥₂IsGroup : IsGroup {G = ∥ FreeGroupoid A ∥₂} ∣ε∣₂ _∣·∣₂_ ∣inv∣₂
∥freeGroupoid∥₂IsGroup = isgroup ∥freeGroupoid∥₂IsMonoid
  (λ x → elim (λ g → isProp→isSet (squash₂ (g ∣·∣₂ (∣inv∣₂ g)) ∣ε∣₂)) (λ g → cong (λ g' → ∣ g' ∣₂) (invr g)) x)
  (λ x → elim (λ g → isProp→isSet (squash₂ ((∣inv∣₂ g) ∣·∣₂ g) ∣ε∣₂)) (λ g → cong (λ g' → ∣ g' ∣₂) (invl g)) x)

∥freeGroupoid∥₂GroupStr : GroupStr ∥ FreeGroupoid A ∥₂
∥freeGroupoid∥₂GroupStr = groupstr ∣ε∣₂ _∣·∣₂_ ∣inv∣₂ ∥freeGroupoid∥₂IsGroup

∥freeGroupoid∥₂Group : Type ℓ → Group ℓ
∥freeGroupoid∥₂Group A = ∥ FreeGroupoid A ∥₂ , ∥freeGroupoid∥₂GroupStr

forgetfulHom : GroupHom (freeGroupGroup A) (∥freeGroupoid∥₂Group A)
forgetfulHom = rec (λ a → ∣ η a ∣₂)

forgetfulHom⁻¹ : GroupHom (∥freeGroupoid∥₂Group A) (freeGroupGroup A)
forgetfulHom⁻¹ = invf , isHom where
  invf : ∥ FreeGroupoid A ∥₂ → FreeGroup A
  invf = recTrunc freeGroupIsSet aux where
    aux : FreeGroupoid A → FreeGroup A
    aux (η a)              = η a
    aux (g1 · g2)          = (aux g1) · (aux g2)
    aux ε                  = ε
    aux (inv g)            = inv (aux g)
    aux (assoc g1 g2 g3 i) = assoc (aux g1) (aux g2) (aux g3) i
    aux (idr g i)          = idr (aux g) i
    aux (idl g i)          = idl (aux g) i
    aux (invr g i)         = invr (aux g) i
    aux (invl g i)         = invl (aux g) i
  isHom : IsGroupHom {A = ∥ FreeGroupoid A ∥₂} {B = FreeGroup A} ∥freeGroupoid∥₂GroupStr invf freeGroupGroupStr
  IsGroupHom.pres· isHom x y = elim2 (λ x y → isProp→isSet (freeGroupIsSet (invf (x ∣·∣₂ y)) ((invf x) · (invf y)))) ind x y where
    ind : ∀ g1 g2 → invf (∣ g1 ∣₂ ∣·∣₂ ∣ g2 ∣₂) ≡ (invf ∣ g1 ∣₂) · (invf ∣ g2 ∣₂)
    ind g1 g2 = refl
  IsGroupHom.pres1 isHom = refl
  IsGroupHom.presinv isHom x = elim (λ x → isProp→isSet (freeGroupIsSet (invf (∣inv∣₂ x)) (inv (invf x)))) ind x where
    ind : ∀ g → invf (∣inv∣₂ ∣ g ∣₂) ≡ inv (invf ∣ g ∣₂)
    ind g = refl

freeGroupTruncIdempotentBiInvEquiv : BiInvEquiv (FreeGroup A) ∥ FreeGroupoid A ∥₂
freeGroupTruncIdempotentBiInvEquiv = biInvEquiv f invf rightInv invf leftInv where
  f : FreeGroup A → ∥ FreeGroupoid A ∥₂
  f = fst forgetfulHom
  invf : ∥ FreeGroupoid A ∥₂ → FreeGroup A
  invf = fst forgetfulHom⁻¹
  rightInv : ∀ (x : ∥ FreeGroupoid A ∥₂) → f (invf x) ≡ x
  rightInv x = elim (λ x → isProp→isSet (squash₂ (f (invf x)) x)) ind x where
    ind : ∀ (g : FreeGroupoid A) → f (invf ∣ g ∣₂) ≡ ∣ g ∣₂
    ind g = elimProp Bprop η-ind ·-ind ε-ind inv-ind g where
      Bprop : ∀ g → isProp (f (invf ∣ g ∣₂) ≡ ∣ g ∣₂)
      Bprop g = squash₂ (f (invf ∣ g ∣₂)) ∣ g ∣₂
      η-ind : ∀ a → f (invf ∣ η a ∣₂) ≡ ∣ η a ∣₂
      η-ind a = refl
      ·-ind : ∀ g1 g2 → f (invf ∣ g1 ∣₂) ≡ ∣ g1 ∣₂ → f (invf ∣ g2 ∣₂) ≡ ∣ g2 ∣₂ → f (invf ∣ g1 · g2 ∣₂) ≡ ∣ g1 · g2 ∣₂
      ·-ind g1 g2 ind1 ind2 =
        f (invf ∣ g1 · g2 ∣₂)
        ≡⟨ cong f (IsGroupHom.pres· (snd forgetfulHom⁻¹) ∣ g1 ∣₂ ∣ g2 ∣₂) ⟩
        f ((invf ∣ g1 ∣₂) · (invf ∣ g2 ∣₂))
        ≡⟨ IsGroupHom.pres· (snd forgetfulHom) (invf ∣ g1 ∣₂) (invf ∣ g2 ∣₂) ⟩
        (f (invf ∣ g1 ∣₂)) ∣·∣₂ (f (invf ∣ g2 ∣₂))
        ≡⟨ cong (λ x → x ∣·∣₂ (f (invf ∣ g2 ∣₂))) ind1 ⟩
        ∣ g1 ∣₂ ∣·∣₂ (f (invf ∣ g2 ∣₂))
        ≡⟨ cong (λ x → ∣ g1 ∣₂ ∣·∣₂ x) ind2 ⟩
        ∣ g1 · g2 ∣₂ ∎
      ε-ind : f (invf ∣ ε ∣₂) ≡ ∣ ε ∣₂
      ε-ind  = refl
      inv-ind : ∀ g → f (invf ∣ g ∣₂) ≡ ∣ g ∣₂ → f (invf ∣ inv g ∣₂) ≡ ∣ inv g ∣₂
      inv-ind g ind =
        f (invf ∣ inv g ∣₂)
        ≡⟨ refl ⟩
        f (invf (∣inv∣₂ ∣ g ∣₂))
        ≡⟨ cong f (IsGroupHom.presinv (snd forgetfulHom⁻¹) ∣ g ∣₂) ⟩
        f (inv (invf ∣ g ∣₂))
        ≡⟨ IsGroupHom.presinv (snd forgetfulHom) (invf ∣ g ∣₂) ⟩
        ∣inv∣₂ (f (invf ∣ g ∣₂))
        ≡⟨ cong ∣inv∣₂ ind ⟩
        ∣inv∣₂ ∣ g ∣₂
        ≡⟨ refl ⟩
        ∣ inv g ∣₂ ∎
  leftInv : ∀ (g : FreeGroup A) → invf (f g) ≡ g
  leftInv g = freeGroupElimProp Bprop η-ind ·-ind ε-ind inv-ind g where
      Bprop : ∀ g → isProp (invf (f g) ≡ g)
      Bprop g = freeGroupIsSet (invf (f g)) g
      η-ind : ∀ a → invf (f (η a)) ≡ (η a)
      η-ind a = refl
      ·-ind : ∀ g1 g2 → invf (f g1) ≡ g1 → invf (f g2) ≡ g2 → invf (f (g1 · g2)) ≡ g1 · g2
      ·-ind g1 g2 ind1 ind2 =
        invf (f (g1 · g2))
        ≡⟨ cong invf (IsGroupHom.pres· (snd forgetfulHom) g1 g2) ⟩
        invf ((f g1) ∣·∣₂ (f g2))
        ≡⟨ IsGroupHom.pres· (snd forgetfulHom⁻¹) (f g1) (f g2) ⟩
        (invf (f g1)) · (invf (f g2))
        ≡⟨ cong (λ x → x · (invf (f g2))) ind1 ⟩
        g1 · (invf (f g2))
        ≡⟨ cong (λ x → g1 · x) ind2 ⟩
        g1 · g2 ∎
      ε-ind : invf (f ε) ≡ ε
      ε-ind  = refl
      inv-ind : ∀ g → invf (f g) ≡ g → invf (f (inv g)) ≡ inv g
      inv-ind g ind =
        invf (f (inv g))
        ≡⟨ cong invf (IsGroupHom.presinv (snd forgetfulHom) g) ⟩
        invf (∣inv∣₂ (f g))
        ≡⟨ IsGroupHom.presinv (snd forgetfulHom⁻¹) (f g) ⟩
        inv (invf (f g))
        ≡⟨ cong inv ind ⟩
        inv g ∎

freeGroupTruncIdempotent≃ : FreeGroup A ≃ ∥ FreeGroupoid A ∥₂
freeGroupTruncIdempotent≃ = biInvEquiv→Equiv-right freeGroupTruncIdempotentBiInvEquiv

freeGroupTruncIdempotent : FreeGroup A ≡ ∥ FreeGroupoid A ∥₂
freeGroupTruncIdempotent = ua freeGroupTruncIdempotent≃

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

-- This is a selection of useful functions and definitions
-- from the standard library that we tend to use a lot.

module Util.Prelude where

  open import Haskell.Prelude public
  open import Dijkstra.All public

  open import Level
    renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
    public

  1ℓ : Level
  1ℓ = ℓ+1 0ℓ

  open import Agda.Builtin.Unit
    public

  open import Function
    using (_∘_; _∘′_; case_of_; _on_; _∋_)
    public
  identity = Function.id

  open import Data.Unit.NonEta
    public

  open import Data.Empty
    public

  -- NOTE: This function is defined to give extra documentation when discharging
  -- absurd cases where Agda can tell by pattern matching that `A` is not
  -- inhabited. For example:
  -- > absurd (just v ≡ nothing) case impossibleProof of λ ()
  infix 0 absurd_case_of_
  absurd_case_of_ : ∀ {ℓ₁ ℓ₂} (A : Set ℓ₁) {B : Set ℓ₂} → A → (A → ⊥) → B
  absurd A case x of f = ⊥-elim (f x)

  open import Data.Nat
    renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_; _≥?_ to _≥?ℕ_; compare to compareℕ; Ordering to Orderingℕ)
    public

  max = _⊔_
  min = _⊓_

  open import Data.Nat.Properties
    hiding (≡-irrelevant ; _≟_)
    public

  open import Data.List
    renaming (map to List-map ; filter to List-filter ; lookup to List-lookup;
              tabulate to List-tabulate; foldl to List-foldl)
    hiding (fromMaybe; [_])
    public

  open import Data.List.Properties
    renaming (≡-dec to List-≡-dec; length-map to List-length-map; map-compose to List-map-compose; filter-++ to List-filter-++; length-filter to List-length-filter)
    using (∷-injective; length-++; map-++-commute; sum-++-commute; map-tabulate; tabulate-lookup; ++-identityʳ; ++-identityˡ)
    public

  open import Data.List.Relation.Binary.Subset.Propositional
    renaming (_⊆_ to _⊆List_)
    public

  open import Data.List.Relation.Unary.Any
    using (Any; here; there)
    renaming (lookup to Any-lookup; map to Any-map; satisfied to Any-satisfied
             ;index to Any-index; any to Any-any)
    public

  open import Data.List.Relation.Unary.Any.Properties
    using    (¬Any[])
    renaming ( map⁺       to Any-map⁺
             ; map⁻       to Any-map⁻
             ; concat⁺    to Any-concat⁺
             ; concat⁻    to Any-concat⁻
             ; ++⁻        to Any-++⁻
             ; ++⁺ʳ       to Any-++ʳ
             ; ++⁺ˡ       to Any-++ˡ
             ; singleton⁻ to Any-singleton⁻
             ; tabulate⁺  to Any-tabulate⁺
             ; filter⁻    to Any-filter⁻
             )
    public

  open import Data.List.Relation.Unary.All
    using (All; []; _∷_)
    renaming (head     to All-head;   tail     to All-tail;
              lookup   to All-lookup; tabulate to All-tabulate;
              reduce   to All-reduce; map      to All-map)
    public

  open import Data.List.Relation.Unary.All.Properties
    hiding   (All-map)
    renaming ( tabulate⁻ to All-tabulate⁻
             ; tabulate⁺ to All-tabulate⁺
             ; map⁺      to All-map⁺
             ; map⁻      to All-map⁻
             ; ++⁺       to All-++
             )
    public

  open import Data.List.Membership.Propositional
    using (_∈_; _∉_)
    public

  open import Data.List.Membership.Propositional.Properties
    renaming (∈-filter⁺ to List-∈-filter⁺; ∈-filter⁻ to List-∈-filter⁻)
    public

  open import Data.Vec
    using (Vec; []; _∷_)
    renaming (replicate to Vec-replicate; lookup to Vec-lookup
             ;map to Vec-map; head to Vec-head; tail to Vec-tail
             ;updateAt to Vec-updateAt; tabulate to Vec-tabulate
             ;allFin to Vec-allFin; toList to Vec-toList; fromList to Vec-fromList
             ;_++_ to _Vec-++_)
    public

  open import Data.Vec.Relation.Unary.All
    using ([]; _∷_)
    renaming (All to Vec-All; lookup to Vec-All-lookup)
    public

  open import Data.Vec.Properties
    using ()
    renaming (updateAt-minimal to Vec-updateAt-minimal
             ;[]=⇒lookup to Vec-[]=⇒lookup
             ;lookup⇒[]= to Vec-lookup⇒[]=
             ;lookup∘tabulate to Vec-lookup∘tabulate
             ;≡-dec to Vec-≡-dec)
    public

  open import Data.List.Relation.Binary.Pointwise
    using (decidable-≡)
    public

  open import Data.Bool
    renaming (_≟_ to _≟Bool_)
    hiding (_≤?_; _<_; _<?_; _≤_; not)
    public

  open import Data.Maybe
    renaming (map to Maybe-map; maybe to Maybe-maybe; zip to Maybe-zip ; _>>=_ to _Maybe->>=_)
    hiding (align; alignWith; zipWith)
    public

  -- a non-dependent eliminator
  -- note the traditional argument order is "switched", hence the 'S'
  maybeS : ∀ {a b} {A : Set a} {B : Set b} →
           (x : Maybe A) → B → ((x : A) → B) → B
  maybeS {B = B} x f t = Maybe-maybe {B = const B} t f x

  -- A Dijkstra version of maybeS, implemented using the version in
  -- Dijkstra.Syntax which has traditional argument order
  maybeSD : ∀ {ℓ₁ ℓ₂} {M : Set ℓ₁ → Set ℓ₂} ⦃ mmd : MonadMaybeD M ⦄
           → ∀ {A B : Set ℓ₁} → Maybe A → M B → (A → M B) → M B
  maybeSD ⦃ mmd ⦄ x y z = maybeD y z x

  module _ {Ev Wr St A B : Set} where
    maybeSMP-RWS : RWS Ev Wr St (Maybe A)
                 → B
                 → (A → RWS Ev Wr St B)
                 → RWS Ev Wr St B
    maybeSMP-RWS x y z = maybeMP-RWS y z x

  open import Data.Maybe.Relation.Unary.Any
    renaming (Any to Maybe-Any; dec to Maybe-Any-dec)
    hiding (map; zip; zipWith; unzip ; unzipWith)
    public

  maybe-any-⊥ : ∀{a}{A : Set a} → Maybe-Any {A = A} (λ _ → ⊤) nothing → ⊥
  maybe-any-⊥ ()

  headMay : ∀ {A : Set} → List A → Maybe A
  headMay     []  = nothing
  headMay (x ∷ _) = just x

  lastMay : ∀ {A : Set} → List A → Maybe A
  lastMay          []  = nothing
  lastMay     (x ∷ []) = just x
  lastMay (_ ∷ x ∷ xs) = lastMay (x ∷ xs)

  open import Data.Maybe.Properties
    using (just-injective)
    renaming (≡-dec to Maybe-≡-dec)
    public

  open import Data.Fin
    using (Fin; suc; zero; fromℕ; fromℕ< ; toℕ ; cast)
    renaming (_≟_ to _≟Fin_; _≤?_ to _≤?Fin_; _≤_ to _≤Fin_ ; _<_ to _<Fin_;
              inject₁ to Fin-inject₁; inject+ to Fin-inject+; inject≤ to Fin-inject≤)
    public

  fins : (n : ℕ) → List (Fin n)
  fins n = Vec-toList (Vec-allFin n)

  open import Data.Fin.Properties
    using (toℕ-injective; toℕ<n)
    renaming (<-cmp to Fin-<-cmp; <⇒≢ to <⇒≢Fin; suc-injective to Fin-suc-injective)
    public

  open import Relation.Binary.PropositionalEquality
    hiding (decSetoid)
    public

  open import Relation.Binary.HeterogeneousEquality
    using (_≅_)
    renaming (cong to ≅-cong; cong₂ to ≅-cong₂)
    public

  open import Relation.Binary
    public

  ≡-irrelevant : ∀{a}{A : Set a} → Irrelevant {a} {A} _≡_
  ≡-irrelevant refl refl = refl

  to-witness-lemma : ∀{ℓ}{A : Set ℓ}{a : A}{f : Maybe A}(x : Is-just f)
                   → to-witness x ≡ a → f ≡ just a
  to-witness-lemma (just x) refl = refl

  open import Relation.Nullary
    hiding (Irrelevant; proof)
    public

  open import Relation.Nullary.Decidable
    hiding (map)
    public

  open import Data.Sum
    renaming (map to ⊎-map; map₁ to ⊎-map₁; map₂ to ⊎-map₂)
    public

  open import Data.Sum.Properties
    using (inj₁-injective ; inj₂-injective)
    public

  ⊎-elimˡ : ∀ {ℓ₀ ℓ₁}{A₀ : Set ℓ₀}{A₁ : Set ℓ₁} → ¬ A₀ → A₀ ⊎ A₁ → A₁
  ⊎-elimˡ ¬a = either (⊥-elim ∘ ¬a) id

  ⊎-elimʳ : ∀ {ℓ₀ ℓ₁}{A₀ : Set ℓ₀}{A₁ : Set ℓ₁} → ¬ A₁ → A₀ ⊎ A₁ → A₀
  ⊎-elimʳ ¬a = either id (⊥-elim ∘ ¬a)

  open import Data.Product
    renaming (map to ×-map; map₂ to ×-map₂; map₁ to ×-map₁; <_,_> to split; swap to ×-swap)
    hiding (zip)
    public

  open import Data.Product.Properties
    public

  module _ {ℓA} {A : Set ℓA} where
    NoneOfKind : ∀ {ℓ} {P : A → Set ℓ} → List A → (p : (a : A) → Dec (P a)) → Set ℓA
    NoneOfKind xs p = List-filter p xs ≡ []

    postulate -- TODO-1: Replace with or prove using library properties?  Move to Lemmas?
      NoneOfKind⇒ : ∀ {ℓ} {P : A → Set ℓ} {Q : A → Set ℓ} {xs : List A}
                  → (p : (a : A) → Dec (P a))
                  → {q : (a : A) → Dec (Q a)}
                  → (∀ {a} → P a → Q a)  -- TODO-1: Use proper notation (Relation.Unary?)
                  → NoneOfKind xs q
                  → NoneOfKind xs p

  infix 4 _<?ℕ_
  _<?ℕ_ : Decidable _<_
  m <?ℕ n = suc m ≤?ℕ n

  infix 0 if-yes_then_else_
  infix 0 if-dec_then_else_
  if-yes_then_else_ : ∀ {ℓA ℓB} {A : Set ℓA} {B : Set ℓB} → Dec A → (A → B) → (¬ A → B) → B
  if-yes (yes prf) then f else _ = f prf
  if-yes (no  prf) then _ else g = g prf

  if-dec_then_else_ : ∀ {ℓA ℓB} {A : Set ℓA} {B : Set ℓB} → Dec A → B → B → B
  if-dec x then f else g = if-yes x then const f else const g

  open import Relation.Nullary.Negation
    using (contradiction; contraposition)
    public

  open import Relation.Binary
    using (Setoid; IsPreorder)
    public

  open import Relation.Unary
    using (_∪_)
    public

  open import Relation.Unary.Properties
    using (_∪?_)
    public

  -- Injectivity for a function of two potentially different types (A and B) via functions to a
  -- common type (C).

  Injective' : ∀ {b c d e}{B : Set b}{C : Set c}{D : Set d} → (hB : B → D) → (hC : C → D) → (_≈_ : B → C → Set e) → Set _
  Injective' {C = C} hB hC _≈_ = ∀ {b c} → hB b ≡ hC c → b ≈ c

  Injective  : ∀ {c d e}{C : Set c}{D : Set d} → (h : C → D) → (_≈_ : Rel C e) → Set _
  Injective h _≈_ = Injective' h h _≈_

  Injective-≡ : ∀ {c d}{C : Set c}{D : Set d} → (h : C → D) → Set _
  Injective-≡ h = Injective h _≡_

  Injective-int : ∀{a b c d e}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
                → (_≈_ : A → B → Set e)
                → (h  : C → D)
                → (f₁ : A → C)
                → (f₂ : B → C)
                → Set (a ℓ⊔ b ℓ⊔ d ℓ⊔ e)
  Injective-int _≈_ h f₁ f₂ = ∀ {a₁} {b₁} → h (f₁ a₁) ≡ h (f₂ b₁) → a₁ ≈ b₁

  NonInjective : ∀{a b c}{A : Set a}{B : Set b}
               → (_≈_ : Rel A c)
               → (A → B) → Set (a ℓ⊔ b ℓ⊔ c)
  NonInjective {A = A} _≈_ f
    = Σ (A × A) (λ { (x₁ , x₂) → ¬ (x₁ ≈ x₂) × f x₁ ≡ f x₂ })

  NonInjective-≡ : ∀{a b}{A : Set a}{B : Set b}
                 → (A → B) → Set (a ℓ⊔ b)
  NonInjective-≡ = NonInjective _≡_

  NonInjective-≡-preds : ∀{a b}{A : Set a}{B : Set b}{ℓ₁ ℓ₂ : Level}
                      → (A → Set ℓ₁)
                      → (A → Set ℓ₂)
                      → (A → B) → Set (a ℓ⊔ b ℓ⊔ ℓ₁ ℓ⊔ ℓ₂)
  NonInjective-≡-preds Pred1 Pred2 f = Σ (NonInjective _≡_ f) λ { ((a₀ , a₁) , _ , _) → Pred1 a₀ × Pred2 a₁ }

  NonInjective-≡-pred : ∀{a b}{A : Set a}{B : Set b}{ℓ : Level}
                      → (P : A → Set ℓ)
                      → (A → B) → Set (a ℓ⊔ b ℓ⊔ ℓ)
  NonInjective-≡-pred Pred = NonInjective-≡-preds Pred Pred

  NonInjective-∘ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
                 → {f : A → B}(g : B → C)
                 → NonInjective-≡  f
                 → NonInjective-≡ (g ∘ f)
  NonInjective-∘ g ((x0 , x1) , (x0≢x1 , fx0≡fx1))
    = ((x0 , x1) , x0≢x1 , (cong g fx0≡fx1))

  --------------------------------------------
  -- Handy fmap and bind for specific types --

  _<M$>_ : ∀{a b}{A : Set a}{B : Set b}
         → (f : A → B)
         → Maybe A → Maybe B
  _<M$>_ = Maybe-map

  <M$>-univ : ∀{a b}{A : Set a}{B : Set b}
            → (f : A → B)(x : Maybe A)
            → {y : B} → f <M$> x ≡ just y
            → ∃[ x' ] (x ≡ just x' × f x' ≡ y)
  <M$>-univ f (just x) refl = x , (refl , refl)

  maybe-lift : {A : Set}
             → {mx : Maybe A}{x : A}
             → (P : A → Set)
             → P x → mx ≡ just x
             → Maybe-maybe {B = const Set} P ⊥ mx
  maybe-lift {mx = just .x} {x} P px refl = px

  <M$>-nothing : ∀ {a b}{A : Set a}{B : Set b}(f : A → B)
               → f <M$> nothing ≡ nothing
  <M$>-nothing _ = refl

  _<⊎$>_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
         → (A → B) → C ⊎ A → C ⊎ B
  f <⊎$> (inj₁ hb) = inj₁ hb
  f <⊎$> (inj₂ x)  = inj₂ (f x)

  _⊎⟫=_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
        → C ⊎ A → (A → C ⊎ B) → C ⊎ B
  (inj₁ x) ⊎⟫= _ = inj₁ x
  (inj₂ a) ⊎⟫= f = f a

  -- a non-dependent eliminator
  -- note the traditional argument order is "switched", hence the 'S'
  eitherS : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
            (x : Either A B) → ((x : A) → C) → ((x : B) → C) → C
  eitherS eab fa fb = case eab of λ where
    (Left  a) → fa a
    (Right b) → fb b

  -- A Dijkstra version of eitherS, implemented using the version in
  -- Dijkstra.Syntax which has traditional argument order
  eitherSD : ∀ {ℓ₁ ℓ₂ ℓ₃} {M : Set ℓ₁ → Set ℓ₂} ⦃ med : MonadEitherD M ⦄
           → ∀ {EL : Set ℓ₁ → Set ℓ₁ → Set ℓ₃} ⦃ _ : EitherLike EL ⦄
           → ∀ {E A B : Set ℓ₁} → EL E A → (E → M B) → (A → M B) → M B
  eitherSD ⦃ med ⦄ ⦃ el ⦄ x y z = eitherD y z x

  open import Data.String as String
    hiding (_==_ ; _≟_ ; concat)

  check : Bool → List String → Either String Unit
  check b t = if b then inj₂ unit else inj₁ (String.intersperse "; " t)

  toWitnessT : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ true → P
  toWitnessT {d = yes proof} _ = proof

  toWitnessF : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ false → ¬ P
  toWitnessF{d = no proof} _ = proof

  Any-satisfied-∈ : ∀{a ℓ}{A : Set a}{P : A → Set ℓ}{xs : List A}
                  → Any P xs → Σ A (λ x → P x × x ∈ xs)
  Any-satisfied-∈ (here px) = _ , (px , here refl)
  Any-satisfied-∈ (there p) = let (a , px , prf) = Any-satisfied-∈ p
                               in (a , px , there prf)

  f-sum : ∀{a}{A : Set a} → (A → ℕ) → List A → ℕ
  f-sum f = sum ∘ List-map f

  maybeSMP : ∀ {ℓ} {A B : Set} {m : Set → Set ℓ} ⦃ _ : Monad m ⦄ → m (Maybe A) → B → (A → m B) → m B
  maybeSMP ma b f = do
    x ← ma
    case x of λ where
      nothing  → pure b
      (just j) → f j

  open import LibraBFT.Base.Util public

  -- Like a Haskell list-comprehension for ℕ : [ n | n <- [from .. to] ]
  fromToList : ℕ → ℕ → List ℕ
  fromToList from to with from ≤′? to
  ... | no ¬pr = []
  ... | yes pr = fromToList-le from to pr []
   where
    fromToList-le : ∀ (from to : ℕ) (klel : from ≤′ to) (acc : List ℕ) → List ℕ
    fromToList-le from ._        ≤′-refl       acc = from ∷ acc
    fromToList-le from (suc to) (≤′-step klel) acc = fromToList-le from to klel (suc to ∷ acc)

  _ : fromToList 1 1 ≡ 1 ∷ []
  _ = refl
  _ : fromToList 1 2 ≡ 1 ∷ 2 ∷ []
  _ = refl
  _ : fromToList 2 1 ≡ []
  _ = refl

ext: agda


text:
module Data.List.Primitive where

-- In Agda 2.2.10 and below, there's no FFI binding for the stdlib
-- List type, so we have to roll our own. This will change.

data #List (X : Set) : Set where
  [] : #List X
  _∷_ : X → #List X → #List X
{-# COMPILED_DATA #List [] [] (:) #-}

max_stars_repo_name: agda/agda-data-bindings

max_issues_repo_name: agda/agda-data-bindings

max_forks_repo_name: agda/agda-data-bindings


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}

-- This file could be proven using the file Sn
-- However the proofs are easier than in Sn
-- And so kept for pedagologic reasons

module Cubical.ZCohomology.CohomologyRings.S1 where

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

open import Cubical.Data.Unit
open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_ ; snotz to nsnotz)
open import Cubical.Data.Int
open import Cubical.Data.Vec
open import Cubical.Data.FinData

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int renaming (ℤGroup to ℤG)
open import Cubical.Algebra.DirectSum.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.Polynomials.Multivariate.Base renaming (base to baseP)
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-notationZ

open import Cubical.HITs.Truncation
open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Sn

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.Groups.Sn

open Iso

module Equiv-S1-Properties where

-----------------------------------------------------------------------------
-- Definitions

  open CommRingStr (snd ℤCR) using ()
    renaming
    ( 0r        to 0ℤ
    ; 1r        to 1ℤ
    ; _+_       to _+ℤ_
    ; -_        to -ℤ_
    ; _·_       to _·ℤ_
    ; +Assoc    to +ℤAssoc
    ; +Identity to +ℤIdentity
    ; +Lid      to +ℤLid
    ; +Rid      to +ℤRid
    ; +Inv      to +ℤInv
    ; +Linv     to +ℤLinv
    ; +Rinv     to +ℤRinv
    ; +Comm     to +ℤComm
    ; ·Assoc    to ·ℤAssoc
    ; ·Identity to ·ℤIdentity
    ; ·Lid      to ·ℤLid
    ; ·Rid      to ·ℤRid
    ; ·Rdist+   to ·ℤRdist+
    ; ·Ldist+   to ·ℤLdist+
    ; is-set    to isSetℤ     )

  open RingStr (snd (H*R (S₊ 1))) using ()
    renaming
    ( 0r        to 0H*
    ; 1r        to 1H*
    ; _+_       to _+H*_
    ; -_        to -H*_
    ; _·_       to _cup_
    ; +Assoc    to +H*Assoc
    ; +Identity to +H*Identity
    ; +Lid      to +H*Lid
    ; +Rid      to +H*Rid
    ; +Inv      to +H*Inv
    ; +Linv     to +H*Linv
    ; +Rinv     to +H*Rinv
    ; +Comm     to +H*Comm
    ; ·Assoc    to ·H*Assoc
    ; ·Identity to ·H*Identity
    ; ·Lid      to ·H*Lid
    ; ·Rid      to ·H*Rid
    ; ·Rdist+   to ·H*Rdist+
    ; ·Ldist+   to ·H*Ldist+
    ; is-set    to isSetH*     )

  open CommRingStr (snd ℤ[X]) using ()
    renaming
    ( 0r        to 0Pℤ
    ; 1r        to 1Pℤ
    ; _+_       to _+Pℤ_
    ; -_        to -Pℤ_
    ; _·_       to _·Pℤ_
    ; +Assoc    to +PℤAssoc
    ; +Identity to +PℤIdentity
    ; +Lid      to +PℤLid
    ; +Rid      to +PℤRid
    ; +Inv      to +PℤInv
    ; +Linv     to +PℤLinv
    ; +Rinv     to +PℤRinv
    ; +Comm     to +PℤComm
    ; ·Assoc    to ·PℤAssoc
    ; ·Identity to ·PℤIdentity
    ; ·Lid      to ·PℤLid
    ; ·Rid      to ·PℤRid
    ; ·Comm     to ·PℤComm
    ; ·Rdist+   to ·PℤRdist+
    ; ·Ldist+   to ·PℤLdist+
    ; is-set    to isSetPℤ     )

  open CommRingStr (snd ℤ[X]/X²) using ()
    renaming
    ( 0r        to 0PℤI
    ; 1r        to 1PℤI
    ; _+_       to _+PℤI_
    ; -_        to -PℤI_
    ; _·_       to _·PℤI_
    ; +Assoc    to +PℤIAssoc
    ; +Identity to +PℤIIdentity
    ; +Lid      to +PℤILid
    ; +Rid      to +PℤIRid
    ; +Inv      to +PℤIInv
    ; +Linv     to +PℤILinv
    ; +Rinv     to +PℤIRinv
    ; +Comm     to +PℤIComm
    ; ·Assoc    to ·PℤIAssoc
    ; ·Identity to ·PℤIIdentity
    ; ·Lid      to ·PℤILid
    ; ·Rid      to ·PℤIRid
    ; ·Rdist+   to ·PℤIRdist+
    ; ·Ldist+   to ·PℤILdist+
    ; is-set    to isSetPℤI     )

-----------------------------------------------------------------------------
-- Direct Sens on ℤ[x]

  ℤ[x]→H*-S¹ : ℤ[x] → H* (S₊ 1)
  ℤ[x]→H*-S¹ = Poly-Rec-Set.f _ _ _ isSetH*
                  0H*
                  base-trad
                  _+H*_
                  +H*Assoc
                  +H*Rid
                  +H*Comm
                  base-neutral-eq
                  base-add-eq
               where
               e : _
               e = Hᵐ-Sⁿ

               base-trad : _
               base-trad (zero ∷ [])        a = base 0 (inv (fst (Hᵐ-Sⁿ 0 1)) a)
               base-trad (one ∷ [])         a = base 1 (inv (fst (Hᵐ-Sⁿ 1 1)) a)
               base-trad (suc (suc n) ∷ []) a = 0H*

               base-neutral-eq :  _
               base-neutral-eq (zero ∷ [])        = cong (base 0) (IsGroupHom.pres1 (snd (invGroupIso (Hᵐ-Sⁿ 0 1)))) ∙ base-neutral _
               base-neutral-eq (one ∷ [])         = cong (base 1) (IsGroupHom.pres1 (snd (invGroupIso (Hᵐ-Sⁿ 1 1)))) ∙ base-neutral _
               base-neutral-eq (suc (suc n) ∷ []) = refl

               base-add-eq : _
               base-add-eq (zero ∷ []) a b        = (base-add _ _ _) ∙ (cong (base 0) (sym (IsGroupHom.pres· (snd (invGroupIso (Hᵐ-Sⁿ 0 1))) a b)))
               base-add-eq (one ∷ []) a b         = (base-add _ _ _) ∙ (cong (base 1) (sym (IsGroupHom.pres· (snd (invGroupIso (Hᵐ-Sⁿ 1 1))) a b)))
               base-add-eq (suc (suc n) ∷ []) a b = +H*Rid _

-----------------------------------------------------------------------------
-- Morphism on ℤ[x]

  ℤ[x]→H*-S¹-pres1Pℤ : ℤ[x]→H*-S¹ (1Pℤ) ≡ 1H*
  ℤ[x]→H*-S¹-pres1Pℤ = refl

  ℤ[x]→H*-S¹-pres+ : (x y : ℤ[x]) → ℤ[x]→H*-S¹ (x +Pℤ y) ≡ ℤ[x]→H*-S¹ x +H* ℤ[x]→H*-S¹ y
  ℤ[x]→H*-S¹-pres+ x y = refl

-- cup product on H⁰ → H⁰ → H⁰
  T0 : (z : ℤ) → coHom 0 (S₊ 1)
  T0 = λ z → inv (fst (Hᵐ-Sⁿ 0 1)) z

  T0g : IsGroupHom (ℤG .snd) (fst (invGroupIso (Hᵐ-Sⁿ 0 1)) .fun) (coHomGr 0 (S₊ (suc 0)) .snd)
  T0g = snd (invGroupIso (Hᵐ-Sⁿ 0 1))

  -- idea : control of the unfolding + simplification of T0 on the left
  pres·-base-case-00 : (a : ℤ) → (b : ℤ) →
                        T0 (a ·ℤ b) ≡ (T0 a) ⌣ (T0 b)
  pres·-base-case-00 (pos zero)       b = (IsGroupHom.pres1 T0g)
  pres·-base-case-00 (pos (suc n))    b = ((IsGroupHom.pres· T0g b (pos n ·ℤ b)))
                                          ∙ (cong (λ X → (T0 b) +ₕ X) (pres·-base-case-00 (pos n) b))
  pres·-base-case-00 (negsuc zero)    b = IsGroupHom.presinv T0g b
  pres·-base-case-00 (negsuc (suc n)) b = cong T0 (+ℤComm (-ℤ b) (negsuc n ·ℤ b)) -- ·ℤ and ·₀ are defined asymetrically !
                                          ∙ IsGroupHom.pres· T0g (negsuc n ·ℤ b) (-ℤ b)
                                          ∙ cong₂ _+ₕ_ (pres·-base-case-00 (negsuc n) b)
                                                         (IsGroupHom.presinv T0g b)
-- cup product on H⁰ → H¹ → H¹
  T1 : (z : ℤ) → coHom 1 (S₊ 1)
  T1 = λ z → inv (fst (Hᵐ-Sⁿ 1 1)) z

  -- idea : control of the unfolding + simplification of T0 on the left
  T1g : IsGroupHom (ℤG .snd) (fst (invGroupIso (Hᵐ-Sⁿ 1 1)) .fun) (coHomGr 1 (S₊ 1) .snd)
  T1g = snd (invGroupIso (Hᵐ-Sⁿ 1 1))

  pres·-base-case-01 : (a : ℤ) → (b : ℤ) →
                        T1 (a ·ℤ b) ≡ (T0 a) ⌣ (T1 b)
  pres·-base-case-01 (pos zero)       b = (IsGroupHom.pres1 T1g)
  pres·-base-case-01 (pos (suc n))    b = ((IsGroupHom.pres· T1g b (pos n ·ℤ b)))
                                          ∙ (cong (λ X → (T1 b) +ₕ X) (pres·-base-case-01 (pos n) b))
  pres·-base-case-01 (negsuc zero)    b = IsGroupHom.presinv T1g b
  pres·-base-case-01 (negsuc (suc n)) b = cong T1 (+ℤComm (-ℤ b) (negsuc n ·ℤ b)) -- ·ℤ and ·₀ are defined asymetrically !
                                          ∙ IsGroupHom.pres· T1g (negsuc n ·ℤ b) (-ℤ b)
                                          ∙ cong₂ _+ₕ_ (pres·-base-case-01 (negsuc n) b)
                                                         (IsGroupHom.presinv T1g b)

-- Nice packaging of the proof
  pres·-base-case-int : (n : ℕ) → (a : ℤ) → (m : ℕ) → (b : ℤ) →
                ℤ[x]→H*-S¹ (baseP (n ∷ []) a ·Pℤ baseP (m ∷ []) b)
              ≡ ℤ[x]→H*-S¹ (baseP (n ∷ []) a) cup ℤ[x]→H*-S¹ (baseP (m ∷ []) b)
  pres·-base-case-int zero          a zero          b = cong (base 0) (pres·-base-case-00 a b)
  pres·-base-case-int zero          a one           b = cong (base 1) (pres·-base-case-01 a b)
  pres·-base-case-int zero          a (suc (suc m)) b = refl
  pres·-base-case-int one           a zero          b = cong ℤ[x]→H*-S¹ (·PℤComm (baseP (1 ∷ []) a) (baseP (zero ∷ []) b))
                                                         ∙ pres·-base-case-int 0 b 1 a
                                                         ∙ gradCommRing (S₊ 1) 0 1 (inv (fst (Hᵐ-Sⁿ 0 1)) b) (inv (fst (Hᵐ-Sⁿ 1 1)) a)
  pres·-base-case-int one           a one           b = sym (base-neutral 2) ∙
                                                         cong (base 2) (isOfHLevelRetractFromIso 1 (fst (Hⁿ-Sᵐ≅0 1 0 nsnotz)) isPropUnit _ _)
  pres·-base-case-int one           a (suc (suc m)) b = refl
  pres·-base-case-int (suc (suc n)) a m             b = refl

  pres·-base-case-vec : (v : Vec ℕ 1) → (a : ℤ) → (v' : Vec ℕ 1) → (b : ℤ) →
                ℤ[x]→H*-S¹ (baseP v a ·Pℤ baseP v' b)
              ≡ ℤ[x]→H*-S¹ (baseP v a) cup ℤ[x]→H*-S¹ (baseP v' b)
  pres·-base-case-vec (n ∷ []) a (m ∷ []) b = pres·-base-case-int n a m b

  -- proof of the morphism
  ℤ[x]→H*-S¹-pres· : (x y : ℤ[x]) → ℤ[x]→H*-S¹ (x ·Pℤ y) ≡ ℤ[x]→H*-S¹ x cup ℤ[x]→H*-S¹ y
  ℤ[x]→H*-S¹-pres· = Poly-Ind-Prop.f _ _ _
                         (λ x p q i y j → isSetH* _ _ (p y) (q y) i j)
                         (λ y → refl)
                         base-case
                         λ {U V} ind-U ind-V y → cong₂ _+H*_ (ind-U y) (ind-V y)
    where
    base-case : _
    base-case (n ∷ []) a = Poly-Ind-Prop.f _ _ _ (λ _ → isSetH* _ _)
                           (sym (RingTheory.0RightAnnihilates (H*R (S₊ 1)) _))
                           (λ v' b → pres·-base-case-vec (n ∷ []) a v' b)
                           λ {U V} ind-U ind-V → (cong₂ _+H*_ ind-U ind-V) ∙ sym (·H*Rdist+ _ _ _)

-----------------------------------------------------------------------------
-- Function on ℤ[x]/x + morphism

  ℤ[x]→H*-S¹-cancelX : (k : Fin 1) → ℤ[x]→H*-S¹ (<X²> k) ≡ 0H*
  ℤ[x]→H*-S¹-cancelX zero = refl

  ℤ[X]→H*-S¹ : RingHom (CommRing→Ring ℤ[X]) (H*R (S₊ 1))
  fst ℤ[X]→H*-S¹ = ℤ[x]→H*-S¹
  snd ℤ[X]→H*-S¹ = makeIsRingHom ℤ[x]→H*-S¹-pres1Pℤ ℤ[x]→H*-S¹-pres+ ℤ[x]→H*-S¹-pres·

  ℤ[X]/X²→H*R-S¹ : RingHom (CommRing→Ring ℤ[X]/X²) (H*R (S₊ 1))
  ℤ[X]/X²→H*R-S¹ = Quotient-FGideal-CommRing-Ring.f ℤ[X] (H*R (S₊ 1)) ℤ[X]→H*-S¹ <X²> ℤ[x]→H*-S¹-cancelX

  ℤ[x]/x²→H*-S¹ : ℤ[x]/x² → H* (S₊ 1)
  ℤ[x]/x²→H*-S¹ = fst ℤ[X]/X²→H*R-S¹

-----------------------------------------------------------------------------
-- Converse Sens on ℤ[X] + ℤ[x]/x

  H*-S¹→ℤ[x] : H* (S₊ 1) → ℤ[x]
  H*-S¹→ℤ[x] = DS-Rec-Set.f _ _ _ _ isSetPℤ
                  0Pℤ
                  base-trad
                  _+Pℤ_
                  +PℤAssoc
                  +PℤRid
                  +PℤComm
                  base-neutral-eq
                  base-add-eq
               where
               base-trad : _
               base-trad zero a          = baseP (0 ∷ []) (fun (fst (Hᵐ-Sⁿ 0 1)) a)
               base-trad one a           = baseP (1 ∷ []) (fun (fst (Hᵐ-Sⁿ 1 1)) a)
               base-trad (suc (suc n)) a = 0Pℤ

               base-neutral-eq : _
               base-neutral-eq zero          = cong (baseP (0 ∷ [])) (IsGroupHom.pres1 (snd (Hᵐ-Sⁿ 0 1))) ∙ base-0P _
               base-neutral-eq one           = cong (baseP (1 ∷ [])) (IsGroupHom.pres1 (snd (Hᵐ-Sⁿ 1 1))) ∙ base-0P _
               base-neutral-eq (suc (suc n)) = refl

               base-add-eq : _
               base-add-eq zero a b        = (base-poly+ _ _ _) ∙ (cong (baseP (0 ∷ [])) (sym (IsGroupHom.pres· (snd (Hᵐ-Sⁿ 0 1)) a b)))
               base-add-eq one a b         = (base-poly+ _ _ _) ∙ (cong (baseP (1 ∷ [])) (sym (IsGroupHom.pres· (snd (Hᵐ-Sⁿ 1 1)) a b)))
               base-add-eq (suc (suc n)) a b = +PℤRid _

  H*-S¹→ℤ[x]-pres+ : (x y : H* (S₊ 1)) → H*-S¹→ℤ[x] ( x +H* y) ≡ H*-S¹→ℤ[x] x +Pℤ H*-S¹→ℤ[x] y
  H*-S¹→ℤ[x]-pres+ x y = refl

  H*-S¹→ℤ[x]/x² : H* (S₊ 1) → ℤ[x]/x²
  H*-S¹→ℤ[x]/x² = [_] ∘ H*-S¹→ℤ[x]

  H*-S¹→ℤ[x]/x²-pres+ : (x y : H* (S₊ 1)) → H*-S¹→ℤ[x]/x² (x +H* y) ≡ (H*-S¹→ℤ[x]/x² x) +PℤI (H*-S¹→ℤ[x]/x² y)
  H*-S¹→ℤ[x]/x²-pres+ x y = refl

-----------------------------------------------------------------------------
-- Section

  e-sect : (x : H* (S₊ 1)) → ℤ[x]/x²→H*-S¹ (H*-S¹→ℤ[x]/x² x) ≡ x
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong₂ _+H*_ ind-U ind-V
           where
           base-case : _
           base-case zero          a = cong (base 0) (leftInv (fst (Hᵐ-Sⁿ 0 1)) a)
           base-case one           a = cong (base 1) (leftInv (fst (Hᵐ-Sⁿ 1 1)) a)
           base-case (suc (suc n)) a = (sym (base-neutral (suc (suc n))))
                                       ∙ cong (base (suc (suc n))) (isOfHLevelRetractFromIso 1 (fst (Hⁿ-Sᵐ≅0 (suc n) 0 nsnotz)) isPropUnit _ _)

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (x : ℤ[x]/x²) → H*-S¹→ℤ[x]/x² (ℤ[x]/x²→H*-S¹ x) ≡ x
  e-retr = SQ.elimProp (λ _ → isSetPℤI _ _)
           (Poly-Ind-Prop.f _ _ _ (λ _ → isSetPℤI _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V)
           where
           base-case : _
           base-case (zero ∷ [])        a = cong [_] (cong (baseP (0 ∷ [])) (rightInv (fst (Hᵐ-Sⁿ 0 1)) a))
           base-case (one ∷ [])         a = cong [_] (cong (baseP (1 ∷ [])) (rightInv (fst (Hᵐ-Sⁿ 1 1)) a))
           base-case (suc (suc n) ∷ []) a = eq/ 0Pℤ (baseP (suc (suc n) ∷ []) a) ∣ ((λ x → baseP (n ∷ []) (-ℤ a)) , helper) ∣₁
             where
             helper : _
             helper = (+PℤLid _) ∙ cong₂ baseP (cong (λ X → X ∷ []) (sym (+-comm n 2))) (sym (·ℤRid _)) ∙ (sym (+PℤRid _))

-----------------------------------------------------------------------------
-- Computation of the Cohomology Ring

module _ where

  open Equiv-S1-Properties

  S¹-CohomologyRing : RingEquiv (CommRing→Ring ℤ[X]/X²) (H*R (S₊ 1))
  fst S¹-CohomologyRing = isoToEquiv is
    where
    is : Iso ℤ[x]/x² (H* (S₊ 1))
    fun is = ℤ[x]/x²→H*-S¹
    inv is = H*-S¹→ℤ[x]/x²
    rightInv is = e-sect
    leftInv is = e-retr
  snd S¹-CohomologyRing = snd ℤ[X]/X²→H*R-S¹

  CohomologyRing-S¹ : RingEquiv (H*R (S₊ 1)) (CommRing→Ring ℤ[X]/X²)
  CohomologyRing-S¹ = RingEquivs.invEquivRing S¹-CohomologyRing

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
{-# OPTIONS --type-in-type
            --no-termination-check
            --no-positivity-check #-}

module IMDesc where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Sigma and friends
--****************

data Sigma (A : Set)(B : A -> Set) : Set where
  _,_ : (x : A)(y : B x) -> Sigma A B

_*_ : (A B : Set) -> Set
A * B = Sigma A \_ -> B

fst : {A : Set}{B : A -> Set} -> Sigma A B -> A
fst (a , _) = a

snd : {A : Set}{B : A -> Set} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero : Set where
record One : Set where

--****************
-- Sum and friends
--****************

data _+_ (A B : Set) : Set where
  l : A -> A + B
  r : B -> A + B

--****************
-- Prop
--****************

data EProp : Set where
  Trivial : EProp

Prf : EProp -> Set
Prf _ = {! !}

--****************
-- Enum
--****************

data EnumU : Set where

data EnumT (E : EnumU) : Set where

Branches : (E : EnumU) -> (P : EnumT E -> Set) -> Set
Branches  _ _ = {! !}

switch : (E : EnumU) -> (e : EnumT E) -> (P : EnumT E -> Set) -> Branches E P -> P e
switch = {! !}

--********************************************
-- IMDesc
--********************************************

--****************
-- Code
--****************

data IDesc (I : Set) : Set where
  iat      : (i : I) -> IDesc I
  ipi      : (S : Set)(T : S -> IDesc I) -> IDesc I
  isigma   : (S : Set)(T : S -> IDesc I) -> IDesc I
  iprf     : (Q : EProp) -> IDesc I
  iprod    : (D : IDesc I)(D : IDesc I) -> IDesc I
  ifsigma  : (E : EnumU)(f : Branches E (\ _ -> IDesc I)) -> IDesc I

--****************
-- Interpretation
--****************

desc : (I : Set)(D : IDesc I)(P : I -> Set) -> Set
desc I (iat i)        P = P i
desc I (ipi S T)      P = (s : S) -> desc I (T s) P
desc I (isigma S T)   P = Sigma S (\ s -> desc I (T s) P)
desc I (iprf q)       P = Prf q
desc I (iprod D D')   P = Sigma (desc I D P) (\ _ -> desc I D' P)
desc I (ifsigma E B)  P = Sigma (EnumT E) (\ e -> desc I (switch E e (\ _ -> IDesc I) B) P)

--****************
-- Curried and uncurried interpretations
--****************

curryD : (I : Set)(D : IDesc I)(P : I -> Set)(R : desc I D P -> Set) -> Set
curryD I (iat i) P R = (x : P i) -> R x
curryD I (ipi S T) P R = (f : (s : S) -> desc I (T s) P) -> R f
curryD I (isigma S T) P R = (s : S) -> curryD I (T s) P (\ d -> R (s , d))
curryD I (iprf Q) P R = (x : Prf Q) -> R x
curryD I (iprod D D') P R = curryD I D P (\ d ->
                             curryD I D' P (\ d' -> R (d , d')))
curryD I (ifsigma E B) P R = Branches E (\e -> curryD I (switch E e (\_ -> IDesc I) B) P (\d -> R (e , d)))

uncurryD : (I : Set)(D : IDesc I)(P : I -> Set)(R : desc I D P -> Set) ->
           curryD I D P R -> (xs : desc I D P) -> R xs
uncurryD I (iat i) P R f xs = f xs
uncurryD I (ipi S T) P R F f = F f
uncurryD I (isigma S T) P R f (s , d) =  uncurryD I (T s) P (\d -> R (s , d)) (f s) d
uncurryD I (iprf Q) P R f q = f q
uncurryD I (iprod D D') P R f (d , d') =  uncurryD I D' P ((\ d' → R (d , d')))
                                           (uncurryD I D P ((\ x → curryD I D' P (\ d0 → R (x , d0)))) f d) d'
uncurryD I (ifsigma E B) P R br (e , d) =  uncurryD I (switch E e (\ _ -> IDesc I) B) P
                                                      (\ d -> R ( e , d ))
                                                      (switch E e ( \ e -> R ( e , d)) br) d

--****************
-- Everywhere
--****************

box : (I : Set)(D : IDesc I)(P : I -> Set) -> desc I D P -> IDesc (Sigma I P)
box I (iat i)        P x         = iat (i , x)
box I (ipi S T)      P f         = ipi S (\ s -> box I (T s) P (f s))
box I (isigma S T)   P (s , d)   = box I (T s) P d
box I (iprf Q)       P q         = iprf Trivial
box I (iprod D D')   P (d , d')  = iprod (box I D P d) (box I D' P d')
box I (ifsigma E B)  P (e , d)   = box I (switch E e (\ _ -> IDesc I) B) P d

mapbox : (I : Set)(D : IDesc I)(Z : I -> Set)(P : Sigma I Z -> Set) ->
         ((x : Sigma I Z) -> P x) ->
         ( d : desc I D Z) -> desc (Sigma I Z) (box I D Z d) P
mapbox = {!!}

--****************
-- Fix-point
--****************

data IMu (I : Set)(D : I -> IDesc I)(i : I) : Set where
  Con : desc I (D i) (\ j -> IMu I D j) -> IMu I D i

--****************
-- Induction, curried
--****************

inductionC : (I : Set)(D : I -> IDesc I)(i : I)(v : IMu I D i)
             (P : Sigma I (IMu I D) -> Set)
             (m : (i : I) ->
                  curryD I (D i) (IMu I D) (\xs ->
                    curryD (Sigma I (IMu I D))
                           (box I (D i) (IMu I D) xs)
                           P
                           (\ _ -> P (i , Con xs)))) ->
             P ( i , v )
inductionC I D i (Con x) P m =
  let t = uncurryD  I
                    (D i)
                    (IMu I D)
                    (\xs ->
                    curryD (Sigma I (IMu I D))
                           (box I (D i) (IMu I D) xs)
                           P
                           (\ _ -> P (i , Con xs)))
                    (m i)
                    x
  in
  uncurryD (Sigma I (IMu I D))
           ( box I (D i) (IMu I D) x)
           P
           (\ _ -> P ( i , Con x))
           t
           (mapbox I ( D i) ( IMu I D) P ind x)
           where ind : (x' : Sigma I (IMu I D)) -> P x'
                 ind ( i , x) = inductionC I D i x P m

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
module Lib.Fin where

open import Lib.Nat
open import Lib.Bool
open import Lib.Id

data Fin : Nat -> Set where
  zero : {n : Nat} -> Fin (suc n)
  suc  : {n : Nat} -> Fin n -> Fin (suc n)

fromNat : (n : Nat) -> Fin (suc n)
fromNat zero    = zero
fromNat (suc n) = suc (fromNat n)

toNat : {n : Nat} -> Fin n -> Nat
toNat zero    = zero
toNat (suc n) = suc (toNat n)

weaken : {n : Nat} -> Fin n -> Fin (suc n)
weaken zero    = zero
weaken (suc n) = suc (weaken n)

lem-toNat-weaken : forall {n} (i : Fin n) -> toNat i ≡ toNat (weaken i)
lem-toNat-weaken zero    = refl
lem-toNat-weaken (suc i) with toNat i | lem-toNat-weaken i
... | .(toNat (weaken i)) | refl = refl

lem-toNat-fromNat : (n : Nat) -> toNat (fromNat n) ≡ n
lem-toNat-fromNat zero = refl
lem-toNat-fromNat (suc n) with toNat (fromNat n) | lem-toNat-fromNat n
... | .n | refl = refl

finEq : {n : Nat} -> Fin n -> Fin n -> Bool
finEq  zero    zero   = true
finEq  zero   (suc _) = false
finEq (suc _)  zero   = false
finEq (suc i) (suc j) = finEq i j

-- A view telling you if a given element is the maximal one.
data MaxView {n : Nat} : Fin (suc n) -> Set where
  theMax : MaxView (fromNat n)
  notMax : (i : Fin n) -> MaxView (weaken i)

maxView : {n : Nat}(i : Fin (suc n)) -> MaxView i
maxView {zero} zero = theMax
maxView {zero} (suc ())
maxView {suc n} zero = notMax zero
maxView {suc n} (suc i) with maxView i
maxView {suc n} (suc .(fromNat n)) | theMax   = theMax
maxView {suc n} (suc .(weaken i))  | notMax i = notMax (suc i)

-- The non zero view

data NonEmptyView : {n : Nat} -> Fin n -> Set where
  ne : {n : Nat}{i : Fin (suc n)} -> NonEmptyView i

nonEmpty : {n : Nat}(i : Fin n) -> NonEmptyView i
nonEmpty zero    = ne
nonEmpty (suc _) = ne

-- The thinning view

thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n)
thin zero    j       = suc j
thin (suc i) zero    = zero
thin (suc i) (suc j) = suc (thin i j)

data EqView : {n : Nat} -> Fin n -> Fin n -> Set where
  equal    : {n : Nat}{i : Fin n} -> EqView i i
  notequal : {n : Nat}{i : Fin (suc n)}(j : Fin n) -> EqView i (thin i j)

compare : {n : Nat}(i j : Fin n) -> EqView i j
compare zero    zero    = equal
compare zero    (suc j) = notequal j
compare (suc i) zero    with nonEmpty i
...                | ne = notequal zero
compare (suc i) (suc j) with compare i j
compare (suc i) (suc .i)          | equal      = equal
compare (suc i) (suc .(thin i j)) | notequal j = notequal (suc j)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Integer division
------------------------------------------------------------------------

module Data.Nat.DivMod where

open import Data.Nat
open import Data.Nat.Properties
open SemiringSolver
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
import Data.Fin.Props as Fin
open import Induction.Nat
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Function

------------------------------------------------------------------------
-- Some boring lemmas

private

  lem₁ : ∀ m k → _
  lem₁ m k = cong suc $ begin
    m
      ≡⟨ Fin.inject+-lemma m k ⟩
    toℕ (Fin.inject+ k (fromℕ m))
      ≡⟨ solve 1 (λ x → x := x :+ con 0) refl _ ⟩
    toℕ (Fin.inject+ k (fromℕ m)) + 0
      ∎

  lem₂ : ∀ n → _
  lem₂ = solve 1 (λ n → con 1 :+ n  :=  con 1 :+ (n :+ con 0)) refl

  lem₃ : ∀ n k q r eq → _
  lem₃ n k q r eq = begin
      suc n + k
        ≡⟨ solve 2 (λ n k → con 1 :+ n :+ k  :=  n :+ (con 1 :+ k))
                   refl n k ⟩
      n + suc k
        ≡⟨ cong (_+_ n) eq ⟩
      n + (toℕ r + q * n)
        ≡⟨ solve 3 (λ n r q → n :+ (r :+ q :* n)  :=
                              r :+ (con 1 :+ q) :* n)
                   refl n (toℕ r) q ⟩
      toℕ r + suc q * n
        ∎

------------------------------------------------------------------------
-- Division

-- A specification of integer division.

data DivMod : ℕ → ℕ → Set where
  result : {divisor : ℕ} (q : ℕ) (r : Fin divisor) →
           DivMod (toℕ r + q * divisor) divisor

-- Sometimes the following type is more usable; functions in indices
-- can be inconvenient.

data DivMod' (dividend divisor : ℕ) : Set where
  result : (q : ℕ) (r : Fin divisor)
           (eq : dividend ≡ toℕ r + q * divisor) →
           DivMod' dividend divisor

-- Integer division with remainder.

-- Note that Induction.Nat.<-rec is used to ensure termination of
-- division. The run-time complexity of this implementation of integer
-- division should be linear in the size of the dividend, assuming
-- that well-founded recursion and the equality type are optimised
-- properly (see "Inductive Families Need Not Store Their Indices"
-- (Brady, McBride, McKinna, TYPES 2003)).

_divMod'_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
            DivMod' dividend divisor
_divMod'_ m n {≢0} = <-rec Pred dm m n {≢0}
  where
  Pred : ℕ → Set
  Pred dividend = (divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
                  DivMod' dividend divisor

  1+_ : ∀ {k n} → DivMod' (suc k) n → DivMod' (suc n + k) n
  1+_ {k} {n} (result q r eq) = result (1 + q) r (lem₃ n k q r eq)

  dm : (dividend : ℕ) → <-Rec Pred dividend → Pred dividend
  dm m       rec zero    {≢0 = ()}
  dm zero    rec (suc n)            = result 0 zero refl
  dm (suc m) rec (suc n)            with compare m n
  dm (suc m) rec (suc .(suc m + k)) | less .m k    = result 0 r  (lem₁ m k)
                                        where r = suc (Fin.inject+ k (fromℕ m))
  dm (suc m) rec (suc .m)           | equal .m     = result 1 zero (lem₂ m)
  dm (suc .(suc n + k)) rec (suc n) | greater .n k =
    1+ rec (suc k) le (suc n)
    where le = s≤′s (s≤′s (n≤′m+n n k))

-- A variant.

_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
           DivMod dividend divisor
_divMod_ m n {≢0} with _divMod'_ m n {≢0}
.(toℕ r + q * n) divMod n | result q r refl = result q r

-- Integer division.

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
_div_ m n {≢0} with _divMod_ m n {≢0}
.(toℕ r + q * n) div n | result q r = q

-- The remainder after integer division.

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
_mod_ m n {≢0} with _divMod_ m n {≢0}
.(toℕ r + q * n) mod n | result q r = r

max_issues_repo_name: larrytheliquid/Lemmachine


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

-- [1] Hofmann, Martin and Thomas Streicher (1998). “The groupoid
--     interpretation on type theory”. In: Twenty-five Years of
--     Constructive Type Theory. Ed. by Giovanni Sambin and Jan
--     M. Smith. Oxford University Press. Chap. 6.

module UIP where

data Id (A : Set)(x : A) : A → Set where
  refl : Id A x x

K : (A : Set)(x : A)(P : Id A x x → Set) → P refl → (p : Id A x x ) → P p
K A x P pr refl = pr

-- From [1, p. 88].
UIP : (A : Set)(a a' : A)(p p' : Id A a a') → Id (Id A a a') p p'
UIP A a .a refl refl = refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Jesper, 2019-05-20: When checking confluence of two rewrite rules,
-- we disable all reductions during unification of the left-hand
-- sides. However, we should not disable reductions at the type-level,
-- as shown by this (non-confluent) example.

{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Unit : Set where unit : Unit

A : Unit → Set
A unit = ⊤

postulate
  a b : (u : Unit) → A u
  f : (u : Unit) → A u → Bool
  f-a : (u : Unit) → f u (a u) ≡ true
  f-b : (u : Unit) → f u (b u) ≡ false

{-# REWRITE f-a #-}
{-# REWRITE f-b #-}

cong-f : (u : Unit) (x y : A u) → x ≡ y → f u x ≡ f u y
cong-f u x y refl = refl

boom : true ≡ false
boom = cong-f unit (a unit) (b unit) refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module UniDB.Morph.Weaken where

open import UniDB.Spec

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

data Weaken : MOR where
  weaken : {γ : Dom} (δ : Dom) → Weaken γ (γ ∪ δ)

instance
  iLkWeaken : {T : STX} {{vrT : Vr T}} → Lk T Weaken
  lk {{iLkWeaken}} (weaken δ) i = vr (wk δ i)

  iWkmWeaken : Wkm Weaken
  wkm {{iWkmWeaken}} = weaken

  iIdmWeaken : Idm Weaken
  idm {{iIdmWeaken}} γ = weaken 0

  iWkWeaken : {γ₁ : Dom} → Wk (Weaken γ₁)
  wk₁ {{iWkWeaken}} (weaken δ) = weaken (suc δ)
  wk {{iWkWeaken}} zero x = x
  wk {{iWkWeaken}} (suc δ) x = wk₁ (wk δ x)
  wk-zero {{iWkWeaken}} x = refl
  wk-suc {{iWkWeaken}} δ x = refl

  iLkWkmWeaken : {T : STX} {{vrT : Vr T}} → LkWkm T Weaken
  lk-wkm {{iLkWkmWeaken}} δ i = refl

  iCompWeaken : Comp Weaken
  _⊙_ {{iCompWeaken}} ξ (weaken δ) = wk δ ξ

wk₁-comp : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken γ₁ γ₂) (ξ₂ : Weaken γ₂ γ₃) →
  wk₁ (ξ₁ ⊙ ξ₂) ≡ ξ₁ ⊙ wk₁ ξ₂
wk₁-comp ξ₁ (weaken δ) = refl

wk-comp : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Weaken γ₁ γ₂) (ξ₂ : Weaken γ₂ γ₃)
  (δ : Dom) → wk δ (ξ₁ ⊙ ξ₂) ≡ ξ₁ ⊙ wk δ ξ₂
wk-comp ξ₁ ξ₂ zero    = refl
wk-comp ξ₁ ξ₂ (suc δ) =
  trans (cong wk₁ (wk-comp ξ₁ ξ₂ δ)) (wk₁-comp ξ₁ (wk δ ξ₂))

module _ (T : STX) {{vrT : Vr T}} where

  lk-wk₁-weaken : {{wkT : Wk T}} {{wkVrT : WkVr T}}
    {γ₁ γ₂ : Dom} (ξ : Weaken γ₁ γ₂) (i : Ix γ₁) →
    lk {T} {Weaken} (wk₁ ξ) i ≡ wk₁ (lk {T} {Weaken} ξ i)
  lk-wk₁-weaken (weaken δ) i = sym (wk₁-vr {T} (wk δ i))

  lk-wk-weaken : {{wkT : Wk T}} {{wkVrT : WkVr T}}
    {γ₁ γ₂ : Dom} (δ : Dom) (ξ : Weaken γ₁ γ₂) (i : Ix γ₁) →
    lk {T} {Weaken} (wk δ ξ) i ≡ wk δ (lk {T} {Weaken} ξ i)
  lk-wk-weaken zero    ξ i = sym (wk-zero (lk {T} {Weaken} ξ i))
  lk-wk-weaken (suc δ) ξ i =
    trans
      (lk-wk₁-weaken (wk δ ξ) i)
      (trans
         (cong wk₁ (lk-wk-weaken δ ξ i))
         (sym (wk-suc {T} δ (lk {T} {Weaken} ξ i)))
      )

instance
  iLkRenWeaken : {T : STX} {{vrT : Vr T}} → LkRen T Weaken
  lk-ren {{iLkRenWeaken}} (weaken δ) i = refl

  iLkRenCompWeaken :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{wkVrT : WkVr T}}  →
    LkRenComp T Weaken
  lk-ren-comp {{iLkRenCompWeaken {T}}} ξ₁ (weaken δ) i = begin
    lk {T} {Weaken} (wk δ ξ₁) i         ≡⟨ lk-wk-weaken T δ ξ₁ i ⟩
    wk δ (lk {T} {Weaken} ξ₁ i)         ≡⟨ cong (wk δ) (lk-ren {T} {Weaken} ξ₁ i) ⟩
    wk δ (vr {T} (lk {Ix} {Weaken} ξ₁ i)) ≡⟨ wk-vr {T} δ (lk {Ix} {Weaken} ξ₁ i) ⟩
    vr {T} (wk δ (lk {Ix} {Weaken} ξ₁ i)) ∎

  iCompIdmWeaken : CompIdm Weaken
  ⊙-idm {{iCompIdmWeaken}} ξ                = refl
  idm-⊙ {{iCompIdmWeaken}} (weaken zero)    = refl
  idm-⊙ {{iCompIdmWeaken}} (weaken (suc δ)) =
    cong wk₁ (idm-⊙ {Weaken} (weaken δ))

  iCompAssocWeaken : CompAssoc Weaken
  ⊙-assoc {{iCompAssocWeaken}} ξ₁ ξ₂ (weaken δ) = sym (wk-comp ξ₁ ξ₂ δ)

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Jesper, 2017-01-23: when instantiating a variable during unification,
-- we should check that the type of the variable is equal to the type
-- of the equation (and not just a subtype of it). See Issue 2407.

open import Agda.Builtin.Equality
open import Agda.Builtin.Size

data D : Size → Set where

J= : ∀ {ℓ} {s : Size} (x₀ : D s)
   → (P : (x : D s) → _≡_ {A = D s} x₀ x → Set ℓ)
   → P x₀ refl → (x : D s) (e : _≡_ {A = D s} x₀ x) → P x e
J= _ P p _ refl = p

J< : ∀ {ℓ} {s : Size} {s' : Size< s} (x₀ : D s)
   → (P : (x : D s) → _≡_ {A = D s} x₀ x → Set ℓ)
   → P x₀ refl → (x : D s') (e : _≡_ {A = D s} x₀ x) → P x e
J< _ P p _ refl = p

J> : ∀ {ℓ} {s : Size} {s' : Size< s} (x₀ : D s')
   → (P : (x : D s) → _≡_ {A = D s} x₀ x → Set ℓ)
   → P x₀ refl → (x : D s) (e : _≡_ {A = D s} x₀ x) → P x e
J> _ P p _ refl = p

J~ : ∀ {ℓ} {s : Size} {s' s'' : Size< s} (x₀ : D s')
   → (P : (x : D s) → _≡_ {A = D s} x₀ x → Set ℓ)
   → P x₀ refl → (x : D s'') (e : _≡_ {A = D s} x₀ x) → P x e
J~ _ P p _ refl = p

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

open import AISEC.Utils
open import Data.Real as ℝ using (ℝ)
open import Data.List

module MyTestModule where

f : Tensor ℝ (1 ∷ []) → Tensor ℝ (1 ∷ [])
f = evaluate record
  { databasePath = DATABASE_PATH
  ; networkUUID  = NETWORK_UUID
  }

monotonic : ∀ (x1 : Tensor ℝ (1 ∷ [])) → ∀ (x2 : Tensor ℝ (1 ∷ [])) → let y1 = f (x1)
y2 = f (x2) in x1 0 ℝ.≤ x2 0 → y1 0 ℝ.≤ y2 0
monotonic = checkProperty record
  { databasePath = DATABASE_PATH
  ; propertyUUID = ????
  }

max_stars_repo_name: Yiergot/vehicle

max_issues_repo_name: Yiergot/vehicle

max_forks_repo_name: Yiergot/vehicle


text:
module Numeral.Natural.Oper.Proofs.Structure where

open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Operator.Monoid

instance
  [+]-monoid : Monoid(_+_)
  Monoid.identity-existence [+]-monoid = [∃]-intro(𝟎)

instance
  [⋅]-monoid : Monoid(_⋅_)
  Monoid.identity-existence [⋅]-monoid = [∃]-intro(𝐒(𝟎))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module Computability.Function where

open import Computability.Prelude
import Function

variable
  l₀ l₁ : Level

Injective : {A : Set l₀}{B : Set l₁} → (A → B) → Set _
Injective = Function.Injective _≡_ _≡_

Surjective : {A : Set l₀}{B : Set l₁} → (A → B) → Set _
Surjective {A = A} {B = B} = Function.Surjective {A = A} {B = B} _≡_ _≡_

Bijective : {A : Set l₀}{B : Set l₁} → (A → B) → Set _
Bijective = Function.Bijective _≡_ _≡_

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


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

module Cubical.HITs.FreeGroup where

open import Cubical.HITs.FreeGroup.Base public
open import Cubical.HITs.FreeGroup.Properties public


text:
mutual
  data ℕμ : Set where
    zero : ℕμ
    succ : ℕμ → ℕμ
    delay : ℕν → ℕμ

  record ℕν : Set where
    coinductive
    field step : ℕμ

open ℕν public

mutual
  data _≤μ_ : ℕμ → ℕμ → Set where
    -- Standard part of the order
    le₀ : (y : ℕμ) → zero ≤μ y
    leₛ : {x y : ℕμ} → x ≤μ y → succ x ≤μ succ y
    -- We can have finite delays on the left and on the right...
    le-stepₗ : {m : ℕν} {y : ℕμ} → step m ≤μ y → delay m ≤μ y
    le-stepᵣ : {x : ℕμ} {n : ℕν} → x ≤μ step n → x ≤μ delay n
    -- or an abritrary sequence of delays on both sides.
    le-step : {m n : ℕν} → m ≤ n → delay m ≤μ delay n

  record _≤_ (m n : ℕν) : Set where
    coinductive
    field step≤ : (step m) ≤μ (step m)

open _≤_ public

≤μ-refl : (x : ℕμ) → x ≤μ x
≤-refl : (m : ℕν) → m ≤ m

step≤ (≤-refl m) = ≤μ-refl (step m)

≤μ-refl zero = le₀ zero
≤μ-refl (succ x) = leₛ (≤μ-refl x)
≤μ-refl (delay x) = le-step (≤-refl x)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Issue329b where

abstract
  infixl 0 D Undeclared
  data D : Set where


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

open import Level hiding (zero)

open import Relation.Binary

module SDG.Extra.OrderedAlgebra.Structures {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Algebra.Structures
open import Algebra.FunctionProperties

record IsOrderedCommutativeRing
    (_<_ : Rel A ℓ)
    (_+_ _*_ : Op₂ A)
    (-_ : Op₁ A)
    (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
    <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
    <-+ : ∀ (a b c) → a < b → (a + c) < (b + c)
    <-* : ∀ (a b) → 0# < a → 0# < b → 0# < (a * b)

  open IsCommutativeRing isCommutativeRing public
    --using (zero)
  open IsStrictTotalOrder <-isStrictTotalOrder public

max_stars_repo_name: wrrnhttn/agda-sdg

max_issues_repo_name: wrrnhttn/agda-sdg

max_forks_repo_name: wrrnhttn/agda-sdg


text:
{-# OPTIONS --no-termination-check #-}

module PiPath where

open import Level
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------
-- Universe of types

-- The type < v > is the singleton type containing the one value v. We can
-- construct values of this type using (singleton v' proof) where the proof
-- asserts that v is propositionally equal to v.

data <_> {a : Level} {A : Set a} (x : A) : Set a where
  singleton : (y : A) → y ≡ x → < x >

-- The types of Pi include 0, 1, +, * as usual but

data B : Set where
  ZERO   : B
  ONE    : B
  PLUS   : B → B → B
  TIMES  : B → B → B
  RECIP  : B → (B → B) → B

⟦_⟧ : B → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS b₁ b₂ ⟧  = ⟦ b₁ ⟧ ⊎ ⟦ b₂ ⟧
⟦ TIMES b₁ b₂ ⟧ = ⟦ b₁ ⟧ × ⟦ b₂ ⟧
⟦ RECIP b ⟧     = (v : ⟦ b ⟧) → ⊤

------------------------------------------------------------------------------
-- syntax and types of combinators ⟷ refers to eval
-- eval refers to evalB
-- evalB refers to eval and reverse
-- reverse refers to reverse'
-- reverse' refers to reverse

-- syntax and types of combinators

data _⟷_ : B → B → Set₁ where
  unite₊ : {b : B} → PLUS ZERO b ⟷ b
  uniti₊ : {b : B} → b ⟷ PLUS ZERO b
  swap₊ : {b₁ b₂ : B} → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆ : {b₁ b₂ : B} → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  id⟷ : {b : B } → b ⟷ b
  op    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)
  ε : {b₁ : B} → TIMES b₁ (TIMES b₁ (RECIP b₁)) ⟷ b₁

-- Semantics
mutual
  eval : {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
  eval unite₊ (inj₁ ())
  eval unite₊ (inj₂ v) = v
  eval uniti₊ v = inj₂ v
  eval swap₊ (inj₁ x) = inj₂ x
  eval swap₊ (inj₂ y) = inj₁ y
  eval assocl₊ (inj₁ x) = inj₁ (inj₁ x)
  eval assocl₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  eval assocl₊ (inj₂ (inj₂ x)) = inj₂ x
  eval assocr₊ (inj₁ (inj₁ x)) = inj₁ x
  eval assocr₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  eval assocr₊ (inj₂ y) = inj₂ (inj₂ y)
  eval unite⋆ (tt , x) = x
  eval uniti⋆ v = ( tt , v)
  eval swap⋆ (v₁ , v₂) = (v₂ , v₁)
  eval assocl⋆ (x , (y , z)) = ((x , y), z)
  eval assocr⋆ ((x , y), z) = (x , (y , z))
  eval id⟷ v = v
  eval (op c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (inj₁ x) = inj₁ (eval c₁ x)
  eval (c₁ ⊕ c₂) (inj₂ y) = inj₂ (eval c₂ y)
  eval (c₁ ⊗ c₂) (x , y) = (eval c₁ x , eval c₂ y)
  eval ε (x , y , z) = x

  evalB :  {b₁ b₂ : B} → (c : b₁ ⟷ b₂) → ⟦ b₂ ⟧ → ⟦ b₁ ⟧
  evalB uniti₊ (inj₁ ())
  evalB uniti₊ (inj₂ v) = v
  evalB unite₊ v = inj₂ v
  evalB swap₊ (inj₁ x) = inj₂ x
  evalB swap₊ (inj₂ y) = inj₁ y
  evalB assocr₊ (inj₁ x) = inj₁ (inj₁ x)
  evalB assocr₊ (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
  evalB assocr₊ (inj₂ (inj₂ x)) = inj₂ x
  evalB assocl₊ (inj₁ (inj₁ x)) = inj₁ x
  evalB assocl₊ (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
  evalB assocl₊ (inj₂ y) = inj₂ (inj₂ y)
  evalB uniti⋆ (tt , x) = x
  evalB unite⋆ v = ( tt , v)
  evalB swap⋆ (v₁ , v₂) = (v₂ , v₁)
  evalB assocr⋆ (x , (y , z)) = ((x , y), z)
  evalB assocl⋆ ((x , y), z) = (x , (y , z))
  evalB id⟷ v = v
  evalB (op c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (inj₁ x) = inj₁ (evalB c₁ x)
  evalB (c₁ ⊕ c₂) (inj₂ y) = inj₂ (evalB c₂ y)
  evalB (c₁ ⊗ c₂) (x , y) = (evalB c₁ x , evalB c₂ y)
  evalB ε x = x , x , (λ _ → tt)

-- reversibility
mutual
  reverse : {b₁ b₂ : B} (c : b₁ ⟷ b₂) → (v : ⟦ b₁ ⟧) → v ≡ evalB c (eval c v)
  reverse unite₊ (inj₁ ())
  reverse unite₊ (inj₂ y) = refl
  reverse uniti₊ v = refl
  reverse swap₊ (inj₁ x) = refl
  reverse swap₊ (inj₂ y) = refl
  reverse assocl₊ (inj₁ x) = refl
  reverse assocl₊ (inj₂ (inj₁ x)) = refl
  reverse assocl₊ (inj₂ (inj₂ y)) = refl
  reverse assocr₊ (inj₁ (inj₁ x)) = refl
  reverse assocr₊ (inj₁ (inj₂ y)) = refl
  reverse assocr₊ (inj₂ y) = refl
  reverse unite⋆ v = refl
  reverse uniti⋆ v = refl
  reverse swap⋆ v = refl
  reverse assocl⋆ v = refl
  reverse assocr⋆ v = refl
  reverse id⟷ v = refl
  reverse (op c) v = reverse' c v
  reverse (c ◎ c₁) v = trans (reverse c v)
                             (cong (evalB c) (reverse c₁ (eval c v)))
  reverse (c ⊕ _) (inj₁ x) = cong inj₁ (reverse c x)
  reverse (_ ⊕ c) (inj₂ y) = cong inj₂ (reverse c y)
  reverse (c₁ ⊗ c₂) (x , y) = cong₂ _,_ (reverse c₁ x) (reverse c₂ y)
  reverse ε (x , y , z) = {!!}

  reverse' : {b₁ b₂ : B} (c : b₁ ⟷ b₂) → (w : ⟦ b₂ ⟧) → w ≡ eval c (evalB c w)
  reverse' unite₊ w = refl
  reverse' uniti₊ (inj₁ ())
  reverse' uniti₊ (inj₂ y) = refl
  reverse' swap₊ (inj₁ x) = refl
  reverse' swap₊ (inj₂ y) = refl
  reverse' assocl₊ (inj₁ (inj₁ x)) = refl
  reverse' assocl₊ (inj₁ (inj₂ y)) = refl
  reverse' assocl₊ (inj₂ y) = refl
  reverse' assocr₊ (inj₁ x) = refl
  reverse' assocr₊ (inj₂ (inj₁ x)) = refl
  reverse' assocr₊ (inj₂ (inj₂ y)) = refl
  reverse' unite⋆ w = refl
  reverse' uniti⋆ w = refl
  reverse' swap⋆ w = refl
  reverse' assocl⋆ w = refl
  reverse' assocr⋆ w = refl
  reverse' id⟷ w = refl
  reverse' (op c) w = reverse c w
  reverse' (c ◎ c₁) w = trans (reverse' c₁ w)
                              (cong (eval c₁) (reverse' c (evalB c₁ w)))
  reverse' (c ⊕ _) (inj₁ x) = cong inj₁ (reverse' c x)
  reverse' (_ ⊕ c) (inj₂ y) = cong inj₂ (reverse' c y)
  reverse' (c₁ ⊗ c₂) (x , y) = cong₂ _,_ (reverse' c₁ x) (reverse' c₂ y)
  reverse' ε _ = refl
------------------------------------------------------------------------------
-- Proofs of reversibility
{-
-- they are properly inverse of each other
-- easy direction
η∘ε : {b : B} (v : ⟦ b ⟧) → eval {b} (η ◎ ε) v ≡ v
η∘ε _ = refl

-- hard direction.
ε∘η : {b : B} (v : ⟦ b ⟧) → { w : Σ < v > (λ _ → < v > → ⊤) }
      → (eval {DTIMES b (leftIdemp {b}) } {_} (ε ◎ η) (v , w)) ≡ (v , w)
ε∘η {b} v {(singleton .v refl , r )} = cong f {v , v , (singleton v refl)} refl
    where f : Σ ⟦ b ⟧ (λ x → Σ ⟦ b ⟧ (λ y → < v >)) →
                Σ ⟦ b ⟧ (λ z → Σ < z > (λ x → < z > → ⊤ ))
          f (_ , (_ , j)) = (v , j , r)

------------------------------------------------------------------------------
-- Examples
-- Now need to write some actual programs...

makeFunc : {b₁ b₂ : B} → (c : b₁ ⟷ b₂) →
            b₁ ⟷ DTIMES b₁ (λ x → TIMES (SING (eval c x)) (RECIP x))
makeFunc c = η ◎ slide (λ {_} →  (lift c refl) ⊗ id⟷)

-}
------------------------------------------------------------------------------
------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.Group (g : Group) where

open Group g
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
⁻¹-involutive x = begin
  x ⁻¹ ⁻¹               ≈⟨ sym $ proj₂ identity _ ⟩
  x ⁻¹ ⁻¹ ∙ ε           ≈⟨ refl ⟨ ∙-pres-≈ ⟩ sym (proj₁ inverse _) ⟩
  x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x)  ≈⟨ sym $ assoc _ _ _ ⟩
  x ⁻¹ ⁻¹ ∙ x ⁻¹ ∙ x    ≈⟨ proj₁ inverse _ ⟨ ∙-pres-≈ ⟩ refl ⟩
  ε ∙ x                 ≈⟨ proj₁ identity _ ⟩
  x                     ∎

left-identity-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
left-identity-unique x y eq = begin
  x              ≈⟨ sym (proj₂ identity x) ⟩
  x ∙ ε          ≈⟨ refl ⟨ ∙-pres-≈ ⟩ sym (proj₂ inverse y) ⟩
  x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ eq ⟨ ∙-pres-≈ ⟩ refl ⟩
       y  ∙ y ⁻¹ ≈⟨ proj₂ inverse y ⟩
  ε              ∎

right-identity-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
right-identity-unique x y eq = begin
  y              ≈⟨ sym (proj₁ identity y) ⟩
  ε          ∙ y ≈⟨ sym (proj₁ inverse x) ⟨ ∙-pres-≈ ⟩ refl ⟩
  (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
  x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-pres-≈ ⟩ eq ⟩
  x ⁻¹ ∙  x      ≈⟨ proj₁ inverse x ⟩
  ε              ∎

identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
identity-unique {x} id = left-identity-unique x x (proj₂ id x)


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

open import lib.Basics
open import lib.Equivalences2
open import lib.NType2
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Truncation

module lib.groups.Homomorphisms where

record GroupHom {i j} (G : Group i) (H : Group j)
  : Type (lsucc (lmax i j)) where
  constructor group-hom

  field
    f : Group.El G → Group.El H
    pres-comp  : ∀ g1 g2 → f (Group.comp G g1 g2) == Group.comp H (f g1) (f g2)

  abstract
    pres-ident : f (Group.ident G) == Group.ident H
    pres-ident = group-cancel-l H (f (Group.ident G)) $
      Group.comp H (f (Group.ident G)) (f (Group.ident G))
        =⟨ ! (pres-comp (Group.ident G) (Group.ident G)) ⟩
      f (Group.comp G (Group.ident G) (Group.ident G))
        =⟨ ap f (Group.unitl G (Group.ident G)) ⟩
      f (Group.ident G)
        =⟨ ! (Group.unitr H (f (Group.ident G))) ⟩
      Group.comp H (f (Group.ident G)) (Group.ident H) ∎

    pres-inv : (g : Group.El G) → f (Group.inv G g) == Group.inv H (f g)
    pres-inv g =
      f (Group.inv G g)
        =⟨ ! (Group.unitr H (f (Group.inv G g))) ⟩
      Group.comp H (f (Group.inv G g)) (Group.ident H)
        =⟨ ! (Group.invr H (f g))
           |in-ctx (λ w → Group.comp H (f (Group.inv G g)) w) ⟩
      Group.comp H (f (Group.inv G g)) (Group.comp H (f g) (Group.inv H (f g)))
        =⟨ ! (Group.assoc H (f (Group.inv G g)) (f g) (Group.inv H (f g))) ⟩
      Group.comp H (Group.comp H (f (Group.inv G g)) (f g)) (Group.inv H (f g))
        =⟨ ! (pres-comp (Group.inv G g) g) ∙ ap f (Group.invl G g) ∙ pres-ident
           |in-ctx (λ w → Group.comp H w (Group.inv H (f g))) ⟩
      Group.comp H (Group.ident H) (Group.inv H (f g))
        =⟨ Group.unitl H (Group.inv H (f g)) ⟩
      Group.inv H (f g) ∎

  ⊙f : Σ (Group.El G → Group.El H)
            (λ f → f (Group.ident G) == Group.ident H)
  ⊙f = (f , pres-ident)

infix 0 _→ᴳ_
_→ᴳ_ = GroupHom

GroupIso : ∀ {i j} (G : Group i) (H : Group j) → Type (lsucc (lmax i j))
GroupIso G H = Σ (G →ᴳ H) (λ φ → is-equiv (GroupHom.f φ))

infix 30 _≃ᴳ_
_≃ᴳ_ = GroupIso

idhom : ∀ {i} (G : Group i) → (G →ᴳ G)
idhom G = group-hom (idf _) (λ _ _ → idp)

idiso : ∀ {i} (G : Group i) → (G ≃ᴳ G)
idiso G = (idhom G , idf-is-equiv _)

infixr 80 _∘ᴳ_

_∘ᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → (H →ᴳ K) → (G →ᴳ H) → (G →ᴳ K)
(group-hom g g-comp) ∘ᴳ (group-hom f f-comp) =
  record {
    f = g ∘ f;
    pres-comp = λ x₁ x₂ → ap g (f-comp x₁ x₂) ∙ g-comp (f x₁) (f x₂)}

infixr 80 _∘eᴳ_

_∘eᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → H ≃ᴳ K → G ≃ᴳ H → G ≃ᴳ K
(φ₂ , ie₂) ∘eᴳ (φ₁ , ie₁) = (φ₂ ∘ᴳ φ₁ , ie₂ ∘ise ie₁)

infixl 120 _⁻¹ᴳ

_⁻¹ᴳ : ∀ {i j} {G : Group i} {H : Group j} → G ≃ᴳ H → H ≃ᴳ G
_⁻¹ᴳ {G = G} {H = H} (φ , ie) =
  (record {
     f = is-equiv.g ie;
     pres-comp = λ h₁ h₂ →
       ap2 (λ w₁ w₂ → is-equiv.g ie (Group.comp H w₁ w₂))
         (! (is-equiv.f-g ie h₁)) (! (is-equiv.f-g ie h₂))
       ∙ ! (ap (is-equiv.g ie)
               (GroupHom.pres-comp φ (is-equiv.g ie h₁) (is-equiv.g ie h₂)))
       ∙ is-equiv.g-f ie (Group.comp G (is-equiv.g ie h₁) (is-equiv.g ie h₂))} ,
   snd ((_ , ie) ⁻¹))

{- a homomorphism which is an equivalence gives a path between groups -}
module _ {i} {G H : Group i} (iso : G ≃ᴳ H) where
  private
    module G = Group G
    module H = Group H
    module φ = GroupHom (fst iso)
    ie = snd iso

  private
    ap3-lemma : ∀ {i j k l} {C : Type i} {D : C → Type j} {E : C → Type k}
      {F : Type l} {c₁ c₂ : C} {d₁ : D c₁} {d₂ : D c₂} {e₁ : E c₁} {e₂ : E c₂}
      (f : (c : C) → D c → E c → F) (p : c₁ == c₂)
      → (d₁ == d₂ [ D ↓ p ]) → (e₁ == e₂ [ E ↓ p ])
      → (f c₁ d₁ e₁ == f c₂ d₂ e₂)
    ap3-lemma f idp idp idp = idp

    ap3-lemma-el : ∀ {i} {G H : Group i}
      (p : Group.El G == Group.El H)
      (q : Group.El-level G == Group.El-level H [ _ ↓ p ])
      (r : Group.group-struct G == Group.group-struct H [ _ ↓ p ])
      → ap Group.El (ap3-lemma group p q r) == p
    ap3-lemma-el idp idp idp = idp

  abstract
    group-ua : G == H
    group-ua =
      ap3-lemma group
        (ua (φ.f , ie))
        (prop-has-all-paths-↓ has-level-is-prop)
        (↓-group-structure= (G.El-level) (ua (φ.f , ie)) ident= inv= comp=)
      where
      ident= : G.ident == H.ident [ (λ C → C) ↓ ua (φ.f , ie) ]
      ident= = ↓-idf-ua-in _ φ.pres-ident

      inv= : G.inv == H.inv [ (λ C → C → C) ↓ ua (φ.f , ie) ]
      inv= =
        ↓-→-from-transp $ λ= $ λ a →
          transport (λ C → C) (ua (φ.f , ie)) (G.inv a)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          φ.f (G.inv a)
            =⟨ φ.pres-inv a ⟩
          H.inv (φ.f a)
            =⟨ ap H.inv (! (to-transp (↓-idf-ua-in _ idp))) ⟩
          H.inv (transport (λ C → C) (ua (φ.f , ie)) a) ∎

      comp=' : (a : G.El)
        → G.comp a == H.comp (φ.f a) [ (λ C → C → C) ↓ ua (φ.f , ie) ]
      comp=' a =
        ↓-→-from-transp $ λ= $ λ b →
          transport (λ C → C) (ua (φ.f , ie)) (G.comp a b)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          φ.f (G.comp a b)
            =⟨ φ.pres-comp a b ⟩
          H.comp (φ.f a) (φ.f b)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp))
               |in-ctx (λ w → H.comp (φ.f a) w) ⟩
          H.comp (φ.f a) (transport (λ C → C) (ua (φ.f , ie)) b) ∎

      comp= : G.comp == H.comp [ (λ C → C → C → C) ↓ ua (φ.f , ie) ]
      comp= =
        ↓-→-from-transp $ λ= $ λ a →
          transport (λ C → C → C) (ua (φ.f , ie)) (G.comp a)
            =⟨ to-transp (comp=' a) ⟩
          H.comp (φ.f a)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp)) |in-ctx (λ w → H.comp w) ⟩
          H.comp (transport (λ C → C) (ua (φ.f , ie)) a) ∎

    group-ua-el : ap Group.El group-ua == ua (φ.f , ie)
    group-ua-el = ap3-lemma-el (ua (φ.f , ie)) _ _

{- equality of homomorphisms -}
abstract
  hom= : ∀ {i j} {G : Group i} {H : Group j} (φ ψ : (G →ᴳ H))
    → GroupHom.f φ == GroupHom.f ψ → φ == ψ
  hom= {H = H} _ _ p =
   ap (uncurry group-hom)
      (pair= p (prop-has-all-paths-↓
                 (Π-level (λ _ → Π-level (λ _ → Group.El-level H _ _)))))

  hom=-↓ : ∀ {i j k} {A : Type i} {G : A → Group j} {H : A → Group k} {x y : A}
    {p : x == y} (φ : G x →ᴳ H x) (ψ : G y →ᴳ H y)
    → GroupHom.f φ == GroupHom.f ψ
      [ (λ a → Group.El (G a) → Group.El (H a)) ↓ p ]
    → φ == ψ [ (λ a → G a →ᴳ H a) ↓ p ]
  hom=-↓ {p = idp} = hom=

{- homomorphism from equality of groups -}
coeᴳ : ∀ {i} {G H : Group i} → G == H → (G →ᴳ H)
coeᴳ idp = idhom _

coe!ᴳ : ∀ {i} {G H : Group i} → G == H → (H →ᴳ G)
coe!ᴳ idp = idhom _

coeᴳ-fun : ∀ {i} {G H : Group i} (p : G == H)
  → GroupHom.f (coeᴳ p) == coe (ap Group.El p)
coeᴳ-fun idp = idp

coe!ᴳ-fun : ∀ {i} {G H : Group i} (p : G == H)
  → GroupHom.f (coe!ᴳ p) == coe! (ap Group.El p)
coe!ᴳ-fun idp = idp

coeᴳ-β : ∀ {i} {G H : Group i} (iso : G ≃ᴳ H)
  → coeᴳ (group-ua iso) == fst iso
coeᴳ-β (φ , ie) = hom= _ _ $
  coeᴳ-fun (group-ua (φ , ie))
  ∙ ap coe (group-ua-el (φ , ie))
  ∙ λ= (coe-β (GroupHom.f φ , ie))

{- algebraic properties -}

∘ᴳ-unit-r : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  → φ ∘ᴳ idhom G == φ
∘ᴳ-unit-r φ = idp

∘ᴳ-unit-l : ∀ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  → idhom H ∘ᴳ φ == φ
∘ᴳ-unit-l φ = hom= _ _ $ idp

∘ᴳ-assoc : ∀ {i j k l} {G : Group i} {H : Group j} {K : Group k} {L : Group l}
  (χ : K →ᴳ L) (ψ : H →ᴳ K) (φ : G →ᴳ H)
  → (χ ∘ᴳ ψ) ∘ᴳ φ == χ ∘ᴳ ψ ∘ᴳ φ
∘ᴳ-assoc χ ψ φ = hom= _ _ $ idp

{- homomorphism with kernel zero is injective -}
module _ {i j} {G : Group i} {H : Group j} (φ : (G →ᴳ H)) where

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

  zero-kernel-injective : ((g : G.El) → φ.f g == H.ident → g == G.ident)
    → ((g₁ g₂ : G.El) → φ.f g₁ == φ.f g₂ → g₁ == g₂)
  zero-kernel-injective f g₁ g₂ p =
    ! (group-inv-inv G g₁) ∙ group-inv-unique-r G (G.inv g₁) g₂ (f _ $
      φ.f (G.comp (G.inv g₁) g₂)
        =⟨ φ.pres-comp (G.inv g₁) g₂ ⟩
      H.comp (φ.f (G.inv g₁)) (φ.f g₂)
        =⟨ φ.pres-inv g₁ |in-ctx (λ w → H.comp w (φ.f g₂)) ⟩
      H.comp (H.inv (φ.f g₁)) (φ.f g₂)
        =⟨ p |in-ctx (λ w → H.comp (H.inv w) (φ.f g₂)) ⟩
      H.comp (H.inv (φ.f g₂)) (φ.f g₂)
        =⟨ H.invl (φ.f g₂) ⟩
      H.ident ∎)

{- constant homomorphism -}
module _ where
  cst-hom : ∀ {i j} {G : Group i} {H : Group j} → (G →ᴳ H)
  cst-hom {H = H} = group-hom (cst ident) (λ _ _ → ! (unitl _))
    where open Group H

  pre∘-cst-hom : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
    (φ : H →ᴳ K)
    → φ ∘ᴳ cst-hom {G = G} {H = H} == cst-hom
  pre∘-cst-hom φ = hom= _ _ (λ= (λ g → GroupHom.pres-ident φ))

{- if an injective homomorphism is merely surjective, then it is
 - fully surjective -}
module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

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

  module _ (inj : (g₁ g₂ : G.El) → φ.f g₁ == φ.f g₂ → g₁ == g₂)
    (msurj : (h : H.El) → Trunc -1 (Σ G.El (λ g → φ.f g == h))) where

{- a surjective and injective homomorphism is an isomorphism -}
module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

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

  module _ (inj : (g₁ g₂ : G.El) → φ.f g₁ == φ.f g₂ → g₁ == g₂)
    (surj : (h : H.El) → Trunc -1 (Σ G.El (λ g → φ.f g == h))) where

    private
      image-prop : (h : H.El) → is-prop (Σ G.El (λ g → φ.f g == h))
      image-prop h = all-paths-is-prop $ λ {(g₁ , p₁) (g₂ , p₂) →
        pair= (inj g₁ g₂ (p₁ ∙ ! p₂)) (prop-has-all-paths-↓ (H.El-level _ _))}

    surj-inj-is-equiv : is-equiv φ.f
    surj-inj-is-equiv = contr-map-is-equiv
      (λ h → let (g₁ , p₁) = Trunc-rec (image-prop h) (idf _) (surj h) in
        ((g₁ , p₁) , (λ {(g₂ , p₂) →
          pair= (inj g₁ g₂ (p₁ ∙ ! p₂))
                (prop-has-all-paths-↓ (H.El-level _ _))})))

module _ {i} {G H : Group i} (φ : G →ᴳ H) where

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

  module _ (inj : (g₁ g₂ : G.El) → φ.f g₁ == φ.f g₂ → g₁ == g₂)
    (surj : (h : H.El) → Trunc -1 (Σ G.El (λ g → φ.f g == h))) where

    surj-inj-iso : G ≃ᴳ H
    surj-inj-iso = (φ , surj-inj-is-equiv φ inj surj)

    surj-inj-path : G == H
    surj-inj-path = group-ua surj-inj-iso

{- negation is a homomorphism in an abelian gruop -}
inv-hom : ∀ {i} (G : Group i) (G-abelian : is-abelian G) → GroupHom G G
inv-hom G G-abelian = record {
  f = Group.inv G;
  pres-comp = λ g₁ g₂ →
    group-inv-comp G g₁ g₂ ∙ G-abelian (Group.inv G g₂) (Group.inv G g₁)}

inv-hom-natural : ∀ {i j} {G : Group i} {H : Group j}
  (G-abelian : is-abelian G) (H-abelian : is-abelian H) (φ : G →ᴳ H)
  → φ ∘ᴳ inv-hom G G-abelian == inv-hom H H-abelian ∘ᴳ φ
inv-hom-natural _ _ φ = hom= _ _ $ λ= $ GroupHom.pres-inv φ

{- two homomorphisms into an abelian group can be composed with
 - the group operation -}
module _ {i} {G H : Group i} (H-abelian : is-abelian H)
  (φ ψ : G →ᴳ H) where

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

  comp-hom : G →ᴳ H
  comp-hom = record {
    f = λ g → H.comp (φ.f g) (ψ.f g);
    pres-comp = λ g₁ g₂ →
      H.comp (φ.f (G.comp g₁ g₂)) (ψ.f (G.comp g₁ g₂))
        =⟨ ap2 H.comp (φ.pres-comp g₁ g₂) (ψ.pres-comp g₁ g₂) ⟩
      H.comp (H.comp (φ.f g₁) (φ.f g₂)) (H.comp (ψ.f g₁) (ψ.f g₂))
        =⟨ lemma (φ.f g₁) (φ.f g₂) (ψ.f g₁) (ψ.f g₂) ⟩
      H.comp (H.comp (φ.f g₁) (ψ.f g₁)) (H.comp (φ.f g₂) (ψ.f g₂)) ∎}

    where
    lemma : (h₁ h₂ h₃ h₄ : H.El) →
      H.comp (H.comp h₁ h₂) (H.comp h₃ h₄)
      == H.comp (H.comp h₁ h₃) (H.comp h₂ h₄)
    lemma h₁ h₂ h₃ h₄ =
      (h₁ □ h₂) □ (h₃ □ h₄)
         =⟨ H.assoc h₁ h₂ (h₃ □ h₄) ⟩
       h₁ □ (h₂ □ (h₃ □ h₄))
         =⟨ H-abelian h₃ h₄ |in-ctx (λ w → h₁ □ (h₂ □ w)) ⟩
       h₁ □ (h₂ □ (h₄ □ h₃))
         =⟨ ! (H.assoc h₂ h₄ h₃) |in-ctx (λ w → h₁ □ w) ⟩
       h₁ □ ((h₂ □ h₄) □ h₃)
         =⟨ H-abelian (h₂ □ h₄) h₃ |in-ctx (λ w → h₁ □ w) ⟩
       h₁ □ (h₃ □ (h₂ □ h₄))
         =⟨ ! (H.assoc h₁ h₃ (h₂ □ h₄)) ⟩
       (h₁ □ h₃) □ (h₂ □ h₄) ∎
       where
        infix 80 _□_
        _□_ = H.comp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --no-unicode #-}

data Two : Set where
  tt ff : Two

data Foo : Set where
  foo : Foo -> Foo -> Foo

test1 : Foo → Two
test1 x₀ = {!!}

test : Foo -> Foo → Two
test x1 = {!!}


text:
module UniDB.Morph.ShiftsPrime where

open import UniDB.Spec
open import UniDB.Basic
open import UniDB.Subst
open import Function
open import Data.Product

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

mutual
  data Shifts* : MOR where
    refl : {γ : Dom} → Shifts* γ γ
    incl : {γ₁ γ₂ : Dom} (ξ : Shifts+ γ₁ γ₂) → Shifts* γ₁ γ₂

  data Shifts+ : MOR where
    step : {γ₁ γ₂ : Dom} (ξ : Shifts* γ₁ γ₂) → Shifts+ γ₁ (suc γ₂)
    skip : {γ₁ γ₂ : Dom} (ξ : Shifts+ γ₁ γ₂) → Shifts+ (suc γ₁) (suc γ₂)

mutual
  shiftIx* : {γ₁ γ₂ : Dom} (ξ : Shifts* γ₁ γ₂) (i : Ix γ₁) → Ix γ₂
  shiftIx* refl     i = i
  shiftIx* (incl ξ) i = shiftIx+ ξ i

  shiftIx+ : {γ₁ γ₂ : Dom} (ξ : Shifts+ γ₁ γ₂) (i : Ix γ₁) → Ix γ₂
  shiftIx+ (skip ξ) zero    = zero
  shiftIx+ (skip ξ) (suc i) = suc (shiftIx+ ξ i)
  shiftIx+ (step ξ) i       = suc (shiftIx* ξ i)

mutual
  _⊙**_ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) → Shifts* γ₁ γ₃
  ξ₁ ⊙** refl    = ξ₁
  ξ₁ ⊙** incl ξ₂ = incl (ξ₁ ⊙*+ ξ₂)

  _⊙*+_ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) → Shifts+ γ₁ γ₃
  refl    ⊙*+ ξ₂ = ξ₂
  incl ξ₁ ⊙*+ ξ₂ = ξ₁ ⊙++ ξ₂

  _⊙+*_ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) → Shifts+ γ₁ γ₃
  ξ₁ ⊙+* refl    = ξ₁
  ξ₁ ⊙+* incl ξ₂ = ξ₁ ⊙++ ξ₂

  _⊙++_ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) → Shifts+ γ₁ γ₃
  ξ₁      ⊙++ step ξ₂ = step (incl (ξ₁ ⊙+* ξ₂))
  step ξ₁ ⊙++ skip ξ₂ = step (incl (ξ₁ ⊙*+ ξ₂))
  skip ξ₁ ⊙++ skip ξ₂ = skip (ξ₁ ⊙++ ξ₂)

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

instance
  iLkShifts* : {T : STX} {{vrT : Vr T}} → Lk T Shifts*
  lk {{iLkShifts*}} ξ i = vr {_} (shiftIx* ξ i)

  iLkShifts+ : {T : STX} {{vrT : Vr T}} → Lk T Shifts+
  lk {{iLkShifts+}} ξ i = vr {_} (shiftIx+ ξ i)

  iUpShifts* : Up Shifts*
  _↑₁ {{iUpShifts*}} refl     = refl
  _↑₁ {{iUpShifts*}} (incl ξ) = incl (skip ξ)
  _↑_ {{iUpShifts*}} ξ 0 = ξ
  _↑_ {{iUpShifts*}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpShifts*}} ξ = refl
  ↑-suc {{iUpShifts*}} ξ δ⁺ = refl

  iUpShifts+ : Up Shifts+
  _↑₁ {{iUpShifts+}} ξ = skip ξ
  _↑_ {{iUpShifts+}} ξ 0 = ξ
  _↑_ {{iUpShifts+}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpShifts+}} ξ = refl
  ↑-suc {{iUpShifts+}} ξ δ⁺ = refl

  iIdmShifts* : Idm Shifts*
  idm {{iIdmShifts*}} γ = refl {γ}

  iWkmShifts* : Wkm Shifts*
  wkm {{iWkmShifts*}} zero    = idm {Shifts*} _
  wkm {{iWkmShifts*}} (suc δ) = incl (step (wkm {Shifts*} δ))

  iCompShifts* : Comp Shifts*
  _⊙_ {{iCompShifts*}} = _⊙**_

  iCompShifts+ : Comp Shifts+
  _⊙_ {{iCompShifts+}} = _⊙++_

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

suc-inj : {γ : Dom} {i j : Ix γ} → _≡_ {A = Ix (suc γ)} (suc i) (suc j) → i ≡ j
suc-inj refl = refl

shift₁≠id : {γ : Dom} (ξ : Shifts+ γ γ) →
  Σ[ i ∈ Ix γ ] shiftIx+ ξ i ≢ i
shift₁≠id (skip ξ) with shift₁≠id ξ
shift₁≠id (skip ξ) | w , ¬p = suc w , ¬p ∘ suc-inj
shift₁≠id (step ξ) = zero , λ ()

mutual
  extensionality-shifts* : {γ₁ γ₂ : Dom} (ξ₁ ξ₂ : Shifts* γ₁ γ₂)
    (hyp : (i : Ix γ₁) → lk {Ix} ξ₁ i ≡ lk {Ix} ξ₂ i) →
    ξ₁ ≡ ξ₂
  extensionality-shifts* refl      refl      hyp = refl
  extensionality-shifts* refl      (incl ξ₂) hyp with shift₁≠id ξ₂
  ... | w , ¬p = case ¬p (sym (hyp w)) of λ()
  extensionality-shifts* (incl ξ₁) refl      hyp with shift₁≠id ξ₁
  ... | w , ¬p = case ¬p (hyp w) of λ()
  extensionality-shifts* (incl ξ₁) (incl ξ₂) hyp = cong incl (extensionality-shifts+ ξ₁ ξ₂ hyp)

  extensionality-shifts+ : {γ₁ γ₂ : Dom} (ξ₁ ξ₂ : Shifts+ γ₁ γ₂)
    (hyp : (i : Ix γ₁) → lk {Ix} ξ₁ i ≡ lk {Ix} ξ₂ i) →
    ξ₁ ≡ ξ₂
  extensionality-shifts+ (skip ξ₁) (skip ξ₂) hyp = cong skip (extensionality-shifts+ ξ₁ ξ₂ (suc-inj ∘ hyp ∘ suc))
  extensionality-shifts+ (skip ξ₁) (step ξ₂) hyp = case hyp zero of λ()
  extensionality-shifts+ (step ξ₁) (skip ξ₂) hyp = case hyp zero of λ()
  extensionality-shifts+ (step ξ₁) (step ξ₂) hyp = cong step (extensionality-shifts* ξ₁ ξ₂ (suc-inj ∘ hyp))

mutual
  shiftIx-⊙** : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) →
    (i : Ix γ₁) → shiftIx* (ξ₁ ⊙** ξ₂) i ≡ shiftIx* ξ₂ (shiftIx* ξ₁ i)
  shiftIx-⊙** ξ₁ refl      i = refl
  shiftIx-⊙** ξ₁ (incl ξ₂) i = shiftIx-⊙*+ ξ₁ ξ₂ i

  shiftIx-⊙*+ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) →
    (i : Ix γ₁) → shiftIx+ (ξ₁ ⊙*+ ξ₂) i ≡ shiftIx+ ξ₂ (shiftIx* ξ₁ i)
  shiftIx-⊙*+ refl      ξ₂ i = refl
  shiftIx-⊙*+ (incl ξ₁) ξ₂ i = shiftIx-⊙++ ξ₁ ξ₂ i

  shiftIx-⊙+* : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) →
    (i : Ix γ₁) → shiftIx+ (ξ₁ ⊙+* ξ₂) i ≡ shiftIx* ξ₂ (shiftIx+ ξ₁ i)
  shiftIx-⊙+* ξ₁ refl      i = refl
  shiftIx-⊙+* ξ₁ (incl ξ₂) i = shiftIx-⊙++ ξ₁ ξ₂ i

  shiftIx-⊙++ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) →
    (i : Ix γ₁) → shiftIx+ (ξ₁ ⊙++ ξ₂) i ≡ shiftIx+ ξ₂ (shiftIx+ ξ₁ i)
  shiftIx-⊙++ ξ₁        (step ξ₂) i       = cong suc (shiftIx-⊙+* ξ₁ ξ₂ i)
  shiftIx-⊙++ (step ξ₁) (skip ξ₂) i       = cong suc (shiftIx-⊙*+ ξ₁ ξ₂ i)
  shiftIx-⊙++ (skip ξ₁) (skip ξ₂) zero    = refl
  shiftIx-⊙++ (skip ξ₁) (skip ξ₂) (suc i) = cong suc (shiftIx-⊙++ ξ₁ ξ₂ i)

⊙**-↑₁ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) →
  (ξ₁ ⊙** ξ₂) ↑₁ ≡ (ξ₁ ↑₁) ⊙** (ξ₂ ↑₁)
⊙**-↑₁ ξ₁        refl      = refl
⊙**-↑₁ refl      (incl ξ₂) = refl
⊙**-↑₁ (incl ξ₁) (incl ξ₂) = refl

⊙++-↑₁ : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) →
  (ξ₁ ⊙++ ξ₂) ↑₁ ≡ (ξ₁ ↑₁) ⊙++ (ξ₂ ↑₁)
⊙++-↑₁ ξ₁        (step ξ₂) = refl
⊙++-↑₁ (step ξ₁) (skip ξ₂) = refl
⊙++-↑₁ (skip ξ₁) (skip ξ₂) = refl

mutual
  ⊙***-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) (ξ₃ : Shifts* γ₃ γ₄) →
    (ξ₁ ⊙** (ξ₂ ⊙** ξ₃)) ≡ ((ξ₁ ⊙** ξ₂) ⊙** ξ₃)
  ⊙***-assoc ξ₁ ξ₂ refl      = refl
  ⊙***-assoc ξ₁ ξ₂ (incl ξ₃) = cong incl (⊙**+-assoc ξ₁ ξ₂ ξ₃)

  ⊙**+-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) (ξ₃ : Shifts+ γ₃ γ₄) →
    (ξ₁ ⊙*+ (ξ₂ ⊙*+ ξ₃)) ≡ ((ξ₁ ⊙** ξ₂) ⊙*+ ξ₃)
  ⊙**+-assoc ξ₁ refl      ξ₃ = refl
  ⊙**+-assoc ξ₁ (incl ξ₂) ξ₃ = ⊙*++-assoc ξ₁ ξ₂ ξ₃

  ⊙*++-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts* γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) (ξ₃ : Shifts+ γ₃ γ₄) →
    (ξ₁ ⊙*+ (ξ₂ ⊙++ ξ₃)) ≡ ((ξ₁ ⊙*+ ξ₂) ⊙++ ξ₃)
  ⊙*++-assoc refl      ξ₂ ξ₃ = refl
  ⊙*++-assoc (incl ξ₁) ξ₂ ξ₃ = ⊙+++-assoc ξ₁ ξ₂ ξ₃

  ⊙++*-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) (ξ₃ : Shifts* γ₃ γ₄) →
    (ξ₁ ⊙++ (ξ₂ ⊙+* ξ₃)) ≡ ((ξ₁ ⊙++ ξ₂) ⊙+* ξ₃)
  ⊙++*-assoc ξ₁ ξ₂ refl      = refl
  ⊙++*-assoc ξ₁ ξ₂ (incl ξ₃) = ⊙+++-assoc ξ₁ ξ₂ ξ₃

  ⊙+*+-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts* γ₂ γ₃) (ξ₃ : Shifts+ γ₃ γ₄) →
    (ξ₁ ⊙++ (ξ₂ ⊙*+ ξ₃)) ≡ ((ξ₁ ⊙+* ξ₂) ⊙++ ξ₃)
  ⊙+*+-assoc ξ₁ refl      ξ₃ = refl
  ⊙+*+-assoc ξ₁ (incl ξ₂) ξ₃ = ⊙+++-assoc ξ₁ ξ₂ ξ₃

  ⊙+++-assoc : {γ₁ γ₂ γ₃ γ₄ : Dom}
    (ξ₁ : Shifts+ γ₁ γ₂) (ξ₂ : Shifts+ γ₂ γ₃) (ξ₃ : Shifts+ γ₃ γ₄) →
    (ξ₁ ⊙++ (ξ₂ ⊙++ ξ₃)) ≡ ((ξ₁ ⊙++ ξ₂) ⊙++ ξ₃)
  ⊙+++-assoc ξ₁        ξ₂        (step ξ₃) = cong (step ∘ incl) (⊙++*-assoc ξ₁ ξ₂ ξ₃)
  ⊙+++-assoc ξ₁        (step ξ₂) (skip ξ₃) = cong (step ∘ incl) (⊙+*+-assoc ξ₁ ξ₂ ξ₃)
  ⊙+++-assoc (step ξ₁) (skip ξ₂) (skip ξ₃) = cong (step ∘ incl) (⊙*++-assoc ξ₁ ξ₂ ξ₃)
  ⊙+++-assoc (skip ξ₁) (skip ξ₂) (skip ξ₃) = cong skip (⊙+++-assoc ξ₁ ξ₂ ξ₃)

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

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkUpShifts* : {{wkT : Wk T}} {{wkVrT : WkVr T}} → LkUp T Shifts*
    lk-↑₁-zero {{iLkUpShifts*}} refl       = refl
    lk-↑₁-zero {{iLkUpShifts*}} (incl ξ)   = refl
    lk-↑₁-suc  {{iLkUpShifts*}} refl i     = sym (wk₁-vr {T} i)
    lk-↑₁-suc  {{iLkUpShifts*}} (incl ξ) i = sym (wk₁-vr {T} (shiftIx+ ξ i))

    iLkRenShifts* : LkRen T Shifts*
    lk-ren {{iLkRenShifts*}} ξ i = refl

    iLkIdmShifts* : LkIdm T Shifts*
    lk-idm {{iLkIdmShifts*}} i = refl

    iLkWkmShifts* : LkWkm T Shifts*
    lk-wkm {{iLkWkmShifts*}} δ i = cong vr (lem δ i)
      where
        lem : {γ : Dom} (δ : Dom) (i : Ix γ) →
          shiftIx* (wkm {Shifts*} δ) i ≡ wk {Ix} δ i
        lem zero i = refl
        lem (suc δ) i = cong suc (lem δ i)

    iLkCompApShifts* : {{apTT : Ap T T}} {{apVrT : ApVr T}} → LkCompAp T Shifts*
    lk-⊙-ap {{iLkCompApShifts*}} {Ξ} ξ₁ ξ₂ i = begin
      vr (lk {Ix} (ξ₁ ⊙ ξ₂) i)     ≡⟨ cong vr (shiftIx-⊙** ξ₁ ξ₂ i) ⟩
      lk {T} ξ₂ (lk {Ix} ξ₁ i)      ≡⟨ sym (ap-vr {T} ξ₂ (lk ξ₁ i)) ⟩
      ap {T} ξ₂ (vr (lk {Ix} ξ₁ i)) ∎ -- sym {!ap-vr {T} !}

instance
  iUpIdmShifts* : UpIdm Shifts*
  idm-↑₁ {{iUpIdmShifts*}} = refl

  iCompIdmShifts* : CompIdm Shifts*
  ⊙-idm {{iCompIdmShifts*}} ξ        = refl
  idm-⊙ {{iCompIdmShifts*}} refl     = refl
  idm-⊙ {{iCompIdmShifts*}} (incl ξ) = refl

  iUpCompShifts* : UpComp Shifts*
  ⊙-↑₁ {{iUpCompShifts*}} ξ₁ ξ₂ = ⊙**-↑₁ ξ₁ ξ₂
    -- extensionality-shifts* ((ξ₁ ⊙ ξ₂) ↑₁) (ξ₁ ↑₁ ⊙ ξ₂ ↑₁)
    --   (lk≃ {Ix} {Shifts*} {ξ = (ξ₁ ⊙ ξ₂) ↑₁} {ξ₁ ↑₁ ⊙ ξ₂ ↑₁}
    --   (⊙-↑₁-pointwise {Ix} {{apWkTT =  iApWk Ix Ix}} {Shifts*} ξ₁ ξ₂))

  iCompAssoc* : CompAssoc Shifts*
  ⊙-assoc {{iCompAssoc*}} = ⊙***-assoc

  iUpCompShifts+ : UpComp Shifts+
  ⊙-↑₁ {{iUpCompShifts+}} = ⊙++-↑₁

  iCompAssoc+ : CompAssoc Shifts+
  ⊙-assoc {{iCompAssoc+}} = ⊙+++-assoc

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

{-
  iWkmHomShifts* : WkmHom Shifts*
  wkm-zero {{iWkmHomShifts*}}   = {!!}
  wkm-suc  {{iWkmHomShifts*}} δ = {!!}
-}


text:
------------------------------------------------------------------------
-- Terminating parser combinator interface
------------------------------------------------------------------------

module RecursiveDescent.Coinductive where

open import RecursiveDescent.Index
import RecursiveDescent.Coinductive.Internal as P
open P public using (Parser)

open import Data.List
open import Data.Bool
open import Data.Maybe
open import Data.Product.Record hiding (map)
import Data.Product as Prod
open import Data.Function
import Data.BoundedVec.Inefficient as BVec

------------------------------------------------------------------------
-- Run function for the parsers

parse : forall {tok i r} ->
        Parser tok i r -> List tok -> List (Prod._×_ r (List tok))
parse p s = map (Prod.map id BVec.toList)
                (P.parse _ p (BVec.fromList s))

-- A variant which only returns parses which leave no remaining input.

parse-complete : forall {tok i r} ->
                 Parser tok i r -> List tok -> List r
parse-complete p s =
  map Prod.proj₁ (filter (null ∘ Prod.proj₂) (parse p s))

------------------------------------------------------------------------
-- Exported combinators

infixl 40 _∣_
infixl 10 _>>=_ _!>>=_

symbol : forall {tok} -> Parser tok 0I tok
symbol = P.symbol

return : forall {tok r} -> r -> Parser tok 1I r
return = P.ret

fail : forall {tok r} -> Parser tok 0I r
fail = P.fail

_>>=_ : forall {tok e₁ c₁ i₂ r₁ r₂} -> let i₁ = (e₁ , c₁) in
        Parser tok i₁ r₁ ->
        (r₁ -> Parser tok i₂ r₂) ->
        Parser tok (i₁ ·I i₂) r₂
_>>=_ {e₁ = true } = P.bind₀
_>>=_ {e₁ = false} = P.bind₁

-- If the first parser is guaranteed to consume something, then the
-- second parser's index can depend on the result of the first parser.

_!>>=_ : forall {tok c₁ r₁ r₂} {i₂ : r₁ -> Index} ->
         let i₁ = (false , c₁) in
         Parser tok i₁ r₁ ->
         ((x : r₁) -> Parser tok (i₂ x) r₂) ->
         Parser tok (i₁ ·I 1I) r₂
_!>>=_ = P.bind₁

_∣_ : forall {tok e₁ c₁ i₂ r} -> let i₁ = (e₁ , c₁) in
      Parser tok i₁ r ->
      Parser tok i₂ r ->
      Parser tok (i₁ ∣I i₂) r
_∣_ {e₁ = true } = P.alt₀
_∣_ {e₁ = false} = P.alt₁ _

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
open import Type

module Formalization.ClassicalPropositionalLogic.TruthTable {ℓₚ}{P : Type{ℓₚ}} where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Operators using () renaming (module Logic to Bool)
import      Data.Boolean.Proofs as Bool
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
open import Data.Either as Either using (_‖_ ; Left ; Right)
open import Data.Tuple as Tuple using ()
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Formalization.ClassicalPropositionalLogic.Semantics
open import Functional
import      Logic.Propositional as Logic
import      Logic.Propositional.Theorems as Logic
open import Logic
open import Relator.Equals.Proofs.Equiv
import      Sets.PredicateSet
open        Sets.PredicateSet.BoundedQuantifiers

private variable ℓ : Lvl.Level

-- `_⊧_`, but decidable.
eval : Model(P) → Formula(P) → Bool
eval env (• p)   = env(p)
eval env (⊤)     = 𝑇
eval env (⊥)     = 𝐹
eval env (¬ φ)   = Bool.¬(eval env (φ))
eval env (φ ∧ ψ) = eval env (φ) Bool.∧ eval env (ψ)
eval env (φ ∨ ψ) = eval env (φ) Bool.∨ eval env (ψ)
eval env (φ ⟶ ψ) = eval env (φ) Bool.⟶ eval env (ψ)
eval env (φ ⟷ ψ) = eval env (φ) Bool.⟷ eval env (ψ)

_⊢_ : Formulas(P){ℓ} → Formula(P) → Stmt
Γ ⊢ φ = ∀{𝔐} → (∀ₛ(Γ) (IsTrue ∘ eval 𝔐)) → IsTrue(eval 𝔐 φ)

private variable Γ Γ₁ Γ₂ : Formulas(P){ℓ}
private variable φ ψ : Formula(P)
private variable 𝔐 : Model(P)

models-to-eval : (𝔐 ⊧ φ) → IsTrue(eval 𝔐 φ)
eval-to-models : IsTrue(eval 𝔐 φ) → (𝔐 ⊧ φ)

eval-to-models {φ = • x}   p = p
eval-to-models {φ = ⊤}     p = <>
eval-to-models {φ = ⊥}     p = p
eval-to-models {φ = ¬ φ}   p = Logic.[↔]-to-[→] IsTrue.preserves-[!][¬] p ∘ models-to-eval {φ = φ}
eval-to-models {φ = φ ∧ ψ} p = Tuple.map (eval-to-models {φ = φ}) (eval-to-models {φ = ψ}) (Logic.[↔]-to-[→] IsTrue.preserves-[&&][∧] p)
eval-to-models {φ = φ ∨ ψ} p = Either.map (eval-to-models {φ = φ}) (eval-to-models {φ = ψ}) (Logic.[↔]-to-[→] IsTrue.preserves-[||][∨] p)
eval-to-models {φ = φ ⟶ ψ} p = Either.map (Logic.contrapositiveᵣ (models-to-eval {φ = φ}) ∘ Logic.[↔]-to-[→] IsTrue.preserves-[!][¬]) (eval-to-models {φ = ψ}) (Logic.[↔]-to-[→] IsTrue.preserves-[||][∨] ([≡]-substitutionᵣ Bool.[→?]-disjunctive-form {f = IsTrue} p))
eval-to-models {φ = φ ⟷ ψ} p = Either.map (Tuple.map (eval-to-models {φ = φ}) (eval-to-models {φ = ψ}) ∘ (Logic.[↔]-to-[→] IsTrue.preserves-[&&][∧])) (Tuple.map (Logic.contrapositiveᵣ (models-to-eval {φ = φ}) ∘ Logic.[↔]-to-[→] IsTrue.preserves-[!][¬]) (Logic.contrapositiveᵣ (models-to-eval {φ = ψ}) ∘ Logic.[↔]-to-[→] IsTrue.preserves-[!][¬]) ∘ Logic.[↔]-to-[→] IsTrue.preserves-[&&][∧]) (Logic.[↔]-to-[→] IsTrue.preserves-[||][∨] ([≡]-substitutionᵣ Bool.[==]-disjunctive-form {f = IsTrue} p))

models-to-eval {φ = • x}   p = p
models-to-eval {φ = ⊤}     p = <>
models-to-eval {φ = ⊥}     p = p
models-to-eval {φ = ¬ φ}   p = Logic.[↔]-to-[←] IsTrue.preserves-[!][¬] (p ∘ eval-to-models {φ = φ})
models-to-eval {φ = φ ∧ ψ} p = Logic.[↔]-to-[←] IsTrue.preserves-[&&][∧] (Tuple.map (models-to-eval {φ = φ}) (models-to-eval {φ = ψ}) p)
models-to-eval {φ = φ ∨ ψ} p = Logic.[↔]-to-[←] IsTrue.preserves-[||][∨] (Either.map (models-to-eval {φ = φ}) (models-to-eval {φ = ψ}) p)
models-to-eval {φ = φ ⟶ ψ} p = [≡]-substitutionₗ Bool.[→?]-disjunctive-form {f = IsTrue} (Logic.[↔]-to-[←] IsTrue.preserves-[||][∨] (Either.map (Logic.[↔]-to-[←] IsTrue.preserves-[!][¬] ∘ Logic.contrapositiveᵣ (eval-to-models {φ = φ})) (models-to-eval {φ = ψ}) p))
models-to-eval {φ = φ ⟷ ψ} p = [≡]-substitutionₗ Bool.[==]-disjunctive-form {f = IsTrue} (Logic.[↔]-to-[←] IsTrue.preserves-[||][∨] (Either.map (Logic.[↔]-to-[←] IsTrue.preserves-[&&][∧] ∘ Tuple.map (models-to-eval {φ = φ}) (models-to-eval {φ = ψ})) (Logic.[↔]-to-[←] IsTrue.preserves-[&&][∧] ∘ Tuple.map (Logic.[↔]-to-[←] IsTrue.preserves-[!][¬] ∘ Logic.contrapositiveᵣ (eval-to-models {φ = φ})) (Logic.[↔]-to-[←] IsTrue.preserves-[!][¬] ∘ Logic.contrapositiveᵣ (eval-to-models {φ = ψ}))) p))

completeness : (Γ ⊨ φ) → (Γ ⊢ φ)
completeness {φ = φ} Γφ {𝔐} a = models-to-eval {φ = φ} (Γφ (\{γ} → eval-to-models {φ = γ} ∘ a))

soundness : (Γ ⊢ φ) → (Γ ⊨ φ)
soundness {φ = φ} Γφ {𝔐} a = eval-to-models {φ = φ} (Γφ (\{γ} → models-to-eval {φ = γ} ∘ a))