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

open import HoTT

-- an attempt to speed up [QuotGroup (im-nprop ...)]
-- which removes most intermediate constructions

module groups.Cokernel {i j}
  {G : Group i} {H : Group j}
  (φ : G →ᴳ H) (H-ab : is-abelian H) where

  --  G ---φ--→ᴳ H

  private
    module G = Group G
    module H = AbGroup (H , H-ab)
    module φ = GroupHom φ

  coker-rel : Rel H.El (lmax i j)
  coker-rel h₁ h₂ = Trunc -1 (hfiber φ.f (H.diff h₁ h₂))

  private
    coker-El : Type (lmax i j)
    coker-El = SetQuot coker-rel

  coker-struct : GroupStructure coker-El
  coker-struct = record {M} where
    module M where
      ident : coker-El
      ident = q[ H.ident ]

      inv : coker-El → coker-El
      inv = SetQuot-rec SetQuot-level inv' inv-rel
        where
          inv' : H.El → coker-El
          inv' h = q[ H.inv h ]

          abstract
            inv-rel : ∀ {h₁ h₂} → coker-rel h₁ h₂ → inv' h₁ == inv' h₂
            inv-rel {h₁} {h₂} = Trunc-rec (SetQuot-level _ _)
              λ{(g , φg=h₁h₂⁻¹) → quot-rel
                [ G.inv g , φ.pres-inv g ∙ ap H.inv φg=h₁h₂⁻¹
                          ∙ H.inv-diff h₁ h₂ ∙ H.comm h₂ (H.inv h₁)
                          ∙ ap (H.comp (H.inv h₁)) (! (H.inv-inv h₂)) ]}

      comp : coker-El → coker-El → coker-El
      comp = SetQuot-rec level comp' comp-rel where
        abstract
          level : is-set (coker-El → coker-El)
          level = →-is-set SetQuot-level

        comp' : H.El → coker-El → coker-El
        comp' h₁ = SetQuot-rec SetQuot-level comp'' comp'-rel where

          comp'' : H.El → coker-El
          comp'' h₂ = q[ H.comp h₁ h₂ ]

          abstract
            comp'-rel : ∀ {h₂ h₂'} → coker-rel h₂ h₂' → comp'' h₂ == comp'' h₂'
            comp'-rel {h₂} {h₂'} = Trunc-rec (SetQuot-level _ _)
              λ{(g , φg=h₂h₂'⁻¹) → quot-rel
                [ g , ! ( ap (H.comp (H.comp h₁ h₂)) (H.inv-comp h₁ h₂')
                        ∙ H.assoc h₁ h₂ (H.comp (H.inv h₂') (H.inv h₁))
                        ∙ ap (H.comp h₁) (! $ H.assoc h₂ (H.inv h₂') (H.inv h₁))
                        ∙ H.comm h₁ (H.comp (H.comp h₂ (H.inv h₂')) (H.inv h₁))
                        ∙ H.assoc (H.comp h₂ (H.inv h₂')) (H.inv h₁) h₁
                        ∙ ap2 H.comp (! φg=h₂h₂'⁻¹) (H.inv-l h₁)
                        ∙ H.unit-r (φ.f g) )]}

        abstract
          comp-rel : ∀ {h₁ h₁'} → coker-rel h₁ h₁' → comp' h₁ == comp' h₁'
          comp-rel {h₁} {h₁'} = Trunc-rec (level _ _)
            λ{(g , φg=h₁h₁'⁻¹) → λ= $ SetQuot-elim (λ _ → =-preserves-set SetQuot-level)
              (λ h₂ → quot-rel
                  [ g , ! ( ap (H.comp (H.comp h₁ h₂)) (H.inv-comp h₁' h₂)
                          ∙ H.assoc h₁ h₂ (H.comp (H.inv h₂) (H.inv h₁'))
                          ∙ ap (H.comp h₁) ( ! (H.assoc h₂ (H.inv h₂) (H.inv h₁'))
                                          ∙ ap (λ h → H.comp h (H.inv h₁')) (H.inv-r h₂)
                                          ∙ H.unit-l (H.inv h₁'))
                          ∙ ! φg=h₁h₁'⁻¹ )])
              (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))}

      abstract
        unit-l : ∀ cok → comp ident cok == cok
        unit-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ h → ap q[_] $ H.unit-l h)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

        assoc : ∀ cok₁ cok₂ cok₃ → comp (comp cok₁ cok₂) cok₃ == comp cok₁ (comp cok₂ cok₃)
        assoc = SetQuot-elim
          (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
          (λ h₁ → SetQuot-elim
            (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
            (λ h₂ → SetQuot-elim
              (λ _ → =-preserves-set SetQuot-level)
              (λ h₃ → ap q[_] $ H.assoc h₁ h₂ h₃)
              (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _)))
            (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _)))
          (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → SetQuot-level _ _))

        inv-l : ∀ cok → comp (inv cok) cok == ident
        inv-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ h → ap q[_] $ H.inv-l h)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

  Coker : Group (lmax i j)
  Coker = group _ SetQuot-level coker-struct

  module Coker = Group Coker

  {- correctness -}

  Coker-β : Coker ≃ᴳ QuotGroup (im-npropᴳ φ H-ab)
  Coker-β = ≃-to-≃ᴳ (ide _) to-pres-comp where
    abstract
      to-pres-comp : preserves-comp Coker.comp
        (QuotGroup.comp (im-npropᴳ φ H-ab)) (idf _)
      to-pres-comp = SetQuot-elim
        (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
        (λ _ → SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ _ → idp)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _)))
        (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.Intersection.Definition {a b : _} {A : Set a} (S : Setoid {a} {b} A) where

open Setoid S
open Equivalence eq
open import Setoids.Subset S

intersectionPredicate : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → A → Set (c ⊔ d)
intersectionPredicate {pred1 = pred1} {pred2} s1 s2 a = pred1 a && pred2 a

intersection : {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset pred1) (s2 : subset pred2) → subset (intersectionPredicate s1 s2)
intersection s1 s2 {x1} {x2} x1=x2 (inS1 ,, inS2) = s1 x1=x2 inS1 ,, s2 x1=x2 inS2

ext: agda


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

module Control.Monad.State where

open import Prelude

record StatePair {s a} (S : Type s) (A : Type a) : Type (a ℓ⊔ s) where
  constructor state-pair
  field
    value : A
    state : S
open StatePair public

State : ∀ {s a} → Type s → Type a → Type (s ℓ⊔ a)
State S A = S → StatePair S A

private
  variable
    s : Level
    S : Type s

pure : A → State S A
pure = state-pair

_<*>_ : State S (A → B) → State S A → State S B
(fs <*> xs) s =
  let state-pair f s′ = fs s
      state-pair x s″ = xs s′
  in state-pair (f x) s″

_>>=_ : State S A → (A → State S B) → State S B
(xs >>= f) s = let state-pair x s′ = xs s in f x s′

get : State S S
value (get s) = s
state (get s) = s

modify : (S → S) → State S ⊤
value (modify f s) = tt
state (modify f s) = f s

put : S → State S ⊤
value (put s _) = tt
state (put s _) = s

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Unit

module Oscar.Class.SimilarityM where

module SimilarityM
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  (_∼₁_ : 𝔄 → 𝔄 → Ø 𝔞̇)
  (_∼₂_ : 𝔅 → 𝔅 → Ø 𝔟̇) (let _∼₂_ = _∼₂_; infix 4 _∼₂_)
  (_◃_ : 𝔉 → 𝔄 → 𝔅) (let _◃_ = _◃_; infix 16 _◃_)
  x y
  = ℭLASS (_◃_ , _∼₁_ , _∼₂_ , x , y) (∀ f → x ∼₁ y → f ◃ x ∼₂ f ◃ y)

module _
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  {∼₁ : 𝔄 → 𝔄 → Ø 𝔞̇}
  {∼₂ : 𝔅 → 𝔅 → Ø 𝔟̇}
  {◃ : 𝔉 → 𝔄 → 𝔅}
  {x y}
  where
  similarityM = SimilarityM.method ∼₁ ∼₂ ◃ x y
  instance SimilarityM--Unit : ⦃ _ : SimilarityM.class ∼₁ ∼₂ ◃ x y ⦄ → Unit.class (SimilarityM.type ∼₁ ∼₂ ◃ x y)
           SimilarityM--Unit .⋆ = similarityM


text:
{-

Definition of a homogeneous pointed type, and proofs that pi, product, path, and discrete types are homogeneous

Portions of this file adapted from Nicolai Kraus' code here:
  https://bitbucket.org/nicolaikraus/agda/src/e30d70c72c6af8e62b72eefabcc57623dd921f04/trunc-inverse.lagda

-}
{-# OPTIONS --safe #-}
module Cubical.Foundations.Pointed.Homogeneous where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary

open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Structures.Pointed

isHomogeneous : ∀ {ℓ} → Pointed ℓ → Type (ℓ-suc ℓ)
isHomogeneous {ℓ} (A , x) = ∀ y → Path (Pointed ℓ) (A , x) (A , y)

-- Pointed functions into a homogeneous type are equal as soon as they are equal
-- as unpointed functions
→∙Homogeneous≡ : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'} {f∙ g∙ : A∙ →∙ B∙}
  (h : isHomogeneous B∙) → f∙ .fst ≡ g∙ .fst → f∙ ≡ g∙
→∙Homogeneous≡ {A∙ = A∙@(_ , a₀)} {B∙@(B , _)} {f∙@(_ , f₀)} {g∙@(_ , g₀)} h p =
  subst (λ Q∙ → PathP (λ i → A∙ →∙ Q∙ i) f∙ g∙) (sym (flipSquare fix)) badPath
  where
  badPath : PathP (λ i → A∙ →∙ (B , (sym f₀ ∙∙ funExt⁻ p a₀ ∙∙ g₀) i)) f∙ g∙
  badPath i .fst = p i
  badPath i .snd j = doubleCompPath-filler (sym f₀) (funExt⁻ p a₀) g₀ j i

  fix : PathP (λ i → B∙ ≡ (B , (sym f₀ ∙∙ funExt⁻ p a₀ ∙∙ g₀) i)) refl refl
  fix i =
    hcomp
      (λ j → λ
        { (i = i0) → lCancel (h (pt B∙)) j
        ; (i = i1) → lCancel (h (pt B∙)) j
        })
      (sym (h (pt B∙)) ∙ h ((sym f₀ ∙∙ funExt⁻ p a₀ ∙∙ g₀) i))

→∙Homogeneous≡Path : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'} {f∙ g∙ : A∙ →∙ B∙}
  (h : isHomogeneous B∙) → (p q : f∙ ≡ g∙) → cong fst p ≡ cong fst q → p ≡ q
→∙Homogeneous≡Path {A∙ = A∙@(A , a₀)} {B∙@(B , b)} {f∙@(f , f₀)} {g∙@(g , g₀)} h p q r =
  transport (λ k
      → PathP (λ i
        → PathP (λ j → (A , a₀) →∙ newPath-refl p q r i j (~ k))
                 (f , f₀) (g , g₀)) p q)
      (badPath p q r)
  where
  newPath : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q)
    → Square (refl {x = b}) refl refl refl
  newPath p q r i j =
    hcomp (λ k → λ {(i = i0) → cong snd p j k
                   ; (i = i1) → cong snd q j k
                   ; (j = i0) → f₀ k
                   ; (j = i1) → g₀ k})
          (r i j a₀)

  newPath-refl : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q)
         → PathP (λ i → (PathP (λ j → B∙ ≡ (B , newPath p q r i j))) refl refl) refl refl
  newPath-refl p q r i j k =
    hcomp (λ w → λ { (i = i0) → lCancel (h b) w k
                    ; (i = i1) → lCancel (h b) w k
                    ; (j = i0) → lCancel (h b) w k
                    ; (j = i1) → lCancel (h b) w k
                    ; (k = i0) → lCancel (h b) w k
                    ; (k = i1) → B , newPath p q r i j})
          ((sym (h b) ∙ h (newPath p q r i j)) k)

  badPath : (p q : f∙ ≡ g∙) (r : cong fst p ≡ cong fst q)
    → PathP (λ i →
        PathP (λ j → A∙ →∙ (B , newPath p q r i j))
             (f , f₀) (g , g₀))
              p q
  fst (badPath p q r i j) = r i j
  snd (badPath p q s i j) k =
    hcomp (λ r → λ { (i = i0) → snd (p j) (r ∧ k)
                    ; (i = i1) → snd (q j) (r ∧ k)
                    ; (j = i0) → f₀ (k ∧ r)
                    ; (j = i1) → g₀ (k ∧ r)
                    ; (k = i0) → s i j a₀})
          (s i j a₀)

isHomogeneousPi : ∀ {ℓ ℓ'} {A : Type ℓ} {B∙ : A → Pointed ℓ'}
                 → (∀ a → isHomogeneous (B∙ a)) → isHomogeneous (Πᵘ∙ A B∙)
isHomogeneousPi h f i .fst = ∀ a → typ (h a (f a) i)
isHomogeneousPi h f i .snd a = pt (h a (f a) i)

isHomogeneousΠ∙ : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : typ A → Type ℓ')
                  → (b₀ : B (pt A))
                  → ((a : typ A) (x : B a) → isHomogeneous (B a , x))
                  → (f : Π∙ A B b₀)
                  → isHomogeneous (Π∙ A B b₀ , f)
fst (isHomogeneousΠ∙ A B b₀ h f g i) =
  Σ[ r ∈ ((a : typ A) → fst ((h a (fst f a) (fst g a)) i)) ]
    r (pt A) ≡ hcomp (λ k → λ {(i = i0) → snd f k
                              ; (i = i1) → snd g k})
                     (snd (h (pt A) (fst f (pt A)) (fst g (pt A)) i))
snd (isHomogeneousΠ∙ A B b₀ h f g i) =
    (λ a → snd (h a (fst f a) (fst g a) i))
  , λ j → hcomp (λ k → λ { (i = i0) → snd f (k ∧ j)
                          ; (i = i1) → snd g (k ∧ j)
                          ; (j = i0) → snd (h (pt A) (fst f (pt A))
                                                      (fst g (pt A)) i)})
                 (snd (h (pt A) (fst f (pt A)) (fst g (pt A)) i))

isHomogeneous→∙ : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'}
  → isHomogeneous B∙ → isHomogeneous (A∙ →∙ B∙ ∙)
isHomogeneous→∙ {A∙ = A∙} {B∙} h f∙ =
  ΣPathP
    ( (λ i → Π∙ A∙ (λ a → T a i) (t₀ i))
    , PathPIsoPath _ _ _ .Iso.inv
        (→∙Homogeneous≡ h
          (PathPIsoPath (λ i → (a : typ A∙) → T a i) (λ _ → pt B∙) _ .Iso.fun
            (λ i a → pt (h (f∙ .fst a) i))))
    )
  where
  T : ∀ a → typ B∙ ≡ typ B∙
  T a i = typ (h (f∙ .fst a) i)

  t₀ : PathP (λ i → T (pt A∙) i) (pt B∙) (pt B∙)
  t₀ = cong pt (h (f∙ .fst (pt A∙))) ▷ f∙ .snd

isHomogeneousProd : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'}
                   → isHomogeneous A∙ → isHomogeneous B∙ → isHomogeneous (A∙ ×∙ B∙)
isHomogeneousProd hA hB (a , b) i .fst = typ (hA a i) × typ (hB b i)
isHomogeneousProd hA hB (a , b) i .snd .fst = pt (hA a i)
isHomogeneousProd hA hB (a , b) i .snd .snd = pt (hB b i)

isHomogeneousPath : ∀ {ℓ} (A : Type ℓ) {x y : A} (p : x ≡ y) → isHomogeneous ((x ≡ y) , p)
isHomogeneousPath A {x} {y} p q
  = pointed-sip ((x ≡ y) , p) ((x ≡ y) , q) (eqv , compPathr-cancel p q)
  where eqv : (x ≡ y) ≃ (x ≡ y)
        eqv = compPathlEquiv (q ∙ sym p)

module HomogeneousDiscrete {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) (y : typ A∙) where

  -- switches pt A∙ with y
  switch : typ A∙ → typ A∙
  switch x with dA x (pt A∙)
  ...         | yes _ = y
  ...         | no _ with dA x y
  ...                | yes _  = pt A∙
  ...                | no  _  = x

  switch-ptA∙ : switch (pt A∙) ≡ y
  switch-ptA∙ with dA (pt A∙) (pt A∙)
  ...         | yes _ = refl
  ...         | no ¬p = ⊥.rec (¬p refl)

  switch-idp : ∀ x → switch (switch x) ≡ x
  switch-idp x with dA x (pt A∙)
  switch-idp x | yes p with dA y (pt A∙)
  switch-idp x | yes p | yes q = q ∙ sym p
  switch-idp x | yes p | no  _ with dA y y
  switch-idp x | yes p | no  _ | yes _ = sym p
  switch-idp x | yes p | no  _ | no ¬p = ⊥.rec (¬p refl)
  switch-idp x | no ¬p with dA x y
  switch-idp x | no ¬p | yes p with dA y (pt A∙)
  switch-idp x | no ¬p | yes p | yes q = ⊥.rec (¬p (p ∙ q))
  switch-idp x | no ¬p | yes p | no  _ with dA (pt A∙) (pt A∙)
  switch-idp x | no ¬p | yes p | no  _ | yes _ = sym p
  switch-idp x | no ¬p | yes p | no  _ | no ¬q = ⊥.rec (¬q refl)
  switch-idp x | no ¬p | no ¬q with dA x (pt A∙)
  switch-idp x | no ¬p | no ¬q | yes p = ⊥.rec (¬p p)
  switch-idp x | no ¬p | no ¬q | no  _ with dA x y
  switch-idp x | no ¬p | no ¬q | no  _ | yes q = ⊥.rec (¬q q)
  switch-idp x | no ¬p | no ¬q | no  _ | no  _ = refl

  switch-eqv : typ A∙ ≃ typ A∙
  switch-eqv = isoToEquiv (iso switch switch switch-idp switch-idp)

isHomogeneousDiscrete : ∀ {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) → isHomogeneous A∙
isHomogeneousDiscrete {ℓ} {A∙} dA y
  = pointed-sip (typ A∙ , pt A∙) (typ A∙ , y) (switch-eqv , switch-ptA∙)
  where open HomogeneousDiscrete {ℓ} {A∙} dA y

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module tests.PrintBool where

open import Prelude.IO
open import Prelude.Bool
open import Prelude.Char
open import Prelude.List
open import Prelude.Unit
open import Prelude.String

isNewline : Char -> Bool
isNewline '\n' = true
isNewline _    = false

sequence : {A : Set} -> List (IO A) -> IO (List A)
sequence [] = return []
sequence (x :: xs) =
    r <- x ,
    rs <- sequence xs ,
    return (r :: rs)

mapM : {A B : Set} -> (A -> IO B) -> List A -> IO (List B)
mapM f xs = sequence (map f xs)

printList : List Char -> IO Unit
printList xs =
  mapM printChar xs ,,
  printChar '\n'

main : IO Unit
main =
    printChar 'a' ,,
    printList ('a' :: 'b' :: 'c' :: []) ,,
    putStrLn "printBool" ,,
    printBool (isNewline '\n') ,,
    printBool (isNewline 'a') ,,
    return unit

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --prop --type-in-type #-}

open import Agda.Primitive

data Squash (A : Setω) : Prop where
  squash : A → Squash A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Testing the translation of higher-order functions
------------------------------------------------------------------------------

{-# OPTIONS --exact-split                    #-}
{-# OPTIONS --no-universe-polymorphism       #-}
{-# OPTIONS --universal-quantified-functions #-}
{-# OPTIONS --without-K                      #-}

-- We can use the Agda pragma @--universal-quantified-functions@ to
-- translate higher-order functions. The canonical examples are the
-- conversion rules for the λ-abstraction and the fixed-point
-- operator.

module NonFOLHigherOrderFunctions where

infixl 6 _∙_
infix  4 _≡_

postulate
  D   : Set
  _≡_ : D → D → Set
  lam : (D → D) → D
  _∙_ : D → D → D
  fix : (D → D) → D

postulate beta : (f : D → D) → (a : D) → (lam f) ∙ a ≡ f a
{-# ATP axiom beta #-}

postulate fix-f : (f : D → D) → fix f ≡ f (fix  f)
{-# ATP axiom fix-f #-}

-- We need to have at least one conjecture to generate a TPTP file.
postulate refl : ∀ d → d ≡ d
{-# ATP prove refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module IO where

open import Base

postulate
  IO       : Set -> Set
  getLine  : IO String
  putStrLn : String -> IO Unit
  mapM₋    : {A : Set} -> (A -> IO Unit) -> List A -> IO Unit
  bindIO   : {A B : Set} -> IO A -> (A -> IO B) -> IO B
  returnIO : {A : Set} -> A -> IO A

{-# COMPILED putStrLn putStrLn #-}
{-# COMPILED mapM₋ (\_ -> mapM_ :: (a -> IO ()) -> [a] -> IO ()) #-}
  -- we need to throw away the type argument to mapM_
  -- and resolve the overloading explicitly (since Alonzo
  -- output is sprinkled with unsafeCoerce#).
{-# COMPILED bindIO (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}
{-# COMPILED returnIO (\_ -> return :: a -> IO a) #-}
{-# COMPILED getLine getLine #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Oscar.Data.Fin.ThickAndThin where

open import Oscar.Data.Fin
open import Oscar.Class.ThickAndThin

import Data.Fin as F
import Data.Fin.Properties as F

instance ThickAndThinFin : ThickAndThin Fin
ThickAndThin.thin ThickAndThinFin = F.thin
ThickAndThin.thick ThickAndThinFin = F.thick
ThickAndThin.thin-injective ThickAndThinFin z = F.thin-injective {z = z}
ThickAndThin.thick∘thin=id ThickAndThinFin = F.thick-thin
ThickAndThin.check ThickAndThinFin = F.check
ThickAndThin.thin-check-id ThickAndThinFin = F.thin-check-id


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

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

open import LibraBFT.Base.Types
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.Impl.OBM.Logging.Logging
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.VoteData where

verify : VoteData → Either ErrLog Unit
verify self = do
  lcheck (self ^∙ vdParent ∙ biEpoch == self ^∙ vdProposed ∙ biEpoch)
         ("parent and proposed epochs do not match" ∷ [])
  lcheck (⌊ self ^∙ vdParent ∙ biRound <?  self ^∙ vdProposed ∙ biRound ⌋)
         ("proposed round is less than parent round" ∷ [])
  -- lcheck (self^.vdParent.biTimestamp <= self^.vdProposed.biTimestamp)
  --       ["proposed happened before parent"]
  lcheck (⌊ (self ^∙ vdParent ∙ biVersion) ≤?-Version (self ^∙ vdProposed ∙ biVersion) ⌋)
         ("proposed version is less than parent version" ∷ [])
         -- , lsVersion (self^.vdProposed.biVersion), lsVersion (self^.vdParent.biVersion)]

new : BlockInfo → BlockInfo → VoteData
new = VoteData∙new


text:
module Dummy where

-- Run this in Acme: go build && ./acme-agda -v

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

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

_*_ : ℕ → ℕ → ℕ
m * n = {!m !}

max_stars_repo_name: neosimsim/acme-agda

max_issues_repo_name: neosimsim/acme-agda

max_forks_repo_name: neosimsim/acme-agda


text:
{-# OPTIONS --cubical --safe #-}
module Label where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude using (isProp; transport)

open import Cubical.Data.Nat using (ℕ; zero; suc; isSetℕ)
open import Cubical.Data.Nat.Order using (_<_; _≤_; ≤-refl; <-weaken; ≤<-trans; m≤n-isProp; <-asym)
open import Cubical.Data.Maybe using (Maybe; nothing; just)
open import Cubical.Data.Empty using () renaming (rec to ⊥-elim)

Label : Set
Label = ℕ

data Record (A : Set) : Label -> Set where
  nil : forall {l} -> Record A l
  cons : forall {l} -> Record A l -> (l' : Label) -> A -> .(l < l') -> Record A l'

data _∈_ {A : Set} (l₁ : Label) {l : Label} : Record A l -> Set where
  here : forall {l'} {r : Record A l'} {x lt} -> l₁ ≡ l -> l₁ ∈ cons r l x lt
  there : forall {l'} {r : Record A l'} {x lt} -> l₁ ∈ r -> l₁ ∈ cons r l x lt

find : forall {A} {l} -> (l₁ : Label) -> (r : Record A l) -> l₁ ∈ r -> A
find l₁ (cons _ _ x _) (here e) = x
find l₁ (cons r _ _ _) (there l₁∈r) = find l₁ r l₁∈r

∈-implies-≤ : forall {A} {l l'} {r : Record A l'} -> l ∈ r -> l ≤ l'
∈-implies-≤ {l = l} (here e) = transport (λ i -> l ≤ e i) ≤-refl
∈-implies-≤ (there {lt = lt} l∈r) = <-weaken (≤<-trans (∈-implies-≤ l∈r) lt)

l∈r-isProp : forall {A} l {l'} (r : Record A l') -> isProp (l ∈ r)
l∈r-isProp l {l'} (cons _ _ _ _) (here {lt = a} e1) (here {lt = b} e2) = λ i -> here {lt = m≤n-isProp a b i} (isSetℕ l l' e1 e2 i)
l∈r-isProp l (cons {l = l₁} r _ _ _) (here {lt = k} e) (there y) = ⊥-elim (<-asym k (transport (λ i -> e i ≤ l₁) (∈-implies-≤ y)))
l∈r-isProp l (cons {l = l₁} r _ _ _) (there {lt = k} x) (here e) = ⊥-elim (<-asym k (transport (λ i -> e i ≤ l₁) (∈-implies-≤ x)))
l∈r-isProp l (cons r _ _ _) (there {lt = k1} x) (there {lt = k2} y) = let a = l∈r-isProp l r x y in λ i → there {lt = m≤n-isProp k1 k2 i} (a i)

max_stars_repo_name: elpinal/subtyping-agda

max_issues_repo_name: elpinal/subtyping-agda

max_forks_repo_name: elpinal/subtyping-agda


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

{-

This file defines

sucPred : ∀ (i : Int) → sucInt (predInt i) ≡ i
predSuc : ∀ (i : Int) → predInt (sucInt i) ≡ i

discreteInt : discrete Int
isSetInt : isSet Int

addition of Int is defined _+_ : Int → Int → Int

as well as its commutativity and associativity
+-comm : ∀ (m n : Int) → m + n ≡ n + m
+-assoc : ∀ (m n o : Int) → m + (n + o) ≡ (m + n) + o

An alternate definition of _+_ is defined via ua,
namely _+'_, which helps us to easily prove

isEquivAddInt : (m : Int) → isEquiv (λ n → n + m)

-}

module Cubical.Data.Int.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Empty
open import Cubical.Data.Nat hiding (+-assoc ; +-comm) renaming (_·_ to _·ℕ_; _+_ to _+ℕ_)
open import Cubical.Data.Bool
open import Cubical.Data.Sum
open import Cubical.Data.Int.Base

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

abs : Int → ℕ
abs (pos n) = n
abs (negsuc n) = suc n

sgn : Int → Bool
sgn (pos n) = true
sgn (negsuc n) = false

sucPred : ∀ i → sucInt (predInt i) ≡ i
sucPred (pos zero)    = refl
sucPred (pos (suc n)) = refl
sucPred (negsuc n)    = refl

predSuc : ∀ i → predInt (sucInt i) ≡ i
predSuc (pos n)          = refl
predSuc (negsuc zero)    = refl
predSuc (negsuc (suc n)) = refl

-- TODO: define multiplication

injPos : ∀ {a b : ℕ} → pos a ≡ pos b → a ≡ b
injPos {a} h = subst T h refl
  where
  T : Int → Type₀
  T (pos x)    = a ≡ x
  T (negsuc _) = ⊥

injNegsuc : ∀ {a b : ℕ} → negsuc a ≡ negsuc b → a ≡ b
injNegsuc {a} h = subst T h refl
  where
  T : Int → Type₀
  T (pos _) = ⊥
  T (negsuc x) = a ≡ x

posNotnegsuc : ∀ (a b : ℕ) → ¬ (pos a ≡ negsuc b)
posNotnegsuc a b h = subst T h 0
  where
  T : Int → Type₀
  T (pos _)    = ℕ
  T (negsuc _) = ⊥

negsucNotpos : ∀ (a b : ℕ) → ¬ (negsuc a ≡ pos b)
negsucNotpos a b h = subst T h 0
  where
  T : Int → Type₀
  T (pos _)    = ⊥
  T (negsuc _) = ℕ

discreteInt : Discrete Int
discreteInt (pos n) (pos m) with discreteℕ n m
... | yes p = yes (cong pos p)
... | no p  = no (λ x → p (injPos x))
discreteInt (pos n) (negsuc m) = no (posNotnegsuc n m)
discreteInt (negsuc n) (pos m) = no (negsucNotpos n m)
discreteInt (negsuc n) (negsuc m) with discreteℕ n m
... | yes p = yes (cong negsuc p)
... | no p  = no (λ x → p (injNegsuc x))

isSetInt : isSet Int
isSetInt = Discrete→isSet discreteInt

isEven : Int → Bool
isEven (pos zero) = true
isEven (pos (suc zero)) = false
isEven (pos (suc (suc n))) = isEven (pos n)
isEven (negsuc zero) = false
isEven (negsuc (suc n)) = isEven (pos n)

_ℕ-_ : ℕ → ℕ → Int
a ℕ- 0 = pos a
0 ℕ- suc b = negsuc b
suc a ℕ- suc b = a ℕ- b

_+pos_ : Int → ℕ  → Int
z +pos 0 = z
z +pos (suc n) = sucInt (z +pos n)

_+negsuc_ : Int → ℕ → Int
z +negsuc 0 = predInt z
z +negsuc (suc n) = predInt (z +negsuc n)

_+_ : Int → Int → Int
m + pos n = m +pos n
m + negsuc n = m +negsuc n

-_ : Int → Int
- pos zero = pos zero
- pos (suc n) = negsuc n
- negsuc n = pos (suc n)

_-_ : Int → Int → Int
m - n = m + (- n)

-pos : ∀ n → - (pos n) ≡ neg n
-pos zero    = refl
-pos (suc n) = refl

-neg : ∀ n → - (neg n) ≡ pos n
-neg zero    = refl
-neg (suc n) = refl

-Involutive : ∀ z → - (- z) ≡ z
-Involutive (pos n)    = (- (-  pos n)) ≡⟨ cong -_ (-pos n) ⟩
                             - (neg n)  ≡⟨ -neg n ⟩
                                pos n   ∎
-Involutive (negsuc n) = refl

sucInt+pos : ∀ n m → sucInt (m +pos n) ≡ (sucInt m) +pos n
sucInt+pos zero m = refl
sucInt+pos (suc n) m = cong sucInt (sucInt+pos n m)

predInt+negsuc : ∀ n m → predInt (m +negsuc n) ≡ (predInt m) +negsuc n
predInt+negsuc zero m = refl
predInt+negsuc (suc n) m = cong predInt (predInt+negsuc n m)

sucInt+negsuc : ∀ n m → sucInt (m +negsuc n) ≡ (sucInt m) +negsuc n
sucInt+negsuc zero m = (sucPred _) ∙ (sym (predSuc _))
sucInt+negsuc (suc n) m =      _ ≡⟨ sucPred _ ⟩
  m +negsuc n                    ≡[ i ]⟨ predSuc m (~ i) +negsuc n ⟩
  (predInt (sucInt m)) +negsuc n ≡⟨ sym (predInt+negsuc n (sucInt m)) ⟩
  predInt (sucInt m +negsuc n) ∎

predInt+pos : ∀ n m → predInt (m +pos n) ≡ (predInt m) +pos n
predInt+pos zero m = refl
predInt+pos (suc n) m =     _ ≡⟨ predSuc _ ⟩
  m +pos n                    ≡[ i ]⟨ sucPred m (~ i) + pos n ⟩
  (sucInt (predInt m)) +pos n ≡⟨ sym (sucInt+pos n (predInt m))⟩
  (predInt m) +pos (suc n)    ∎

predInt-pos : ∀ n → predInt(- (pos n)) ≡ negsuc n
predInt-pos zero = refl
predInt-pos (suc n) = refl

predInt+ : ∀ m n → predInt (m + n) ≡ (predInt m) + n
predInt+ m (pos n) = predInt+pos n m
predInt+ m (negsuc n) = predInt+negsuc n m

+predInt : ∀ m n → predInt (m + n) ≡ m + (predInt n)
+predInt m (pos zero) = refl
+predInt m (pos (suc n)) = (predSuc (m + pos n)) ∙ (cong (_+_ m) (sym (predSuc (pos n))))
+predInt m (negsuc n) = refl

sucInt+ : ∀ m n → sucInt (m + n) ≡ (sucInt m) + n
sucInt+ m (pos n) = sucInt+pos n m
sucInt+ m (negsuc n) = sucInt+negsuc n m

+sucInt : ∀ m n → sucInt (m + n) ≡  m + (sucInt n)
+sucInt m (pos n) = refl
+sucInt m (negsuc zero) = sucPred _
+sucInt m (negsuc (suc n)) = (sucPred (m +negsuc n)) ∙ (cong (_+_ m) (sym (sucPred (negsuc n))))

pos0+ : ∀ z → z ≡ pos 0 + z
pos0+ (pos zero) = refl
pos0+ (pos (suc n)) = cong sucInt (pos0+ (pos n))
pos0+ (negsuc zero) = refl
pos0+ (negsuc (suc n)) = cong predInt (pos0+ (negsuc n))

negsuc0+ : ∀ z → predInt z ≡ negsuc 0 + z
negsuc0+ (pos zero) = refl
negsuc0+ (pos (suc n)) = (sym (sucPred (pos n))) ∙ (cong sucInt (negsuc0+ _))
negsuc0+ (negsuc zero) = refl
negsuc0+ (negsuc (suc n)) = cong predInt (negsuc0+ (negsuc n))

ind-comm : {A : Type₀} (_∙_ : A → A → A) (f : ℕ → A) (g : A → A)
           (p : ∀ {n} → f (suc n) ≡ g (f n))
           (g∙ : ∀ a b → g (a ∙ b) ≡ g a ∙ b)
           (∙g : ∀ a b → g (a ∙ b) ≡ a ∙ g b)
           (base : ∀ z → z ∙ f 0 ≡ f 0 ∙ z)
         → ∀ z n → z ∙ f n ≡ f n ∙ z
ind-comm _∙_ f g p g∙ ∙g base z 0 = base z
ind-comm _∙_ f g p g∙ ∙g base z (suc n) =
  z ∙ f (suc n) ≡[ i ]⟨ z ∙ p {n} i ⟩
  z ∙ g (f n)   ≡⟨ sym ( ∙g z (f n)) ⟩
  g (z ∙ f n)   ≡⟨ cong g IH ⟩
  g (f n ∙ z)   ≡⟨ g∙ (f n) z ⟩
  g (f n) ∙ z   ≡[ i ]⟨ p {n} (~ i) ∙ z ⟩
  f (suc n) ∙ z ∎
  where
  IH = ind-comm _∙_ f g p g∙ ∙g base z n

ind-assoc : {A : Type₀} (_·_ : A → A → A) (f : ℕ → A)
        (g : A → A) (p : ∀ a b → g (a · b) ≡ a · (g b))
        (q : ∀ {c} → f (suc c) ≡ g (f c))
        (base : ∀ m n → (m · n) · (f 0) ≡ m · (n · (f 0)))
        (m n : A) (o : ℕ)
      → m · (n · (f o)) ≡ (m · n) · (f o)
ind-assoc _·_ f g p q base m n 0 = sym (base m n)
ind-assoc _·_ f g p q base m n (suc o) =
    m · (n · (f (suc o))) ≡[ i ]⟨ m · (n · q {o} i) ⟩
    m · (n · (g (f o)))   ≡[ i ]⟨ m · (p n (f o) (~ i)) ⟩
    m · (g (n · (f o)))   ≡⟨ sym (p m (n · (f o)))⟩
    g (m · (n · (f o)))   ≡⟨ cong g IH ⟩
    g ((m · n) · (f o))   ≡⟨ p (m · n) (f o) ⟩
    (m · n) · (g (f o))   ≡[ i ]⟨ (m · n) · q {o} (~ i) ⟩
    (m · n) · (f (suc o)) ∎
    where
    IH = ind-assoc _·_ f g p q base m n o

+-comm : ∀ m n → m + n ≡ n + m
+-comm m (pos n) = ind-comm _+_ pos sucInt refl sucInt+ +sucInt pos0+ m n
+-comm m (negsuc n) = ind-comm _+_ negsuc predInt refl predInt+ +predInt negsuc0+ m n

+-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
+-assoc m n (pos o) = ind-assoc _+_ pos sucInt +sucInt refl (λ _ _ → refl) m n o
+-assoc m n (negsuc o) = ind-assoc _+_ negsuc predInt +predInt refl +predInt m n o

-- Compose sucPathInt with itself n times. Transporting along this
-- will be addition, transporting with it backwards will be subtraction.
-- Use this to define _+'_ for which is easier to prove
-- isEquiv (λ n → n +' m) since _+'_ is defined by transport

sucPathInt : Int ≡ Int
sucPathInt = ua (sucInt , isoToIsEquiv (iso sucInt predInt sucPred predSuc))

addEq : ℕ → Int ≡ Int
addEq zero = refl
addEq (suc n) = (addEq n) ∙ sucPathInt

predPathInt : Int ≡ Int
predPathInt = ua (predInt , isoToIsEquiv (iso predInt sucInt predSuc sucPred))

subEq : ℕ → Int ≡ Int
subEq zero = refl
subEq (suc n) = (subEq n) ∙ predPathInt

_+'_ : Int → Int → Int
m +' pos n    = transport (addEq n) m
m +' negsuc n = transport (subEq (suc n)) m

+'≡+ : _+'_ ≡ _+_
+'≡+ i m (pos zero) = m
+'≡+ i m (pos (suc n)) = sucInt (+'≡+ i m (pos n))
+'≡+ i m (negsuc zero) = predInt m
+'≡+ i m (negsuc (suc n)) = predInt (+'≡+ i m (negsuc n)) --
  -- compPath (λ i → (+'≡+ i (predInt m) (negsuc n))) (sym (predInt+negsuc n m)) i

isEquivAddInt' : (m : Int) → isEquiv (λ n → n +' m)
isEquivAddInt' (pos n)    = isEquivTransport (addEq n)
isEquivAddInt' (negsuc n) = isEquivTransport (subEq (suc n))

isEquivAddInt : (m : Int) → isEquiv (λ n → n + m)
isEquivAddInt = subst (λ add → (m : Int) → isEquiv (λ n → add n m)) +'≡+ isEquivAddInt'

-- below is an alternate proof of isEquivAddInt for comparison
-- We also have two useful lemma here.

minusPlus : ∀ m n → (n - m) + m ≡ n
minusPlus (pos zero) n = refl
minusPlus (pos 1) = sucPred
minusPlus (pos (suc (suc m))) n =
  sucInt ((n +negsuc (suc m)) +pos (suc m)) ≡⟨ sucInt+pos (suc m) _ ⟩
  sucInt (n +negsuc (suc m)) +pos (suc m)   ≡[ i ]⟨ sucPred (n +negsuc m) i +pos (suc m) ⟩
  (n - pos (suc m)) +pos (suc m)            ≡⟨ minusPlus (pos (suc m)) n ⟩
  n ∎
minusPlus (negsuc zero) = predSuc
minusPlus (negsuc (suc m)) n =
  predInt (sucInt (sucInt (n +pos m)) +negsuc m) ≡⟨ predInt+negsuc m _ ⟩
  predInt (sucInt (sucInt (n +pos m))) +negsuc m ≡[ i ]⟨ predSuc (sucInt (n +pos m)) i +negsuc m ⟩
  sucInt (n +pos m) +negsuc m                    ≡⟨ minusPlus (negsuc m) n ⟩
  n ∎

plusMinus : ∀ m n → (n + m) - m ≡ n
plusMinus (pos zero) n = refl
plusMinus (pos (suc m)) = minusPlus (negsuc m)
plusMinus (negsuc m) = minusPlus (pos (suc m))

private
  alternateProof : (m : Int) → isEquiv (λ n → n + m)
  alternateProof m = isoToIsEquiv (iso (λ n → n + m)
                                       (λ n → n - m)
                                       (minusPlus m)
                                       (plusMinus m))

-Cancel : ∀ z → z - z ≡ pos zero
-Cancel z = z - z             ≡⟨ cong (_- z) (pos0+ z) ⟩
           (pos zero + z) - z ≡⟨ plusMinus z (pos zero) ⟩
            pos zero          ∎

pos+ : ∀ m n → pos (m +ℕ n) ≡ pos m + pos n
pos+ zero zero = refl
pos+ zero (suc n)    =
  pos (zero +ℕ suc n)    ≡⟨ +-comm (pos (suc n)) (pos zero) ⟩
  pos zero + pos (suc n) ∎
pos+ (suc m) zero    =
  pos (suc (m +ℕ zero))  ≡⟨ cong pos (cong suc (+-zero m)) ⟩
  pos (suc m) + pos zero ∎
pos+ (suc m) (suc n) =
  pos (suc m +ℕ suc n)            ≡⟨ cong pos (cong suc (+-suc m n)) ⟩
  sucInt (pos (suc (m +ℕ n)))     ≡⟨ cong sucInt (cong sucInt (pos+ m n)) ⟩
  sucInt (sucInt (pos m + pos n)) ≡⟨ sucInt+ (pos m) (sucInt (pos n)) ⟩
  pos (suc m) + pos (suc n)       ∎

negsuc+ : ∀ m n → negsuc (m +ℕ n) ≡ negsuc m - pos n
negsuc+ zero zero       = refl
negsuc+ zero (suc n)    =
  negsuc (zero +ℕ suc n)    ≡⟨ negsuc0+ (negsuc n) ⟩
  negsuc zero + negsuc n    ≡⟨ cong (negsuc zero +_) (-pos (suc n)) ⟩
  negsuc zero - pos (suc n) ∎
negsuc+ (suc m) zero    =
  negsuc (suc m +ℕ zero)    ≡⟨ cong negsuc (cong suc (+-zero m)) ⟩
  negsuc (suc m) - pos zero ∎
negsuc+ (suc m) (suc n) =
  negsuc (suc m +ℕ suc n)        ≡⟨ cong negsuc (sym (+-suc m (suc n))) ⟩
  negsuc (m +ℕ suc (suc n))      ≡⟨ negsuc+ m (suc (suc n)) ⟩
  negsuc m - pos (suc (suc n))   ≡⟨ sym (+predInt (negsuc m) (negsuc n)) ⟩
  predInt (negsuc m + negsuc n ) ≡⟨ predInt+ (negsuc m) (negsuc n) ⟩
  negsuc (suc m) - pos (suc n)   ∎

neg+ : ∀ m n → neg (m +ℕ n) ≡ neg m + neg n
neg+ zero zero       = refl
neg+ zero (suc n)    = neg (zero +ℕ suc n)    ≡⟨ +-comm (neg (suc n)) (pos zero) ⟩
                       neg zero + neg (suc n) ∎
neg+ (suc m) zero    = neg (suc (m +ℕ zero))  ≡⟨ cong neg (cong suc (+-zero m)) ⟩
                       neg (suc m) + neg zero ∎
neg+ (suc m) (suc n) = neg (suc m +ℕ suc n)      ≡⟨ negsuc+ m (suc n) ⟩
                       neg (suc m) + neg (suc n) ∎

ℕ-AntiComm : ∀ m n → m ℕ- n ≡ - (n ℕ- m)
ℕ-AntiComm zero zero       = refl
ℕ-AntiComm zero (suc n)    = refl
ℕ-AntiComm (suc m) zero    = refl
ℕ-AntiComm (suc m) (suc n) = suc m ℕ- suc n  ≡⟨ ℕ-AntiComm m n ⟩
                          - (suc n ℕ- suc m) ∎

pos- : ∀ m n → m ℕ- n ≡ pos m - pos n
pos- zero zero       = refl
pos- zero (suc n)    = zero ℕ- suc n          ≡⟨ +-comm (negsuc n) (pos zero) ⟩
                       pos zero - pos (suc n) ∎
pos- (suc m) zero    = refl
pos- (suc m) (suc n) =
  suc m ℕ- suc n                       ≡⟨ pos- m n ⟩
  pos m - pos n                        ≡⟨ sym (sucPred (pos m - pos n)) ⟩
  sucInt (predInt (pos m - pos n))     ≡⟨ cong sucInt (+predInt (pos m) (- pos n)) ⟩
  sucInt (pos m + predInt (- (pos n))) ≡⟨ cong sucInt (cong (pos m +_) (predInt-pos n)) ⟩
  sucInt (pos m + negsuc n)            ≡⟨ sucInt+negsuc n (pos m) ⟩
  pos (suc m) - pos (suc n)            ∎

-AntiComm : ∀ m n → m - n ≡ - (n - m)
-AntiComm (pos n) (pos m)       = pos n - pos m   ≡⟨ sym (pos- n m) ⟩
                                   n ℕ- m         ≡⟨ ℕ-AntiComm n m ⟩
                                - (m ℕ- n)        ≡⟨ cong -_ (pos- m n) ⟩
                                - (pos m - pos n) ∎
-AntiComm (pos n) (negsuc m)    =
     pos n - negsuc m     ≡⟨ +-comm (pos n) (pos (suc m)) ⟩
     pos (suc m) + pos n  ≡⟨ sym (pos+ (suc m) n) ⟩
     pos (suc m +ℕ n)     ≡⟨ sym (-neg (suc m +ℕ n)) ⟩
  -  neg (suc m +ℕ n)     ≡⟨ cong -_ (neg+ (suc m) n) ⟩
  - (neg (suc m) + neg n) ≡⟨ cong -_ (cong (negsuc m +_) (sym (-pos n))) ⟩
  - (negsuc m - pos n)    ∎
-AntiComm (negsuc n) (pos m)    =
     negsuc n - pos m     ≡⟨ sym (negsuc+ n m) ⟩
     negsuc (n +ℕ m)      ≡⟨ cong -_ (pos+ (suc n) m) ⟩
  - (pos (suc n) + pos m) ≡⟨ cong -_ (+-comm (pos (suc n)) (pos m)) ⟩
  - (pos m - negsuc n)    ∎
-AntiComm (negsuc n) (negsuc m) =
     negsuc n - negsuc m        ≡⟨ +-comm (negsuc n) (pos (suc m)) ⟩
     pos (suc m) + negsuc n     ≡⟨ sym (pos- (suc m) (suc n)) ⟩
     suc m ℕ- suc n             ≡⟨ ℕ-AntiComm (suc m) (suc n) ⟩
  - (suc n ℕ- suc m)            ≡⟨ cong -_ (pos- (suc n) (suc m)) ⟩
  - (pos (suc n) - pos (suc m)) ≡⟨ cong -_ (+-comm (pos (suc n)) (negsuc m)) ⟩
  - (negsuc m - negsuc n)       ∎

-Dist+ : ∀ m n → - (m + n) ≡ (- m) + (- n)
-Dist+ (pos n) (pos m)       =
   - (pos n + pos m)     ≡⟨ cong -_ (sym (pos+ n m)) ⟩
   -  pos (n +ℕ m)       ≡⟨ -pos (n +ℕ m) ⟩
      neg (n +ℕ m)       ≡⟨ neg+ n m ⟩
      neg n + neg m      ≡⟨ cong (neg n +_) (sym (-pos m)) ⟩
      neg n + (- pos m)  ≡⟨ cong (_+ (- pos m)) (sym (-pos n)) ⟩
  (-  pos n) + (- pos m) ∎
-Dist+ (pos n) (negsuc m)    =
   - (pos n + negsuc m)     ≡⟨ sym (-AntiComm (pos (suc m)) (pos n)) ⟩
      pos (suc m) - pos n   ≡⟨ +-comm (pos (suc m)) (- pos n) ⟩
  (-  pos n) + (- negsuc m) ∎
-Dist+ (negsuc n) (pos m)    =
   - (negsuc n + pos m)     ≡⟨ cong -_ (+-comm (negsuc n) (pos m)) ⟩
   - (pos m + negsuc n)     ≡⟨ sym (-AntiComm (- negsuc n) (pos m)) ⟩
  (-  negsuc n) + (- pos m) ∎
-Dist+ (negsuc n) (negsuc m) =
   - (negsuc n + negsuc m)     ≡⟨ cong -_ (sym (neg+ (suc n) (suc m))) ⟩
   -  neg (suc n +ℕ suc m)     ≡⟨ pos+ (suc n) (suc m) ⟩
  (-  negsuc n) + (- negsuc m) ∎

_·_ : Int → Int → Int
pos zero · m = pos zero
pos (suc n) · m = m + (pos n · m)
negsuc zero · m = (- m)
negsuc (suc n) · m = (- m) + ((negsuc n) · m)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module *-distrib-+ where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)

open import Induction′ using (+-assoc; +-comm; +-suc)

-- 積が和に対して分配的であることの証明
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p =
  begin
    (zero + n) * p
  ≡⟨⟩
    n * p
  ≡⟨⟩
    zero * p + n * p
  ∎
*-distrib-+ (suc m) n p =
  begin
    ((suc m) + n) * p
  ≡⟨ cong (_* p) (+-comm (suc m) n) ⟩
    (n + (suc m)) * p
  ≡⟨ cong (_* p) (+-suc n m) ⟩
    (suc (n + m)) * p
  ≡⟨⟩
    p + ((n + m) * p)
  ≡⟨ cong (p +_) (*-distrib-+ n m p) ⟩
    p + (n * p + m * p)
  ≡⟨ cong (p +_) (+-comm (n * p) (m * p)) ⟩
    p + (m * p + n * p)
  ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
    (p + (m * p)) + n * p
  ≡⟨⟩
    (suc m) * p + n * p
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

module Data.List.Kleene.Relation.Unary where

open import Data.List.Kleene
open import Prelude
open import Data.Fin
open import Relation.Nullary

private
  variable
    p : Level

◇⁺ : ∀ {A : Type a} (P : A → Type p) → A ⁺ → Type _
◇⁺ P xs = ∃[ i ] P (xs !⁺ i)

◇⋆ : ∀ {A : Type a} (P : A → Type p) → A ⋆ → Type _
◇⋆ P xs = ∃[ i ] P (xs !⋆ i)

module Exists {a} {A : Type a} {p} (P : A → Type p) where
  push : ∀ {x xs} → ◇⋆ P xs → ◇⁺ P (x & xs)
  push (n , x∈xs) = (fs n , x∈xs)

  pull : ∀ {x xs} → ¬ P x → ◇⁺ P (x & xs) → ◇⋆ P xs
  pull ¬Px (f0  , p∈xs) = ⊥-elim (¬Px p∈xs)
  pull ¬Px (fs n , p∈xs) = (n , p∈xs)

◻⁺ : {A : Type a} (P : A → Type p) → A ⁺ → Type _
◻⁺ P xs = ∀ i → P (xs !⁺ i)

◻⋆ : {A : Type a} (P : A → Type p) → A ⋆ → Type _
◻⋆ P xs = ∀ i → P (xs !⋆ i)

module Forall {a} {A : Type a} {p} (P : A → Type p) where
  push⁺ : ∀ {x xs} → P x → ◻⋆ P xs → ◻⁺ P (x & xs)
  push⁺ px pxs f0 = px
  push⁺ px pxs (fs n) = pxs n

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdList (flatten-OrdList-helper)
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.OrdList.FlattenI where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- See the combined proof.
postulate
  flatten-OrdList-helper : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                           OrdTree (node t₁ i t₂) →
                           ≤-Lists (flatten t₁) (flatten t₂)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Product where

open import Categories.Category
open import Categories.Functor using (Functor)
import Categories.Object.Product as Product
import Categories.Object.BinaryProducts as BinaryProducts

-- Ugh, we should start bundling things (categories with binary products, in this case) up consistently
_[_][_×-] : ∀ {o ℓ e} → (C : Category o ℓ e) → BinaryProducts.BinaryProducts C → Category.Obj C → Functor C C
C [ P ][ O ×-] = record
  { F₀ = λ x → Product.A×B (product {O} {x})
  ; F₁ = λ f → ⟨ π₁ , f ∘ π₂ ⟩
  ; identity = λ {x} → identity′ {x}
  ; homomorphism = λ {x} {y} {z} {f} {g} → homomorphism′ {x} {y} {z} {f} {g}
  ; F-resp-≡ = λ f≡g → ⟨⟩-cong₂ refl (∘-resp-≡ˡ f≡g)
  }
  where
  open Category C
  open Equiv
  open Product C
  open BinaryProducts.BinaryProducts P

  .identity′ : {A : Obj} → ⟨ π₁ , id ∘ π₂ ⟩ ≡ id
  identity′ =
    begin
      ⟨ π₁ , id ∘ π₂ ⟩
    ≈⟨ ⟨⟩-cong₂ refl identityˡ ⟩
      ⟨ π₁ , π₂ ⟩
    ≈⟨ η ⟩
      id
    ∎
    where open HomReasoning

  .homomorphism′ : {X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} → ⟨ π₁ , (g ∘ f) ∘ π₂ ⟩ ≡ ⟨ π₁ , g ∘ π₂ ⟩ ∘ ⟨ π₁ , f ∘ π₂ ⟩
  homomorphism′ {f = f} {g} =
    begin
      ⟨ π₁ , (g ∘ f) ∘ π₂ ⟩
    ↓⟨ ⟨⟩-cong₂ refl assoc ⟩
      ⟨ π₁ , g ∘ (f ∘ π₂) ⟩
    ↑⟨ ⟨⟩-cong₂ refl (∘-resp-≡ʳ commute₂) ⟩
      ⟨ π₁ , g ∘ (π₂ ∘ ⟨ π₁ , f ∘ π₂ ⟩) ⟩
    ↑⟨ ⟨⟩-cong₂ commute₁ assoc ⟩
       ⟨ π₁ ∘ ⟨ π₁ , f ∘ π₂ ⟩  , (g ∘ π₂) ∘ ⟨ π₁ , f ∘ π₂ ⟩ ⟩
    ↑⟨ ⟨⟩∘ ⟩
      ⟨ π₁ , g ∘ π₂ ⟩ ∘ ⟨ π₁ , f ∘ π₂ ⟩
    ∎
    where open HomReasoning

_[_][-×_] : ∀ {o ℓ e} → (C : Category o ℓ e) → BinaryProducts.BinaryProducts C → Category.Obj C → Functor C C
C [ P ][-× O ] = record
  { F₀ = λ x → Product.A×B (product {x} {O})
  ; F₁ = λ f → ⟨ f ∘ π₁ , π₂ ⟩
  ; identity = λ {x} → identity′ {x}
  ; homomorphism = λ {x} {y} {z} {f} {g} → homomorphism′ {x} {y} {z} {f} {g}
  ; F-resp-≡ = λ f≡g → ⟨⟩-cong₂ (∘-resp-≡ˡ f≡g) refl
  }
  where
  open Category C
  open Equiv
  open Product C
  open BinaryProducts.BinaryProducts P

  .identity′ : {A : Obj} → ⟨ id ∘ π₁ , π₂ ⟩ ≡ id
  identity′ =
    begin
      ⟨ id ∘ π₁ , π₂ ⟩
    ≈⟨ ⟨⟩-cong₂ identityˡ refl ⟩
      ⟨ π₁ , π₂ ⟩
    ≈⟨ η ⟩
      id
    ∎
    where open HomReasoning

  .homomorphism′ : {X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} → ⟨ (g ∘ f) ∘ π₁ , π₂ ⟩ ≡ ⟨ g ∘ π₁ , π₂ ⟩ ∘ ⟨ f ∘ π₁ , π₂ ⟩
  homomorphism′ {f = f} {g} =
    begin
      ⟨ (g ∘ f) ∘ π₁ , π₂ ⟩
    ↓⟨ ⟨⟩-cong₂ assoc refl ⟩
      ⟨ g ∘ (f ∘ π₁) , π₂ ⟩
    ↑⟨ ⟨⟩-cong₂ (∘-resp-≡ʳ commute₁) refl ⟩
      ⟨ g ∘ (π₁ ∘ ⟨ f ∘ π₁ , π₂ ⟩) , π₂ ⟩
    ↑⟨ ⟨⟩-cong₂ assoc commute₂ ⟩
      ⟨ (g ∘ π₁) ∘ ⟨ f ∘ π₁ , π₂ ⟩ , π₂ ∘ ⟨ f ∘ π₁ , π₂ ⟩ ⟩
    ↑⟨ ⟨⟩∘ ⟩
      ⟨ g ∘ π₁ , π₂ ⟩ ∘ ⟨ f ∘ π₁ , π₂ ⟩
    ∎
    where open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Sodium where

open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Data.Unit
open import Data.Bool
open import Data.Maybe
open import Data.Product
open import IO.Primitive

postulate

  -- Core.

  Reactive : Set → Set
  sync     : ∀ {A} → Reactive A → IO A

  Event     : Set → Set
  Behaviour : Set → Set

  listen    : ∀ {A} → Event A → (A → IO ⊤) → Reactive (IO ⊤)

  filterJust    : ∀ {A} → Event (Maybe A) → Event A
  hold          : ∀ {A} → A → Event A → Reactive (Behaviour A)
  updates value : ∀ {A} → Behaviour A → Event A
  snapshot      : ∀ {A B C} → (A → B → C) → Event A → Behaviour B → Event C

  -- Derived.

  gate     : ∀ {A} → Event A → Behaviour Bool → Event A
  filterE  : ∀ {A} → (A → Bool) → Event A → Event A

  collectE : ∀ {A B} {S : Set} → (A → S → (B × S)) → S →
             Event A → Reactive (Event B)

  collect  : ∀ {A B} {S : Set} → (A → S → (B × S)) → S →
             Behaviour A → Reactive (Behaviour B)

  accum    : ∀ {A} → A → Event (A → A) → Reactive (Behaviour A)

  -- IO.

  executeSyncIO executeAsyncIO : ∀ {A} → Event (IO A) → Event A

  -- Instances.

  reactiveMonad        : RawMonad Reactive
  behaviourApplicative : RawApplicative Behaviour
  eventFunctor         : RawFunctor Event

max_stars_repo_name: stevana/haarss

max_issues_repo_name: stevana/haarss

max_forks_repo_name: stevana/haarss


text:
postulate
  F : (Set → Set) → Set

syntax F (λ x → y) = [ x ] y

X : Set
X = [ ? ] x

max_stars_repo_name: masondesu/agda


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

module SafeFlagPostulate where

data Empty : Set where

postulate inhabitant : Empty


text:
{-# OPTIONS --cubical --safe --guardedness #-}
module Cubical.Codata.Stream.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Codata.Stream.Base

open Stream

mapS : ∀ {A B} → (A → B) → Stream A → Stream B
head (mapS f xs) = f (head xs)
tail (mapS f xs) = mapS f (tail xs)

even : ∀ {A} → Stream A → Stream A
head (even a) = head a
tail (even a) = even (tail (tail a))

odd : ∀ {A} → Stream A → Stream A
head (odd a) = head (tail a)
tail (odd a) = odd (tail (tail a))

merge : ∀ {A} → Stream A → Stream A → Stream A
head (merge a _) = head a
head (tail (merge _ b)) = head b
tail (tail (merge a b)) = merge (tail a) (tail b)

mapS-id : ∀ {A} {xs : Stream A} → mapS (λ x → x) xs ≡ xs
head (mapS-id {xs = xs} i) = head xs
tail (mapS-id {xs = xs} i) = mapS-id {xs = tail xs} i

Stream-η : ∀ {A} {xs : Stream A} → xs ≡ (head xs , tail xs)
head (Stream-η {A} {xs} i) = head xs
tail (Stream-η {A} {xs} i) = tail xs

elimS : ∀ {A} (P : Stream A → Type₀) (c : ∀ x xs → P (x , xs)) (xs : Stream A) → P xs
elimS P c xs = transp (λ i → P (Stream-η {xs = xs} (~ i))) i0
                      (c (head xs) (tail xs))

odd≡even∘tail : ∀ {A} → (a : Stream A) → odd a ≡ even (tail a)
head (odd≡even∘tail a i) = head (tail a)
tail (odd≡even∘tail a i) = odd≡even∘tail (tail (tail a)) i

mergeEvenOdd≡id : ∀ {A} → (a : Stream A) → merge (even a) (odd a) ≡ a
head (mergeEvenOdd≡id a i) = head a
head (tail (mergeEvenOdd≡id a i)) = head (tail a)
tail (tail (mergeEvenOdd≡id a i)) = mergeEvenOdd≡id (tail (tail a)) i

module Equality≅Bisimulation where

-- Bisimulation
  record _≈_ {A : Type₀} (x y : Stream A) : Type₀ where
    coinductive
    field
      ≈head : head x ≡ head y
      ≈tail : tail x ≈ tail y

  open _≈_

  bisim : {A : Type₀} → {x y : Stream A} → x ≈ y → x ≡ y
  head (bisim x≈y i) = ≈head x≈y i
  tail (bisim x≈y i) = bisim (≈tail x≈y) i

  misib : {A : Type₀} → {x y : Stream A} → x ≡ y → x ≈ y
  ≈head (misib p) = λ i → head (p i)
  ≈tail (misib p) = misib (λ i → tail (p i))

  iso1 : {A : Type₀} → {x y : Stream A} → (p : x ≡ y) → bisim (misib p) ≡ p
  head (iso1 p i j) = head (p j)
  tail (iso1 p i j) = iso1 (λ i → tail (p i)) i j

  iso2 : {A : Type₀} → {x y : Stream A} → (p : x ≈ y) → misib (bisim p) ≡ p
  ≈head (iso2 p i) = ≈head p
  ≈tail (iso2 p i) = iso2 (≈tail p) i

  path≃bisim : {A : Type₀} → {x y : Stream A} → (x ≡ y) ≃ (x ≈ y)
  path≃bisim = isoToEquiv (iso misib bisim iso2 iso1)

  path≡bisim : {A : Type₀} → {x y : Stream A} → (x ≡ y) ≡ (x ≈ y)
  path≡bisim = ua path≃bisim

  -- misib can be implemented by transport as well.
  refl≈ : {A : Type₀} {x : Stream A} → x ≈ x
  ≈head refl≈ = refl
  ≈tail refl≈ = refl≈

  cast : ∀ {A : Type₀} {x y : Stream A} (p : x ≡ y) → x ≈ y
  cast {x = x} p = transport (λ i → x ≈ p i) refl≈

  misib-refl : ∀ {A : Type₀} {x : Stream A} → misib {x = x} refl ≡ refl≈
  ≈head (misib-refl i) = refl
  ≈tail (misib-refl i) = misib-refl i

  misibTransp : ∀ {A : Type₀} {x y : Stream A} (p : x ≡ y) → cast p ≡ misib p
  misibTransp p = J (λ _ p → cast p ≡ misib p) ((transportRefl refl≈) ∙ (sym misib-refl)) p

module Stream≅Nat→ {A : Type₀} where
  lookup : {A : Type₀} → Stream A → ℕ → A
  lookup xs zero = head xs
  lookup xs (suc n) = lookup (tail xs) n

  tabulate : {A : Type₀} → (ℕ → A) → Stream A
  head (tabulate f) = f zero
  tail (tabulate f) = tabulate (λ n → f (suc n))

  lookup∘tabulate : (λ (x : _ → A) → lookup (tabulate x)) ≡ (λ x → x)
  lookup∘tabulate i f zero = f zero
  lookup∘tabulate i f (suc n) = lookup∘tabulate i (λ n → f (suc n)) n

  tabulate∘lookup : (λ (x : Stream A) → tabulate (lookup x)) ≡ (λ x → x)
  head (tabulate∘lookup i xs) = head xs
  tail (tabulate∘lookup i xs) = tabulate∘lookup i (tail xs)

  Stream≡Nat→ : Stream A ≡ (ℕ → A)
  Stream≡Nat→ = isoToPath (iso lookup tabulate (λ f i → lookup∘tabulate i f) (λ xs i → tabulate∘lookup i xs))

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Monoids where

open import Library

record Monoid {a} : Set (lsuc a) where
  field S   : Set a
        ε   : S
        _•_ : S → S → S
        lid : ∀{m} → ε • m ≅ m
        rid : ∀{m} → m • ε ≅ m
        ass : ∀{m n o} → (m • n) • o ≅ m • (n • o)

  infix 10 _•_

Nat+Mon : Monoid
Nat+Mon = record {
  S   = ℕ;
  ε   = zero;
  _•_ = _+_;
  lid = refl;
  rid = ≡-to-≅ $ +-right-identity _;
  ass = λ{m} → ≡-to-≅ $ +-assoc m _ _}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Species where

-- The Category of Species, as the Functor category from Core (FinSetoids) to Setoids.
-- Setoids used here because that's what fits best in this setting.
-- The constructions of the theory of Species are in Species.Construction

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Construction.Functors
open import Categories.Category.Construction.Core using (Core)
open import Categories.Category.Instance.FinSetoids using (FinSetoids)
open import Categories.Category.Instance.Setoids using (Setoids)

private
  variable
    o ℓ o′ ℓ′ : Level

-- note how Species, as a category, raises levels.
Species : (o ℓ o′ ℓ′ : Level) → Category (suc (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)) (suc (o ⊔ ℓ) ⊔ (o′ ⊔ ℓ′)) (suc (o ⊔ ℓ) ⊔ o′ ⊔ ℓ′)
Species o ℓ o′ ℓ′ = Functors (Core (FinSetoids o ℓ)) (Setoids o′ ℓ′)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Issue451 where

infix 10 _==_
data _==_ {A : Set} (x : A) : (y : A) -> Set where
 refl : x == x

postulate
 Nat : Set

data G : Nat -> Nat -> Set where
 I : (place : Nat) -> G place place
 s : (n m : Nat) -> G n m

mul : (l m n : Nat) -> G m n -> G l m -> G l n
mul a b .b (I .b)   x         = x
mul a .a b x        (I .a)    = x
mul a b c (s .b .c) (s .a .b) = s a c

postulate
  a b c : Nat
  f : G a b

bad : mul a a b (s a b) (I a) == s a b
bad = refl


text:
module guarded-recursion where
import guarded-recursion.prelude
import guarded-recursion.model
import guarded-recursion.model.Agda
import guarded-recursion.embedding
import guarded-recursion.compute
import guarded-recursion.clocks

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
open import Oscar.Prelude
open import Oscar.Class.Successor₀
open import Oscar.Class.Successor₁
open import Oscar.Class.Injectivity
open import Oscar.Class.Thickandthin
open import Oscar.Class.Congruity
open import Oscar.Class.Fmap
open import Oscar.Data.¶
open import Oscar.Data.Fin
open import Oscar.Data.Proposequality
open import Oscar.Data.Maybe
import Oscar.Property.Monad.Maybe
import Oscar.Class.Congruity.Proposequality

module Oscar.Property.Thickandthin.FinFinProposequalityMaybeProposequality where

instance

  𝓢uccessor₀¶ : 𝓢uccessor₀ ¶
  𝓢uccessor₀¶ .𝓢uccessor₀.successor₀ = ↑_

  [𝓢uccessor₁]Fin : [𝓢uccessor₁] Fin
  [𝓢uccessor₁]Fin = ∁

  𝓢uccessor₁Fin : 𝓢uccessor₁ Fin
  𝓢uccessor₁Fin .𝓢uccessor₁.successor₁ = ↑_

  [𝓘njectivity₁]Fin : ∀ {m} → [𝓘njectivity₁] (λ (_ : Fin m) → Fin (⇑₀ m)) Proposequality Proposequality
  [𝓘njectivity₁]Fin = ∁

  𝓘njectivity₁Fin : ∀ {m} → 𝓘njectivity₁ (λ (_ : Fin m) → Fin (⇑₀ m)) Proposequality Proposequality
  𝓘njectivity₁Fin .𝓘njectivity₁.injectivity₁ ∅ = ∅

  [𝓣hick]Fin,Fin : [𝓣hick] Fin Fin
  [𝓣hick]Fin,Fin = ∁

  𝓣hickFin,Fin : 𝓣hick Fin Fin
  𝓣hickFin,Fin .𝓣hick.thick {∅} () ∅
  𝓣hickFin,Fin .𝓣hick.thick {↑ _} _ ∅ = ∅
  𝓣hickFin,Fin .𝓣hick.thick ∅ (↑ y) = y
  𝓣hickFin,Fin .𝓣hick.thick (↑ x) (↑ y) = ↑ thick x y

  [𝓣hin]Fin,Fin : [𝓣hin] Fin Fin
  [𝓣hin]Fin,Fin = ∁

  𝓣hinFin,Fin : 𝓣hin Fin Fin
  𝓣hinFin,Fin .𝓣hin.thin ∅ = ↑_
  𝓣hinFin,Fin .𝓣hin.thin (↑ x) ∅ = ∅
  𝓣hinFin,Fin .𝓣hin.thin (↑ x) (↑ y) = ↑ (thin x y)

  [𝓘njectivity₂,₁]ThinFinFin : ∀ {m} → [𝓘njectivity₂,₁] (𝔱hin Fin Fin m) Proposequality Proposequality
  [𝓘njectivity₂,₁]ThinFinFin = ∁

  𝓘njectivity₂,₁ThinFinFin : ∀ {m} → 𝓘njectivity₂,₁ (𝔱hin Fin Fin m) Proposequality Proposequality
  𝓘njectivity₂,₁ThinFinFin .𝓘njectivity₂,₁.injectivity₂,₁ ∅ ∅ = ∅
  𝓘njectivity₂,₁ThinFinFin .𝓘njectivity₂,₁.injectivity₂,₁ (↑ _) {∅}    {∅} _ = ∅
  𝓘njectivity₂,₁ThinFinFin .𝓘njectivity₂,₁.injectivity₂,₁ (↑ _) {∅}    {↑ _} ()
  𝓘njectivity₂,₁ThinFinFin .𝓘njectivity₂,₁.injectivity₂,₁ (↑ _) {↑ _}  {∅}   ()
  𝓘njectivity₂,₁ThinFinFin .𝓘njectivity₂,₁.injectivity₂,₁ (↑ x) {↑ _}  {↑ _} = congruity ↑_ ∘ injectivity₂,₁ x ∘ injectivity₁[ Proposequality ]

  [𝓒heck]FinFinMaybe : [𝓒heck] Fin Fin Maybe
  [𝓒heck]FinFinMaybe = ∁

  𝓒heckFinFinMaybe : 𝓒heck Fin Fin Maybe
  𝓒heckFinFinMaybe .𝓒heck.check ∅ ∅ = ∅
  𝓒heckFinFinMaybe .𝓒heck.check ∅ (↑ y) = ↑ y
  𝓒heckFinFinMaybe .𝓒heck.check {∅} (↑ ()) _
  𝓒heckFinFinMaybe .𝓒heck.check {↑ _} (↑ x) ∅ = ↑ ∅
  𝓒heckFinFinMaybe .𝓒heck.check {↑ _} (↑ x) (↑ y) = fmap′ ¶⟨<_⟩.↑_ $ check x y

  [𝓣hick/thin=1]FinFin : [𝓣hick/thin=1] Fin Fin Proposequality
  [𝓣hick/thin=1]FinFin = ∁

  𝓣hick/thin=1FinFin : 𝓣hick/thin=1 Fin Fin Proposequality
  𝓣hick/thin=1FinFin .𝓣hick/thin=1.thick/thin=1 x ∅ = ∅
  𝓣hick/thin=1FinFin .𝓣hick/thin=1.thick/thin=1 ∅ (↑ y) = ∅
  𝓣hick/thin=1FinFin .𝓣hick/thin=1.thick/thin=1 (↑ x) (↑ y) = congruity ↑_ (thick/thin=1 x y)

  [𝓒heck/thin=1FinFin] : [𝓒heck/thin=1] Fin Fin Maybe Proposequality
  [𝓒heck/thin=1FinFin] = ∁

  𝓒heck/thin=1FinFin : 𝓒heck/thin=1 Fin Fin Maybe Proposequality
  𝓒heck/thin=1FinFin .𝓒heck/thin=1.check/thin=1 ∅ y = ∅
  𝓒heck/thin=1FinFin .𝓒heck/thin=1.check/thin=1 (↑ x) ∅ = ∅
  𝓒heck/thin=1FinFin .𝓒heck/thin=1.check/thin=1 (↑ x) (↑ y) rewrite check/thin=1 {_≈_ = Proposequality⟦ Maybe _ ⟧} x y = ∅

  IsThickandthinFinFin : IsThickandthin Fin Fin Proposequality Maybe Proposequality
  IsThickandthinFinFin = ∁

ThickandthinFinFin : Thickandthin _ _ _ _ _ _
ThickandthinFinFin = ∁ Fin Fin Proposequality Maybe Proposequality


text:
module UniDB.Subst.Subs where

open import UniDB.Subst.Core
open import UniDB.Morph.Subs

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

module _ {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} where

  instance
    iCompSubs : Comp (Subs T)
    _⊙_ {{iCompSubs}} (refl)      ξ₂          = ξ₂
    _⊙_ {{iCompSubs}} (step ξ₁ t) ξ₂          = step (ξ₁ ⊙ ξ₂) (ap {T} ξ₂ t )
    _⊙_ {{iCompSubs}} (skip ξ₁)   refl        = skip ξ₁
    _⊙_ {{iCompSubs}} (skip ξ₁)   (step ξ₂ t) = step (ξ₁ ⊙ ξ₂) t
    _⊙_ {{iCompSubs}} (skip ξ₁)   (skip ξ₂)   = skip (ξ₁ ⊙ ξ₂)

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

open import Numbers.ClassicalReals.RealField
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition

module Numbers.ClassicalReals.Examples (ℝ : RealField) where

open RealField ℝ
open Setoid S
open Equivalence eq
open Ring R
open Field F
open SetoidPartialOrder pOrder
open import Fields.Orders.LeastUpperBounds.Definition pOrder
open import Rings.Orders.Total.Lemmas orderedRing
open import Rings.Orders.Partial.Lemmas pOrderedRing
open Group additiveGroup
open PartiallyOrderedRing pOrderedRing
open SetoidTotalOrder (TotallyOrderedRing.total orderedRing)
open import Rings.InitialRing R
open import Fields.Orders.Lemmas oField
open import Rings.Lemmas R
open import Groups.Lemmas additiveGroup
open import Numbers.Intervals.Definition pOrderedRing
open import Numbers.Intervals.Arithmetic pOrderedRing
open import Fields.Lemmas F

squarePositive : (a : A) → (((a ∼ 0R) → False) && (0R < (a * a))) || (a ∼ 0R)
squarePositive a with totality 0R a
squarePositive a | inl (inl x) = inl ((λ a=0 → irreflexive (<WellDefined reflexive a=0 x)) ,, orderRespectsMultiplication x x)
squarePositive a | inl (inr x) = inl ((λ a=0 → irreflexive (<WellDefined a=0 reflexive x)) ,, <WellDefined reflexive twoNegativesTimes (orderRespectsMultiplication (<WellDefined invIdent reflexive (ringSwapNegatives' x)) (<WellDefined invIdent reflexive (ringSwapNegatives' x))))
squarePositive a | inr 0=a = inr (symmetric 0=a)

fraction<1 : (n m : ℕ) → n <N m → (0<m : fromN m ∼ 0G → False) → ((fromN n) * underlying (allInvertible (fromN m) 0<m)) < 1R
fraction<1 n m n<m 0<m with allInvertible (fromN m) 0<m
... | 1/m , prM = <WellDefined reflexive (transitive *Commutative prM) (ringCanMultiplyByPositive (inversePositiveIsPositive prM (fromNPreservesOrder (0<1 nontrivial) {0} {m} (zeroLeast n<m))) (fromNPreservesOrder (0<1 nontrivial) n<m))

1/2 : A
1/2 = underlying (allInvertible (1R + 1R) (orderedImpliesCharNot2 nontrivial))

pr1/2 : (1/2 * (1R + 1R)) ∼ 1R
pr1/2 with allInvertible (1R + 1R) (orderedImpliesCharNot2 nontrivial)
... | x , pr = pr

pr1/2' : (1/2 + 1/2) ∼ 1R
pr1/2' = transitive (symmetric (transitive *DistributesOver+ (+WellDefined (transitive *Commutative identIsIdent) (transitive *Commutative identIsIdent)))) pr1/2

1/2<1 : 1/2 < 1R
1/2<1 = <WellDefined (transitive (*WellDefined identRight (allInvertibleWellDefined (+WellDefined reflexive identRight))) identIsIdent) reflexive (fraction<1 1 2 (le 0 refl) λ p → charZero 1 (symmetric p))

3/2<2 : (fromN 3 * 1/2) < (1R + 1R)
3/2<2 = <WellDefined (transitive (+WellDefined reflexive (transitive (symmetric pr1/2) (transitive *Commutative (*WellDefined (+WellDefined reflexive (symmetric identRight)) reflexive)))) (symmetric *DistributesOver+')) reflexive (orderRespectsAddition (<WellDefined (symmetric identIsIdent) reflexive 1/2<1) 1R)

2<9/4 : (1R + 1R) < ((fromN 3 * 1/2) * (fromN 3 * 1/2))
2<9/4 = <WellDefined reflexive (symmetric *Associative) (halveInequality _ _ 1/2 pr1/2' (<WellDefined reflexive (transitive (symmetric *Associative) *Commutative) (halveInequality _ _ 1/2 pr1/2' (<WellDefined (transitive (fromNPreserves* 4 2) (transitive (*WellDefined (+WellDefined reflexive (+WellDefined reflexive (+WellDefined reflexive identRight))) (+WellDefined reflexive identRight)) (transitive *DistributesOver+ (+WellDefined (transitive *Commutative (transitive identIsIdent +Associative)) (transitive *Commutative (transitive identIsIdent +Associative)))))) (fromNPreserves* 3 3) (fromNPreservesOrder (0<1 nontrivial) (le {8} 0 refl))))))

0<2 : 0R < (1R + 1R)
0<2 = <WellDefined identLeft reflexive (ringAddInequalities (0<1 nontrivial) (0<1 nontrivial))

0<3/2 : 0R < (fromN 3 * 1/2)
0<3/2 = orderRespectsMultiplication (fromNPreservesOrder (0<1 nontrivial) (le {0} {3} 2 refl)) (inversePositiveIsPositive pr1/2 0<2)

3/2ub : {r : A} → (r * r) < (1R + 1R) → (r < (fromN 3 * 1/2))
3/2ub {r} r^2<2 with totality r (fromN 3 * 1/2)
3/2ub {r} r^2<2 | inl (inl r<3/2) = r<3/2
3/2ub {r} r^2<2 | inl (inr 3/2<r) = exFalso (irreflexive (<Transitive r^2<2 (<Transitive 2<9/4 (ringMultiplyPositives 0<3/2 0<3/2 3/2<r 3/2<r))))
3/2ub {r} r^2<2 | inr r=3/2 = exFalso (irreflexive (<Transitive r^2<2 (<WellDefined reflexive (symmetric (*WellDefined r=3/2 r=3/2)) 2<9/4)))

2/6<1 : ((1R + 1R) * underlying (allInvertible (fromN 6) (charZero' 5))) < 1R
2/6<1 with allInvertible (fromN 6) (charZero' 5)
2/6<1 | 1/6 , pr1/6 = <WellDefined reflexive (transitive *Commutative pr1/6) (ringCanMultiplyByPositive (inversePositiveIsPositive pr1/6 (fromNPreservesOrder (0<1 nontrivial) {0} {6} (le 5 refl))) (<WellDefined (+WellDefined reflexive identRight) reflexive (fromNPreservesOrder (0<1 nontrivial) {2} {6} (le 3 refl))))

2<2*2 : (1R + 1R) < ((1R + 1R) * (1R + 1R))
2<2*2 = (<WellDefined (+WellDefined reflexive identRight) (transitive (fromNPreserves* 2 2) (*WellDefined (+WellDefined reflexive identRight) (+WellDefined reflexive identRight))) (fromNPreservesOrder (0<1 nontrivial) {2} {4} (le 1 refl)))

square<2Means<2 : (u : A) → (u * u) < (1R + 1R) → u < (1R + 1R)
square<2Means<2 u u^2<2 with totality u (1R + 1R)
square<2Means<2 u u^2<2 | inl (inl x) = x
square<2Means<2 u u^2<2 | inl (inr x) = exFalso (irreflexive (<Transitive u^2<2 (<Transitive 2<2*2 (ringMultiplyPositives 0<2 0<2 x x))))
square<2Means<2 u u^2<2 | inr u=2 = exFalso (irreflexive (<Transitive (<WellDefined (*WellDefined u=2 u=2) reflexive u^2<2) 2<2*2))

2=2*2-2 : (fromN 2) ∼ (((1R + 1R) * (1R + 1R)) + inverse (fromN 2))
2=2*2-2 = transitive (+WellDefined reflexive identRight) (transitive (transitive (transitive (transitive (symmetric identRight) (+WellDefined reflexive (symmetric invRight))) +Associative) (+WellDefined (symmetric (+WellDefined (+WellDefined identIsIdent identIsIdent) (+WellDefined identIsIdent identIsIdent))) reflexive)) (+WellDefined (transitive (+WellDefined (symmetric *DistributesOver+') (symmetric *DistributesOver+')) (symmetric *DistributesOver+)) (inverseWellDefined (symmetric (+WellDefined reflexive identRight)))))

sqrtRespectsInequality : {x y : A} → (x * x) < (y * y) → 0R < y → x < y
sqrtRespectsInequality {x} {y} x^2<y^2 _ with totality x y
sqrtRespectsInequality {x} {y} x^2<y^2 _ | inl (inl x<y) = x<y
sqrtRespectsInequality {x} {y} x^2<y^2 0<y | inl (inr y<x) = exFalso (irreflexive (<Transitive x^2<y^2 (ringMultiplyPositives 0<y 0<y y<x y<x)))
sqrtRespectsInequality {x} {y} x^2<y^2 _ | inr x=y = exFalso (irreflexive (<WellDefined (*WellDefined x=y x=y) reflexive x^2<y^2))

sqrt2 : Sg A (λ i → (i * i) ∼ (1R + 1R))
sqrt2 = sqrt2' , sqrt2IsSqrt2
  where
    pred : A → Set c
    pred a = (a * a) < (1R + 1R)
    sub : subset S pred
    sub {y} x=y x^2<2 = <WellDefined (*WellDefined x=y x=y) reflexive x^2<2
    abstract
      2ub : UpperBound sub (1R + 1R)
      2ub y y^2<2 with totality y (1R + 1R)
      2ub y y^2<2 | inl (inl y<2) = inl y<2
      2ub y y^2<2 | inl (inr 2<y) = exFalso (irreflexive (<Transitive y^2<2 (<Transitive s r)))
        where
          r : ((1R + 1R) * (1R + 1R)) < (y * y)
          r = ringMultiplyPositives 0<2 0<2 2<y 2<y
          s : (1R + 1R) < ((1R + 1R) * (1R + 1R))
          s = <WellDefined reflexive (symmetric *DistributesOver+) (<WellDefined reflexive (+WellDefined (transitive (symmetric identIsIdent) *Commutative) (transitive (symmetric identIsIdent) *Commutative)) (<WellDefined identLeft reflexive (orderRespectsAddition 0<2 (1R + 1R))))
      2ub y y^2<2 | inr y=2 = inr y=2
    abstract
      sup : Sg A (LeastUpperBound sub)
      sup = lub sub (0R , <Transitive (<WellDefined (symmetric timesZero) (symmetric identLeft) (0<1 nontrivial)) (orderRespectsAddition (0<1 nontrivial) 1R)) ((1R + 1R) , 2ub)
    sqrt2' : A
    sqrt2' = underlying sup
    sqrt2IsSqrt2 : (sqrt2' * sqrt2') ∼ (1R + 1R)
    sqrt2IsSqrt2 with totality (sqrt2' * sqrt2') (1R + 1R)
    sqrt2IsSqrt2 | inl (inl sup^2<2) with sup
    sqrt2IsSqrt2 | inl (inl sup^2<2) | sqrt2' , record { upperBound = upperBound ; leastUpperBound = leastUpperBound } = exFalso bad
      where
        abstract
          t : A
          t = ((fromN 2) + inverse (sqrt2' * sqrt2')) * (underlying (allInvertible (fromN 6) (charZero' 5)))
          pr' : (underlying (allInvertible (fromN 6) (charZero' 5)) * fromN 6) ∼ 1R
          pr' with allInvertible (fromN 6) (charZero' 5)
          ... | x , p = p
          crudeBound : isInInterval (sqrt2' * sqrt2') record { minBound = 0R ; maxBound = 1R + 1R }
          crudeBound with squarePositive sqrt2'
          crudeBound | inl (_ ,, snd) = snd ,, sup^2<2
          crudeBound | inr sqrt2=0 with upperBound 1R (<WellDefined (transitive identRight (symmetric identIsIdent)) (+WellDefined reflexive identRight) (fromNPreservesOrder (0<1 nontrivial) {1} {2} (le 0 refl)))
          crudeBound | inr sqrt2=0 | inl 1<sqrt2 = exFalso (irreflexive (<Transitive 1<sqrt2 (<WellDefined (symmetric sqrt2=0) reflexive (0<1 nontrivial))))
          crudeBound | inr sqrt2=0 | inr 1=sqrt2 = exFalso (nontrivial (transitive (symmetric sqrt2=0) (symmetric 1=sqrt2)))
          crudeBound' : isInInterval (inverse (sqrt2' * sqrt2')) record { minBound = inverse (1R + 1R) ; maxBound = inverse 0R }
          crudeBound' = intervalInverseContains crudeBound
          numeratorBound : isInInterval (inverse (sqrt2' * sqrt2') + fromN 2) record { minBound = 0R ; maxBound = 1R + 1R }
          numeratorBound = intervalWellDefined (transitive groupIsAbelian (transferToRight'' (transitive +Associative identRight)) ,, transitive (+WellDefined invIdent reflexive) (transitive identLeft (+WellDefined reflexive identRight))) (intervalConstantSumContains (fromN 2) crudeBound')
          numeratorBound' : isInInterval (fromN 2 + inverse (sqrt2' * sqrt2')) record { minBound = 0R ; maxBound = 1R + 1R }
          numeratorBound' = intervalWellDefined' groupIsAbelian numeratorBound
          tBound : isInInterval t record { minBound = 0R ; maxBound = (1R + 1R) * (underlying (allInvertible (fromN 6) (charZero' 5))) }
          tBound = intervalWellDefined (transitive *Commutative timesZero ,, reflexive) (intervalConstantProductContains (inversePositiveIsPositive pr' (fromNPreservesOrder (0<1 nontrivial) {0} {6} (le 5 refl))) numeratorBound')
          u : ((((fromN 5) * ((fromN 2) + inverse (sqrt2' * sqrt2'))) * underlying (allInvertible (fromN 6) (charZero' 5))) + (sqrt2' * sqrt2')) < ((fromN 2 + inverse (sqrt2' * sqrt2')) + (sqrt2' * sqrt2'))
          u = orderRespectsAddition (<WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive *Commutative) *Associative)) identIsIdent (ringCanMultiplyByPositive {(fromN 5) * underlying (allInvertible (fromN 6) (charZero' 5))} {1R} {fromN 2 + inverse (sqrt2' * sqrt2')} (moveInequality (<WellDefined reflexive (transitive (symmetric identRight) (symmetric +Associative)) sup^2<2)) (fraction<1 5 6 (le zero refl) λ pr → charZero' 5 pr))) (sqrt2' * sqrt2')
          tBound' : (((fromN 5) * t) + (sqrt2' * sqrt2')) < (1R + 1R)
          tBound' = <WellDefined (+WellDefined (symmetric *Associative) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) (transitive identRight (+WellDefined reflexive identRight)))) u
          sqrt2<2 : sqrt2' < (1R + 1R)
          sqrt2<2 with leastUpperBound (fromN 3 * 1/2) (λ r s → inl (3/2ub s))
          sqrt2<2 | inl x = <Transitive x 3/2<2
          sqrt2<2 | inr x = <WellDefined (symmetric x) reflexive 3/2<2
          2sqrt2<4 : (sqrt2' + sqrt2') < fromN 4
          2sqrt2<4 = <WellDefined (transitive *DistributesOver+ (+WellDefined (transitive *Commutative identIsIdent) (transitive *Commutative identIsIdent))) (transitive (transitive (*WellDefined (symmetric identRight) (symmetric identRight)) (*WellDefined (symmetric +Associative) (symmetric +Associative))) (symmetric (fromNPreserves* 2 2))) (ringCanMultiplyByPositive {sqrt2'} {1R + 1R} {1R + 1R} (<WellDefined identLeft reflexive (ringAddInequalities (0<1 nontrivial) (0<1 nontrivial))) sqrt2<2)
          t<1 : t < 1R
          t<1 = <Transitive (_&&_.snd tBound) 2/6<1
          newElementIsElement : ((sqrt2' + t) * (sqrt2' + t)) < (1R + 1R)
          newElementIsElement = <WellDefined (symmetric *DistributesOver+') reflexive (<WellDefined (+WellDefined (symmetric *DistributesOver+) reflexive) reflexive (<WellDefined (transitive groupIsAbelian +Associative) reflexive (<Transitive (orderRespectsAddition (<WellDefined (+WellDefined *Commutative reflexive) reflexive (<WellDefined (transitive *Commutative *DistributesOver+) reflexive (ringCanMultiplyByPositive (_&&_.fst tBound) (<WellDefined (symmetric +Associative) reflexive (<Transitive (orderRespectsAddition 2sqrt2<4 t) (<WellDefined groupIsAbelian reflexive (<WellDefined reflexive (reflexive {fromN 5}) (orderRespectsAddition t<1 (fromN 4))))))))) (sqrt2' * sqrt2')) tBound')))
        bad : False
        bad with upperBound (sqrt2' + t) newElementIsElement
        bad | inl x = irreflexive (<Transitive x (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (_&&_.fst tBound) sqrt2')))
        bad | inr x = irreflexive (<WellDefined identLeft (transitive groupIsAbelian x) (orderRespectsAddition (_&&_.fst tBound) sqrt2'))
    sqrt2IsSqrt2 | inl (inr 2<sup^2) with sup
    sqrt2IsSqrt2 | inl (inr 2<sup^2) | sqrt2' , record { upperBound = upperBound ; leastUpperBound = leastUpperBound } = exFalso bad
      where
        abstract
          1<sqrt2 : 1R < sqrt2'
          1<sqrt2 with upperBound 1R (<WellDefined (transitive identRight (symmetric identIsIdent)) (+WellDefined reflexive identRight) (fromNPreservesOrder (0<1 nontrivial) {1} {2} (le zero refl)))
          1<sqrt2 | inl x = x
          1<sqrt2 | inr x = exFalso (irreflexive (<Transitive 2<sup^2 (<WellDefined (transitive identRight (transitive (symmetric identIsIdent) (*WellDefined x x))) (+WellDefined reflexive identRight) (fromNPreservesOrder (0<1 nontrivial) {1} {2} (le 0 refl)))))
          0<sqrt2 : 0R < sqrt2'
          0<sqrt2 = <Transitive (0<1 nontrivial) 1<sqrt2
          sqrt2<2 : sqrt2' < (1R + 1R)
          sqrt2<2 with leastUpperBound (fromN 3 * 1/2) (λ r s → inl (3/2ub s))
          sqrt2<2 | inl x = <Transitive x 3/2<2
          sqrt2<2 | inr x = <WellDefined (symmetric x) reflexive 3/2<2
          2sqrt2<4 : (sqrt2' + sqrt2') < fromN 4
          2sqrt2<4 = <WellDefined (transitive *DistributesOver+ (+WellDefined (transitive *Commutative identIsIdent) (transitive *Commutative identIsIdent))) (transitive (transitive (*WellDefined (symmetric identRight) (symmetric identRight)) (*WellDefined (symmetric +Associative) (symmetric +Associative))) (symmetric (fromNPreserves* 2 2))) (ringCanMultiplyByPositive {sqrt2'} {1R + 1R} {1R + 1R} (<WellDefined identLeft reflexive (ringAddInequalities (0<1 nontrivial) (0<1 nontrivial))) sqrt2<2)
          t : A
          t = ((sqrt2' * sqrt2') + inverse (fromN 2)) * underlying (allInvertible (fromN 4) (charZero' 3))
          pr1 : inverse (fromN 4 * t) ∼ (inverse (sqrt2' * sqrt2') + (fromN 2))
          pr1 with allInvertible (fromN 4) (charZero' 3)
          ... | 1/4 , pr1/4 = transitive (transitive (transitive (transitive (symmetric ringMinusExtracts) (transitive (transitive (*WellDefined reflexive (transitive (symmetric ringMinusExtracts') (transitive *Commutative (*WellDefined reflexive (transitive invContravariant (transitive groupIsAbelian (+WellDefined reflexive invInv))))))) *Associative) *Commutative)) (*WellDefined reflexive (transitive *Commutative pr1/4))) *Commutative) identIsIdent
          t<sqrt2 : t < sqrt2'
          t<sqrt2 with allInvertible (fromN 4) (charZero' 3)
          ... | 1/4 , pr4 = <WellDefined reflexive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive (transitive *Commutative pr4)) (transitive *Commutative identIsIdent))) (ringCanMultiplyByPositive (inversePositiveIsPositive pr4 (fromNPreservesOrder (0<1 nontrivial) {0} {4} (le 3 refl))) (<Transitive (orderRespectsAddition (ringMultiplyPositives 0<sqrt2 0<sqrt2 sqrt2<2 sqrt2<2) (inverse (1R + (1R + 0G)))) (<WellDefined {fromN 2} 2=2*2-2 reflexive (<Transitive {fromN 2} {sqrt2' * fromN 2} (<WellDefined identIsIdent reflexive (ringCanMultiplyByPositive (fromNPreservesOrder (0<1 nontrivial) {0} (le 1 refl)) 1<sqrt2)) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive 0<sqrt2 (fromNPreservesOrder (0<1 nontrivial) {2} (le 1 refl))))))))
          0<t : 0R < t
          0<t with allInvertible (fromN 4) (charZero' 3)
          ... | 1/4 , pr4 = orderRespectsMultiplication (<WellDefined reflexive (+WellDefined reflexive (inverseWellDefined (+WellDefined reflexive (symmetric identRight)))) (moveInequality 2<sup^2)) (inversePositiveIsPositive pr4 (fromNPreservesOrder (0<1 nontrivial) {0} {4} (le 3 refl)))
        anotherUpperBound : A
        anotherUpperBound = (sqrt2' + inverse t) * (sqrt2' + inverse t)
        abstract
          u : anotherUpperBound ∼ ((sqrt2' * sqrt2') + (inverse ((t * sqrt2') + (t * sqrt2')) + (t * t)))
          u = transitive *DistributesOver+' (transitive (+WellDefined *DistributesOver+ reflexive) (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined ringMinusExtracts *DistributesOver+) (transitive +Associative (+WellDefined (transitive (+WellDefined (inverseWellDefined *Commutative) ringMinusExtracts') (symmetric invContravariant)) twoNegativesTimes))))))
          w : ((sqrt2' * sqrt2') + inverse ((fromN 4) * t)) < anotherUpperBound
          w = <WellDefined reflexive (symmetric u) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<WellDefined (ringMinusExtracts') (+WellDefined (inverseWellDefined (*DistributesOver+)) reflexive) (<WellDefined reflexive (+WellDefined ringMinusExtracts reflexive) (<WellDefined reflexive *DistributesOver+ (<WellDefined reflexive *Commutative (ringCanMultiplyByPositive 0<t (<WellDefined identRight reflexive (ringAddInequalities (ringSwapNegatives' (<WellDefined reflexive (transitive (+WellDefined (+WellDefined reflexive (symmetric identRight)) (+WellDefined reflexive (symmetric identRight))) (symmetric (fromNPreserves+ 2 2))) (ringAddInequalities sqrt2<2 sqrt2<2))) 0<t))))))) (sqrt2' * sqrt2')))
          w' : ((sqrt2' * sqrt2') + inverse ((fromN 4) * t)) ∼ (1R + 1R)
          w' = transitive (+WellDefined reflexive pr1) (transitive +Associative (transitive (+WellDefined invRight reflexive) (transitive identLeft (+WellDefined reflexive identRight))))
          anotherUpperBoundBounds : (1R + 1R) < anotherUpperBound
          anotherUpperBoundBounds = <WellDefined w' reflexive w
        aubIsBound : UpperBound sub (sqrt2' + inverse t)
        aubIsBound y y^2<2 with totality y (sqrt2' + inverse t)
        aubIsBound y y^2<2 | inl (inl x) = inl x
        aubIsBound y y^2<2 | inl (inr x) = exFalso (irreflexive (<Transitive (<Transitive anotherUpperBoundBounds (ringMultiplyPositives (moveInequality t<sqrt2) (moveInequality t<sqrt2) x x)) y^2<2))
        aubIsBound y y^2<2 | inr x = inr x
        bad : False
        bad with leastUpperBound (sqrt2' + inverse t) aubIsBound
        bad | inl x = irreflexive (<Transitive x (<WellDefined groupIsAbelian identLeft (orderRespectsAddition (ringMinusFlipsOrder 0<t) sqrt2')))
        bad | inr x = irreflexive (<WellDefined (symmetric (transitive x groupIsAbelian)) identLeft (orderRespectsAddition (ringMinusFlipsOrder 0<t) sqrt2'))
    sqrt2IsSqrt2 | inr x = x


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

open import Cubical.Algebra.Field.Base public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

import Agda.Primitive.Cubical as C

-- Cannot alias module exporting primitives with typechecking constraints.
module M = C

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Fragment.Setoid.Morphism where

open import Fragment.Setoid.Morphism.Base public
open import Fragment.Setoid.Morphism.Setoid public
open import Fragment.Setoid.Morphism.Properties public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------------
-- Totality properties respect to Tree
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.TreeATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList
open import FOTC.Data.Nat.Inequalities

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

toTree-Tree : ∀ {item t} → N item → Tree t → Tree (toTree · item · t)
toTree-Tree {item} Nitem tnil = prf
  where postulate prf : Tree (toTree · item · nil)
        {-# ATP prove prf #-}

toTree-Tree {item} Nitem (ttip {i} Ni) = prf (x>y∨x≤y Ni Nitem)
  where postulate prf : i > item ∨ i ≤ item → Tree (toTree · item · tip i)
        {-# ATP prove prf x>y→x≰y #-}
toTree-Tree {item} Nitem (tnode {t₁} {i} {t₂} Tt₁ Ni Tt₂) =
  prf (x>y∨x≤y Ni Nitem) (toTree-Tree Nitem Tt₁) (toTree-Tree Nitem Tt₂)
  where
  postulate prf : i > item ∨ i ≤ item →
                  Tree (toTree · item · t₁) →
                  Tree (toTree · item · t₂) →
                  Tree (toTree · item · node t₁ i t₂)
  {-# ATP prove prf x>y→x≰y #-}

makeTree-Tree : ∀ {is} → ListN is → Tree (makeTree is)
makeTree-Tree lnnil = prf
  where postulate prf : Tree (makeTree [])
        {-# ATP prove prf #-}

makeTree-Tree (lncons {i} {is} Nn Lis) = prf (makeTree-Tree Lis)
  where postulate prf : Tree (makeTree is) → Tree (makeTree (i ∷ is))
        {-# ATP prove prf toTree-Tree #-}


text:
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --show-implicit #-}

open import Oscar.Prelude
open import Oscar.Class

-- classes
open import Oscar.Class.Transitivity

-- data
open import Oscar.Data.Substitunction
open import Oscar.Data.Term

module Test.EquivalentCandidates-2 where

module _
  {a}
  where

  instance

    𝓣ransitivityFunction₁ : Transitivity.class Function⟦ a ⟧
    𝓣ransitivityFunction₁ .⋆ f g = g ∘ f

    𝓣ransitivityFunction₂ : Transitivity.class Function⟦ a ⟧
    𝓣ransitivityFunction₂ .⋆ f g = g ∘ f

module _ (𝔓 : Ø₀) where

  open Substitunction 𝔓
  open Term 𝔓

  test-1 test-2 test-3 test-4 test-5 test-6 :
    ∀ {m n} (f : Substitunction m n) → Substitunction m n

  test-1 f = transitivity {!!} {!!}
  test-2 f = transitivity {𝔒 = Ø₀} {_∼_ = Function⟦ ∅̂ ⟧} {!!} {!!}
  test-3 f = transitivity f {!!}
  test-4 {m} {n} f = transitivity {𝔒 = Ø₀} f (¡ {𝔒 = Term n})
  test-5 f = transitivity {_∼_ = Function⟦ ∅̂ ⟧} f {!!}
  test-6 {m} {n} f = transitivity {𝔒 = Ø₀} ⦃ {!!} ⦄ f (¡ {𝔒 = Term n})


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

open import lib.Base

module test.fail.Test1 where

module _ where

  private
    data #I-aux : Type₀ where
      #zero : #I-aux
      #one : #I-aux

    data #I : Type₀ where
      #i : #I-aux → (Unit → Unit) → #I

  I : Type₀
  I = #I

  zero : I
  zero = #i #zero _

  one : I
  one = #i #one _

  postulate
    seg : zero == one

absurd : zero ≠ one
absurd ()  -- fails

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero + b = b
suc a + b = suc (a + b)
infix 100 _+_

data _≡_ : ℕ → ℕ → Set where
  refl : {n : ℕ} → n ≡ n

sym : {n m : ℕ} → n ≡ m → m ≡ n
sym refl = refl

trans : {m n o : ℕ} → m ≡ n → n ≡ o → m ≡ o
trans refl p₂ = p₂

suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ n
suc-inj refl = refl

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

_≢_ : ℕ → ℕ → Set
m ≢ n = ¬(m ≡ n)

zero-img : ∀ {m} → suc m ≢ 0
zero-img ()

induction : (P : ℕ → Set) → P 0 → (∀ {n} → P n → P (suc n)) → (∀ m → P m)
induction pred base hypo zero = base
induction pred base hypo (suc m) = hypo (induction pred base hypo m)

cong : ∀ {m n} → (f : ℕ → ℕ) → m ≡ n → f m ≡ f n
cong f refl = refl

assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
assoc zero n o = refl
assoc (suc m) n o = cong suc (assoc m n o)

n+zero : ∀ n → n ≡ n + 0
n+zero zero = refl
n+zero (suc n) = cong suc (n+zero n)

suc+ : ∀ m n → suc (n + m) ≡ (n + suc m)
suc+ m zero = refl
suc+ m (suc n) = cong suc (suc+ m n)

comm : ∀ m n → m + n ≡ n + m
comm zero n = n+zero n
comm (suc m) n = trans (cong suc (comm m n)) (suc+ m n)

-- Where to go from here?
-- Agda:
--   • Aaron Stump - Verified Functional Programming in Agda, https://svn.divms.uiowa.edu/repos/clc/projects/agda/book/book.pdf
--   • Conor McBride - Dependently Typed Metaprogramming (in Agda), http://cs.ioc.ee/ewscs/2014/mcbride/mcbride-deptypedmetaprog.pdf
-- Type theory:
--   • So you want to learn type theory, http://purelytheoretical.com/sywtltt.html


text:
module UnifyTermF (FunctionName : Set) where

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

data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : Term n
  _fork_ : (s t : Term n) -> Term n
  function : FunctionName → ∀ {f} → Vec (Term n) f → Term n

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

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

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

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

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

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

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

_~>_ : (m n : ℕ) -> Set
m ~> n = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

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

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

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

open Substitution ⦃ … ⦄ public

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

mutual

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

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

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

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

open SubstitutionExtensionality ⦃ … ⦄ public

mutual

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

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

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

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

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

open import Prelude using (it)

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

  open Fact1 ⦃ … ⦄ public

  mutual

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

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

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

  open Fact2 ⦃ … ⦄ public

  mutual

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

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

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

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

open import Agda.Primitive

Injectivity : ∀ {a} {A : Set a} {b} {B : Set b} (f : A → B) → Set (a ⊔ b)
Injectivity f = ∀ {x y} → f x ≡ f y → x ≡ y

Injectivity₂ : ∀ {a} {A : Set a} {b} {B : Set b} {c} {C : Set c} (f : A → B → C) → Set (a ⊔ b ⊔ c)
Injectivity₂ f = ∀ {w x y z} → f w x ≡ f y z → x ≡ z

record Injective {a} {A : Set a} {b} {B : Set b} (f : A → B) : Set (a ⊔ b) where
  field injectivity : ∀ x y → f x ≡ f y → x ≡ y

open Injective public -- ⦃ … ⦄ public

record Thin (T : ℕ → Set) : Set where
  field
    thin : ∀ {n} -> Fin (suc n) → T n → T (suc n)
    thinfact1 : ∀ {n} (f : Fin (suc n)) → Injectivity (thin f)

term-i-inj : ∀ {n} → Injectivity (Term.i {n})
term-i-inj refl = refl

term-fork-l-inj : ∀ {n} → Injectivity₂ (flip (_fork_ {n}))
term-fork-l-inj refl = refl

term-fork-r-inj : ∀ {n} → Injectivity₂ (_fork_ {n})
term-fork-r-inj refl = refl

open Thin ⦃ … ⦄ public

p : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
p (suc x) = x
p zero = zero

instance ThinFin : Thin Fin
Thin.thin ThinFin zero y = suc y
Thin.thin ThinFin (suc x) zero = zero
Thin.thin ThinFin (suc x) (suc y) = suc (thin x y)
Thin.thinfact1 ThinFin zero refl = refl
Thin.thinfact1 ThinFin (suc x) {zero} {zero} r = refl
Thin.thinfact1 ThinFin (suc x) {zero} {(suc z)} ()
Thin.thinfact1 ThinFin (suc x) {(suc y)} {zero} ()
Thin.thinfact1 ThinFin (suc x) {(suc y)} {(suc z)} r =
  cong suc (thinfact1 x (cong p r))

{- TODO defining using the below leads to termination checker problem -}
tfact1 : ∀ {n} (x : Fin (suc n)) (y : Fin _) (z : Fin n) -> thin x y ≡ thin x z -> y ≡ z
tfact1 zero y .y refl = refl
tfact1 (suc x) zero zero r = refl
tfact1 (suc x) zero (suc z) ()
tfact1 (suc x) (suc y) zero ()
tfact1 (suc x) (suc y) (suc z) r = cong suc (tfact1 x y z (cong p r))

mutual

  mapTerm : ∀ {n m} → (Fin n → Fin m) → Term n → Term m
  mapTerm x (i x₁) = i (x x₁)
  mapTerm x leaf = leaf
  mapTerm x (x₁ fork x₂) = mapTerm x x₁ fork mapTerm x x₂
  mapTerm x (function x₁ x₂) = function x₁ (mapTerms x x₂)

  mapTerms : ∀ {n m} → (Fin n → Fin m) → ∀ {N} → Vec (Term n) N → Vec (Term m) N
  mapTerms x [] = []
  mapTerms x (x₁ ∷ x₂) = mapTerm x x₁ ∷ mapTerms x x₂

mutual

  thinfact1Term : ∀ {n} (f : Fin (suc n)) → Injectivity (mapTerm (thin f))
  thinfact1Term x₁ {i x} {i x₃} x₂ = cong i (thinfact1 x₁ (term-i-inj x₂))
  thinfact1Term x₁ {i x} {leaf} ()
  thinfact1Term x₁ {i x} {y fork y₁} ()
  thinfact1Term x₁ {i x} {function x₂ x₃} ()
  thinfact1Term x₁ {leaf} {i x} ()
  thinfact1Term x₁ {leaf} {leaf} x₂ = refl
  thinfact1Term x₁ {leaf} {y fork y₁} ()
  thinfact1Term x₁ {leaf} {function x x₂} ()
  thinfact1Term x₁ {x fork x₂} {i x₃} ()
  thinfact1Term x₁ {x fork x₂} {leaf} ()
  thinfact1Term x₁ {x fork x₂} {y fork y₁} x₃ = cong₂ _fork_ (thinfact1Term x₁ (term-fork-l-inj x₃)) ((thinfact1Term x₁ (term-fork-r-inj x₃)))
  thinfact1Term x₁ {x fork x₂} {function x₃ x₄} ()
  thinfact1Term x₁ {function x x₂} {i x₃} ()
  thinfact1Term x₁ {function x x₂} {leaf} ()
  thinfact1Term x₁ {function x x₂} {y fork y₁} ()
  thinfact1Term x₁ {function f1 {n} ts1} {function f2 ts2} r rewrite Term-function-inj-FunctionName r with Term-function-inj-VecSize r
  thinfact1Term x₁ {function f1 {n} ts1} {function f2 ts2} r | refl with Term-function-inj-Vector r
  thinfact1Term {m} x₁ {function f1 {n} ts1} {function f2 {.n} ts2} r | refl | w = cong (function f2) (((thinfact1Terms x₁ w)))

  thinfact1Terms : ∀ {N} {n} (f : Fin (suc n)) → Injectivity (mapTerms (thin f) {N})
  thinfact1Terms {.0} f {[]} {[]} x₁ = refl
  thinfact1Terms {.(suc _)} f {x ∷ x₁} {x₂ ∷ y} x₃ = cong₂ _∷_ (thinfact1Term f (cong Data.Vec.head x₃)) (thinfact1Terms f (cong Data.Vec.tail x₃))

mutual

  instance ThinTerm : Thin Term
  Thin.thin ThinTerm = mapTerm ∘ thin
  Thin.thinfact1 ThinTerm = thinfact1Term

  instance ThinTermVec : ∀ {N} → Thin (flip Vec N ∘ Term)
  Thin.thin ThinTermVec x x₁ = mapTerms (thin x) x₁
  Thin.thinfact1 ThinTermVec = thinfact1Terms

module ThinFact where

  fact2 : ∀ {n} x (y : Fin n) -> ¬ thin x y ≡ x
  fact2 zero y ()
  fact2 (suc x) zero ()
  fact2 (suc x) (suc y) r = fact2 x y (cong p r)

  fact3 : ∀{n} x (y : Fin (suc n)) -> ¬ x ≡ y -> ∃ λ y' -> thin x y' ≡ y
  fact3 zero zero ne = ⊥-elim (ne refl)
  fact3 zero (suc y) _ = y , refl
  fact3 {zero} (suc ()) _ _
  fact3 {suc n} (suc x) zero ne = zero , refl
  fact3 {suc n} (suc x) (suc y) ne with y | fact3 x y (ne ∘ cong suc)
  ... | .(thin x y') | y' , refl = suc y' , refl

open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

thick : ∀ {n} -> (x y : Fin (suc n)) -> Maybe (Fin n)
thick zero zero = nothing
thick zero (suc y) = just y
thick {zero} (suc ()) _
thick {suc _} (suc x) zero = just zero
thick {suc _} (suc x) (suc y) = suc <$> (thick x y)

open import Data.Sum

_≡Fin_ : ∀ {n} -> (x y : Fin n) -> Dec (x ≡ y)
zero ≡Fin zero = yes refl
zero ≡Fin suc y = no λ ()
suc x ≡Fin zero = no λ ()
suc {suc _} x ≡Fin suc y with x ≡Fin y
...              | yes r = yes (cong suc r)
...              | no r = no λ e -> r (cong p e)
suc {zero} () ≡Fin _

module Thick where

  half1 : ∀ {n} (x : Fin (suc n)) -> thick x x ≡ nothing
  half1 zero = refl
  half1 {suc _} (suc x) = cong (_<$>_ suc) (half1 x)
  half1 {zero} (suc ())

  half2 : ∀ {n} (x : Fin (suc n)) y -> ∀ y' -> thin x y' ≡ y -> thick x y ≡ just y'
  half2 zero zero y' ()
  half2 zero (suc y) .y refl = refl
  half2 {suc n} (suc x) zero zero refl = refl
  half2 {suc _} (suc _) zero (suc _) ()
  half2 {suc n} (suc x) (suc y) zero ()
  half2 {suc n} (suc x) (suc .(thin x y')) (suc y') refl with thick x (thin x y') | half2 x (thin x y') y' refl
  ...                                                       | .(just y')          | refl = refl
  half2 {zero} (suc ()) _ _ _

  fact1 : ∀ {n} (x : Fin (suc n)) y r
    -> thick x y ≡ r
    -> x ≡ y × r ≡ nothing ⊎ ∃ λ y' -> thin x y' ≡ y × r ≡ just y'
  fact1 x y .(thick x y) refl with x ≡Fin y
  fact1 x .x ._ refl | yes refl = inj₁ (refl , half1 x)
  ... | no el with ThinFact.fact3 x y el
  ...            | y' , thinxy'=y = inj₂ (y' , ( thinxy'=y , half2 x y y' thinxy'=y ))

record Check (T : ℕ → Set) : Set where
  field
    check : ∀{n} (x : Fin (suc n)) (t : T (suc n)) -> Maybe (T n)

open Check ⦃ … ⦄ public

_<*>_ = _⊛_

mutual

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

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

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

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

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

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

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

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

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

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

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

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


text:
module L.Base.Sigma.Core where

-- Import the Σ record with constructors fst, snd
open import Agda.Builtin.Sigma public

split : ∀{a b c} {A : Set a} {B : A → Set b} (C : Σ A B → Set c)
        → ((x : A)(y : B x) → C (x , y)) → (p : Σ A B) → C p
split C g (a , b) = g a b

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
module Prelude.List where

open import Prelude.Bool
open import Prelude.Nat
open import Prelude.Fin

infixr 40 _::_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _::_ #-}

infixr 30 _++_

_++_ : {A : Set} -> List A -> List A -> List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

snoc : {A : Set} -> List A -> A -> List A
snoc []        e = e :: []
snoc (x :: xs) e = x :: snoc xs e

length : {A : Set} -> List A -> Nat
length [] = 0
length (x :: xs) = 1 + length xs

zipWith : ∀ {A B C} -> (A -> B -> C) -> List A -> List B -> List C
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
zipWith _ _ _ = []

map : ∀ {A B} -> (A -> B) -> List A -> List B
map _ []        = []
map f (x :: xs) = f x :: map f xs

mapIgen : ∀ {A B} -> (A -> B) -> List A -> List B
mapIgen = map

_!_ : ∀ {A} -> (xs : List A) -> Fin (length {A} xs) -> A
_!_ {A} (x :: xs) (fz .{length xs})   = x
_!_ {A} (x :: xs) (fs .{length xs} n) = _!_ {A} xs n
_!_ {A} [] ()

_[_]=_ : {A : Set} -> (xs : List A) -> Fin (length xs) -> A -> List A
(a :: as) [ fz ]= e = e :: as
(a :: as) [ fs n ]= e = a :: (as [ n ]= e)
[] [ () ]= e

listEq : {A : Set} -> (A -> A -> Bool) -> List A -> List A -> Bool
listEq _    []        [] = true
listEq _==_ (a :: as) (b :: bs) with a == b
... | true  = listEq _==_ as bs
... | false = false
listEq _ _ _ = false

tail : {A : Set} -> List A -> List A
tail [] = []
tail (x :: xs) = xs

reverse : {A : Set} -> List A -> List A
reverse [] = []
reverse (x :: xs) = reverse xs ++ (x :: [])

init : {A : Set} -> List A -> List A
init xs = reverse (tail (reverse xs))

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (a :: as) with p a
... | true  = a :: filter p as
... | false = filter p as