text:
open import Signature

-- | In this module, we construct the free monad and the free completely
-- iterative monad over a signature Σ (see Aczel, Adamek, Milius and Velebil).
-- The first assigns to a set V of variables the set TV of finite terms over Σ
-- (that is, finite trees labelled with symbols in f ∈ ∥Σ∥ and ar(f) branching).
-- The second extends this to also allow for infinite trees, the set of those
-- is then denoted by T∞(V).
-- Categorically, T(V) is the initial (Σ + V)-algebra, whereas T∞(V) is the
-- final (Σ + V)-coalgebra.
module Terms (Σ : Sig) where

open import Function
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Nat as Nat
open import Data.Sum as Sum
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Binary hiding (_⇒_)
open import Relation.Unary hiding (_⇒_)
import Streams as Str
open import Streams hiding (corec)

-- | Natural transformations
Nat : (Set → Set) → (Set → Set) → Set₁
Nat F G = ∀{X} → F X → G X

Id : Set → Set
Id = id

least : {X : Set} (_⊑_ : Rel X _) (P : X → Set) → X → Set
least _⊑_ P x = (P x) × (∀ {y} → P y → x ⊑ y)

least-unique : {X : Set} {_⊑_ : Rel X _} → (IsTotalOrder _≡_ _⊑_) →
               {P : X → Set} → (x y : X) → least _⊑_ P x → least _⊑_ P y → x ≡ y
least-unique isTO x y (p , l₁) (q , l₂) with IsTotalOrder.total isTO x y
least-unique isTO x y (p , l₁) (q , l₂) | inj₁ x⊑y =
  IsTotalOrder.antisym isTO x⊑y (l₂ p)
least-unique isTO x y (p , l₁) (q , l₂) | inj₂ y⊑x =
  IsTotalOrder.antisym isTO (l₁ q) y⊑x

infixr 1 _⇒_
_⇒_ = Nat

data T (V : Set) : Set where
  sup : ⟪ Σ ⟫ (T V) ⊎ V → T V

rec : ∀{V X} → (f : ⟪ Σ ⟫ X ⊎ V → X) → T V → X
rec f (sup (inj₁ (s , α))) = f (inj₁ (s , λ i → rec f (α i)))
rec f (sup (inj₂ y))       = f (inj₂ y)

-- | Functor T, on morphisms
T₁ : ∀ {V W} → (V → W) → T V → T W
T₁ f = rec (sup ∘ Sum.map id f)

η : Id ⇒ T
η = sup ∘ inj₂

μ : T ∘ T ⇒ T
μ {V} = rec f
  where
    f : ⟪ Σ ⟫ (T V) ⊎ T V → T V
    f = [ sup ∘ inj₁ , id ]

-- | T is free over Σ with inclusion
ι : ⟪ Σ ⟫ ⇒ T
ι = sup ∘ inj₁ ∘ ⟪ Σ ⟫₁ η

-- | Kleisli morphsims for T∞ V
Subst : Set → Set → Set
Subst V W = V → T W

infixr 9 _•_

-- | Kleisli composition
_•_ : ∀ {U V W} → Subst V W → Subst U V → Subst U W
τ • σ = μ ∘ T₁ τ ∘ σ

-- | Application of substitutions to infinite terms
app : ∀ {V W} → Subst V W → T V → T W
app σ = μ ∘ T₁ σ

infixl 1 _≡ₛ_

_≡ₛ_ : ∀{V W} → Rel (Subst V W) _
σ ≡ₛ τ = ∀ {v} → σ v ≡ τ v

-- | Order on subsitutions
_⊑_ : ∀{V W} → Rel (Subst V W) _
σ₁ ⊑ σ₂ = ∃ λ σ → σ • σ₁ ≡ₛ σ₂

matches : ∀{V W} → T V → T W → Subst V W → Set
matches t s σ = app σ t ≡ s

-- | Most general matcher
mgm : ∀{V W} → T V → T W → Subst V W → Set
mgm t s = least _⊑_ (matches t s)

unifies : ∀{V W} → T V → T V → Subst V W → Set
unifies t s σ = app σ t ≡ app σ s

-- | Most general unifier
mgu : ∀{V W} → T V → T V → Subst V W → Set
mgu t s = least _⊑_ (unifies t s)

-- | Free variables
fv : ∀{V} → T V → Pred V _
fv (sup (inj₁ (s , α))) v = ⨿ (Sig.ar Σ s) λ i → (fv (α i) v)
fv (sup (inj₂ v₁))      v = v₁ ≡ v

isVar : ∀{V} → Pred (T V) _
isVar (sup (inj₁ x)) = ⊥
isVar (sup (inj₂ y)) = ⊤

record T∞ (V : Set) : Set where
  coinductive
  field out : ⟪ Σ ⟫ (T∞ V) ⊎ V
open T∞ public

sum-lift : {A B : Set} (R₁ : A → A → Set) (R₂ : B → B → Set) (x y : A ⊎ B) → Set
sum-lift R₁ R₂ (inj₁ x) (inj₁ y) = R₁ x y
sum-lift R₁ R₂ (inj₁ x) (inj₂ y) = ⊥
sum-lift R₁ R₂ (inj₂ x) (inj₁ y) = ⊥
sum-lift R₁ R₂ (inj₂ x) (inj₂ y) = R₂ x y

~-data : ∀{V} (R : T∞ V → T∞ V → Set) (u w : ⟪ Σ ⟫ (T∞ V) ⊎ V) → Set
~-data R = sum-lift (sig-lift R) _≡_

record _~_ {V : Set} (t s : T∞ V) : Set where
  coinductive
  field out~ : ~-data _~_ (out t) (out s)
open _~_ public

corec : ∀{V X} → (f : X → ⟪ Σ ⟫ X ⊎ V) → X → T∞ V
out (corec f x) with f x
... | inj₁ (s , α) = inj₁ (s , (λ i → corec f (α i)))
... | inj₂ v       = inj₂ v

prim-corec : ∀{V X} → (f : X → ⟪ Σ ⟫ X ⊎ V ⊎ T∞ V) → X → T∞ V
out (prim-corec {V} {X} f x) with f x
... | inj₁ (s , α)  = inj₁ (s , (λ i → prim-corec f (α i)))
... | inj₂ (inj₁ v) = inj₂ v
... | inj₂ (inj₂ t) = out t

sup∞ : ∀{V} → ⟪ Σ ⟫ (T∞ V) ⊎ V → T∞ V
out (sup∞ (inj₁ u)) = inj₁ u
out (sup∞ (inj₂ v)) = inj₂ v

-- | Functor T∞, on morphisms
T∞₁ : ∀ {V W} → (V → W) → T∞ V → T∞ W
T∞₁ f = corec (Sum.map id f ∘ out)

η∞ : Id ⇒ T∞
η∞ = sup∞ ∘ inj₂

μ∞ : T∞ ∘ T∞ ⇒ T∞
μ∞ {V} = corec f
  where
    g : T∞ V → ⟪ Σ ⟫ (T∞ (T∞ V)) ⊎ V
    g = Sum.map (⟪ Σ ⟫₁ η∞) id ∘ out

    f : T∞ (T∞ V) → ⟪ Σ ⟫ (T∞ (T∞ V)) ⊎ V
    f = [ inj₁ , g ] ∘ out

ι∞ : ⟪ Σ ⟫ ⇒ T∞
ι∞ {V} = g ∘ inj₁
  where
    g : ⟪ Σ ⟫ V ⊎ T∞ V → T∞ V
    g = prim-corec [ inj₁ ∘ ⟪ Σ ⟫₁ (inj₂ ∘ η∞) , inj₂ ∘ inj₂ ]

-- | T is a submonad of T∞
χ : T ⇒ T∞
χ = rec sup∞

-- | Kleisli morphsims for T∞ V
Subst∞ : Set → Set → Set
Subst∞ V W = V → T∞ W

infixl 1 _≡ₛ∞_

_≡ₛ∞_ : ∀{V W} → Rel (Subst∞ V W) _
σ ≡ₛ∞ τ = ∀ {v} → σ v ~ τ v

infixr 9 _•∞_

-- | Kleisli composition
_•∞_ : ∀ {U V W} → Subst∞ V W → Subst∞ U V → Subst∞ U W
τ •∞ σ = μ∞ ∘ T∞₁ τ ∘ σ

-- | Application of substitutions to infinite terms
app∞ : ∀ {V W} → Subst∞ V W → T∞ V → T∞ W
app∞ σ = μ∞ ∘ T∞₁ σ

isVar∞ : ∀{V} → Pred (T∞ V) _
isVar∞ t with out t
isVar∞ t | inj₁ x = ⊥
isVar∞ t | inj₂ v = ⊤

varNowOrLater : ∀{V} → (T∞ V → Pred V _) → T∞ V → Pred V _
varNowOrLater R t v with out t
... | inj₁ (f , α) = ∃ (λ i → R (α i) v)
... | inj₂ v₁      = v ≡ v₁

record fv∞ {V : Set} (t : T∞ V) (v : V) : Set where
  coinductive
  field isFv∞ : varNowOrLater fv∞ t v

root-matches : ∀{V} → T V → ∥ Σ ∥ → Set
root-matches (sup (inj₁ (g , _))) f = g ≡ f
root-matches (sup (inj₂ y))       f = ⊥

record RootsMatch {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) : Set where
  coinductive
  field
    hd-match : root-matches (hd s) f
    tl-match : RootsMatch (tl s) f
open RootsMatch

-- | Nasty hack: assume that RootsMatch is propositional
postulate
  RootsMatch-unique : ∀{V} {s : Stream (T V)} {f : ∥ Σ ∥}
                      (p q : RootsMatch s f) → p ≡ q

split : {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) → RootsMatch s f →
        ar Σ f → Stream (T V)
hd (split s f p i) with hd s | hd-match p
hd (split s f p i) | sup (inj₁ (.f , α)) | refl = α i
hd (split s f p i) | sup (inj₂ y) | ()
tl (split s f p i) = split (tl s) f (tl-match p) i

root-matches∞ : ∀{V} → T∞ V → ∥ Σ ∥ → Set
root-matches∞ t f with out t
root-matches∞ t f | inj₁ (g , _) = f ≡ g
root-matches∞ t f | inj₂ v       = ⊥

split∞ : {V : Set} → (t : T∞ V) (f : ∥ Σ ∥) → root-matches∞ t f →
        ar Σ f → T∞ V
split∞ t f p i with out t
split∞ t f refl i | inj₁ (.f , α) = α i
split∞ t f ()   i | inj₂ y

data AnyRootMatch {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) : Stream (T V) → Set where
  match-hd : root-matches (hd s) f → AnyRootMatch s f s
  match-tl : AnyRootMatch (tl s) f (tl s) → AnyRootMatch s f (tl s)

first-root-match : ∀{V} → Stream (T V) → ∥ Σ ∥ → ℕ → Set
first-root-match s f = least _≤_ (λ k → root-matches (s at k) f)

conv-branch : {V : Set} (R : Stream (T V) → T∞ V → Set) →
               Stream (T V) → T∞ V → T V → ⟪ Σ ⟫ (T∞ V) ⊎ V → Set
conv-branch R s t (sup (inj₁ (f , α))) (inj₁ (g , β)) =
  ⨿ (f ≡ g) λ p →
  ⨿ (RootsMatch (tl s) f) λ q →
  ∀ i → R (split (tl s) f q i) (β (subst (ar Σ) p i))
conv-branch R s t (sup (inj₁ (f , α))) (inj₂ v) = ⊥
conv-branch R s t (sup (inj₂ v)) (inj₁ (f , α)) =
  ∃ λ s' → AnyRootMatch s f s' × R s' t
conv-branch R s t (sup (inj₂ v)) (inj₂ w) = v ≡ w × R (tl s) t

{-
conv-branch : {V : Set} (R : Stream (T V) → T∞ V → Set) →
              Stream (T V) → T∞ V → Set
conv-branch R s t with hd s | out t
conv-branch R s t | sup (inj₁ (f , α)) | inj₁ (g , β) =
  ⨿ (f ≡ g) λ p →
  ⨿ (RootsMatch (tl s) f) λ q →
  ∀ i → R (split (tl s) f q i) (β (subst (ar Σ) p i))
conv-branch R s t | sup (inj₁ x) | inj₂ v       = ⊥
conv-branch R s t | sup (inj₂ v) | inj₁ (f , α) =
  ∃ λ n → first-root-match s f n × R (δ n s) t
conv-branch R s t | sup (inj₂ v) | inj₂ w       = v ≡ w × R (tl s) t
-}

-- | A sequence s of finite terms converges to a possibly infinite term,
-- if for all i, sᵢ₊₁ = sᵢ[σ] for some substitution σ : V → T V and t = sᵢ[τ]
-- for some τ : V → T∞ V.
-- Note that this coincides with convergence in the prefix metric.
record _→∞_ {V : Set} (s : Stream (T V)) (t : T∞ V) : Set where
  coinductive
  field
    conv-out : conv-branch _→∞_ s t (hd s) (out t)
{-
    hd-matches   : ∃ λ σ → hd (tl s) ≡ app σ (hd s)
    hd-prefix    : ∃ λ τ → t ~ app∞ τ (χ (hd s))
    tl-converges : tl s →∞ t
-}

open _→∞_ public

{-
lem₂ : ∀{V n f} {s : Stream (T V)} →
       first-root-match s f (suc n) → first-root-match (tl s) f n
lem₂ {n = n} {f} {s} (p , q) = (p , λ m → ≤-pred (q m))
-}

{-
lem₃ : ∀{V f} (s : Stream (T V)) → ∀{t} →
      first-root-match s f zero → s →∞ t → first-root-match (tl s) f zero
lem₃ s {t} m          c with hd s      | out t  | conv-out c
lem₃ s     (refl , q) c | sup (inj₁ _) | inj₁ _ | refl , p , _
  = (hd-match p , (λ m → z≤n))
lem₃ s     (refl , q) c | sup (inj₁ _) | inj₂ v | ()
lem₃ s     (() ,   q) c | sup (inj₂ v) | u      | r
-}

lem₆ : ∀{V} (s : Stream (T V)) → ∀{t f} →
       root-matches (hd s) f → s →∞ t → RootsMatch (tl s) f
hd-match (lem₆ s {t} m    c) with hd s | out t | conv-out c
hd-match (lem₆ s     refl c) | sup (inj₁ (f , α)) | inj₁ (.f , β) | refl , m₁ , br = hd-match m₁
hd-match (lem₆ s     refl c) | sup (inj₁ (f , α)) | inj₂ y | ()
hd-match (lem₆ s     ()   c) | sup (inj₂ v) | x | y
tl-match (lem₆ s {t} m    c) with hd s | out t | conv-out c
tl-match (lem₆ s     refl c) | sup (inj₁ (f , α)) | inj₁ (.f , β) | refl , m₁ , br = tl-match m₁
tl-match (lem₆ s     refl c) | sup (inj₁ (f , α)) | inj₂ y | ()
tl-match (lem₆ s     ()   c) | sup (inj₂ v) | x | y

lem₅ : ∀{V} (s : Stream (T V)) → ∀{t f} →
       root-matches (hd s) f → s →∞ t → tl s →∞ t
conv-out (lem₅ s {t} m    c) with hd s | out t | conv-out c
conv-out (lem₅ s     refl c) | sup (inj₁ (f , α)) | inj₁ (.f , β) | refl , m , br = {!!}
conv-out (lem₅ s     refl c) | sup (inj₁ (f , α)) | inj₂ y | ()
conv-out (lem₅ s     ()   c) | sup (inj₂ v) | x | y

lem₇ : ∀{V} (s : Stream (T V)) → ∀{t f α} →
       RootsMatch (tl s) f → s →∞ t → hd s ≡ sup (inj₁ (f , α)) →
       ∃ λ β → hd (tl s) ≡ sup (inj₁ (f , β))
lem₇ = {!!}

lem₄ : ∀{V} (s : Stream (T V)) → ∀{t} →
      s →∞ t → tl s →∞ t
lem₄ {V} s {t} p = q {s} {t} (hd s) (out t) refl refl (conv-out p)
  where
    q : ∀{s t} → (u : T V) → (x : ⟪ Σ ⟫ (T∞ V) ⊎ V) →
        hd s ≡ u → out t ≡ x → conv-branch _→∞_ s t u x → tl s →∞ t
    conv-out (q {s} {t} (sup (inj₁ (f , α))) (inj₁ (.f , β)) hs≡u ot≡x (refl , m , br))
      = subst₂ (λ u₁ u₂ → conv-branch _→∞_ (tl s) t u₁ u₂)
               (sym (proj₂ (lem₇ s m
                                 (record { conv-out =
                                   subst₂ (λ u₁ u₂ → conv-branch _→∞_ s t u₁ u₂)
                                 (sym hs≡u) (sym ot≡x) (refl , (m , br)) })
                                 hs≡u)
                    )
               )
               (sym ot≡x) (refl , tl-match m , (λ i → lem₅ (split (tl s) f m i) {!!} (br i)))
      -- conv-branch _→∞_ (tl s₁) t₁ (hd (tl s₁)) (out t₁)
      -- conv-branch _→∞_ (tl .s) .t (hd (tl .s)) (out .t)
    q (sup (inj₁ x)) (inj₂ y) hs≡u ot≡x ()
    q (sup (inj₂ y)) (inj₁ (g , β)) hs≡u ot≡x (s₁ , match-hd x , c) = lem₅ s₁ x c
    q (sup (inj₂ y)) (inj₁ (g , β)) hs≡u ot≡x (._ , match-tl m , c) = c
--    conv-out (q (sup (inj₂ y)) (inj₁ (g , β)) hs≡u ot≡x (zero , m , br)) = {!!}
--    conv-out (q {s} {t} (sup (inj₂ y)) (inj₁ x) hs≡u ot≡x (suc n , m , br)) = {!!}
--      q {s} {t} (hd (δ n s)) (inj₁ x) {!!} ot≡x {!!}
--      q (hd (tl s)) (inj₁ x) ? ot≡x br
      --q (hd (δ n s)) (out t) refl refl (conv-out br)
    q (sup (inj₂ y)) (inj₂ y₁) hs≡u ot≡x br = proj₂ br

{-
lem₄ : ∀{V} (s : Stream (T V)) → ∀{t} →
      s →∞ t → tl s →∞ t
lem₄ {V} s {t} p = q {s} {t} (hd s) (out t) refl refl (conv-out p)
  where
    q : ∀{s t} → (u : T V) → (x : ⟪ Σ ⟫ (T∞ V) ⊎ V) →
        hd s ≡ u → out t ≡ x → conv-branch _→∞_ s t u x → tl s →∞ t
    q (sup (inj₁ (f , α))) (inj₁ (.f , β)) hs≡u ot≡x (refl , m , br) = {!!}
    q (sup (inj₁ x)) (inj₂ y) hs≡u ot≡x ()
    conv-out (q (sup (inj₂ y)) (inj₁ (g , β)) hs≡u ot≡x (zero , m , br)) = {!!}
    conv-out (q {s} {t} (sup (inj₂ y)) (inj₁ x) hs≡u ot≡x (suc n , m , br)) = {!!}
--      q {s} {t} (hd (δ n s)) (inj₁ x) {!!} ot≡x {!!}
--      q (hd (tl s)) (inj₁ x) ? ot≡x br
      --q (hd (δ n s)) (out t) refl refl (conv-out br)
    q (sup (inj₂ y)) (inj₂ y₁) hs≡u ot≡x br = proj₂ br
-}
{-
lem₄ {V} s {t} p | sup (inj₁ (f , α)) | inj₁ (.f , β) | refl , m , r =
  q {!!} m r
  where
     q : {s' : Stream (T V)} {t : T∞ V} {f : ∥ Σ ∥} {β : ar Σ f → T∞ V} →
         out t ≡ inj₁ (f , β) →
         (m : RootsMatch s' f) →
         ((i : ar Σ f) → split s' f m i →∞ β i) →
         s' →∞ t
     conv-out (q {s'} {t} ts m n) with hd s' | hd-match m | out t
     conv-out (q {s'} refl m n) | sup (inj₁ (f₁ , α₁)) | refl | inj₁ (.f₁ , β₁)
       = (refl , tl-match m , (λ i → lem₄ (split s' f₁ m i) (n i)))
     conv-out (q () m₁ n) | sup (inj₁ (f₁ , α₁)) | refl | inj₂ v
     conv-out (q ts m n) | sup (inj₂ y) | () | u
lem₄ s p | sup (inj₁ x) | inj₂ y | ()
lem₄ s p | sup (inj₂ y) | inj₁ x | r = {!!}
lem₄ s p | sup (inj₂ y) | inj₂ y₁ | r = proj₂ r
-}

{-
lem₁ : ∀{V} (n k : ℕ) (s : Stream (T V)) → ∀{f g t} →
      first-root-match s f n → first-root-match s g k →
      δ n s →∞ t → δ k s →∞ t → f ≡ g
lem₁ n k s {f} {g} {t} m₁ m₂ c₁ c₂
  with s at n | s at k | m₁ | m₂
       | out t | conv-out c₁ | conv-out c₂
lem₁ zero zero s _ _ c₁ c₂
  | sup (inj₁ (f , α)) | sup (inj₁ (g , β)) | (refl , p) | (refl , q)
  | inj₁ x | w | r =
    trans (proj₁ w) (sym (proj₁ r))
lem₁ zero zero s _ _ c₁ c₂
  | sup (inj₁ (f , α)) | sup (inj₁ (g , β)) | (refl , p) | (refl , q)
  | inj₂ y | () | r
lem₁ zero zero s _ _ c₁ c₂
  | sup (inj₁ (f , α)) | sup (inj₂ y) | (refl , p) | (() , q)
  | v | w | r
lem₁ zero zero s _ _ c₁ c₂
  | sup (inj₂ y) | u | (() , p) | m₂
  | v | w | r
lem₁ zero (suc k) s m₁ m₂ c₁ c₂ | u | u₁ | m₁' | m₂'
  | v | w | r = lem₁ zero k (tl s) (lem₃ s m₁ c₁) {!m₂!} (lem₄ s c₁) c₂
lem₁ (suc n) zero s _ _ c₁ c₂ | u | u₁ | m₁ | m₂ | v | w | r = {!!}
lem₁ (suc n) (suc k) s m₁ m₂ c₁ c₂
  | u | u₁ | _ | _
  | v | w | r = lem₁ n k (tl s) (lem₂ m₁) (lem₂ m₂) c₁ c₂

lem : ∀{V} (n k : ℕ) {s : Stream (T V)} → ∀{f g t} →
      first-root-match s f n → first-root-match s g k →
      δ n s →∞ t → δ k s →∞ t → n ≡ k
lem n k p q c₁ c₂ =
  least-unique NatTO n k p (subst _ (sym (lem₁ n k _ p q c₁ c₂)) q)
  where
    NatTO = TotalOrder.isTotalOrder (DecTotalOrder.totalOrder Nat.decTotalOrder)
{-
lem n k {s} {f} {g} {t} (m₁ , p) (m₂ , q) c₁ c₂ with conv-out c₁ | conv-out c₂
lem zero zero (m₁ , p) (m₂ , q) c₁ c₂ | u | v = refl
lem zero (suc k) (m₁ , p) (m₂ , q) c₁ c₂ | u | v = {!!}
lem (suc n) zero (m₁ , p) (m₂ , q) c₁ c₂ | u | v = {!!}
lem (suc n) (suc k) {s} (m₁ , p) (m₂ , q) c₁ c₂ | u | v =
  cong suc (lem n k {tl s} (m₁ , {!!}) {!!} {!!} {!!})
-}

unique-conv : ∀{V} (s : Stream (T V)) (t₁ t₂ : T∞ V) →
              s →∞ t₁ → s →∞ t₂ → t₁ ~ t₂
out~ (unique-conv s t₁ t₂ p q)
  with hd s | out t₁ | out t₂ | conv-out p | conv-out q
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₁ (._ , α)) | inj₁ (._ , β) | inj₁ (f , γ)
  | refl , q₁ , ω₁ | refl , q₂ , ω₂
  = refl
    , (λ {i} → unique-conv (split (tl s) f q₁ i)
                           (β i)
                           (γ i)
                           (ω₁ i)
                           (subst (λ u → split (tl s) f u i →∞ γ i)
                                  (RootsMatch-unique q₂ q₁)
                                  (ω₂ i)))
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₁ x) | inj₁ x₁ | inj₂ y | y₁ | ()
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₁ x) | inj₂ y | x₁ | () | z
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₂ v) | inj₁ (f , α) | inj₁ (g , β) | (n , mg , p₁) | (k , mf , q₁)
  with s at n | s at k
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₂ v) | inj₁ (f , α) | inj₁ (.g , β) | n , m₁ , p₁ | k , (refl , r₂) , q₁
  | sup (inj₁ (f' , γ)) | sup (inj₁ (g , ρ)) =
  (lem₁ n k s ({!m₁!} , {!!}) {!!} {!!} {!!}) , {!!}
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₂ v) | inj₁ (f , α) | inj₁ (g , β) | n , mg , p₁ | k , (() , _) , q₁
  | sup (inj₁ x) | sup (inj₂ y)
out~ (unique-conv s t₁ t₂ p q)
  | sup (inj₂ v) | inj₁ (f , α) | inj₁ (g , β) | n , (() , _) , p₁ | k , mf , q₁
  | sup (inj₂ y) | b
out~ (unique-conv s t₁ t₂ p q) | sup (inj₂ y) | inj₁ x | inj₂ y₁ | y₂ | z = {!!}
out~ (unique-conv s t₁ t₂ p q) | sup (inj₂ y) | inj₂ y₁ | x₁ | y₂ | z = {!!}
-}

-- | A non-trivial substitution is a substitution σ, such that, for all v ∈ V
-- we have that either σ(v) is a non-trivial term or if it is a variable w, then
-- w = v.
-- This allows us to stop substituting the first time we hit a variable.
NonTrivSubst : Set → Set
NonTrivSubst V = ⨿ (Subst V V) λ σ → (∀ v → isVar (σ v) → σ v ≡ η v)

term-seq-from-subst-seq : ∀{V} → Stream (NonTrivSubst V) → T V → Stream (T V)
hd (term-seq-from-subst-seq Δ t) = t
tl (term-seq-from-subst-seq Δ t) = term-seq-from-subst-seq (tl Δ) (app (proj₁ (hd Δ)) t)

∞term-from-subst-seq : ∀{V} → Stream (NonTrivSubst V) → T V → T∞ V
out (∞term-from-subst-seq Δ (sup (inj₁ (s , α)))) =
  inj₁ (s , (λ i → ∞term-from-subst-seq Δ (α i)))
out (∞term-from-subst-seq Δ (sup (inj₂ v))) with proj₁ (hd Δ) v | proj₂ (hd Δ) v
... | sup (inj₁ (s , α)) | f =
  inj₁ (s , (λ i → ∞term-from-subst-seq (tl Δ) (α i)))
... | sup (inj₂ v₁)      | f with f tt
out (∞term-from-subst-seq Δ (sup (inj₂ v))) | sup (inj₂ .v) | f | refl =
  inj₂ v

{-
∞term-from-subst-seq-converges :
  ∀{V} → (Δ : Stream (NonTrivSubst V)) → (t : T V) →
  term-seq-from-subst-seq Δ t →∞ ∞term-from-subst-seq Δ t
hd-matches   (∞term-from-subst-seq-converges Δ t) = (proj₁ (hd Δ) , refl)
hd-prefix    (∞term-from-subst-seq-converges Δ t) = {!!}
tl-converges (∞term-from-subst-seq-converges Δ t) = {!∞term-from-subst-seq-converges!}
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Function.Axioms where

open import Lang.Instance
open import Logic.Predicate
open import Logic
import      Lvl
import      Structure.Function.Names as Names
open import Structure.Setoid
open import Type

private variable ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ : Lvl.Level

module _
  {A : Type{ℓₒ₁}}
  {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₗ₂}(B) ⦄
  ⦃ _ : Equiv{ℓₗ₃}(A → B) ⦄
  (f g : A → B)
  where

  record FunctionExtensionalityOn : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field proof : Names.FunctionExtensionalityOn(f)(g)
  functionExtensionalityOn = inst-fn FunctionExtensionalityOn.proof

  record FunctionApplicationOn : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field proof : Names.FunctionApplicationOn(f)(g)
  functionApplicationOn = inst-fn FunctionApplicationOn.proof

module _ (A : Type{ℓₒ₁}) (B : Type{ℓₒ₂}) ⦃ _ : Equiv{ℓₗ₂}(B) ⦄ ⦃ _ : Equiv{ℓₗ₃}(A → B) ⦄ where
  FunctionExtensionality : Stmt
  FunctionExtensionality = ∀²(FunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})
  functionExtensionality : ⦃ funcExt : FunctionExtensionality ⦄ → Names.FunctionExtensionality(A)(B)
  functionExtensionality {f}{g} = functionExtensionalityOn f g

  FunctionApplication : Stmt
  FunctionApplication = ∀²(FunctionApplicationOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})
  functionApplication : ⦃ funcApp : FunctionApplication ⦄ → Names.FunctionApplication(A)(B)
  functionApplication {f}{g} = functionApplicationOn f g

module _
  {A : Type{ℓₒ₁}}
  {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄
  ⦃ _ : Equiv{ℓₗ₃}((a : A) → B(a)) ⦄
  (f g : ((a : A) → B(a)))
  where

  record DependentFunctionExtensionalityOn : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field proof : Names.DependentFunctionExtensionalityOn(f)(g)
  dependentFunctionExtensionalityOn = inst-fn DependentFunctionExtensionalityOn.proof

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}((a : A) → B(a)) ⦄ where
  DependentFunctionExtensionality : Stmt
  DependentFunctionExtensionality = ∀²(DependentFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})
  dependentFunctionExtensionality : ⦃ depFuncExt : DependentFunctionExtensionality ⦄ → Names.DependentFunctionExtensionality(A)(B)
  dependentFunctionExtensionality {f}{g} = dependentFunctionExtensionalityOn f g

module _
  {A : Type{ℓₒ₁}}
  {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄
  ⦃ _ : Equiv{ℓₗ₃}({a : A} → B(a)) ⦄
  (f g : ({a : A} → B(a)))
  where

  record DependentImplicitFunctionExtensionalityOn : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field proof : Names.DependentImplicitFunctionExtensionalityOn(f)(g)
  dependentImplicitFunctionExtensionalityOn = inst-fn DependentImplicitFunctionExtensionalityOn.proof

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}({a : A} → B(a)) ⦄ where
  DependentImplicitFunctionExtensionality : Stmt
  DependentImplicitFunctionExtensionality = ∀²(DependentImplicitFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})
  dependentImplicitFunctionExtensionality : ⦃ depFuncExt : DependentImplicitFunctionExtensionality ⦄ → Names.DependentImplicitFunctionExtensionality(A)(B)
  dependentImplicitFunctionExtensionality {f}{g} = dependentImplicitFunctionExtensionalityOn f g

module _
  {A : Type{ℓₒ₁}}
  {B : A → Type{ℓₒ₂}} ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄
  ⦃ _ : Equiv{ℓₗ₃}(⦃ a : A ⦄ → B(a)) ⦄
  (f g : (⦃ a : A ⦄ → B(a)))
  where

  record DependentInstanceFunctionExtensionalityOn : Stmt{ℓₒ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓₗ₃} where
    constructor intro
    field proof : Names.DependentInstanceFunctionExtensionalityOn(f)(g)
  dependentInstanceFunctionExtensionalityOn = inst-fn DependentInstanceFunctionExtensionalityOn.proof

module _ (A : Type{ℓₒ₁}) (B : A → Type{ℓₒ₂}) ⦃ _ : ∀{a} → Equiv{ℓₗ₂}(B(a)) ⦄ ⦃ _ : Equiv{ℓₗ₃}(⦃ a : A ⦄ → B(a)) ⦄ where
  DependentInstanceFunctionExtensionality : Stmt
  DependentInstanceFunctionExtensionality = ∀²(DependentInstanceFunctionExtensionalityOn{ℓₒ₁}{ℓₒ₂}{ℓₗ₂}{ℓₗ₃}{A}{B})
  dependentInstanceFunctionExtensionality : ⦃ depFuncExt : DependentInstanceFunctionExtensionality ⦄ → Names.DependentInstanceFunctionExtensionality(A)(B)
  dependentInstanceFunctionExtensionality {f}{g} = dependentInstanceFunctionExtensionalityOn f g

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Various forms of induction for natural numbers
------------------------------------------------------------------------

module Induction.Nat where

open import Function
open import Data.Nat
open import Data.Fin using (_≺_)
open import Data.Fin.Properties
open import Data.Product
open import Data.Unit
open import Induction
open import Induction.WellFounded as WF
open import Level using (Lift)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary

------------------------------------------------------------------------
-- Ordinary induction

Rec : ∀ ℓ → RecStruct ℕ ℓ ℓ
Rec _ P zero    = Lift ⊤
Rec _ P (suc n) = P n

rec-builder : ∀ {ℓ} → RecursorBuilder (Rec ℓ)
rec-builder P f zero    = _
rec-builder P f (suc n) = f n (rec-builder P f n)

rec : ∀ {ℓ} → Recursor (Rec ℓ)
rec = build rec-builder

------------------------------------------------------------------------
-- Complete induction

CRec : ∀ ℓ → RecStruct ℕ ℓ ℓ
CRec _ P zero    = Lift ⊤
CRec _ P (suc n) = P n × CRec _ P n

cRec-builder : ∀ {ℓ} → RecursorBuilder (CRec ℓ)
cRec-builder P f zero    = _
cRec-builder P f (suc n) = f n ih , ih
  where ih = cRec-builder P f n

cRec : ∀ {ℓ} → Recursor (CRec ℓ)
cRec = build cRec-builder

------------------------------------------------------------------------
-- Complete induction based on _<′_

<-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
<-Rec = WfRec _<′_

mutual

  <-well-founded : Well-founded _<′_
  <-well-founded n = acc (<-well-founded′ n)

  <-well-founded′ : ∀ n → <-Rec (Acc _<′_) n
  <-well-founded′ zero     _ ()
  <-well-founded′ (suc n) .n ≤′-refl       = <-well-founded n
  <-well-founded′ (suc n)  m (≤′-step m<n) = <-well-founded′ n m m<n

module _ {ℓ} where
  open WF.All <-well-founded ℓ public
    renaming ( wfRec-builder to <-rec-builder
             ; wfRec to <-rec
             )

------------------------------------------------------------------------
-- Complete induction based on _≺_

≺-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
≺-Rec = WfRec _≺_

≺-well-founded : Well-founded _≺_
≺-well-founded = Subrelation.well-founded ≺⇒<′ <-well-founded

module _ {ℓ} where
  open WF.All ≺-well-founded ℓ public
    renaming ( wfRec-builder to ≺-rec-builder
             ; wfRec to ≺-rec
             )

------------------------------------------------------------------------
-- Examples

private

 module Examples where

  -- Doubles its input.

  twice : ℕ → ℕ
  twice = rec _ λ
    { zero    _       → zero
    ; (suc n) twice-n → suc (suc twice-n)
    }

  -- Halves its input (rounding downwards).
  --
  -- The step function is mentioned in a proof below, so it has been
  -- given a name. (The mutual keyword is used to avoid having to give
  -- a type signature for the step function.)

  mutual

    half₁-step = λ
      { zero          _                → zero
      ; (suc zero)    _                → zero
      ; (suc (suc n)) (_ , half₁n , _) → suc half₁n
      }

    half₁ : ℕ → ℕ
    half₁ = cRec _ half₁-step

  -- An alternative implementation of half₁.

  mutual

    half₂-step = λ
      { zero          _   → zero
      ; (suc zero)    _   → zero
      ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
      }

    half₂ : ℕ → ℕ
    half₂ = <-rec _ half₂-step

  -- The application half₁ (2 + n) is definitionally equal to
  -- 1 + half₁ n. Perhaps it is instructive to see why.

  half₁-2+ : ∀ n → half₁ (2 + n) ≡ 1 + half₁ n
  half₁-2+ n = begin

    half₁ (2 + n)                                                         ≡⟨⟩

    cRec (λ _ → ℕ) half₁-step (2 + n)                                     ≡⟨⟩

    half₁-step (2 + n) (cRec-builder (λ _ → ℕ) half₁-step (2 + n))        ≡⟨⟩

    half₁-step (2 + n)
      (let ih = cRec-builder (λ _ → ℕ) half₁-step (1 + n) in
       half₁-step (1 + n) ih , ih)                                        ≡⟨⟩

    half₁-step (2 + n)
      (let ih = cRec-builder (λ _ → ℕ) half₁-step n in
       half₁-step (1 + n) (half₁-step n ih , ih) , half₁-step n ih , ih)  ≡⟨⟩

    1 + half₁-step n (cRec-builder (λ _ → ℕ) half₁-step n)                ≡⟨⟩

    1 + cRec (λ _ → ℕ) half₁-step n                                       ≡⟨⟩

    1 + half₁ n                                                           ∎

    where open ≡-Reasoning

  -- The application half₂ (2 + n) is definitionally equal to
  -- 1 + half₂ n. Perhaps it is instructive to see why.

  half₂-2+ : ∀ n → half₂ (2 + n) ≡ 1 + half₂ n
  half₂-2+ n = begin

    half₂ (2 + n)                                                         ≡⟨⟩

    <-rec (λ _ → ℕ) half₂-step (2 + n)                                    ≡⟨⟩

    half₂-step (2 + n) (<-rec-builder (λ _ → ℕ) half₂-step (2 + n))       ≡⟨⟩

    1 + <-rec-builder (λ _ → ℕ) half₂-step (2 + n) n (≤′-step ≤′-refl)    ≡⟨⟩

    1 + Some.wfRec-builder (λ _ → ℕ) half₂-step (2 + n)
          (<-well-founded (2 + n)) n (≤′-step ≤′-refl)                    ≡⟨⟩

    1 + Some.wfRec-builder (λ _ → ℕ) half₂-step (2 + n)
          (acc (<-well-founded′ (2 + n))) n (≤′-step ≤′-refl)             ≡⟨⟩

    1 + half₂-step n
          (Some.wfRec-builder (λ _ → ℕ) half₂-step n
             (<-well-founded′ (2 + n) n (≤′-step ≤′-refl)))               ≡⟨⟩

    1 + half₂-step n
          (Some.wfRec-builder (λ _ → ℕ) half₂-step n
             (<-well-founded′ (1 + n) n ≤′-refl))                         ≡⟨⟩

    1 + half₂-step n
          (Some.wfRec-builder (λ _ → ℕ) half₂-step n (<-well-founded n))  ≡⟨⟩

    1 + half₂-step n (<-rec-builder (λ _ → ℕ) half₂-step n)               ≡⟨⟩

    1 + <-rec (λ _ → ℕ) half₂-step n                                      ≡⟨⟩

    1 + half₂ n                                                           ∎

    where open ≡-Reasoning

  -- Some properties that the functions above satisfy, proved using
  -- cRec.

  half₁-+₁ : ∀ n → half₁ (twice n) ≡ n
  half₁-+₁ = cRec _ λ
    { zero          _                        → refl
    ; (suc zero)    _                        → refl
    ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
        cong (suc ∘ suc) half₁twice-n≡n
    }

  half₂-+₁ : ∀ n → half₂ (twice n) ≡ n
  half₂-+₁ = cRec _ λ
    { zero          _                        → refl
    ; (suc zero)    _                        → refl
    ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
        cong (suc ∘ suc) half₁twice-n≡n
    }

  -- Some properties that the functions above satisfy, proved using
  -- <-rec.

  half₁-+₂ : ∀ n → half₁ (twice n) ≡ n
  half₁-+₂ = <-rec _ λ
    { zero          _   → refl
    ; (suc zero)    _   → refl
    ; (suc (suc n)) rec →
        cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
    }

  half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
  half₂-+₂ = <-rec _ λ
    { zero          _   → refl
    ; (suc zero)    _   → refl
    ; (suc (suc n)) rec →
        cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
    }


text:
module AuxDefs where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

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

data Bool : Set where
  true  : Bool
  false : Bool

data Comparison : Set where
  less    : Comparison
  equal   : Comparison
  greater : Comparison

_<_ : ℕ → ℕ → Bool
zero < y      = true
suc x < zero  = false
suc x < suc y = x < y


text:
module Splitting where

open import Basics
open import All

data _<[_]>_ {X : Set} : List X -> List X -> List X -> Set where
  sz : [] <[ [] ]> []
  sl : forall {l ls ms rs} -> ls <[ ms ]> rs -> (l ,- ls) <[ l ,- ms ]> rs
  sr : forall {r ls ms rs} -> ls <[ ms ]> rs -> ls <[ r ,- ms ]> (r ,- rs)

riffle : {X : Set}{ls ms rs : List X} -> ls <[ ms ]> rs ->
         {P : X -> Set} -> All P ls -> All P rs -> All P ms
riffle sz <> <> = <>
riffle (sl x) (p , lp) rp = p , riffle x lp rp
riffle (sr x) lp (p , rp) = p , riffle x lp rp

srs : forall {X : Set}(xs : List X) -> [] <[ xs ]> xs
srs [] = sz
srs (x ,- xs) = sr (srs xs)

data SRS {X : Set}(ms : List X) : (xs : List X) -> [] <[ ms ]> xs -> Set where
  mkSRS : SRS ms ms (srs ms)

isSRS : {X : Set}{ms xs : List X}(i : [] <[ ms ]> xs) -> SRS ms xs i
isSRS sz = mkSRS
isSRS (sr i) with isSRS i
isSRS (sr .(srs _)) | mkSRS = mkSRS

slrs : forall {X : Set}(xs ys : List X) -> xs <[ xs +L ys ]> ys
slrs [] ys = srs ys
slrs (x ,- xs) ys = sl (slrs xs ys)

cat : forall {X}{P : X -> Set}(xs ys : List X) -> All P xs -> All P ys -> All P (xs +L ys)
cat xs ys ps qs = riffle (slrs xs ys) ps qs

data IsRiffle {X : Set}{ls ms rs : List X}(i : ls <[ ms ]> rs){P : X -> Set}
  : All P ms -> Set where
  mkRiffle : (lp : All P ls)(rp : All P rs) -> IsRiffle i (riffle i lp rp)
isRiffle : {X : Set}{ls ms rs : List X}(i : ls <[ ms ]> rs){P : X -> Set}(mp : All P ms) -> IsRiffle i mp
isRiffle sz <> = mkRiffle <> <>
isRiffle (sl i) (p , mp) with isRiffle i mp
isRiffle (sl i) (p , .(riffle i lp rp)) | mkRiffle lp rp = mkRiffle (p , lp) rp
isRiffle (sr i) (p , mp) with isRiffle i mp
isRiffle (sr i) (p , .(riffle i lp rp)) | mkRiffle lp rp = mkRiffle lp (p , rp)

mirror : {X : Set}{ls ms rs : List X} -> ls <[ ms ]> rs -> rs <[ ms ]> ls
mirror sz = sz
mirror (sl x) = sr (mirror x)
mirror (sr x) = sl (mirror x)

rotatel : {X : Set}{ls ms rs lrs rrs : List X} -> ls <[ ms ]> rs -> lrs <[ rs ]> rrs ->
  Sg (List X) \ ns -> (ls <[ ns ]> lrs) * (ns <[ ms ]> rrs)
rotatel sz sz = [] , sz , sz
rotatel (sl x) y with rotatel x y
... | _ , a , b = _ , sl a , sl b
rotatel (sr x) (sl y) with rotatel x y
... | _ , a , b = _ , sr a , sl b
rotatel (sr x) (sr y) with rotatel x y
... | _ , a , b = _ , a , sr b

rotater : {X : Set}{lls rls ls ms rs : List X} -> lls <[ ls ]> rls -> ls <[ ms ]> rs ->
  Sg (List X) \ ns -> (lls <[ ms ]> ns) * (rls <[ ns ]> rs)
rotater x y with rotatel (mirror y) (mirror x)
... | _ , a , b = _ , mirror b , mirror a

llswap : {X : Set}{ls ms lrs rrs : List X} ->
 (Sg (List X) \ rs -> (ls <[ ms ]> rs) * (lrs <[ rs ]> rrs)) ->
  Sg (List X) \ ns -> (lrs <[ ms ]> ns) * (ls <[ ns ]> rrs)
llswap (_ , x , y) with rotatel x y
... | _ , a , b = rotater (mirror a) b

insS : {X : Set}(xs : List X)(y : X)(zs : List X) -> (y ,- []) <[ (xs +L y ,- zs) ]> (xs +L zs)
insS [] y zs = sl (srs zs)
insS (x ,- xs) y zs = sr (insS xs y zs)

catS : forall {X}{as abs bs cs cds ds : List X} ->
        as <[ abs ]> bs -> cs <[ cds ]> ds ->
        (as +L cs) <[ (abs +L cds) ]> (bs +L ds)
catS sz y = y
catS (sl x) y = sl (catS x y)
catS (sr x) y = sr (catS x y)

splimap : forall {X Y}(f : X -> Y){xs xys ys} -> xs <[ xys ]> ys ->
           list f xs <[ list f xys ]> list f ys
splimap f sz = sz
splimap f (sl s) = sl (splimap f s)
splimap f (sr s) = sr (splimap f s)

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


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

module Function.Injective where

open import Function.Injective.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Open where

open import bool
open import nat
open import product
open import sum
open import functor

data Row : Set₁ where
  Empty : Row
  Ty : Set → Row
  Prod : Row → Row → Row

infixr 19 _♯_

_′ = Ty
_♯_ = Prod

all : Row → Set
all Empty = ⊤
all (Ty x) = x
all (Prod r₁ r₂) = (all r₁) × (all r₂)

one : Row → Set
one Empty = ⊥
one (Ty x) = x
one (Prod r₁ r₂) = (one r₁) ⊎ (one r₂)

_⊗_ : {A B : Row} → all A → all B → all (A ♯ B)
_⊗_ p₁ p₂ = p₁ , p₂

_&_ : {A : Set}{B : Row} → A → all B → all (A ′ ♯ B)
_&_ {A}{B} = _⊗_ {A ′}{B}

_⊕_ : {A B : Row} → (one A) ⊎ (one B) → one (A ♯ B)
_⊕_ p = p

⊕inj₁ : {A B : Row} → one A → one (A ♯ B)
⊕inj₁ = inj₁
⊕inj₂ : {A B : Row} → one B → one (A ♯ B)
⊕inj₂ = inj₂

inj : {A : Set}{B : Row} → A → one (A ′ ♯ B)
inj {A}{B} = ⊕inj₁ {A ′}{B}

test₁ : all (ℕ ′ ♯ 𝔹 ′ ♯ Empty)
test₁ = _&_ {ℕ}{𝔹 ′ ♯ Empty} 1 (_&_ {𝔹}{Empty} tt triv)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2017-08-24, issue #2717, reported by m0davis
--
-- Internal error in DisplayForm.hs triggered by -v 100.
-- Regression introduced by #2590

{-# OPTIONS -v tc.display.top:100 -v tc.polarity.dep:20 #-} -- KEEP

module _ (A : Set) where

module M (_ : Set) where
  data D (n : Set) : Set where
    d : D n

open M A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Path.Reasoning where

open import Prelude

infixr 2 ≡˘⟨⟩-syntax _≡⟨⟩_ ≡⟨∙⟩-syntax

≡˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≡ z → y ≡ x → x ≡ z
≡˘⟨⟩-syntax _ y≡z y≡x = sym y≡x ; y≡z

syntax ≡˘⟨⟩-syntax x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

≡⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≡ z → x ≡ y → x ≡ z
≡⟨∙⟩-syntax _ y≡z x≡y = x≡y ; y≡z

syntax ≡⟨∙⟩-syntax x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

_≡⟨⟩_ : ∀ (x : A) {y} → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

infix 2.5 _∎
_∎ : ∀ {A : Type a} (x : A) → x ≡ x
_∎ x = refl


text:
module Generic.Lib.Reflection.Fold where

open import Generic.Lib.Intro
open import Generic.Lib.Decidable
open import Generic.Lib.Category
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.String
open import Generic.Lib.Data.Maybe
open import Generic.Lib.Data.List
open import Generic.Lib.Reflection.Core

foldTypeOf : Data Type -> Type
foldTypeOf (packData d a b cs ns) = appendType iab ∘ pi "π" π ∘ pi "P" P $ cs ʰ→ from ‵→ to where
  infixr 5 _ʰ→_
  i    = countPis a
  j    = countPis b
  ab   = appendType a b
  iab  = implicitize ab
  π    = implRelArg (quoteTerm Level)
  P    = explRelArg ∘ appendType (shiftBy (suc j) b) ∘ agda-sort ∘ set $ pureVar j
  hyp  = mapName (λ p -> appVar p ∘ drop i) d ∘ shiftBy (2 + j)
  _ʰ→_ = flip $ foldr (λ c r -> hyp c ‵→ shift r)
  from = appDef d (pisToArgVars (2 + i + j) ab)
  to   = appVar 1 (pisToArgVars (3 + j) b)

foldClausesOf : Name -> Data Type -> List Clause
foldClausesOf f (packData d a b cs ns) = allToList $ mapAllInd (λ {a} n -> clauseOf n a) ns where
  k = length cs

  clauseOf : ℕ -> Type -> Name -> Clause
  clauseOf i c n = clause lhs rhs where
    args = explPisToNames c
    j    = length args
    lhs  = patVars ("P" ∷ unmap (λ n -> "f" ++ˢ showName n) ns)
         ∷ʳ explRelArg (patCon n (patVars args))

    tryHyp : ℕ -> ℕ -> Type -> Maybe Term
    tryHyp m l (explPi r s a b) = explLam s <$> tryHyp (suc m) l b
    tryHyp m l (pi       s a b) = tryHyp m l b
    tryHyp m l (appDef e _)     = d == e ?> vis appDef f (pars ∷ʳ rarg) where
      pars = map (λ i -> pureVar (m + i)) $ downFromTo (suc k + j) j
      rarg = vis appVar (m + l) $ map pureVar (downFrom m)
    tryHyp m l  b               = nothing

    hyps : ℕ -> Type -> List Term
    hyps (suc l) (explPi r s a b) = fromMaybe (pureVar l) (tryHyp 0 l a) ∷ hyps l b
    hyps  l      (pi       s a b) = hyps l b
    hyps  l       b               = []

    rhs = vis appVar (k + j ∸ suc i) (hyps j c)

    -- i = 1: f
    -- j = 3: x t r
    -- k = 2: g f
    --      5 4 3       2 1 0    3 2       4 3 1     1 0         6 5  2 1 0
    -- fold P g f (cons x t r) = f x (fold g f t) (λ y u -> fold g f (r y u))

defineFold : Name -> Data Type -> TC _
defineFold f D =
  declareDef (explRelArg f) (foldTypeOf D) >>
  defineFun f (foldClausesOf f D)

deriveFold : Name -> Data Type -> TC Name
deriveFold d D =
  freshName ("fold" ++ˢ showName d) >>= λ f ->
  f <$ defineFold f D

deriveFoldTo : Name -> Name -> TC _
deriveFoldTo f = getData >=> defineFold f

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module MacroNotToTerm where

open import Common.Reflection
open import Common.Prelude

data X : Set where

macro
  f : Term -> Set
  f x _ = X


text:
{-# OPTIONS --sized-types #-}
module SOList.Total {A : Set}(_≤_ : A → A → Set)  where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Size

data SOList : {ι : Size} → Bound → Bound → Set where
  onil : {ι : Size}{b t : Bound}
                   → LeB b t
                   → SOList {↑ ι} b t
  ocons : {ι : Size}{b t : Bound}(x : A)
                   → SOList {ι} b (val x)
                   → SOList {ι} (val x) t
                   → SOList {↑ ι} b t

forget : {b t : Bound} → SOList b t → List A
forget (onil _) = []
forget (ocons x xs ys) = forget xs ++ (x ∷ forget ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Embedding
open import Tools.Product

-- Validity of the natural number type.
ℕᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ]
ℕᵛ [Γ] ⊢Δ [σ] = ℕᵣ (idRed:*: (ℕⱼ ⊢Δ)) , λ _ x₂ → ιx (ℕ₌ (id (ℕⱼ ⊢Δ)))

-- Validity of the natural number type as a term.
ℕᵗᵛ : ∀ {Γ} ([Γ] : ⊩ᵛ Γ)
    → Γ ⊩ᵛ⟨ ¹ ⟩ ℕ ∷ U / [Γ] / Uᵛ [Γ]
ℕᵗᵛ [Γ] ⊢Δ [σ] = let ⊢ℕ  = ℕⱼ ⊢Δ
                     [ℕ] = ℕᵣ (idRed:*: (ℕⱼ ⊢Δ))
                 in  Uₜ ℕ (idRedTerm:*: ⊢ℕ) ℕₙ (≅ₜ-ℕrefl ⊢Δ) [ℕ]
                 ,   (λ x x₁ → Uₜ₌ ℕ ℕ (idRedTerm:*: ⊢ℕ) (idRedTerm:*: ⊢ℕ) ℕₙ ℕₙ
                                   (≅ₜ-ℕrefl ⊢Δ) [ℕ] [ℕ] (ιx (ℕ₌ (id (ℕⱼ ⊢Δ)))))

-- Validity of zero.
zeroᵛ : ∀ {Γ l} ([Γ] : ⊩ᵛ Γ)
      → Γ ⊩ᵛ⟨ l ⟩ zero ∷ ℕ / [Γ] / ℕᵛ [Γ]
zeroᵛ [Γ] ⊢Δ [σ] =
  ιx (ℕₜ zero (idRedTerm:*: (zeroⱼ ⊢Δ)) (≅ₜ-zerorefl ⊢Δ) zeroᵣ)
    , (λ _ x₁ → ιx (ℕₜ₌ zero zero (idRedTerm:*: (zeroⱼ ⊢Δ)) (idRedTerm:*: (zeroⱼ ⊢Δ))
                    (≅ₜ-zerorefl ⊢Δ) zeroᵣ))

-- Validity of successor of valid natural numbers.
sucᵛ : ∀ {Γ n l} ([Γ] : ⊩ᵛ Γ)
         ([ℕ] : Γ ⊩ᵛ⟨ l ⟩ ℕ / [Γ])
     → Γ ⊩ᵛ⟨ l ⟩ n ∷ ℕ / [Γ] / [ℕ]
     → Γ ⊩ᵛ⟨ l ⟩ suc n ∷ ℕ / [Γ] / [ℕ]
sucᵛ ⊢Γ [ℕ] [n] ⊢Δ [σ] =
  sucTerm (proj₁ ([ℕ] ⊢Δ [σ])) (proj₁ ([n] ⊢Δ [σ]))
  , (λ x x₁ → sucEqTerm (proj₁ ([ℕ] ⊢Δ [σ])) (proj₂ ([n] ⊢Δ [σ]) x x₁))

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Sets.Facts.Initial where

open import Data.Empty using (⊥ ; ⊥-elim)
open import Level using (Lift ; lift ; lower)

open import Cats.Category
open import Cats.Category.Sets using (Sets)

instance
  hasInitial : ∀ {l} → HasInitial (Sets l)
  hasInitial = record
    { ⊥ = Lift _ ⊥
    ; isInitial = λ X → record
      { arr = λ()
      ; unique = λ { _ () }
      }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


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

module 02-natural-numbers where

import 00-preamble
open 00-preamble public

-- Definition 2.2.3
id : {i : Level} {A : UU i} → A → A
id a = a

-- Definition 2.2.4
_∘_ :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} →
  (B → C) → ((A → B) → (A → C))
(g ∘ f) a = g (f a)

data ℕ : UU lzero where
  zero-ℕ : ℕ
  succ-ℕ : ℕ → ℕ

one-ℕ : ℕ
one-ℕ = succ-ℕ zero-ℕ

-- induction: for any dependent type P over ℕ, define a section of P
-- built out of a term in P 0 and a section of P n → P(Nsucc n)
ind-ℕ : {i : Level} {P : ℕ → UU i} → P zero-ℕ → ((n : ℕ) → P n → P(succ-ℕ n)) → ((n : ℕ) → P n)
ind-ℕ p0 pS zero-ℕ = p0
ind-ℕ p0 pS (succ-ℕ n) = pS n (ind-ℕ p0 pS n)

-- use the general induction principle to define addition
-- in this case P is ℕ, the special non-dependent type over ℕ, and
-- so sections of P (dependent functions Π_{x:ℕ} P(x)) are functions ℕ → ℕ

add-ℕ : ℕ → ℕ → ℕ
add-ℕ zero-ℕ y = y
add-ℕ (succ-ℕ x) y = succ-ℕ (add-ℕ x y)

-- Exercise 2.2
const : {i j : Level} (A : UU i) (B : UU j) (b : B) → A → B
const A B b x = b

-- Exercise 2.3

-- In this exercise we are asked to construct some standard functions on the
-- natural numbers.

-- Exercise 2.3(a)
max-ℕ : ℕ → (ℕ → ℕ)
max-ℕ zero-ℕ n = n
max-ℕ (succ-ℕ m) zero-ℕ = succ-ℕ m
max-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (max-ℕ m n)

min-ℕ : ℕ → (ℕ → ℕ)
min-ℕ zero-ℕ n = zero-ℕ
min-ℕ (succ-ℕ m) zero-ℕ = zero-ℕ
min-ℕ (succ-ℕ m) (succ-ℕ n) = succ-ℕ (min-ℕ m n)

-- Exercise 2.3(b)
mul-ℕ : ℕ → (ℕ → ℕ)
mul-ℕ zero-ℕ n = zero-ℕ
mul-ℕ (succ-ℕ m) n = add-ℕ (mul-ℕ m n) n

-- Exercise 2.3(c)
_^_ : ℕ → (ℕ → ℕ)
m ^ zero-ℕ = one-ℕ
m ^ (succ-ℕ n) = mul-ℕ m (m ^ n)

-- Exercise 2.3(d)
factorial : ℕ → ℕ
factorial zero-ℕ = one-ℕ
factorial (succ-ℕ m) = mul-ℕ (succ-ℕ m) (factorial m)

-- Exercise 2.3(e)
_choose_ : ℕ → ℕ → ℕ
zero-ℕ choose zero-ℕ = one-ℕ
zero-ℕ choose succ-ℕ k = zero-ℕ
(succ-ℕ n) choose zero-ℕ = one-ℕ
(succ-ℕ n) choose (succ-ℕ k) = add-ℕ (n choose k) (n choose (succ-ℕ k))

-- Exercise 2.3(f)
Fibonacci : ℕ → ℕ
Fibonacci zero-ℕ = zero-ℕ
Fibonacci (succ-ℕ zero-ℕ) = one-ℕ
Fibonacci (succ-ℕ (succ-ℕ n)) = add-ℕ (Fibonacci n) (Fibonacci (succ-ℕ n))

-- Exercise 2.4
_∘'_ :
  {i j k : Level} {A : UU i} {B : A → UU j} {C : (x : A) → B x → UU k} →
  (g : (x : A) → (y : B x) → C x y) (f : (x : A) → B x) → (x : A) → C x (f x)
(g ∘' f) x = g x (f x)

-- Exercise 2.5
Π-swap : {i j k : Level} {A : UU i} {B : UU j} {C : A → (B → UU k)} →
  ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
Π-swap f y x = f x y

-- Note: apparently Agda still allows us to define a sequence of universe levels indexed by ℕ

Level-ℕ : ℕ → Level
Level-ℕ zero-ℕ = lzero
Level-ℕ (succ-ℕ n) = lsuc (Level-ℕ n)

sequence-UU : (n : ℕ) → UU (Level-ℕ (succ-ℕ n))
sequence-UU n = UU (Level-ℕ n)

-- However, the following definition is unacceptable for Agda, since it runs
-- into Setω.

{-
Π-sequence-UU : Setω
Π-sequence-UU = (n : ℕ) → sequence-UU n
-}

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
{-#  OPTIONS --type-in-type #-}
module TooManyArgs where

open import AgdaPrelude

myFun : (a : Set) -> a -> a -> a
myFun a x y = x

myApp = myFun _ Zero Zero Zero Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
------------------------------------------------------------------------
-- A coinductive definition of (strong) bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Bisimilarity {ℓ} (lts : LTS ℓ) where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

import Function-universe equality-with-J as F

import Bisimilarity.General
open import Indexed-container using (Container; ν; ν′)
open import Relation
open import Up-to

open LTS lts

private
  module General = Bisimilarity.General lts _[_]⟶_ _[_]⟶_ id id

open General public
  using (module StepC; ⟨_,_⟩; left-to-right; right-to-left; force;
         reflexive-∼; reflexive-∼′; ≡⇒∼; ∼:_; ∼′:_;
         [_]_≡_; [_]_≡′_; []≡↔; module Bisimilarity-of-∼;
         Extensionality; extensionality)

-- StepC is given in the following way, rather than via open public,
-- to make hyperlinks to it more informative.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC

-- The following definitions are given explicitly, to make the code
-- easier to follow for readers of the paper.

Bisimilarity : Size → Rel₂ ℓ Proc
Bisimilarity = ν StepC

Bisimilarity′ : Size → Rel₂ ℓ Proc
Bisimilarity′ = ν′ StepC

infix 4 [_]_∼_ [_]_∼′_ _∼_ _∼′_

[_]_∼_ : Size → Proc → Proc → Type ℓ
[ i ] p ∼ q = ν StepC i (p , q)

[_]_∼′_ : Size → Proc → Proc → Type ℓ
[ i ] p ∼′ q = ν′ StepC i (p , q)

_∼_ : Proc → Proc → Type ℓ
_∼_ = [ ∞ ]_∼_

_∼′_ : Proc → Proc → Type ℓ
_∼′_ = [ ∞ ]_∼′_

private

  -- However, these definitions are definitionally equivalent to
  -- corresponding definitions in General.

  indirect-Bisimilarity : Bisimilarity ≡ General.Bisimilarity
  indirect-Bisimilarity = refl

  indirect-Bisimilarity′ : Bisimilarity′ ≡ General.Bisimilarity′
  indirect-Bisimilarity′ = refl

  indirect-[]∼ : [_]_∼_ ≡ General.[_]_∼_
  indirect-[]∼ = refl

  indirect-[]∼′ : [_]_∼′_ ≡ General.[_]_∼′_
  indirect-[]∼′ = refl

  indirect-∼ : _∼_ ≡ General._∼_
  indirect-∼ = refl

  indirect-∼′ : _∼′_ ≡ General._∼′_
  indirect-∼′ = refl

-- Combinators that can perhaps make the code a bit nicer to read.

infix -3 _⟶⟨_⟩ʳˡ_ _[_]⟶⟨_⟩ʳˡ_
         lr-result-with-action lr-result-without-action

_⟶⟨_⟩ʳˡ_ : ∀ {i p′ q′ μ} p → p [ μ ]⟶ p′ → [ i ] p′ ∼′ q′ →
           ∃ λ p′ → p [ μ ]⟶ p′ × [ i ] p′ ∼′ q′
_ ⟶⟨ p⟶p′ ⟩ʳˡ p′∼′q′ = _ , p⟶p′ , p′∼′q′

_[_]⟶⟨_⟩ʳˡ_ : ∀ {i p′ q′} p μ → p [ μ ]⟶ p′ → [ i ] p′ ∼′ q′ →
              ∃ λ p′ → p [ μ ]⟶ p′ × [ i ] p′ ∼′ q′
_ [ _ ]⟶⟨ p⟶p′ ⟩ʳˡ p′∼′q′ = _ ⟶⟨ p⟶p′ ⟩ʳˡ p′∼′q′

lr-result-without-action :
  ∀ {i p′ q′ μ} → [ i ] p′ ∼′ q′ → ∀ q → q [ μ ]⟶ q′ →
  ∃ λ q′ → q [ μ ]⟶ q′ × [ i ] p′ ∼′ q′
lr-result-without-action p′∼′q′ _ q⟶q′ = _ , q⟶q′ , p′∼′q′

lr-result-with-action :
  ∀ {i p′ q′} → [ i ] p′ ∼′ q′ → ∀ μ q → q [ μ ]⟶ q′ →
  ∃ λ q′ → q [ μ ]⟶ q′ × [ i ] p′ ∼′ q′
lr-result-with-action p′∼′q′ _ _ q⟶q′ =
  lr-result-without-action  p′∼′q′ _ q⟶q′

syntax lr-result-without-action p′∼q′   q q⟶q′ = p′∼q′      ⟵⟨ q⟶q′ ⟩ q
syntax lr-result-with-action    p′∼q′ μ q q⟶q′ = p′∼q′ [ μ ]⟵⟨ q⟶q′ ⟩ q

-- Strong bisimilarity is a weak simulation (of a certain kind).

strong-is-weak⇒̂ :
  ∀ {p p′ q μ} →
  p ∼ q → p [ μ ]⇒̂ p′ →
  ∃ λ q′ → q [ μ ]⇒̂ q′ × p′ ∼ q′
strong-is-weak⇒̂ =
  is-weak⇒̂ StepC.left-to-right (λ p∼′q → force p∼′q)
           (λ s tr → step s tr done) ⟶→⇒̂

mutual

  -- Bisimilarity is symmetric.

  symmetric-∼ : ∀ {i p q} → [ i ] p ∼ q → [ i ] q ∼ p
  symmetric-∼ p∼q =
    StepC.⟨ Σ-map id (Σ-map id symmetric-∼′) ∘ StepC.right-to-left p∼q
          , Σ-map id (Σ-map id symmetric-∼′) ∘ StepC.left-to-right p∼q
          ⟩

  symmetric-∼′ : ∀ {i p q} → [ i ] p ∼′ q → [ i ] q ∼′ p
  force (symmetric-∼′ p∼q) = symmetric-∼ (force p∼q)

private

  -- An alternative proof of symmetry.

  alternative-proof-of-symmetry : ∀ {i p q} → [ i ] p ∼ q → [ i ] q ∼ p
  alternative-proof-of-symmetry {i} =
    uncurry [ i ]_∼_ ⁻¹  ⊆⟨ ν-symmetric _ _ swap refl F.id ⟩∎
    uncurry [ i ]_∼_     ∎

-- Strong bisimilarity is transitive.

transitive-∼ : ∀ {i p q r} → [ i ] p ∼ q → [ i ] q ∼ r → [ i ] p ∼ r
transitive-∼ {i} = λ p q →
  StepC.⟨ lr p q
        , Σ-map id (Σ-map id symmetric-∼′) ∘
          lr (symmetric-∼ q) (symmetric-∼ p)
        ⟩
  where
  lr : ∀ {p p′ q r μ} →
       [ i ] p ∼ q → [ i ] q ∼ r → p [ μ ]⟶ p′ →
       ∃ λ r′ → r [ μ ]⟶ r′ × [ i ] p′ ∼′ r′
  lr p q tr =
    let (_ , tr′ , p′) = StepC.left-to-right p tr
        (_ , tr″ , q′) = StepC.left-to-right q tr′
    in  (_ , tr″ , λ { .force → transitive-∼ (force p′) (force q′) })

transitive-∼′ :
  ∀ {i p q r} → [ i ] p ∼′ q → [ i ] q ∼′ r → [ i ] p ∼′ r
force (transitive-∼′ p∼q q∼r) = transitive-∼ (force p∼q) (force q∼r)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
------------------------------------------------------------------------------
-- A proof that was rejected using the --without-K option
------------------------------------------------------------------------------

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

module ListsSL where

open import Data.List
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Relation.Binary
module NDTO = DecTotalOrder ≤-decTotalOrder

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

LTC : {A : Set} → List A → List A → Set
LTC xs ys = ∃ (λ x → ys ≡ x ∷ xs)

LTL : {A : Set} → List A → List A → Set
LTL xs ys = (length xs) < (length ys)

helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))
helper y []       = s≤s z≤n
helper y (x ∷ xs) = s≤s NDTO.refl

-- 25 April 2014. The proof is accepted using Cockx's --without-K
-- implementation.
foo : {A : Set}(xs ys : List A) → LTC xs ys → LTL xs ys
foo xs .(x ∷ xs) (x , refl) = helper x xs

foo' : {A : Set}(xs ys : List A) → LTC xs ys → LTL xs ys
foo' xs ys (x , h) =
  subst (λ ys' → length xs < length ys') (sym h) (helper x xs)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --universe-polymorphism --no-irrelevant-projections --cubical-compatible #-}
module SafeFlagSafePragmas where


text:
module Data.List.Equiv where

open import Logic.Propositional
import      Lvl
open import Data.List
open import Structure.Operator
open import Structure.Setoid
open import Type

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

-- A correct equality relation on lists should state that prepend is a function and have the generalized cancellation properties for lists.
record Extensionality ⦃ equiv : Equiv{ℓₑ}(T) ⦄ (equiv-List : Equiv{ℓₚ}(List(T))) : Type{ℓₑ Lvl.⊔ Lvl.of(T) Lvl.⊔ ℓₚ} where
  constructor intro
  private instance _ = equiv-List
  field
    ⦃ binaryOperator ⦄ : BinaryOperator(List._⊰_)
    generalized-cancellationᵣ : ∀{x y : T}{l₁ l₂ : List(T)} → (x ⊰ l₁ ≡ y ⊰ l₂) → (x ≡ y)
    generalized-cancellationₗ : ∀{x y : T}{l₁ l₂ : List(T)} → (x ⊰ l₁ ≡ y ⊰ l₂) → (l₁ ≡ l₂)
    case-unequality : ∀{x : T}{l : List(T)} → (∅ ≢ x ⊰ l)

  generalized-cancellation : ∀{x y : T}{l₁ l₂ : List(T)} → (x ⊰ l₁ ≡ y ⊰ l₂) → ((x ≡ y) ∧ (l₁ ≡ l₂))
  generalized-cancellation p = [∧]-intro (generalized-cancellationᵣ p) (generalized-cancellationₗ p)
open Extensionality ⦃ … ⦄ renaming
  ( binaryOperator to [⊰]-binaryOperator
  ; generalized-cancellationₗ to [⊰]-generalized-cancellationₗ
  ; generalized-cancellationᵣ to [⊰]-generalized-cancellationᵣ
  ; generalized-cancellation to [⊰]-generalized-cancellation
  ; case-unequality to [∅][⊰]-unequal
  ) public


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

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Orders.Total.Definition
open import Rings.IntegralDomains.Definition

module Rings.Orders.Total.AbsoluteValue {n m p : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {pOrderRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pOrderRing) where

open Ring R
open Group additiveGroup
open Setoid S
open SetoidPartialOrder pOrder
open TotallyOrderedRing order
open SetoidTotalOrder total
open PartiallyOrderedRing pOrderRing
open import Rings.Lemmas R
open import Rings.Orders.Partial.Lemmas pOrderRing
open import Rings.Orders.Total.Lemmas order

abs : A → A
abs a with totality 0R a
abs a | inl (inl 0<a) = a
abs a | inl (inr a<0) = inverse a
abs a | inr 0=a = a

absWellDefined : (a b : A) → a ∼ b → abs a ∼ abs b
absWellDefined a b a=b with totality 0R a
absWellDefined a b a=b | inl (inl 0<a) with totality 0R b
absWellDefined a b a=b | inl (inl 0<a) | inl (inl 0<b) = a=b
absWellDefined a b a=b | inl (inl 0<a) | inl (inr b<0) = exFalso (irreflexive {0G} (<Transitive 0<a (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<0)))
absWellDefined a b a=b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) 0<a))
absWellDefined a b a=b | inl (inr a<0) with totality 0R b
absWellDefined a b a=b | inl (inr a<0) | inl (inl 0<b) = exFalso (irreflexive {0G} (<Transitive 0<b (<WellDefined a=b (Equivalence.reflexive eq) a<0)))
absWellDefined a b a=b | inl (inr a<0) | inl (inr b<0) = inverseWellDefined additiveGroup a=b
absWellDefined a b a=b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) (Equivalence.reflexive eq) a<0))
absWellDefined a b a=b | inr 0=a with totality 0R b
absWellDefined a b a=b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) 0<b))
absWellDefined a b a=b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) (Equivalence.reflexive eq) b<0))
absWellDefined a b a=b | inr 0=a | inr 0=b = a=b

triangleInequality : (a b : A) → ((abs (a + b)) < ((abs a) + (abs b))) || (abs (a + b) ∼ (abs a) + (abs b))
triangleInequality a b with totality 0R (a + b)
triangleInequality a b | inl (inl 0<a+b) with totality 0R a
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a+b (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities a<0 b<0))))
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inr 0=b = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inr a+b<0) with totality 0G a
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<a 0<b)) a+b<0))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (invContravariant additiveGroup)) (inverseWellDefined additiveGroup groupIsAbelian)) (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder (lemm2' _ 0<a) 0<a) (inverse b)))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<a (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) identRight) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inl 0<b) = inl (<WellDefined (Equivalence.symmetric eq (invContravariant additiveGroup)) groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder (lemm2' _ 0<b) 0<b) (inverse a)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian)
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inr 0=b = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=b)) (invIdent additiveGroup)) (Equivalence.reflexive eq)) identLeft) (Equivalence.symmetric eq identRight)) (+WellDefined (Equivalence.reflexive eq) 0=b)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<b (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) identLeft) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (inverseWellDefined additiveGroup 0=a)) (invIdent additiveGroup)) 0=a) (Equivalence.reflexive eq))))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.symmetric eq 0=b)) identLeft) (Equivalence.reflexive eq) a+b<0))
triangleInequality a b | inr 0=a+b with totality 0G a
triangleInequality a b | inr 0=a+b | inl (inl 0<a) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined identLeft (Equivalence.symmetric eq 0=a+b) (ringAddInequalities 0<a 0<b)))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder b<0 (lemm2 _ b<0)) a))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) 0<a))
triangleInequality a b | inr 0=a+b | inl (inr a<0) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.<Transitive pOrder a<0 (lemm2 _ a<0)) b)
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=a+b) identLeft (ringAddInequalities a<0 b<0)))
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) (Equivalence.reflexive eq) a<0))
triangleInequality a b | inr 0=a+b | inr 0=a with totality 0G b
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) 0<b))
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) (Equivalence.reflexive eq) b<0))
triangleInequality a b | inr 0=a+b | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)

absZero : abs (Ring.0R R) ≡ Ring.0R R
absZero with totality (Ring.0R R) (Ring.0R R)
absZero | inl (inl x) = exFalso (irreflexive x)
absZero | inl (inr x) = exFalso (irreflexive x)
absZero | inr x = refl

absNegation : (a : A) → (abs a) ∼ (abs (inverse a))
absNegation a with totality 0R a
absNegation a | inl (inl 0<a) with totality 0G (inverse a)
absNegation a | inl (inl 0<a) | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<-a (lemm2' a 0<a)))
absNegation a | inl (inl 0<a) | inl (inr -a<0) = Equivalence.symmetric eq (invTwice additiveGroup a)
absNegation a | inl (inl 0<a) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invTwice additiveGroup a)) (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=-a))) (invIdent additiveGroup)) 0<a))
absNegation a | inl (inr a<0) with totality 0G (inverse a)
absNegation a | inl (inr a<0) | inl (inl 0<-a) = Equivalence.reflexive eq
absNegation a | inl (inr a<0) | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) -a<0)) a<0))
absNegation a | inl (inr a<0) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (inverseWellDefined additiveGroup 0=-a) (invTwice additiveGroup a))) (invIdent additiveGroup)) (Equivalence.reflexive eq) a<0))
absNegation a | inr 0=a with totality 0G (inverse a)
absNegation a | inr 0=a | inl (inl 0<-a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) 0<-a))
absNegation a | inr 0=a | inl (inr -a<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) (Equivalence.reflexive eq) -a<0))
absNegation a | inr 0=a | inr 0=-a = Equivalence.transitive eq (Equivalence.symmetric eq 0=a) 0=-a

absRespectsTimes : (a b : A) → abs (a * b) ∼ (abs a) * (abs b)
absRespectsTimes a b with totality 0R a
absRespectsTimes a b | inl (inl 0<a) with totality 0R b
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (orderRespectsMultiplication 0<a 0<b) ab<0))
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (orderRespectsMultiplication 0<a 0<b)))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inl 0<ab) with <WellDefined (Equivalence.reflexive eq) ringMinusExtracts (orderRespectsMultiplication 0<a (lemm2 b b<0))
... | bl = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<ab (<WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ bl))))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=ab) (Equivalence.reflexive eq) (posTimesNeg a b 0<a b<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inr ab<0) = exFalso ((irreflexive {0G} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) (Equivalence.reflexive eq) ab<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inl (inr a<0) with totality 0R b
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inl 0<ab) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder 0<ab (<WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0))))
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts'
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=ab *Commutative)) (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0)))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inl 0<ab) = Equivalence.symmetric eq twoNegativesTimes
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (negTimesPos a b a<0 b<0) ab<0))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inr 0=ab = exFalso (exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (negTimesPos a b a<0 b<0))))
absRespectsTimes a b | inl (inr a<0) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inr 0=ab = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (Equivalence.transitive eq (Equivalence.transitive eq timesZero (Equivalence.symmetric eq timesZero)) (*WellDefined (Equivalence.reflexive eq) 0=b))
absRespectsTimes a b | inr 0=a with totality 0R b
absRespectsTimes a b | inr 0=a | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inr ab<0) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (invIdent additiveGroup)) (Equivalence.transitive eq (Equivalence.symmetric eq timesZero) *Commutative)) (*WellDefined 0=a (Equivalence.reflexive eq))
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inl 0<ab) = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inr 0=ab = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) 0<ab))
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inr 0=a | inr 0=b | inr 0=ab = Equivalence.reflexive eq

absNonnegative : {a : A} → (abs a < 0R) → False
absNonnegative {a} pr with totality 0R a
absNonnegative {a} pr | inl (inl x) = irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder x pr)
absNonnegative {a} pr | inl (inr x) = irreflexive {0G} (SetoidPartialOrder.<Transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) pr)) x)
absNonnegative {a} pr | inr x = irreflexive {0G} (<WellDefined (Equivalence.symmetric eq x) (Equivalence.reflexive eq) pr)

absZeroImpliesZero : {a : A} → abs a ∼ 0R → a ∼ 0R
absZeroImpliesZero {a} a=0 with totality 0R a
absZeroImpliesZero {a} a=0 | inl (inl 0<a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) a=0 0<a))
absZeroImpliesZero {a} a=0 | inl (inr a<0) = Equivalence.symmetric eq (lemm3 (inverse a) a (Equivalence.symmetric eq invLeft) (Equivalence.symmetric eq a=0))
absZeroImpliesZero {a} a=0 | inr 0=a = a=0

addingAbsCannotShrink : {a b : A} → 0G < b → 0G < ((abs a) + b)
addingAbsCannotShrink {a} {b} 0<b with totality 0G a
addingAbsCannotShrink {a} {b} 0<b | inl (inl x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities x 0<b)
addingAbsCannotShrink {a} {b} 0<b | inl (inr x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (lemm2 a x) 0<b)
addingAbsCannotShrink {a} {b} 0<b | inr x = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined x (Equivalence.reflexive eq))) 0<b

greaterZeroImpliesEqualAbs : {a : A} → 0R < a → a ∼ abs a
greaterZeroImpliesEqualAbs {a} 0<a with totality 0R a
... | inl (inl _) = Equivalence.reflexive eq
... | inl (inr a<0) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined 0=a (Equivalence.reflexive eq) 0<a))

lessZeroImpliesEqualNegAbs : {a : A} → a < 0R → abs a ∼ inverse a
lessZeroImpliesEqualNegAbs {a} a<0 with totality 0R a
... | inl (inr _) = Equivalence.reflexive eq
... | inl (inl 0<a) = exFalso (irreflexive (SetoidPartialOrder.<Transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined (Equivalence.reflexive eq) 0=a a<0))

absZeroIsZero : abs 0R ∼ 0R
absZeroIsZero with totality 0R 0R
... | inl (inl bad) = exFalso (irreflexive bad)
... | inl (inr bad) = exFalso (irreflexive bad)
... | inr _ = Equivalence.reflexive eq

greaterThanAbsImpliesGreaterThan0 : {a b : A} → (abs a) < b → 0R < b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b with totality 0R a
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inl 0<a) = SetoidPartialOrder.<Transitive pOrder 0<a a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inr a<0) = SetoidPartialOrder.<Transitive pOrder (lemm2 _ a<0) a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inr 0=a = <WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq) a<b

abs1Is1 : abs 1R ∼ 1R
abs1Is1 with totality 0R 1R
abs1Is1 | inl (inl 0<1) = Equivalence.reflexive eq
abs1Is1 | inl (inr 1<0) = exFalso (1<0False 1<0)
abs1Is1 | inr 0=1 = Equivalence.reflexive eq

absBoundedImpliesBounded : {a b : A} → abs a < b → a < b
absBoundedImpliesBounded {a} {b} a<b with totality 0G a
absBoundedImpliesBounded {a} {b} a<b | inl (inl x) = a<b
absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.<Transitive pOrder x (SetoidPartialOrder.<Transitive pOrder (lemm2 a x) a<b)
absBoundedImpliesBounded {a} {b} a<b | inr x = a<b

a-bPos : {a b : A} → ((a ∼ b) → False) → 0R < abs (a + inverse b)
a-bPos {a} {b} a!=b with totality 0R (a + inverse b)
a-bPos {a} {b} a!=b | inl (inl x) = x
a-bPos {a} {b} a!=b | inl (inr x) = lemm2 _ x
a-bPos {a} {b} a!=b | inr x = exFalso (a!=b (transferToRight additiveGroup (Equivalence.symmetric eq x)))


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.AbGroup.TensorProduct where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function hiding (flip)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels

open import Cubical.Relation.Binary

open import Cubical.Data.Nat as ℕ
open import Cubical.Data.Int using (ℤ)
open import Cubical.Data.List
open import Cubical.Data.Sigma
open import Cubical.Data.Sum hiding (map)

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup.Base

private
  variable
    ℓ ℓ' : Level

module _ (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  data _⨂₁_ : Type (ℓ-max ℓ ℓ') where
   _⊗_     : (a : A) → (b : B) → _⨂₁_
   _+⊗_    : (w : _⨂₁_) → (u : _⨂₁_) → _⨂₁_

   +⊗Comm   : (x y : _) → x +⊗ y ≡ y +⊗ x
   +⊗Assoc  : (x y z : _) → x +⊗ (y +⊗ z) ≡ (x +⊗ y) +⊗ z
   +⊗IdL    : (x : _) → (0A ⊗ 0B) +⊗ x ≡ x

   ⊗DistR+⊗ : (x : A) (y z : B) → x ⊗ (y +B z) ≡ ((x ⊗ y) +⊗ (x ⊗ z))
   ⊗DistL+⊗ : (x y : A) (z : B) → (x +A y) ⊗ z ≡ ((x ⊗ z) +⊗ (y ⊗ z))

   ⊗squash : isSet _⨂₁_

module _ {AGr : AbGroup ℓ} {BGr : AbGroup ℓ'} where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  A⊗B = AGr ⨂₁ BGr

  ⊗elimProp : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ}
           → ((x : _) → isProp (C x))
           → (f : (x : A) (b : B) → C (x ⊗ b))
           → (g : ((x y : _) → C x → C y → C (x +⊗ y)))
           → (x : _) → C x
  ⊗elimProp p f g (a ⊗ b) = f a b
  ⊗elimProp p f g (x +⊗ y) = g x y (⊗elimProp p f g x) (⊗elimProp p f g y)
  ⊗elimProp {C = C} p f g (+⊗Comm x y j) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g x y (⊗elimProp p f g x) (⊗elimProp p f g y))
      (g y x (⊗elimProp p f g y) (⊗elimProp p f g x)) (+⊗Comm x y) j
  ⊗elimProp {C = C} p f g (+⊗Assoc x y z j) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g x (y +⊗ z) (⊗elimProp p f g x)
         (g y z (⊗elimProp p f g y) (⊗elimProp p f g z)))
         (g (x +⊗ y) z (g x y (⊗elimProp p f g x)
           (⊗elimProp p f g y)) (⊗elimProp p f g z)) (+⊗Assoc x y z) j
  ⊗elimProp {C = C} p f g (+⊗IdL x i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g (0A ⊗ 0B) x (f 0A 0B) (⊗elimProp p f g x))
      (⊗elimProp p f g x)
      (+⊗IdL x) i
  ⊗elimProp {C = C} p f g (⊗DistR+⊗ x y z i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (f x (y +B z)) (g (x ⊗ y) (x ⊗ z) (f x y) (f x z)) (⊗DistR+⊗ x y z) i
  ⊗elimProp {C = C} p f g (⊗DistL+⊗ x y z i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (f (x +A y) z) (g (x ⊗ z) (y ⊗ z) (f x z) (f y z)) (⊗DistL+⊗ x y z) i
  ⊗elimProp {C = C} p f g (⊗squash x y q r i j) =
    isOfHLevel→isOfHLevelDep 2 {B = C} (λ x → isProp→isSet (p x))
      _ _ (λ j → ⊗elimProp p f g (q j)) (λ j → ⊗elimProp p f g (r j))
          (⊗squash x y q r) i j

  -- Group structure
  0⊗ : AGr ⨂₁ BGr
  0⊗ = 0A ⊗ 0B

  -⊗ : AGr ⨂₁ BGr → AGr ⨂₁ BGr
  -⊗ (a ⊗ b) = (-A a) ⊗ b
  -⊗ (x +⊗ x₁) = -⊗ x +⊗ -⊗ x₁
  -⊗ (+⊗Comm x y i) = +⊗Comm (-⊗ x) (-⊗ y) i
  -⊗ (+⊗Assoc x y z i) = +⊗Assoc (-⊗ x) (-⊗ y) (-⊗ z) i
  -⊗ (+⊗IdL x i) = ((λ i → (GroupTheory.inv1g (AbGroup→Group AGr) i ⊗ 0B) +⊗ -⊗ x)
                   ∙ +⊗IdL (-⊗ x)) i
  -⊗ (⊗DistR+⊗ x y z i) = ⊗DistR+⊗ (-A x) y z i
  -⊗ (⊗DistL+⊗ x y z i) = ((λ i → (GroupTheory.invDistr (AbGroup→Group AGr) x y
                           ∙ +Comm strA (-A y) (-A x)) i ⊗ z)
                           ∙ ⊗DistL+⊗ (-A x) (-A y) z) i
  -⊗ (⊗squash x y p q i j) = ⊗squash _ _ (λ j → -⊗ (p j)) (λ j → -⊗ (q j)) i j

  +⊗IdR : (x : A⊗B) → x +⊗ 0⊗ ≡ x
  +⊗IdR x = +⊗Comm x 0⊗ ∙ +⊗IdL x

  -------------------------------------------------------------------------------
  -- Useful induction principle, which lets us view elements of A ⨂ B as lists
  -- over (A × B). Used for the right cancellation law
  unlist : List (A × B) → AGr ⨂₁ BGr
  unlist [] = 0A ⊗ 0B
  unlist (x ∷ x₁) = (fst x ⊗ snd x) +⊗ unlist x₁

  unlist++ : (x y : List (A × B))  → unlist (x ++ y) ≡ (unlist x +⊗ unlist y)
  unlist++ [] y = sym (+⊗IdL (unlist y))
  unlist++ (x ∷ x₁) y = (λ i → (fst x ⊗ snd x) +⊗ (unlist++ x₁ y i))
                        ∙ +⊗Assoc (fst x ⊗ snd x) (unlist x₁) (unlist y)

  ∃List : (x : AGr ⨂₁ BGr) → ∃[ l ∈ List (A × B) ] (unlist l ≡ x)
  ∃List = ⊗elimProp (λ _ → squash₁)
          (λ a b → ∣ [ a , b ] , +⊗IdR (a ⊗ b) ∣₁)
          λ x y → rec2 squash₁ λ {(l1 , p) (l2 , q) →
                  ∣ (l1 ++ l2) , unlist++ l1 l2 ∙ cong₂ _+⊗_ p q ∣₁}

  ⊗elimPropUnlist : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ}
           → ((x : _) → isProp (C x))
           → ((x : _) → C (unlist x))
           → (x : _) → C x
  ⊗elimPropUnlist {C = C} p f =
    ⊗elimProp p (λ x y → subst C (+⊗IdR (x ⊗ y)) (f [ x , y ]))
      λ x y → PT.rec (isPropΠ2 λ _ _ → p _)
                    (PT.rec (isPropΠ3 λ _ _ _ → p _)
                      (λ {(l1 , p) (l2 , q) ind1 ind2
                        → subst C (unlist++ l2 l1 ∙ cong₂ _+⊗_ q p) (f (l2 ++ l1))})
                      (∃List y))
                    (∃List x)
  -----------------------------------------------------------------------------------

  ⊗AnnihilL : (x : B) → (0A ⊗ x) ≡ 0⊗
  ⊗AnnihilL x = sym (+⊗IdR _)
                 ∙∙ cong ((0A ⊗ x) +⊗_) (sym cancelLem)
                 ∙∙ +⊗Assoc (0A ⊗ x) (0A ⊗ x) (0A ⊗ (-B x))
                 ∙∙ cong (_+⊗ (0A ⊗ (-B x))) inner
                 ∙∙ cancelLem
    where
    cancelLem : (0A ⊗ x) +⊗ (0A ⊗ (-B x)) ≡ 0⊗
    cancelLem = sym (⊗DistR+⊗ 0A x (-B x)) ∙ (λ i → 0A ⊗ +InvR strB x i)

    inner : (0A ⊗ x) +⊗ (0A ⊗ x) ≡ 0A ⊗ x
    inner = sym (⊗DistL+⊗ 0A 0A x) ∙ (λ i → +IdR strA 0A i ⊗ x)

  ⊗AnnihilR : (x : A) → (x ⊗ 0B) ≡ 0⊗
  ⊗AnnihilR x = sym (+⊗IdR _)
                ∙∙ cong ((x ⊗ 0B) +⊗_) (sym cancelLem)
                ∙∙ +⊗Assoc (x ⊗ 0B) (x ⊗ 0B) ((-A x) ⊗ 0B)
                ∙∙ cong (_+⊗ ((-A x) ⊗ 0B)) inner
                ∙∙ cancelLem
    where
    cancelLem : (x ⊗ 0B) +⊗ ((-A x) ⊗ 0B) ≡ 0⊗
    cancelLem = sym (⊗DistL+⊗ x (-A x) 0B) ∙ (λ i → +InvR strA x i ⊗ 0B)

    inner : (x ⊗ 0B) +⊗ (x ⊗ 0B) ≡ x ⊗ 0B
    inner = sym (⊗DistR+⊗ x 0B 0B) ∙ (λ i → x ⊗ +IdR strB 0B i)

  flip : (x : A) (b : B) → x ⊗ (-B b) ≡ ((-A x) ⊗ b)
  flip x b = sym (+⊗IdR _)
             ∙ cong ((x ⊗ (-B b)) +⊗_) (sym cancelLemA)
             ∙ +⊗Assoc (x ⊗ (-B b)) (x ⊗ b) ((-A x) ⊗ b)
             ∙ cong (_+⊗ ((-A x) ⊗ b)) cancelLemB
             ∙ +⊗IdL _
    where
    cancelLemA : (x ⊗ b) +⊗ ((-A x) ⊗ b) ≡ 0⊗
    cancelLemA = sym (⊗DistL+⊗ x (-A x) b) ∙ (λ i → +InvR strA x i ⊗ b) ∙ ⊗AnnihilL b

    cancelLemB : (x ⊗ (-B b)) +⊗ (x ⊗ b) ≡ 0⊗
    cancelLemB = sym (⊗DistR+⊗ x (-B b) b) ∙ (λ i → x ⊗ +InvL strB b i) ∙ ⊗AnnihilR x

  +⊗InvR : (x : AGr ⨂₁ BGr) → (x +⊗ -⊗ x) ≡ 0⊗
  +⊗InvR =
    ⊗elimPropUnlist (λ _ → ⊗squash _ _) h
    where
    h : (x : List (A × B)) → (unlist x +⊗ -⊗ (unlist x)) ≡ 0⊗
    h [] = sym (⊗DistL+⊗ 0A (-A 0A) (0B))
            ∙ cong (λ x →  _⊗_ {AGr = AGr} {BGr = BGr} x 0B) (+InvR strA 0A)
    h (x ∷ x₁) = move4 (fst x ⊗ snd x) (unlist x₁) ((-A fst x) ⊗ snd x) (-⊗ (unlist x₁))
                       _+⊗_ +⊗Assoc +⊗Comm
                 ∙∙ cong₂ _+⊗_ (sym (⊗DistL+⊗ (fst x) (-A (fst x)) (snd x))
                               ∙∙ (λ i → +InvR strA (fst x) i ⊗ (snd x))
                               ∙∙ ⊗AnnihilL (snd x))
                               (h x₁)
                 ∙∙ +⊗IdR 0⊗

  +⊗InvL : (x : AGr ⨂₁ BGr) → (-⊗ x +⊗ x) ≡ 0⊗
  +⊗InvL x = +⊗Comm _ _ ∙ +⊗InvR x

module _ where
  open AbGroupStr

  _⨂_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
  fst (A ⨂ B) = A ⨂₁ B
  0g (snd (A ⨂ B)) = 0⊗
  AbGroupStr._+_ (snd (A ⨂ B)) = _+⊗_
  AbGroupStr.- snd (A ⨂ B) = -⊗
  isAbGroup (snd (A ⨂ B)) = makeIsAbGroup ⊗squash +⊗Assoc +⊗IdR +⊗InvR +⊗Comm

-------------- Elimination principle into AbGroups --------------
module _ {ℓ ℓ' : Level} {A : AbGroup ℓ}  {B : AbGroup ℓ'} where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G)
    _+A_ = _+G_ (snd A)
    _+B_ = _+G_ (snd B)

    0A = 0g (snd A)
    0B = 0g (snd B)

  ⨂→AbGroup-elim : ∀ {ℓ} (C : AbGroup ℓ)
         → (f : (fst A × fst B) → fst C)
         → (f (0A , 0B) ≡ 0g (snd C))
         → (linR : (a : fst A) (x y : fst B)
                 → f (a , x +B y) ≡ _+G_ (snd C) (f (a , x)) (f (a , y)))
         → (linL : (x y : fst A) (b : fst B)
                 → f (x +A y , b) ≡ _+G_ (snd C) (f (x , b)) (f (y , b)))
         → A ⨂₁ B → fst C
  ⨂→AbGroup-elim C f p linR linL (a ⊗ b) = f (a , b)
  ⨂→AbGroup-elim C f p linR linL (x +⊗ x₁) =
    _+G_ (snd C) (⨂→AbGroup-elim C f p linR linL x)
                 (⨂→AbGroup-elim C f p linR linL x₁)
  ⨂→AbGroup-elim C f p linR linL (+⊗Comm x x₁ i) =
    +Comm (snd C) (⨂→AbGroup-elim C f p linR linL x)
                  (⨂→AbGroup-elim C f p linR linL x₁) i
  ⨂→AbGroup-elim C f p linR linL (+⊗Assoc x x₁ x₂ i) =
    +Assoc (snd C) (⨂→AbGroup-elim C f p linR linL x)
                   (⨂→AbGroup-elim C f p linR linL x₁)
                   (⨂→AbGroup-elim C f p linR linL x₂) i
  ⨂→AbGroup-elim C f p linR linL (+⊗IdL x i) =
    (cong (λ y → (snd C +G y) (⨂→AbGroup-elim C f p linR linL x)) p
                     ∙ (+IdL (snd C) (⨂→AbGroup-elim C f p linR linL x))) i
  ⨂→AbGroup-elim C f p linR linL (⊗DistR+⊗ x y z i) = linR x y z i
  ⨂→AbGroup-elim C f p linR linL (⊗DistL+⊗ x y z i) = linL x y z i
  ⨂→AbGroup-elim C f p linR linL (⊗squash x x₁ x₂ y i i₁) =
    is-set (snd C) _ _
           (λ i → ⨂→AbGroup-elim C f p linR linL (x₂ i))
           (λ i → ⨂→AbGroup-elim C f p linR linL (y i)) i i₁

  ⨂→AbGroup-elim-hom : ∀ {ℓ} (C : AbGroup ℓ)
        → (f : (fst A × fst B) → fst C) (linR : _) (linL : _) (p : _)
        → AbGroupHom (A ⨂ B) C
  fst (⨂→AbGroup-elim-hom C f linR linL p) = ⨂→AbGroup-elim C f p linR linL
  snd (⨂→AbGroup-elim-hom C f linR linL p) = makeIsGroupHom (λ x y → refl)

private
  _* = AbGroup→Group

----------- Definition of universal property ------------
tensorFun : (A : Group ℓ) (B : Group ℓ') (T C : AbGroup (ℓ-max ℓ ℓ'))
            (f : GroupHom A (HomGroup B T *))
            → GroupHom (T *) (C *)
            → GroupHom A (HomGroup B C *)
fst (fst (tensorFun A B T C (f , p) (g , q)) a) b = g (fst (f a) b)
snd (fst (tensorFun A B T C (f , p) (g , q)) a) =
     makeIsGroupHom
     λ x y → cong g (IsGroupHom.pres· (snd (f a)) x y)
              ∙ IsGroupHom.pres· q _ _
snd (tensorFun A B T C (f , p) (g , q)) =
     makeIsGroupHom
     λ x y → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                     (funExt λ b → cong g (funExt⁻ (cong fst (IsGroupHom.pres· p x y)) b)
                                    ∙ IsGroupHom.pres· q _ _)

isTensorProductOf_and_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')→ Type _
isTensorProductOf_and_ {ℓ} {ℓ'} A B T =
  Σ[ f ∈ GroupHom (A *) ((HomGroup (B *) T) *) ]
    ((C : AbGroup (ℓ-max ℓ ℓ')) → isEquiv {A = GroupHom (T *) (C *)}
                                           {B = GroupHom (A *) ((HomGroup (B *) C) *)}
                                           (tensorFun (A *) (B *) T C f))

------ _⨂_ satisfies the universal property --------
module UP (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  mainF : GroupHom (AGr *) (HomGroup (BGr *) (AGr ⨂ BGr) *)
  fst (fst mainF a) b = a ⊗ b
  snd (fst mainF a) = makeIsGroupHom (⊗DistR+⊗ a)
  snd mainF = makeIsGroupHom
              λ x y → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                              (funExt (⊗DistL+⊗ x y))

  isTensorProduct⨂ : (isTensorProductOf AGr and BGr) (AGr ⨂ BGr)
  fst isTensorProduct⨂ = mainF
  snd isTensorProduct⨂ C = isoToIsEquiv mainIso
    where
    invF : GroupHom (AGr *) (HomGroup (BGr *) C *) → GroupHom ((AGr ⨂ BGr) *) (C *)
    fst (invF (f , p)) = F
      where
      lem : f (0g (snd AGr)) .fst (0g (snd BGr)) ≡ 0g (snd C)
      lem = funExt⁻ (cong fst (IsGroupHom.pres1 p)) (0g (snd BGr))
      F : ((AGr ⨂ BGr) *) .fst → (C *) .fst
      F (a ⊗ b) = f a .fst b
      F (x +⊗ x₁) = _+G_ (snd C) (F x) (F x₁)
      F (+⊗Comm x x₁ i) = +Comm (snd C) (F x) (F x₁) i
      F (+⊗Assoc x y z i) = +Assoc (snd C) (F x) (F y) (F z) i
      F (+⊗IdL x i) = (cong (λ y → _+G_ (snd C) y (F x)) lem ∙ +IdL (snd C) (F x)) i
      F (⊗DistR+⊗ x y z i) = IsGroupHom.pres· (f x .snd) y z i
      F (⊗DistL+⊗ x y z i) = fst (IsGroupHom.pres· p x y i) z
      F (⊗squash x x₁ x₂ y i i₁) = is-set (snd C) (F x) (F x₁)
                                   (λ i → F (x₂ i)) (λ i → F (y i)) i i₁
    snd (invF (f , p)) = makeIsGroupHom λ x y → refl

    mainIso : Iso (GroupHom ((AGr ⨂ BGr) *) (C *))
                  (GroupHom (AGr *) (HomGroup (BGr *) C *))
    Iso.fun mainIso = _
    Iso.inv mainIso = invF
    Iso.rightInv mainIso (f , p) = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                                   (funExt λ a → Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl)
    Iso.leftInv mainIso (f , p) =
        Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                (funExt (⊗elimProp (λ _ → is-set (snd C) _ _)
                                   (λ _ _ → refl)
                                    λ x y ind1 ind2 → cong₂ (_+G_ (snd C)) ind1 ind2
                                                       ∙ sym (IsGroupHom.pres· p x y)))

-------------------- Commutativity ------------------------
commFun : ∀ {ℓ ℓ'} {A : AbGroup ℓ}  {B : AbGroup ℓ'} → A ⨂₁ B → B ⨂₁ A
commFun (a ⊗ b) = b ⊗ a
commFun (x +⊗ x₁) = commFun x +⊗ commFun x₁
commFun (+⊗Comm x x₁ i) = +⊗Comm (commFun x) (commFun x₁) i
commFun (+⊗Assoc x x₁ x₂ i) = +⊗Assoc (commFun x) (commFun x₁) (commFun x₂) i
commFun (+⊗IdL x i) = +⊗IdL (commFun x) i
commFun (⊗DistR+⊗ x y z i) = ⊗DistL+⊗ y z x i
commFun (⊗DistL+⊗ x y z i) = ⊗DistR+⊗ z x y i
commFun (⊗squash x x₁ x₂ y i i₁) = ⊗squash (commFun x) (commFun x₁)
                                           (λ i → commFun (x₂ i)) (λ i → commFun (y i)) i i₁

commFun²≡id : ∀ {ℓ ℓ'} {A : AbGroup ℓ}  {B : AbGroup ℓ'} (x : A ⨂₁ B)
               → commFun (commFun x) ≡ x
commFun²≡id = ⊗elimProp (λ _ → ⊗squash _ _)
                        (λ _ _ → refl)
                        (λ _ _ p q → cong₂ _+⊗_ p q)

⨂-commIso : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'}
          → GroupIso ((A ⨂ B) *) ((B ⨂ A) *)
Iso.fun (fst ⨂-commIso) = commFun
Iso.inv (fst ⨂-commIso) = commFun
Iso.rightInv (fst ⨂-commIso) = commFun²≡id
Iso.leftInv (fst ⨂-commIso) = commFun²≡id
snd ⨂-commIso = makeIsGroupHom λ x y → refl

⨂-comm : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} → AbGroupEquiv (A ⨂ B) (B ⨂ A)
fst ⨂-comm = isoToEquiv (fst (⨂-commIso))
snd ⨂-comm = snd ⨂-commIso

open AbGroupStr

-------------------- Associativity ------------------------
module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where
  private
    f : (c : fst C) → AbGroupHom (A ⨂ B) (A ⨂ (B ⨂ C))
    f c = ⨂→AbGroup-elim-hom (A ⨂ (B ⨂ C))
                               (λ ab → (fst ab) ⊗ ((snd ab) ⊗ c))
                               (λ a b b' → (λ i → a ⊗ (⊗DistL+⊗ b b' c i)) ∙ ⊗DistR+⊗ a (b ⊗ c) (b' ⊗ c))
                               (λ a a' b → ⊗DistL+⊗ a a' (b ⊗ c))
                               (⊗AnnihilL _ ∙ sym (⊗AnnihilL _))

  assocHom : AbGroupHom ((A ⨂ B) ⨂ C) (A ⨂ (B ⨂ C))
  assocHom = ⨂→AbGroup-elim-hom (A ⨂ (B ⨂ C))
                                  (λ x → f (snd x) .fst (fst x))
                                  helper
                                  (λ x y b → IsGroupHom.pres· (snd (f b)) x y)
                                  refl
    where
    helper : _
    helper = ⊗elimProp (λ _ → isPropΠ2 λ _ _ → ⊗squash _ _)
                       (λ a b x y → (λ i → a ⊗ (⊗DistR+⊗ b x y i))
                                     ∙∙ ⊗DistR+⊗ a (b ⊗ x) (b ⊗ y)
                                     ∙∙ refl)
                       λ a b ind1 ind2 x y → cong₂ _+⊗_ (ind1 x y) (ind2 x y)
                                              ∙∙ move4 (f x .fst a) (f y .fst a) (f x .fst b) (f y .fst b)
                                                       _+⊗_ +⊗Assoc +⊗Comm
                                              ∙∙ cong₂ _+⊗_
                                                       (sym (IsGroupHom.pres· (snd (f x)) a b))
                                                       (IsGroupHom.pres· (snd (f y)) a b)

module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where
  private
    f' : (a : fst A) → AbGroupHom (B ⨂ C) ((A ⨂ B) ⨂ C)
    f' a = ⨂→AbGroup-elim-hom
               ((A ⨂ B) ⨂ C)
               (λ bc → (a ⊗ fst bc) ⊗ snd bc)
               (λ x y b → ⊗DistR+⊗ (a ⊗ x) y b)
               (λ x y b → (λ i → (⊗DistR+⊗ a x y i) ⊗ b)
                           ∙ ⊗DistL+⊗ (a ⊗ x) (a ⊗ y) b)
               λ i → ⊗AnnihilR a i ⊗ (0g (snd C))

  assocHom⁻ : AbGroupHom (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C)
  assocHom⁻ = ⨂→AbGroup-elim-hom
                  ((A ⨂ B) ⨂ C)
                  (λ abc → f' (fst abc) .fst (snd abc))
                  (λ a → IsGroupHom.pres· (snd (f' a)))
                  helper
                  refl
       where
       helper : _
       helper = λ x y → ⊗elimProp
                         (λ _ → ⊗squash _ _)
                         (λ b c → (λ i → ⊗DistL+⊗ x y b i ⊗ c)
                                           ∙ ⊗DistL+⊗ (x ⊗ b) (y ⊗ b) c)
                          λ a b ind1 ind2 → cong₂ _+⊗_ ind1 ind2
                                             ∙∙ move4 _ _ _ _ _+⊗_ +⊗Assoc +⊗Comm
                                             ∙∙ cong₂ _+⊗_ (IsGroupHom.pres· (snd (f' x)) a b)
                                                (IsGroupHom.pres· (snd (f' y)) a b)

  ⨂assocIso : Iso (A ⨂₁ (B ⨂ C)) ((A ⨂ B) ⨂₁ C)
  Iso.fun ⨂assocIso = fst assocHom⁻
  Iso.inv ⨂assocIso = fst assocHom
  Iso.rightInv ⨂assocIso =
    ⊗elimProp (λ _ → ⊗squash _ _)
               (⊗elimProp (λ _ → isPropΠ (λ _ → ⊗squash _ _))
                           (λ a b c → refl)
                           λ a b ind1 ind2 c → cong₂ _+⊗_ (ind1 c) (ind2 c)
                                                ∙ sym (⊗DistL+⊗ a b c))
                λ x y p q → cong (fst assocHom⁻) (IsGroupHom.pres· (snd assocHom) x y)
                             ∙∙ IsGroupHom.pres· (snd assocHom⁻) (fst assocHom x) (fst assocHom y)
                             ∙∙ cong₂ _+⊗_ p q
  Iso.leftInv ⨂assocIso =
    ⊗elimProp (λ _ → ⊗squash _ _)
               (λ a → ⊗elimProp (λ _ → ⊗squash _ _)
                                  (λ b c → refl)
                                   λ x y ind1 ind2 →
                                        cong (fst assocHom ∘ fst assocHom⁻) (⊗DistR+⊗ a x y)
                                     ∙∙ cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) (a ⊗ x) (a ⊗ y))
                                     ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ (a ⊗ x)) (fst assocHom⁻ (a ⊗ y))
                                     ∙∙ cong₂ _+⊗_ ind1 ind2
                                     ∙∙ sym (⊗DistR+⊗ a x y))
                λ x y p q → cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) x y)
                             ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ x) (fst assocHom⁻ y)
                             ∙∙ cong₂ _+⊗_ p q

  ⨂assoc : AbGroupEquiv (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C)
  fst ⨂assoc = isoToEquiv ⨂assocIso
  snd ⨂assoc = snd assocHom⁻

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module int where

open import bool
open import eq
open import nat
open import product

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data pol : Set where
  pos : pol
  neg : pol

data sign : Set where
  nonzero : pol → sign
  zero : sign

data int : sign → Set where
  +0 : int zero
  unit : ∀ {p : pol} → int (nonzero p)
  next_ : ∀ {p : pol} → int (nonzero p) → int (nonzero p)

data nonneg : sign → Set where
  pos-nonneg : nonneg (nonzero pos)
  zero-nonneg : nonneg zero

data nonpos : sign → Set where
  neg-nonpos : nonpos (nonzero neg)
  zero-nonpos : nonpos zero

ℤ = Σi sign int

ℤ-≥-0 = Σi sign (λ s → nonneg s × int s)

ℤ-≤-0 = Σi sign (λ s → nonpos s × int s)

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixl 6 _+ℤ_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

eq-pol : pol → pol → 𝔹
eq-pol pos pos = tt
eq-pol neg neg = tt
eq-pol pos neg = ff
eq-pol neg pos = ff

{- add a unit with the given polarity to the given int (so if the polarity
   is pos we are adding one, if it is neg we are subtracting one).
   Return the new int, together with its sign, which could change. -}
add-unit : pol → ∀{s : sign} → int s → ℤ
add-unit p +0 = , unit{p}
add-unit p (unit{p'}) = if eq-pol p p' then , next (unit{p}) else , +0
add-unit p (next_{p'} x) = if eq-pol p p' then , next (next x) else , x

_+ℤ_ : ℤ → ℤ → ℤ
(, +0) +ℤ (, x) = , x
(, x) +ℤ (, +0) = , x
(, x) +ℤ (, unit{p}) = add-unit p x
(, unit{p}) +ℤ (, x) = add-unit p x
(, next_{p} x) +ℤ (, next_{p'} y) with ((, x) +ℤ (, next y))
... | , r = add-unit p r

ℕ-to-ℤ : ℕ → ℤ-≥-0
ℕ-to-ℤ zero = , (zero-nonneg , +0)
ℕ-to-ℤ (suc x) with ℕ-to-ℤ x
... | , (zero-nonneg , y) = , ( pos-nonneg , unit )
... | , (pos-nonneg , y) = , ( pos-nonneg , next y)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Int where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Int
  renaming (ℤ to ℤType ; _+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Properties

open GroupStr

ℤ : Group₀
fst ℤ = ℤType
1g (snd ℤ) = 0
_·_ (snd ℤ) = _+ℤ_
inv (snd ℤ) = _-ℤ_ 0
isGroup (snd ℤ) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos 0) _+ℤ_ (_-ℤ_ (pos 0))
    isGroupℤ = makeIsGroup isSetℤ +Assoc (λ _ → refl) (+Comm 0)
                           (λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
                           (λ x → minusPlus x 0)

ℤHom : (n : ℤType) → GroupHom ℤ ℤ
fst (ℤHom n) x = n ·ℤ x
snd (ℤHom n) =
  makeIsGroupHom λ x y → ·DistR+ n x y

negEquivℤ : GroupEquiv ℤ ℤ
fst negEquivℤ =
  isoToEquiv
    (iso (GroupStr.inv (snd ℤ))
         (GroupStr.inv (snd ℤ))
         (GroupTheory.invInv ℤ)
         (GroupTheory.invInv ℤ))
snd negEquivℤ =
  makeIsGroupHom λ x y
    → +Comm (pos 0) (-ℤ (x +ℤ y))
    ∙ -Dist+ x y
    ∙ cong₂ _+ℤ_ (+Comm (-ℤ x) (pos 0)) (+Comm (-ℤ y) (pos 0))

max_stars_repo_name: MatthiasHu/cubical