text:
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Data.Nat.Base where

open import Cubical.Core.Primitives

open import Agda.Builtin.Nat public
  using (zero; suc; _+_)
  renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_)

open import Cubical.Data.Nat.Literals public
open import Cubical.Data.Bool.Base
open import Cubical.Data.Sum.Base hiding (elim)
open import Cubical.Data.Empty.Base hiding (elim)
open import Cubical.Data.Unit.Base

predℕ : ℕ → ℕ
predℕ zero = zero
predℕ (suc n) = n

caseNat : ∀ {ℓ} → {A : Type ℓ} → (a0 aS : A) → ℕ → A
caseNat a0 aS zero    = a0
caseNat a0 aS (suc n) = aS

doubleℕ : ℕ → ℕ
doubleℕ zero = zero
doubleℕ (suc x) = suc (suc (doubleℕ x))

-- doublesℕ n m = 2^n · m
doublesℕ : ℕ → ℕ → ℕ
doublesℕ zero m = m
doublesℕ (suc n) m = doublesℕ n (doubleℕ m)

-- iterate
iter : ∀ {ℓ} {A : Type ℓ} → ℕ → (A → A) → A → A
iter zero f z    = z
iter (suc n) f z = f (iter n f z)

elim : ∀ {ℓ} {A : ℕ → Type ℓ}
  → A zero
  → ((n : ℕ) → A n → A (suc n))
  → (n : ℕ) → A n
elim a₀ _ zero = a₀
elim a₀ f (suc n) = f n (elim a₀ f n)

isEven isOdd : ℕ → Bool
isEven zero = true
isEven (suc n) = isOdd n
isOdd zero = false
isOdd (suc n) = isEven n

--Typed version
private
  toType : Bool → Type
  toType false = ⊥
  toType true = Unit

isEvenT : ℕ → Type
isEvenT n = toType (isEven n)

isOddT : ℕ → Type
isOddT n = isEvenT (suc n)

isZero : ℕ → Bool
isZero zero = true
isZero (suc n) = false

-- exponential

_^_ : ℕ → ℕ → ℕ
m ^ 0 = 1
m ^ (suc n) = m · m ^ n

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --no-auto-inline #-}
module DefaultMethods where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat using (Nat)
import Agda.Builtin.Nat as Nat
open import Agda.Builtin.List
open import Agda.Builtin.String renaming (primStringAppend to _++_)
open import Agda.Builtin.Char
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

open import Haskell.Prim
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Foldable

{-# FOREIGN AGDA2HS
{-# LANGUAGE TypeSynonymInstances #-}
import Prelude hiding (Show, ShowS, show, showList, showString, showParen, Ord, (<), (>))
#-}

-- ** Ord

record Ord (a : Set) : Set where
  field
    _<_ _>_ : a → a → Bool

record Ord₁ (a : Set) : Set where
  field
    _<_ : a → a → Bool

  _>_ : a → a → Bool
  x > y = y < x

record Ord₂ (a : Set) : Set where
  field
    _>_ : a → a → Bool

  _<_ : a → a → Bool
  _<_ = flip _>_

open Ord ⦃ ... ⦄

{-# COMPILE AGDA2HS Ord class Ord₁ Ord₂ #-}

OB : Ord₁ Bool
OB .Ord₁._<_ false b = b
OB .Ord₁._<_ true  _ = false

instance
  OrdBool₀ : Ord Bool
  OrdBool₀ ._<_ = Ord₁._<_ OB
  OrdBool₀ ._>_ = Ord₁._>_ OB
{-# COMPILE AGDA2HS OrdBool₀ #-}

data Bool1 : Set where
  Mk1 : Bool -> Bool1
{-# COMPILE AGDA2HS Bool1 #-}
instance
  OrdBool₁ : Ord Bool1
  OrdBool₁ = record {Ord₁ ord₁}
    where
      ord₁ : Ord₁ Bool1
      ord₁ .Ord₁._<_ (Mk1 false) (Mk1 b) = b
      ord₁ .Ord₁._<_ (Mk1 true)  _       = false
{-# COMPILE AGDA2HS OrdBool₁ #-}

data Bool2 : Set where
  Mk2 : Bool -> Bool2
{-# COMPILE AGDA2HS Bool2 #-}
instance
  OrdBool₂ : Ord Bool2
  OrdBool₂ = record {_<_ = _<:_; _>_ = flip _<:_}
    where
      _<:_ : Bool2 → Bool2 → Bool
      (Mk2 false) <: (Mk2 b) = b
      (Mk2 true)  <: _       = false
{-# COMPILE AGDA2HS OrdBool₂ #-}

data Bool3 : Set where
  Mk3 : Bool -> Bool3
{-# COMPILE AGDA2HS Bool3 #-}
instance
  OrdBool₃ : Ord Bool3
  OrdBool₃ = record {Ord₁ (λ where .Ord₁._<_ → _<:_)}
    where
      _<:_ : Bool3 → Bool3 → Bool
      (Mk3 false) <: (Mk3 b) = b
      (Mk3 true)  <: _       = false
{-# COMPILE AGDA2HS OrdBool₃ #-}

data Bool4 : Set where
  Mk4 : Bool -> Bool4
{-# COMPILE AGDA2HS Bool4 #-}
lift4 : (Bool → Bool → a) → (Bool4 → Bool4 → a)
lift4 f (Mk4 x) (Mk4 y) = f x y
{-# COMPILE AGDA2HS lift4 #-}
instance
  OrdBool₄ : Ord Bool4
  OrdBool₄ = record {Ord₁ (λ where .Ord₁._<_ → lift4 (λ x y → not x && y))}
{-# COMPILE AGDA2HS OrdBool₄ #-}

data Bool5 : Set where
  Mk5 : Bool -> Bool5
{-# COMPILE AGDA2HS Bool5 #-}
instance
  OrdBool₅ : Ord Bool5
  OrdBool₅ = record {Ord₂ (λ where .Ord₂._>_ → _>:_)}
    where
      _>:_ : Bool5 → Bool5 → Bool
      (Mk5 false) >: _       = false
      (Mk5 true)  >: (Mk5 b) = not b
{-# COMPILE AGDA2HS OrdBool₅ #-}

data Bool6 : Set where
  Mk6 : Bool -> Bool6
{-# COMPILE AGDA2HS Bool6 #-}
instance
  OrdBool₆ : Ord Bool6
  OrdBool₆ = record {Ord₂ (λ where .Ord₂._>_ → _>:_); _<_ = flip _>:_}
    where
      _>:_ : Bool6 → Bool6 → Bool
      (Mk6 false) >: _       = false
      (Mk6 true)  >: (Mk6 b) = not b
{-# COMPILE AGDA2HS OrdBool₆ #-}

instance
  Ordℕ : Ord Nat
  Ordℕ = record {Ord₁ (λ where .Ord₁._<_ → Nat._<_)}
-- {-# COMPILE AGDA2HS Ordℕ #-}

ShowS : Set
ShowS = String → String
{-# COMPILE AGDA2HS ShowS #-}

showString : String → ShowS
showString = _++_
{-# COMPILE AGDA2HS showString #-}

showParen : Bool → ShowS → ShowS
showParen false s = s
showParen true  s = showString "(" ∘ s ∘ showString ")"
{-# COMPILE AGDA2HS showParen #-}

defaultShowList : (a → ShowS) → List a → ShowS
defaultShowList _     []       = showString "[]"
defaultShowList shows (x ∷ xs) = showString "[" ∘ foldl (λ s x → s ∘ showString "," ∘ shows x) (shows x) xs ∘ showString "]"
{-# COMPILE AGDA2HS defaultShowList #-}

record Show (a : Set) : Set where
  field
    show : a → String
    showPrec : Nat → a → ShowS
    showList : List a → ShowS

record Show₁ (a : Set) : Set where
  field
    showPrec : Nat → a → ShowS

  show : a → String
  show x = showPrec 0 x ""

  showList : List a → ShowS
  showList = defaultShowList (showPrec 0)

record Show₂ (a : Set) : Set where
  field
    show : a → String

  showPrec : Nat → a → ShowS
  showPrec _ x s = show x ++ s

  showList : List a → ShowS
  showList = defaultShowList (showPrec 0)

open Show ⦃ ... ⦄

{-# COMPILE AGDA2HS Show class Show₁ Show₂ #-}

SB : Show₂ Bool
SB .Show₂.show true  = "true"
SB .Show₂.show false = "false"

instance
  ShowBool : Show Bool
  ShowBool .show     = Show₂.show SB
  ShowBool .showPrec = Show₂.showPrec SB
  ShowBool .showList []       = showString ""
  ShowBool .showList (true ∷ bs) = showString "1" ∘ showList bs
  ShowBool .showList (false ∷ bs) = showString "0" ∘ showList bs
{-# COMPILE AGDA2HS ShowBool #-}

instance
  ShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
  ShowMaybe {a = a} = record {Show₁ s₁}
    where
      s₁ : Show₁ (Maybe a)
      s₁ .Show₁.showPrec n Nothing = showString "nothing"
      s₁ .Show₁.showPrec n (Just x) = showParen true {-(9 < n)-} (showString "just " ∘ showPrec 10 x)
{-# COMPILE AGDA2HS ShowMaybe #-}

instance
  ShowList : ⦃ Show a ⦄ → Show (List a)
  ShowList = record {Show₁ (λ where .Show₁.showPrec _ → showList)}
{-# COMPILE AGDA2HS ShowList #-}

ext: agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.OrderedCommMonoid.Base where
{-
  Definition of an ordered monoid.
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.SIP using (TypeWithStr)
open import Cubical.Foundations.Structure using (⟨_⟩)

open import Cubical.Algebra.CommMonoid.Base

open import Cubical.Relation.Binary.Poset

private
  variable
    ℓ ℓ' : Level

record IsOrderedCommMonoid
       {M : Type ℓ}
       (_·_ : M → M → M) (1m : M) (_≤_ : M → M → Type ℓ') : Type (ℓ-max ℓ ℓ')
       where
  field
    isPoset     : IsPoset _≤_
    isCommMonoid   : IsCommMonoid 1m _·_
    MonotoneR  : {x y z : M} → x ≤ y → (x · z) ≤ (y · z) -- both versions, just for convenience
    MonotoneL  : {x y z : M} → x ≤ y → (z · x) ≤ (z · y)

record OrderedCommMonoidStr (ℓ' : Level) (M : Type ℓ) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    _≤_ : M → M → Type ℓ'
    _·_ : M → M → M
    ε : M
    isOrderedCommMonoid : IsOrderedCommMonoid _·_ ε _≤_

  open IsOrderedCommMonoid isOrderedCommMonoid public
  open IsPoset isPoset public
  open IsCommMonoid isCommMonoid public

  infixl 4 _≤_

OrderedCommMonoid : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
OrderedCommMonoid ℓ ℓ' = TypeWithStr ℓ (OrderedCommMonoidStr ℓ')

module _
    {M : Type ℓ} {1m : M} {_·_ : M → M → M} {_≤_ : M → M → Type ℓ'}
    (is-setM : isSet M)
    (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
    (rid : (x : M) → x · 1m ≡ x)
    (lid : (x : M) → 1m · x ≡ x)
    (comm : (x y : M) → x · y ≡ y · x)
    (isProp≤ : (x y : M) → isProp (x ≤ y))
    (isRefl : (x : M) → x ≤ x)
    (isTrans : (x y z : M) → x ≤ y → y ≤ z → x ≤ z)
    (isAntisym : (x y : M) → x ≤ y → y ≤ x → x ≡ y)
    (rmonotone : (x y z : M) → x ≤ y → (x · z) ≤ (y · z))
    (lmonotone : (x y z : M) → x ≤ y → (z · x) ≤ (z · y))
  where
  open IsOrderedCommMonoid

  makeIsOrderedCommMonoid : IsOrderedCommMonoid _·_ 1m _≤_
  isCommMonoid makeIsOrderedCommMonoid = makeIsCommMonoid is-setM assoc rid comm
  isPoset makeIsOrderedCommMonoid = isposet is-setM isProp≤ isRefl isTrans isAntisym
  MonotoneR makeIsOrderedCommMonoid = rmonotone _ _ _
  MonotoneL makeIsOrderedCommMonoid = lmonotone _ _ _

module _
    {M : Type ℓ} {1m : M} {_·_ : M → M → M} {_≤_ : M → M → Type ℓ'}
    (isCommMonoid : IsCommMonoid 1m _·_)
    (isProp≤ : (x y : M) → isProp (x ≤ y))
    (isRefl : (x : M) → x ≤ x)
    (isTrans : (x y z : M) → x ≤ y → y ≤ z → x ≤ z)
    (isAntisym : (x y : M) → x ≤ y → y ≤ x → x ≡ y)
    (rmonotone : (x y z : M) → x ≤ y → (x · z) ≤ (y · z))
    (lmonotone : (x y z : M) → x ≤ y → (z · x) ≤ (z · y))
  where
  module CM = IsOrderedCommMonoid

  IsOrderedCommMonoidFromIsCommMonoid : IsOrderedCommMonoid _·_ 1m _≤_
  CM.isPoset IsOrderedCommMonoidFromIsCommMonoid =
    isposet (isSetFromIsCommMonoid isCommMonoid) isProp≤ isRefl isTrans isAntisym
  CM.isCommMonoid IsOrderedCommMonoidFromIsCommMonoid = isCommMonoid
  CM.MonotoneR IsOrderedCommMonoidFromIsCommMonoid = rmonotone _ _ _
  CM.MonotoneL IsOrderedCommMonoidFromIsCommMonoid = lmonotone _ _ _

OrderedCommMonoid→CommMonoid : OrderedCommMonoid ℓ ℓ' → CommMonoid ℓ
OrderedCommMonoid→CommMonoid M .fst = M .fst
OrderedCommMonoid→CommMonoid M .snd =
  let open OrderedCommMonoidStr (M .snd)
  in commmonoidstr _ _ isCommMonoid

isSetOrderedCommMonoid : (M : OrderedCommMonoid ℓ ℓ') → isSet ⟨ M ⟩
isSetOrderedCommMonoid M = isSetCommMonoid (OrderedCommMonoid→CommMonoid M)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Auto.Prelude

mutual
 data Even : ℕ → Set where
  even-0 : Even zero
  even-s : {n : ℕ} → Odd n → Even (succ n)

 data Odd : ℕ → Set where
  odd-1 : Odd (succ zero)
  odd-s : {n : ℕ} → Even n → Odd (succ n)

double : ℕ → ℕ
double zero = zero
double (succ n) = succ (succ (double n))

h0 : ∀ {n} → Even (double n)
h0 {n} = {!-c!}
--h0 {zero} = even-0
--h0 {succ x} = even-s (odd-s h0)

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

module VecMap where

 map : {X Y : Set} → {n : ℕ} → (X → Y) → Vec X n → Vec Y n
 map f xs = {!-c!}  -- h1
{-
 map f [] = []
 map f (x ∷ x₁) = f x ∷ map f x₁
-}

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

data Type : Set₁ where
 <_> : Set → Type
 _⇒_ : Type → Type → Type

∥_∥ : Type → Set
∥ < X > ∥ = X
∥ a ⇒ b ∥ = ∥ a ∥ → ∥ b ∥

data Ctx : Set₁ where
 [] : Ctx
 _,_ : Ctx → Type → Ctx

data _∈_ (a : Type) : Ctx → Set₁ where
 zero : ∀ {Γ} → a ∈ (Γ , a)
 succ : ∀ {b Γ} → a ∈ Γ → a ∈ (Γ , b)

data Exp (Γ : Ctx) : Type → Set₁ where
 app : ∀ {α β} → Exp Γ (α ⇒ β) → Exp Γ α → Exp Γ β
 var : ∀ {α} → α ∈ Γ → Exp Γ α
 lam : ∀ {a b} → Exp (Γ , a) b → Exp Γ (a ⇒ b)

data Env : Ctx → Set₁ where
 nil : Env []
 cons : ∀ {Γ a} → ∥ a ∥ → Env Γ → Env (Γ , a)

lookup : ∀ {Γ a} → a ∈ Γ → Env Γ → ∥ a ∥
lookup x σ = {!-c!}  -- h2
{-
lookup {._} {< x >} zero (cons x₁ x₂) = x₁
lookup {._} {< x >} (succ x₁) (cons x₂ x₃) = lookup x₁ x₃
lookup {._} {x ⇒ x₁} zero (cons x₂ x₃) = x₂
lookup {._} {x ⇒ x₁} (succ x₂) (cons x₃ x₄) = lookup x₂ x₄
-}

lookup' : ∀ {Γ a} → a ∈ Γ → Env Γ → ∥ a ∥
lookup' zero (cons x σ) = x
lookup' (succ v) (cons x σ) = lookup' v σ

eval : ∀ {Γ a} → Env Γ → Exp Γ a → ∥ a ∥
--eval σ e = {!-c lookup!}  -- no solution found
eval σ (app e e₁) = {!!}  -- h3
eval σ (var x) = {!lookup'!}  -- h4, -c also works, repeats the solution for lookup
eval σ (lam e) x = {!!}  -- h5
{-
eval σ (app e e₁) = eval σ e (eval σ e₁)
eval σ (var x) = lookup x σ
eval σ (lam e) x = eval (cons x σ) e
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Selective.Examples.TestSelectiveReceive-calc where

open import Selective.ActorMonad
open import Prelude

open import Debug
open import Data.Nat.Show using (show)

UniqueTag = ℕ
TagField = ValueType UniqueTag

ℕ-ReplyMessage : MessageType
ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ

ℕ-Reply : InboxShape
ℕ-Reply = [ ℕ-ReplyMessage ]ˡ

ℕ×ℕ→ℕ-Message : MessageType
ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ

Calculate : InboxShape
Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ

Calculator : InboxShape
Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ

calculator-actor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
calculator-actor .force = receive ∞>>= λ {
  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
    Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do
    strengthen []
    calculator-actor)
  ; (Msg (S Z) (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
    (Z ![t: Z ] (lift tag ∷ ([ lift (n * m) ]ᵃ))) ∞>> (do
    (strengthen [])
    calculator-actor)
  ; (Msg (S (S ())) _)
  }

TestBox : InboxShape
TestBox = ℕ-Reply

accept-tagged-ℕ : UniqueTag → MessageFilter TestBox
accept-tagged-ℕ tag (Msg Z (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
accept-tagged-ℕ tag (Msg (S ()) _)

calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
calculator-test-actor = do
  spawn∞ calculator-actor
  self
  (S Z ![t: Z ] ((lift 0) ∷ (([ Z ]>: ⊆-refl) ∷ lift 32 ∷ [ lift 10 ]ᵃ)))
  (strengthen (⊆-suc ⊆-refl))
  sm: Msg Z (_ ∷ n ∷ []) [ _ ] ← (selective-receive (accept-tagged-ℕ 0))
    where
      sm: Msg (S ()) _ [ _ ]
  self
  (S Z ![t: S Z ] ((lift 0) ∷ (([ Z ]>: ⊆-refl) ∷ lift 32 ∷ [ lift 10 ]ᵃ)))
  strengthen (⊆-suc ⊆-refl)
  sm: Msg Z (_ ∷ m ∷ []) [ _ ] ← (selective-receive (accept-tagged-ℕ 0))
    where
      sm: Msg (S ()) _ [ _ ]
  strengthen []
  return m

max_stars_repo_name: Zalastax/singly-typed-actors

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Issue535 where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Vec A : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

replicate : ∀ {A n} → A → Vec A n
replicate {n = n} x = {!n!}

replicate′ : ∀ {n A} → A → Vec A n
replicate′ {n} x = {!n!}

extlam : Nat → {n m : Nat} → Vec Nat n
extlam = λ { x {m = m} → {!m!} }

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

data Vec (A : Set) : Nat → Set where

variable
  A  : Set
  x  : A
  n  : Nat
  xs : Vec A n

postulate
  IsHead : A → Vec A (suc n) → Set

-- Should also work if there is pruning
solve_==_by_ : (m n : Nat) → m ≡ n → Set
solve_==_by_ _ _ _ = Nat

mutual-block : Set

meta : Nat
meta = _

-- `n` gets pruned due to the meta == suc n constraint, so we can't generalize over it
module _ (X : Set) where
  tricky : let n = _
               _ = solve meta == suc n by refl
           in IsHead {n = n} x xs → Nat
  tricky h = 0

mutual-block = Nat


text:
-- This is not valid with magic mutual blocks that guess how far down the
-- file the mutual block extends
constructor
  zero : Nat
  suc : Nat → Nat

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

module Cubical.Data.FinSet.Binary.Small where

open import Cubical.Data.FinSet.Binary.Small.Base public
open import Cubical.Data.FinSet.Binary.Small.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module YonedaLemma where

open import Library
open import Categories
open import Categories.Sets
open import Functors
open import Naturals
open import FunctorCat

HomF[-,_] : ∀{l m}{C : Cat {l}{m}}(X : Cat.Obj C) -> Fun (C Op) (Sets {m})
HomF[-,_] {C = C} B = functor
  (\ X -> Hom X B)
  (\ f g -> comp g f)
  (ext \ _ -> idr)
  (ext \ _ -> sym ass)
  where open Cat C

HomN[-,_] : ∀{l m}{C : Cat {l}{m}}{X Y : Cat.Obj C}(f : Cat.Hom C X Y) ->
            NatT (HomF[-,_] {C = C} X) HomF[-, Y ]
HomN[-,_] {C = C} f = natural
  (comp f)
  (ext \ _ -> ass)
  where open Cat C

y : ∀{l m}(C : Cat {l}{m}) -> Fun C (FunctorCat (C Op) (Sets {m}))
y C = functor
  HomF[-,_]
  HomN[-,_]
  (NatTEq (iext \ _ -> ext \ _ -> idl))
  (NatTEq (iext \ _ -> ext \ _ -> ass))
  where open Cat C

yleminv : ∀{l m}(C : Cat {l}{m})(F : Fun (C Op) (Sets {m}))(X : Cat.Obj C) ->
          NatT (Fun.OMap (y C) X) F -> Fun.OMap F X
yleminv C F X α = NatT.cmp α {X} (Cat.iden C)

ylem : ∀{l m}(C : Cat {l}{m})(F : Fun (C Op) (Sets {m}))(X : Cat.Obj C) ->
       Fun.OMap F X -> NatT (Fun.OMap (y C) X) F
ylem C F X FX = natural
  (\ {X'} f -> HMap f FX)
  (\{X'}{Y}{f} -> ext \ g -> sym (fcong FX (fcomp {f = f}{g = g})) )
  where open Cat C; open Fun F

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 #-}

{- This module serves to develop some basic theory about pointed types.
   After defining the usual notions of pointed types, pointed equivalences,
   and loop spaces, we derive a version of univalence for pointed equivalences
   and observe that univalence between identical types is a pointed equivalence.

   We define pointed versions of dependent sums and products using the usual
   notion of pointed families and observe that they commute in a certain sense
   with taking loop spaces. -}

module Pointed where

open import lib.Basics hiding (_⊔_)
open import lib.NType2
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel

open import Preliminaries
open import UniverseOfNTypes

{- This file contains
     2.2.15: Fam•
   and
     2.2.17: has-level-equiv-contr-loops  (see end of file)
-}

{- Pointed types.
   A pointed type is a type (base) together with a chosen element (pt).
   The loop space construction Ω takes a pointed type and returns the type
   of all loops at the given basepoint. The trivial loop is taken as
   canonical element, thus forming a new pointed type. -}
Type• : (i : ULevel) → Type (lsucc i)
Type• i = Σ (Type i) (idf _)

module _ {i} (X : Type• i) where
  base = fst X
  pt   = snd X

-- Definition 2.2.15
{- Pointed families.
   A pointed family over a pointed type is a family over the base
   together with a inhabitant of the family at the point.
   Note that pointed types are equivalent to pointed families
   over the pointed unit type (not shown here). -}
Fam• : ∀ {i} (X : Type• i) (j : ULevel) → Type (i ⊔ lsucc j)
Fam• X j = Σ (base X → Type j) (λ P → P (pt X))

-- Alternate definition: Σ (n -Type i) ⟦_⟧
_-Type•_ : (n : ℕ₋₂) (i : ULevel) → Type (lsucc i)
n -Type• i = Σ (Type• i) (has-level n ∘ base)

-- For alternate definition: Σ-≤ (n -Type-≤ i) raise
_-Type•-≤_ : (n : ℕ₋₂) (i : ULevel) → S n -Type lsucc i
n -Type•-≤ i = ((n -Type• i)
              , equiv-preserves-level Σ-comm-snd
                                      (snd (Σ-≤ (n -Type-≤ i) raise)))

{- Pointed equivalences.
   An equivalence of pointed types is an equivalences of the bases
   that preserves the points -}
_≃•_ : ∀ {i j} → Type• i → Type• j → Set (i ⊔ j)
A ≃• B = Σ (base A ≃ base B) (λ f → –> f (pt A) == pt B)

ide• : ∀ {i} (X : Type• i) → X ≃• X
ide• _ = ide _ , idp

_∘e•_ : ∀ {i j k} {X : Type• i} {Y : Type• j} {Z : Type• k}
       → Y ≃• Z → X ≃• Y → X ≃• Z
(u , p) ∘e• (v , q) = (u ∘e v , ap (–> u) q ∙ p)

_⁻¹• : ∀ {i j} {X : Type• i} {Y : Type• j} → X ≃• Y → Y ≃• X
(u , p) ⁻¹• = u ⁻¹ , ap (<– u) (! p) ∙ <–-inv-l u _

-- Equational reasoning for pointed equivalences.
infix  2 _≃•∎
infixr 2 _≃•⟨_⟩_

_≃•⟨_⟩_ : ∀ {i j k} (X : Type• i) {Y : Type• j} {Z : Type• k}
          → X ≃• Y → Y ≃• Z → X ≃• Z
_ ≃•⟨ u ⟩ v = v ∘e• u

_≃•∎ : ∀ {i} (X : Type• i) → X ≃• X
_≃•∎ = ide•

-- The loop space construction.
Ω : ∀ {i} → Type• i → Type• i
Ω (A , a) = ((a == a) , idp)

Ω-≤ : ∀ {i} {n : ℕ₋₂} → (S n) -Type• i → n -Type• i
Ω-≤ ((A , a) , t) = (Ω (A , a) , t a a)

-- Loop spaces are preserved by pointed equivalences.
equiv-Ω : ∀ {i j} {X : Type• i} {Y : Type• j} → X ≃• Y → Ω X ≃• Ω Y
equiv-Ω (u , p) = split u p where
  split : ∀ u {a} {b} → –> u a == b → Ω (_ , a) ≃• Ω (_ , b)
  split u idp = (equiv-ap u _ _ , idp)

equiv-Ω^ : ∀ {i j} {X : Type• i} {Y : Type• j} (n : ℕ)
           → X ≃• Y → (Ω ^ n) X ≃• (Ω ^ n) Y
equiv-Ω^ 0     e = e
equiv-Ω^ (S n) e = equiv-Ω^ n (equiv-Ω e)

{- We call a pointed type n-truncated if its base is.
   Constructing the loop space decrements the truncation level. -}
has-level• : ∀ {i} → ℕ₋₂ → Type• i → Type i
has-level• n = has-level n ∘ base

trunc-many : ∀ {i} {X : Type• i} {k : ℕ} (n : ℕ)
             → has-level• ((k + n) -2)          X
             → has-level• (k     -2) ((Ω ^ n) X)
trunc-many 0     t = t
trunc-many (S n) t = trunc-many n (t _ _)

--Ω^-≤ : ∀ {i} {k : ℕ} (n : ℕ) → (k + n -2) -Type• i → (k -2) -Type• i
--Ω^-≤ O     X = X
--Ω^-≤ (S n) X = Ω^-≤ n (Ω-≤ X)

Ω^-≤ : ∀ {i} {k : ℕ} (n : ℕ) → ((k + n) -2) -Type• i → (k -2) -Type• i
Ω^-≤ n (X , t) = ((Ω ^ n) X , trunc-many n t)

Ω^-≤' : ∀ {i} {k : ℕ} (n : ℕ) → ((n + k) -2) -Type• i → (k -2) -Type• i
Ω^-≤' n (X , t) =
  ((Ω ^ n) X , trunc-many n (transport (λ z → has-level• (z -2) X)
                                       (+-comm _ n) t))

{- Pointedness allows for a more direct notion of contractibility.
   Beware that is-contr• will be equivalent --- not definitionally equal ---
   to has-level∙ ⟨-2⟩. -}
module _ {i} (X : Type• i) where
  is-contr• : Type i
  is-contr• = ∀ a → pt X == a

{- Since pointed types are always inhabited,
   being contractible and propositional is equivalent. -}
module _ {i} {X : Type• i} where
  contr•-equiv-contr : is-contr• X ≃ is-contr (base X)
  contr•-equiv-contr = prop-equiv'
                         (λ c → Π-level (λ a → raise-level-<T (ltSR ltS) c _ _))
                         (cst is-contr-is-prop)
                         (λ x → (pt X , x))
                         (λ y _ → prop-has-all-paths (contr-is-prop y) _ _)

  is-contr•-is-prop : is-prop (is-contr• X)
  is-contr•-is-prop = equiv-preserves-level (contr•-equiv-contr ⁻¹)
                                            is-contr-is-prop

  prop-equiv-contr : is-prop (base X) ≃ is-contr (base X)
  prop-equiv-contr = prop-equiv is-prop-is-prop
                                is-contr-is-prop
                                (inhab-prop-is-contr (pt X))
                                contr-is-prop

  contr•-equiv-prop : is-contr• X ≃ is-prop (base X)
  contr•-equiv-prop = prop-equiv-contr ⁻¹ ∘e contr•-equiv-contr

-- Pointed equivalences preserve (pointed) contractibility.
equiv-is-contr• : ∀ {i j} {X : Type• i} {Y : Type• j}
                → X ≃• Y → is-contr• X ≃ is-contr• Y
equiv-is-contr• (u , p) = contr•-equiv-contr ⁻¹
                       ∘e equiv-level u
                       ∘e contr•-equiv-contr

-- Univalence for pointed equivalences.
module _ {i} {A B : Type• i} where
  ua•-equiv : (A ≃• B) ≃ (A == B)
  ua•-equiv =
      A ≃• B
    ≃⟨ ide _ ⟩
      Σ (base A ≃ base B) (λ f → –> f (pt A) == pt B)
    ≃⟨ equiv-Σ-fst _ (snd (ua-equiv ⁻¹)) ⁻¹ ⟩
      Σ (base A == base B) (λ q → coe q (pt A) == pt B)
    ≃⟨ equiv-Σ-snd (λ q → coe-equiv (ap (λ f → coe f (pt A) == pt B)
                                        (! (ap-idf q)))) ⟩
      Σ (base A == base B) (λ q → coe (ap (idf _) q) (pt A) == pt B)
    ≃⟨ equiv-Σ-snd (λ q → to-transp-equiv _ q ⁻¹) ⟩
      Σ (base A == base B) (λ q → pt A == pt B [ idf _ ↓ q ])
    ≃⟨ =Σ-eqv _ _ ⟩
      A == B
    ≃∎

  ua• : A ≃• B → A == B
  ua• = –> ua•-equiv

  coe•-equiv : A == B → A ≃• B
  coe•-equiv = <– ua•-equiv

-- Normal univalence can be made pointed in the endo-setting.
module _ {i} {A : Type i} where
  ua-equiv• : ((A ≃ A) , ide _) ≃• ((A == A) , idp)
  ua-equiv• = ((ua-equiv ⁻¹) , idp) ⁻¹•

-- Lemma 2.2.17
{- The induction step for Lemma 7.2.9 in the HoTT Book is
   more complicated than necesarry. Associating iterated loop spaces in
   the reverse order, we can do it with the prerequisites 7.2.7 and 7.2.8
   (of the book) as well as further auxiliary steps. -}
has-level-equiv-contr-loops : ∀ {i} {n : ℕ} {A : Type i}
                              →   has-level (n -1) A
                                ≃ ((a : A) → is-contr• ((Ω ^ n) (A , a)))
has-level-equiv-contr-loops {n = O} {A} =
    is-prop A                      ≃⟨ prop-equiv-inhab-to-contr ⟩
    (A → is-contr A)               ≃⟨ equiv-Π-r (λ _ → contr•-equiv-contr ⁻¹) ⟩
    ((a : A) → is-contr• (A , a))  ≃∎
has-level-equiv-contr-loops {n = S n} {A} = equiv-Π-r lem where
  lem = λ a →
      (((b : A) → has-level (n -1) (a == b)))
    ≃⟨ equiv-Π-r (λ _ → has-level-equiv-contr-loops) ⟩
      (((b : A) (p : a == b) → is-contr• ((Ω ^ n) ((a == b) , p))))
    ≃⟨ Π₁-contr (pathfrom-is-contr _) ∘e curry-equiv ⁻¹ ⟩
      is-contr• ((Ω ^ n) ((a == a) , idp))
    ≃∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module StateSized.GUI.SpaceShipExtendedExample where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Data.Bool.Base
open import Data.List.Base
open import Data.Integer

open import Data.Product hiding (map)
open import SizedIO.Object
open import SizedIO.IOObject

open import NativeIO
open import Size

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

open import StateSizedIO.GUI.WxGraphicsLib

open import StateSized.GUI.BitMaps

spaceShipMove = 10

data RockMethod : Set where
  move : RockMethod
  getPoint : RockMethod
  draw : DC → Rect → RockMethod

RockResult : RockMethod → Set
RockResult getPoint = Point
RockResult _        = Unit

RockInterface : Interface
Method RockInterface = RockMethod
Result RockInterface = RockResult

RockObject : ∀{i} → Set
RockObject {i} = IOObject GuiLev1Interface RockInterface i

rockObject : ∀{i} → Point → RockObject {i}
method (rockObject (x , y)) move =
  return ( _ , rockObject (x , (y + (+ 2))))
method (rockObject p) (draw dc rect) =
  exec (drawBitmap dc rock p true) λ _ →
  return (_ , rockObject p)
method (rockObject p) getPoint =
  return (p , rockObject p)

data SpaceshipMethod : Set where
  move : Point → SpaceshipMethod
  draw : DC → Rect → SpaceshipMethod
  collide : RockObject → SpaceshipMethod

SpaceshipResult : SpaceshipMethod  →  Set
SpaceshipResult _  = Unit

SpaceshipInterface : Interface
Method SpaceshipInterface = SpaceshipMethod
Result SpaceshipInterface = SpaceshipResult

SpaceshipObject : ∀{i} → Set
SpaceshipObject {i} = IOObject GuiLev1Interface SpaceshipInterface i

spaceshipObject : ∀{i} → Point → SpaceshipObject {i}
method (spaceshipObject (x , y)) (move (deltaX , deltaY)) =
  return ( _ , spaceshipObject ((x + deltaX) , (y + deltaY)))
method (spaceshipObject p) (draw dc rect) =
  exec (drawBitmap dc ship p true) λ _ →
       return (_ , spaceshipObject p)
method (spaceshipObject p) (collide rock) =
   return (_ , spaceshipObject p)

data GraphicServerMethod : Set where
  onPaintM                :   DC → Rect → GraphicServerMethod
  repaintM                :   Frame → GraphicServerMethod
  moveSpaceShipM          :   Point → GraphicServerMethod
  moveWorldM              :   GraphicServerMethod

GraphicServerResult : GraphicServerMethod  →  Set
GraphicServerResult _ = Unit

GraphicServerInterface : Interface
Method GraphicServerInterface  = GraphicServerMethod
Result GraphicServerInterface  = GraphicServerResult

GraphicServerObject : ∀{i} → Set
GraphicServerObject {i} = IOObject GuiLev1Interface GraphicServerInterface i

graphicServerObject : ∀{i} → SpaceshipObject → RockObject →
                             GraphicServerObject {i}
method (graphicServerObject ship rock) (onPaintM dc rect) =
               method ship (draw dc rect) >>= λ { (_ , ship') →
               method rock (draw dc rect) >>= λ { (_ , rock') →
               return (_ , graphicServerObject ship' rock') }}
method (graphicServerObject ship rock) (repaintM fra) =
               exec (repaint fra)                λ _ →
               return (_ , graphicServerObject ship rock)
method (graphicServerObject ship rock) (moveSpaceShipM (deltaX , deltaY)) =
               method ship (move (deltaX , deltaY)) >>= λ { (_ , ship') →
               return (_ , graphicServerObject ship' rock) }
method (graphicServerObject ship rock) moveWorldM =
               method rock move >>= λ { (_ , rock') →
               return (_ , graphicServerObject ship rock') }

VarType : Set
VarType = GraphicServerObject {∞}

varInit : VarType
varInit = graphicServerObject (spaceshipObject (+ 150 , + 150))
                              (rockObject (+ 20 , + 10))

onPaint  : ∀{i} → VarType → DC → Rect → IO GuiLev1Interface i VarType
onPaint obj dc rect = mapIO proj₂  (method obj (onPaintM dc rect))

moveSpaceShip : ∀{i} → Point → VarType  → IO GuiLev1Interface i VarType
moveSpaceShip p obj = mapIO proj₂ (method obj (moveSpaceShipM p))

moveWorld : ∀{i} → VarType  → IO GuiLev1Interface i VarType
moveWorld obj = mapIO proj₂ (method obj moveWorldM)

callRepaint  : ∀{i} → Frame → VarType  → IO GuiLev1Interface i VarType
callRepaint fra obj = mapIO proj₂ (method obj (repaintM fra))

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  execˢ (level1C makeFrame)           λ fra →
           execˢ (level1C (makeButton fra))    λ bt →
           execˢ (level1C (addButton fra bt))  λ _ →
           execˢ (createVar varInit)           λ _ →
           execˢ (setButtonHandler bt (moveSpaceShip (+ 20 , + 0)
                                     ∷ [ callRepaint fra ])) λ _ →
           execˢ (setKeyHandler bt
             (moveSpaceShip (+ spaceShipMove , + 0)  ∷ [ callRepaint fra ])
             (moveSpaceShip (-[1+ spaceShipMove ] , + 0) ∷ [ callRepaint fra ])
             (moveSpaceShip (+ 0 , -[1+ spaceShipMove ]) ∷ [ callRepaint fra ])
             (moveSpaceShip (+ 0 , + spaceShipMove) ∷ [ callRepaint fra ]))
             λ _ →

           execˢ (setOnPaint fra ([ onPaint  ]))  λ _ →
           execˢ (setTimer fra (+ 50)
               (moveWorld ∷ [ callRepaint fra ]))  λ _ →
           returnˢ unit

main : NativeIO Unit
main = (start (translateLev2 program)) native>>= (λ _ → nativePutStrLn "stephan test2")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
record R (A : Set) : Set where
  field
    f : A → A

open R {{...}}

test : {A : Set} → R A
f {{test}} = {!!}


text:
------------------------------------------------------------------------------
-- Twice funcion
------------------------------------------------------------------------------

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

module FOTC.Twice where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base

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

module HigherOrder where

  -- We cannot translate this function as a definition because it is
  -- higher-order.
  twice : (D → D) → D → D
  twice f x = f (f x)
  -- {-# ATP definition twice #-}

  postulate twice-succ : ∀ n → twice succ₁ n ≡ succ₁ (succ₁ n)
  -- {-# ATP prove twice-succ #-}

module FirstOrderAxiom where

  postulate
    twice    : D → D → D
    twice-eq : ∀ f x → twice f x ≡ f · (f · x)
  {-# ATP axiom twice-eq #-}

  twice-succI : ∀ n → twice succ n ≡ succ · (succ · n)
  twice-succI n = twice succ n      ≡⟨ twice-eq succ n ⟩
                  succ · (succ · n) ∎

  postulate twice-succATP : ∀ n → twice succ n ≡ succ · (succ · n)
  {-# ATP prove twice-succATP #-}

module FirstOrderDefinition where

  twice : D → D → D
  twice f x = f · (f · x)
  {-# ATP definition twice #-}

  twice-succI : ∀ n → twice succ n ≡ succ · (succ · n)
  twice-succI n = refl

  postulate twice-succATP : ∀ n → twice succ n ≡ succ · (succ · n)
  {-# ATP prove twice-succATP #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- From the Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Common.Size where

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZESUC  ↑_     #-}
{-# BUILTIN SIZEINF  ∞      #-}
{-# BUILTIN SIZEMAX  _⊔ˢ_  #-}

{-# FOREIGN OCaml
  let up _ = ();;
  let inf = ();;
  let union _ _ = ();;
#-}

{-# COMPILE OCaml ↑_     = up    #-}
{-# COMPILE OCaml ∞      = inf   #-}
{-# COMPILE OCaml _⊔ˢ_   = union #-}

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


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

open import LogicalFormulae
open import Groups.Definition
open import Groups.Abelian.Definition
open import Groups.FiniteGroups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Setoids.Setoids
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Functions.Definition
open import Functions.Lemmas
open import Semirings.Definition
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Addition
open import Orders.Total.Definition
open import Numbers.Modulo.ModuloFunction

module Numbers.Modulo.Group where

open TotalOrder ℕTotalOrder
open Semiring ℕSemiring

private
  0<s : {n : ℕ} → 0 <N succ n
  0<s {n} = le n (applyEquality succ (Semiring.sumZeroRight ℕSemiring n))

  inverseN : {n : ℕ} → .(0<n : 0 <N n) → (x : ℤn n 0<n) → ℤn n 0<n
  inverseN 0<n record { x = 0 ; xLess = _ } = record { x = 0 ; xLess = 0<n }
  inverseN 0<n record { x = succ x ; xLess = xLess } with <NProp xLess
  ... | le subtr pr = record { x = succ subtr ; xLess = le x (transitivity (commutative (succ x) (succ subtr)) pr) }

  invLeft : {n : ℕ} → .(0<n : 0 <N n) → (x : ℤn n 0<n) → _+n_ 0<n (inverseN 0<n x) x ≡ record { x = 0 ; xLess = 0<n }
  invLeft {n} 0<n record { x = 0 ; xLess = xLess } = plusZnIdentityLeft 0<n (record { x = 0 ; xLess = 0<n })
  invLeft {n} 0<n record { x = (succ x) ; xLess = xLess } with <NProp xLess
  ... | le subtr pr rewrite pr = equalityZn (modN 0<n)

ℤnGroup : (n : ℕ) → .(pr : 0 <N n) → Group (reflSetoid (ℤn n pr)) (_+n_ pr)
Group.+WellDefined (ℤnGroup n 0<n) refl refl = refl
Group.0G (ℤnGroup n 0<n) = record { x = 0 ; xLess = 0<n }
Group.inverse (ℤnGroup n 0<n) = inverseN 0<n
Group.+Associative (ℤnGroup n 0<n) {a} {b} {c} = equalityCommutative (plusZnAssociative 0<n a b c)
Group.identRight (ℤnGroup n 0<n) {a} = plusZnIdentityRight 0<n a
Group.identLeft (ℤnGroup n 0<n) {a} = plusZnIdentityLeft 0<n a
Group.invLeft (ℤnGroup n 0<n) {a} = invLeft 0<n a
Group.invRight (ℤnGroup n 0<n) {a} = transitivity (plusZnCommutative 0<n a (inverseN 0<n a)) (invLeft 0<n a)

ℤnAbGroup : (n : ℕ) → (pr : 0 <N n) → AbelianGroup (ℤnGroup n pr)
AbelianGroup.commutative (ℤnAbGroup n pr) {a} {b} = plusZnCommutative pr a b

ℤnFinite : (n : ℕ) → (pr : 0 <N n) → FiniteGroup (ℤnGroup n pr) (FinSet n)
SetoidToSet.project (FiniteGroup.toSet (ℤnFinite (succ n) 0<n)) record { x = x ; xLess = xLess } = ofNat x xLess
SetoidToSet.wellDefined (FiniteGroup.toSet (ℤnFinite (succ n) 0<n)) x y x=y rewrite x=y = refl
SetoidToSet.surj (FiniteGroup.toSet (ℤnFinite (succ n) 0<n)) b = record { x = toNat b ; xLess = toNatSmaller b } , ofNatToNat b
SetoidToSet.inj (FiniteGroup.toSet (ℤnFinite (succ n) 0<n)) record { x = x ; xLess = xLess } record { x = y ; xLess = yLess } eq = equalityZn (ofNatInjective x y xLess yLess eq)
FiniteGroup.finite (ℤnFinite n pr) = record { size = n ; mapping = id ; bij = idIsBijective }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for equational reasoning
------------------------------------------------------------------------

-- Example use:

-- n*0≡0 : ∀ n → n * 0 ≡ 0
-- n*0≡0 zero    = refl
-- n*0≡0 (suc n) =
--   begin
--     suc n * 0
--   ≈⟨ refl ⟩
--     n * 0 + 0
--   ≈⟨ ... ⟩
--     n * 0
--   ≈⟨ n*0≡0 n ⟩
--     0
--   ∎

-- Note that some modules contain generalised versions of specific
-- instantiations of this module. For instance, the module ≡-Reasoning
-- in Relation.Binary.PropositionalEquality is recommended for
-- equational reasoning when the underlying equality is
-- Relation.Binary.PropositionalEquality._≡_.

open import Relation.Binary

module Relation.Binary.EqReasoning {s₁ s₂} (S : Setoid s₁ s₂) where

open Setoid S
import Relation.Binary.PreorderReasoning as PreR
open PreR preorder public
       renaming ( _∼⟨_⟩_  to _≈⟨_⟩_
                ; _≈⟨_⟩_  to _≡⟨_⟩_
                ; _≈⟨⟩_  to _≡⟨⟩_
                )


text:
module FixityOutOfScopeInRecord where

record R : Set where
  infixl 30 _+_

max_stars_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------------
-- Testing the use of ATP axioms with data constructors
------------------------------------------------------------------------------

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

module DataConstructorsAxioms where

postulate
  D    : Set
  zero : D
  succ : D → D

data N : D → Set where
  zN : N zero
  sN : ∀ {n} → N n → N (succ n)
{-# ATP axioms zN sN #-}

postulate 0-N : N zero
{-# ATP prove 0-N #-}

postulate 1-N : N (succ zero)
{-# ATP prove 1-N #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module CombiningProofs.CommAddGlobalHints where

open import PA.Axiomatic.Standard.Base

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity = PA₃

+-rightIdentity : ∀ n → n + zero ≡ n
+-rightIdentity = ℕ-ind A A0 is
  where
  A : ℕ → Set
  A i = i + zero ≡ i
  {-# ATP definition A #-}

  A0 : A zero
  A0 = +-leftIdentity zero

  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is #-}

x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)
x+Sy≡S[x+y] m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + succ n ≡ succ (i + n)
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 #-}

  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is #-}

-- Global hints
{-# ATP hints x+Sy≡S[x+y] +-rightIdentity #-}

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≡ n + i
  {-# ATP definition A #-}

  postulate A0 : A zero
  {-# ATP prove A0 #-}

  postulate is : ∀ i → A i → A (succ i)
  {-# ATP prove is #-}


text:
open import OutsideIn.Prelude
module OutsideIn.X where
   open import Data.Product public hiding (map)
   open import Relation.Nullary

   record Types : Set₁ where
     field Type : Set → Set
           type-is-monad : Monad Type
           funType : ∀ {n} → Type n → Type n → Type n
           appType : ∀ {n} → Type n → Type n → Type n
     type-is-functor = Monad.is-functor type-is-monad

   record QConstraints ⦃ types : Types ⦄ : Set₁ where
     open Types(types)
     field QConstraint : Set → Set
           qconstraint-is-functor : Functor QConstraint
           _∼_ : ∀ {n} → Type n → Type n → QConstraint n
           _∧_ : ∀ {n} → QConstraint n → QConstraint n → QConstraint n
           ε : ∀ {n} → QConstraint n
           constraint-types : ∀ {a b} → (Type a → Type b) → QConstraint a → QConstraint b
           is-ε : ∀ {n} (x : QConstraint n) → Dec (x ≡ ε)
     open Monad   (type-is-monad)
     open Functor (is-functor)
     qc-substitute : ∀{a b} →  (a → Type b) → (QConstraint a → QConstraint b)
     qc-substitute f =  constraint-types (join ∘ map f)

   record AxiomSchemes ⦃ types : Types ⦄ : Set₁ where
     open Types(types)
     field AxiomScheme : Set → Set
           axiomscheme-is-functor : Functor AxiomScheme
           axiomscheme-types : ∀ {a b} → (Type a → Type b) → AxiomScheme a → AxiomScheme b
     open Monad   (type-is-monad)
     open Functor (is-functor)
     ax-substitute : ∀{a b} →  (a → Type b) → (AxiomScheme a → AxiomScheme b)
     ax-substitute f =  axiomscheme-types (join ∘ map f)

   record Entailment ⦃ types : Types ⦄ ⦃ axiomschemes : AxiomSchemes ⦄ ⦃ qconstraints : QConstraints ⦄ : Set₁ where
     open Types(types)
     open AxiomSchemes(axiomschemes)
     open QConstraints(qconstraints)

     open Monad(type-is-monad)
     open Functor(type-is-functor)

     field _,_⊩_ : ∀ {n} → AxiomScheme n → QConstraint n → QConstraint n → Set
           ent-refl : ∀ {n}{Q : AxiomScheme n}{q q′ : QConstraint n}
                    → Q , (q ∧ q′) ⊩ q′
           ent-trans : ∀ {n}{Q : AxiomScheme n}{q q₁ q₂ q₃ : QConstraint n}
                     → Q , (q ∧ q₁) ⊩ q₂ → Q , (q ∧ q₂) ⊩ q₃ → Q , (q ∧ q₁) ⊩ q₃
           ent-subst : ∀ {a b}{θ : a → Type b}{Q : AxiomScheme a}{q q₁ q₂ : QConstraint a}
                     → Q , (q ∧ q₁) ⊩ q₂ → axiomscheme-types (join ∘ map θ) Q
                                         , constraint-types (join ∘ map θ) (q ∧ q₁)
                                         ⊩ constraint-types (join ∘ map θ) q₂
           ent-typeq-refl : ∀ {n}{Q : AxiomScheme n}{q : QConstraint n}{τ : Type n}
                          → Q , q ⊩ (τ ∼ τ)
           ent-typeq-sym : ∀ {n}{Q : AxiomScheme n}{q : QConstraint n}{τ₁ τ₂ : Type n}
                         → Q , q ⊩ (τ₁ ∼ τ₂) → Q , q ⊩ (τ₂ ∼ τ₁)
           ent-typeq-trans : ∀ {n}{Q : AxiomScheme n}{q : QConstraint n}{τ₁ τ₂ τ₃ : Type n}
                           → Q , q ⊩ (τ₁ ∼ τ₂) → Q , q ⊩ (τ₂ ∼ τ₃) → Q , q ⊩ (τ₁ ∼ τ₃)
           ent-typeq-subst : ∀ {a b}{Q : AxiomScheme a}{q : QConstraint a}{τ₁ τ₂ : Type a}{θ : a → Type b}
                         → Q , q ⊩ (τ₁ ∼ τ₂) → axiomscheme-types (join ∘ map θ) Q
                                             , constraint-types (join ∘ map θ) q  ⊩ ((join ∘ map θ) τ₁ ∼ (join ∘ map θ) τ₂)
           ent-conj : ∀ {n}{Q : AxiomScheme n}{q q₁ q₂ : QConstraint n}
                           → Q , q ⊩ q₁ → Q , q ⊩ q₂ → Q , q ⊩ (q₁ ∧ q₂)

   module SimplificationPrelude ⦃ types : Types ⦄
                                ⦃ axiomschemes : AxiomSchemes ⦄
                                ⦃ qconstraints : QConstraints ⦄
                                ⦃ entailment   : Entailment   ⦄ where
     open Types(types)
     open AxiomSchemes(axiomschemes)
     open QConstraints(qconstraints)
     open Entailment(entailment)

     data SimplifierResult′ (x : Set)( n m : ℕ ) : QConstraint (x ⨁ m) → Set where
       solved : (q : QConstraint (x ⨁ m)) → (x ⨁ n → Type (x ⨁ m)) → SimplifierResult′ x n m q

     SimplifierResult : Set → ℕ → Set
     SimplifierResult x n = ∃ (λ m → ∃ (SimplifierResult′ x n m))

     SimplifierResultNoResidual : Set → ℕ → Set
     SimplifierResultNoResidual x n = ∃ (λ m → SimplifierResult′ x n m ε)

     IsSound′ : ∀ {x : Set}{n m : ℕ}{Qr : QConstraint (x ⨁ m)}
                  (Q : AxiomScheme (x ⨁ m))(Qg : QConstraint (x ⨁ m))
                  (Qw : QConstraint (x ⨁ n))(s : SimplifierResult′ x n m Qr) → Set
     IsSound′ Q Qg Qw (solved Qr θ) = Q , Qg ∧ Qr ⊩ qc-substitute θ Qw

     IsSound : ∀ {x : Set}{n : ℕ}
                 (Q : AxiomScheme x)(Qg : QConstraint x)
                 (Qw : QConstraint (x ⨁ n))(s : SimplifierResult x n) → Set
     IsSound {x}{n} Q Qg Qw (m , .Qr , solved Qr θ) = IsSound′ {n = n}{m = m} (Ax-f.map pm-m.unit Q) (Qc-f.map pm-m.unit Qg) Qw (solved Qr θ)
        where module Ax-f = Functor(axiomscheme-is-functor)
              module Qc-f = Functor(qconstraint-is-functor)
              module pm-m = Monad(PlusN-is-monad {m})

   record Simplification ⦃ types : Types ⦄
                         ⦃ axiomschemes : AxiomSchemes ⦄
                         ⦃ qconstraints : QConstraints ⦄
                         ⦃ entailment   : Entailment   ⦄ : Set₁ where
     open Types(types)
     open AxiomSchemes(axiomschemes)
     open QConstraints(qconstraints)
     open Entailment(entailment)
     open SimplificationPrelude

     field simplifier : ∀ {x : Set} → Eq x → (n : ℕ) → AxiomScheme x
                      → QConstraint x → QConstraint (x ⨁ n) → SimplifierResult x n

     field simplifier-sound : ∀ {x : Set}{n : ℕ}{eq : Eq x}
                 (Q : AxiomScheme x)(Qg : QConstraint x)
                 (Qw : QConstraint (x ⨁ n)) → IsSound Q Qg Qw (simplifier eq n Q Qg Qw)

     simplifier′ : ∀ {x : Set} → Eq x → (n : ℕ) → AxiomScheme x
                 → QConstraint x → QConstraint (x ⨁ n) → Ⓢ (SimplifierResultNoResidual x n)
     simplifier′ eq n ax g e with simplifier eq n ax g e
     simplifier′ eq n ax g e | m , Qr , result with is-ε Qr
     simplifier′ eq n ax g e | m , .ε , result | yes refl = suc (m , result)
     simplifier′ eq n ax g e | m , Qr , result | no  p = zero

   record X : Set₂ where
     field dc : ℕ → Set
     field types : Types
     field axiom-schemes : AxiomSchemes
     field qconstraints : QConstraints
     field entailment : Entailment
     field simplification : Simplification
     open Types(types) public
     open AxiomSchemes(axiom-schemes) public
     open QConstraints(qconstraints) public
     open Entailment(entailment) public
     open Simplification(simplification) public
     open SimplificationPrelude public

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
module PatternSynonymOverloaded where

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

pattern ss x = suc (suc x)
pattern ss x = suc x


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

open import Relation.Binary.PropositionalEquality using (_≢_; _≡_; refl; sym; subst; cong; trans)
open import Function using (_∘_)
open import Relation.Nullary using (yes; no)

import Data.Empty as Empty
import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Nat as Nat
import Data.Vec as Vec
import Data.Vec.Properties as Vecₚ
import Data.Fin as Fin
import Data.Fin.Properties as Finₚ
import Data.Vec.Relation.Unary.All as All

open Empty using (⊥-elim)
open Nat using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (Σ-syntax; _×_; _,_; proj₁; proj₂)

import PiCalculus.Syntax
open PiCalculus.Syntax.Scoped
open import PiCalculus.Semantics
open import PiCalculus.Semantics.Properties
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Exchange (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω

private
  variable
    n : ℕ
    i j : Fin n
    idx : Idx
    idxs : Idxs n
    P Q : Scoped n

⊢-unused : {γ : PreCtx n} {Γ Θ : Ctx idxs}
         → (i : Fin n)
         → Unused i P
         → γ ； Γ ⊢ P ▹ Θ
         → All.lookup i Γ ≡ All.lookup i Θ
⊢-unused i uP 𝟘 = refl
⊢-unused i uP (ν t m μ ⊢P) = ⊢-unused (suc i) uP ⊢P
⊢-unused i (i≢x , uP) ((_ , x) ⦅⦆ ⊢P) = trans
  (∋-lookup-≢ x i i≢x)
  (⊢-unused (suc i) uP ⊢P)
⊢-unused i (i≢x , i≢y , uP) ((_ , x) ⟨ _ , y ⟩ ⊢P) = trans (trans
  (∋-lookup-≢ x i i≢x)
  (∋-lookup-≢ y i i≢y))
  (⊢-unused i uP ⊢P)
⊢-unused i (uP , uQ) (⊢P ∥ ⊢Q) = trans
  (⊢-unused i uP ⊢P)
  (⊢-unused i uQ ⊢Q)

module _ {a} {A : Set a} where
  exchangeᵥ : (i : Fin n) → Vec A (suc n) → Vec A (suc n)
  exchangeᵥ zero (xs -, y -, x) = xs -, x -, y
  exchangeᵥ (suc i) (xs -, y -, x) = exchangeᵥ i (xs -, y) -, x

  exchangeₐ : ∀ {b} {P : A → Set b} (i : Fin n) {xs : Vec A (suc n)} → All P xs → All P (exchangeᵥ i xs)
  exchangeₐ zero (xs -, y -, x) = xs -, x -, y
  exchangeₐ (suc i) (xs -, y -, x) = exchangeₐ i (xs -, y) -, x

-- TODO: rewrite this crap
∋-exchange : {γ : PreCtx (suc n)} {idxs : Idxs (suc n)} {Γ Θ : Ctx idxs} {t : Type} {x : Usage idx ²}
       → (i : Fin n)
       → γ ； Γ ∋[ j ] t ； x ▹ Θ
       → exchangeᵥ i γ ； exchangeₐ i Γ ∋[ exchangeFin i j ] t ； x ▹ exchangeₐ i Θ
∋-exchange {γ = _ -, _ -, _} {idxs = _ -, _ -, _} {Γ = _ -, _ -, _} zero (zero , zero xyz) = (suc zero , suc (zero xyz))
∋-exchange {γ = _ -, _ -, _} zero (suc zero , suc (zero xyz)) = zero , zero xyz
∋-exchange {γ = _ -, _ -, _} zero (suc (suc t) , suc (suc x)) = suc (suc t) , suc (suc x)
∋-exchange {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc i) (zero , zero xyz) = zero , zero xyz
∋-exchange {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc zero) (suc zero , suc (zero xyz)) = suc (suc zero) , suc (suc (zero xyz))
∋-exchange {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc (suc i)) (suc zero , suc (zero xyz)) = suc zero , suc (zero xyz)
∋-exchange {j = suc (suc j)} {γ = γ -, _} {Γ = Γ -, _} (suc i) (suc (suc t) , suc (suc x)) with Fin.inject₁ i Finₚ.≟ suc j
∋-exchange {j = suc (suc j)} {γ = γ -, _} {Γ = Γ -, _} (suc zero) (suc (suc t) , suc (suc x)) | yes ()
∋-exchange {j = suc (suc ._)} {γ = γ -, _} {Γ = Γ -, _} {Θ = Θ -, _} (suc (suc i)) (suc st@(suc t) , suc sx@(suc x)) | yes refl =
  let s' = subst (λ ● → exchangeᵥ (suc i) γ ； exchangeₐ (suc i) Γ ∋[ ● ] _ ； _ ▹ exchangeₐ (suc i) Θ)
                 (sym (trans (cong suc (sym (trans (exchangeFin-injectˡ i) (cong suc (sym (Finₚ.lower₁-inject₁′ i _))))))
                 (exchangeFin-suc i (Fin.inject₁ i)))) (∋-exchange (suc i) (st , sx))
  in there s'
∋-exchange {j = suc (suc j)} {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc i) (suc st@(suc t) , suc sx@(suc x)) | no ¬p with i Finₚ.≟ j
∋-exchange {j = suc (suc j)} {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc i) (suc st@(suc t) , suc sx@(suc x)) | no ¬p | yes refl rewrite sym (exchangeFin-injectʳ i) = there (∋-exchange i (st , sx))
∋-exchange {j = suc (suc j)} {γ = _ -, _ -, _ -, _} {Γ = _ -, _ -, _ -, _} (suc i) (suc st@(suc t) , suc sx@(suc x)) | no ¬p | no ¬q rewrite sym (exchangeFin-neq i j ¬q ¬p) = there (∋-exchange i (st , sx))

⊢-exchange : {γ : PreCtx (suc n)} {Γ Θ : Ctx idxs}
       → (i : Fin n)
       → γ ； Γ ⊢ P ▹ Θ
       → exchangeᵥ i γ ； exchangeₐ i Γ ⊢ exchange i P ▹ exchangeₐ i Θ
⊢-exchange {γ = _ -, _ -, _} {Γ = _ -, _ -, _} {Θ = _ -, _ -, _} i 𝟘 = 𝟘
⊢-exchange {γ = _ -, _ -, _} {Γ = _ -, _ -, _} {Θ = _ -, _ -, _} i (ν t m μ ⊢P) = ν t m μ (⊢-exchange (suc i) ⊢P)
⊢-exchange {γ = _ -, _ -, _} {Γ = _ -, _ -, _} {Θ = _ -, _ -, _} i (_⦅⦆_ {Ξ = _ -, _ -, _} x ⊢P) = ∋-exchange i x ⦅⦆ ⊢-exchange (suc i) ⊢P
⊢-exchange {γ = _ -, _ -, _} {Γ = _ -, _ -, _} {Θ = _ -, _ -, _} i (x ⟨ y ⟩ ⊢P) = ∋-exchange i x ⟨ ∋-exchange i y ⟩ (⊢-exchange i ⊢P)
⊢-exchange {γ = _ -, _ -, _} {Γ = _ -, _ -, _} {Θ = _ -, _ -, _} i (⊢P ∥ ⊢Q) = ⊢-exchange i ⊢P ∥ ⊢-exchange i ⊢Q

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
{-

Part 4: Higher inductive types

- Quotients via HITs
- Propositional truncation for logic?
- CS example using quotients (maybe finite multisets or queues)
- Synthetic homotopy theory (probably Torus = S^1 * S^1, pi_1(S^1) =
  Z, pi_1(Torus) = Z * Z)

-}

{-# OPTIONS --cubical #-}
module Part4 where

open import Cubical.Foundations.Prelude hiding (refl ; cong ; subst ; sym)
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Int
open import Cubical.Data.Prod

open import Part3

-----------------------------------------------------------------------------
-- Higher inductive types

-- The following definition of finite multisets is due to Vikraman
-- Choudhury and Marcelo Fiore.

infixr 5 _∷_

data FMSet (A : Type ℓ) : Type ℓ where
  [] : FMSet A
  _∷_ : (x : A) → (xs : FMSet A) → FMSet A
  comm : (x y : A) (xs : FMSet A) → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
--  trunc : (xs ys : FMSet A) (p q : xs ≡ ys) → p ≡ q

-- We need to add the trunc constructor for FMSets to be sets, omitted
-- here for simplicity.

_++_ : ∀ {A : Type ℓ} (xs ys : FMSet A) → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys
comm x y xs i ++ ys = comm x y (xs ++ ys) i
-- trunc xs zs p q i j ++ ys =
--   trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

unitr-++ : {A : Type ℓ} (xs : FMSet A) → xs ++ [] ≡ xs
unitr-++ [] = refl
unitr-++ (x ∷ xs) = cong (x ∷_) (unitr-++ xs)
unitr-++ (comm x y xs i) j = comm x y (unitr-++ xs j) i
-- unitr-++ (trunc xs ys x y i j) = {!!}

-- This is a special case of set quotients! Very useful for
-- programming and set level mathematics

data _/_ (A : Type ℓ) (R : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  [_] : A → A / R
  eq/ : (a b : A) → R a b → [ a ] ≡ [ b ]
  trunc : (a b : A / R) (p q : a ≡ b) → p ≡ q

-- Proving that they are effective ((a b : A) → [ a ] ≡ [ b ] → R a b)
-- requires univalence for propositions.

-------------------------------------------------------------------------
-- Topological examples of things that are not sets

-- We can define the circle as the following simple data declaration:
data S¹ : Type₀ where
  base : S¹
  loop : base ≡ base

-- We can write functions on S¹ using pattern-matching equations:
double : S¹ → S¹
double base = base
double (loop i) = (loop ∙ loop) i

helix : S¹ → Type₀
helix base     = Int
helix (loop i) = sucPathInt i

ΩS¹ : Type₀
ΩS¹ = base ≡ base

winding : ΩS¹ → Int
winding p = subst helix p (pos 0)

_ : winding (λ i → double ((loop ∙ loop) i)) ≡ pos 4
_ = refl

-- We can define the Torus as:
data Torus : Type₀ where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

-- And prove that it is equivalent to two circle:
t2c : Torus → S¹ × S¹
t2c point        = (base , base)
t2c (line1 i)    = (loop i , base)
t2c (line2 j)    = (base , loop j)
t2c (square i j) = (loop i , loop j)

c2t : S¹ × S¹ → Torus
c2t (base   , base)   = point
c2t (loop i , base)   = line1 i
c2t (base   , loop j) = line2 j
c2t (loop i , loop j) = square i j

c2t-t2c : (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point        = refl
c2t-t2c (line1 _)    = refl
c2t-t2c (line2 _)    = refl
c2t-t2c (square _ _) = refl

t2c-c2t : (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base   , base)   = refl
t2c-c2t (base   , loop _) = refl
t2c-c2t (loop _ , base)   = refl
t2c-c2t (loop _ , loop _) = refl

-- Using univalence we get the following equality:
Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath' (iso t2c c2t t2c-c2t c2t-t2c)

windingTorus : point ≡ point → Int × Int
windingTorus l = ( winding (λ i → proj₁ (t2c (l i)))
                 , winding (λ i → proj₂ (t2c (l i))))

_ : windingTorus (line1 ∙ sym line2) ≡ (pos 1 , negsuc 0)
_ = refl

-- We have many more topological examples, including Klein bottle, RP^n,
-- higher spheres, suspensions, join, wedges, smash product:
open import Cubical.HITs.KleinBottle
open import Cubical.HITs.RPn
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Susp
open import Cubical.HITs.Join
-- open import Cubical.HITs.Wedge
open import Cubical.HITs.SmashProduct

-- There's also a proof of the "3x3 lemma" for pushouts in less than
-- 200LOC. In HoTT-Agda this took about 3000LOC. For details see:
-- https://github.com/HoTT/HoTT-Agda/tree/master/theorems/homotopy/3x3
open import Cubical.HITs.Pushout

-- We also defined the Hopf fibration and proved that its total space
-- is S³ in about 300LOC:
open import Cubical.HITs.Hopf

-- There is also some integer cohomology:
open import Cubical.ZCohomology.Everything
-- To compute cohomology groups of various spaces we need a bunch of
-- interesting theorems: Freudenthal suspension theorem,
-- Mayer-Vietoris sequence...
open import Cubical.Homotopy.Freudenthal
-- open import Cubical.ZCohomology.MayerVietorisUnreduced


text:
--------------------------------------------------------------------
-- This file contains the definition of and facts about functors. --
--------------------------------------------------------------------
module Category.Funct where

open import Level

open import Relation.Relation

open import Relation.Binary.PropositionalEquality public renaming (_≡_ to _P≡_; sym to prop-sym ; trans to prop-trans; refl to prop-refl)

open import Setoid.Total
open import Category.Category

record Functor {l₁ l₂ : Level} (ℂ₁ : Cat {l₁}) (ℂ₂ : Cat {l₂}) : Set (l₁ ⊔ l₂) where
  constructor Funct_,_,_,_
  field
    -- The object map.
    omap : Obj ℂ₁ → Obj ℂ₂

    -- The morphism map.
    fmap : {A B : Obj ℂ₁}
      → SetoidFun (Hom ℂ₁ A B) (Hom ℂ₂ (omap A) (omap B))

    -- The morphism map must send identities to identities.
    idPF : ∀{A}
     → ⟨  Hom ℂ₂ (omap A) (omap A) ⟩[ appT fmap (id ℂ₁) ≡ id ℂ₂ ]
    -- The morphism map must respect composition.
    compPF : ∀{A B C}{f : el (Hom ℂ₁ A B)}{g : el (Hom ℂ₁ B C)}
      → ⟨ Hom ℂ₂ (omap A) (omap C) ⟩[ appT fmap (f ○[ comp ℂ₁ ] g) ≡ (appT fmap f) ○[ comp ℂ₂ ] (appT fmap g) ]

open Functor public

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------------
-- The alternating bit protocol (ABP) is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the ABP by simplifing the
-- formalization in Dybjer and Sander (1989) using a stronger (maybe
-- invalid) co-induction principle.

module FOT.FOTC.Program.ABP.StrongerInductionPrinciple.CorrectnessProofATP
  where

open import FOT.FOTC.Relation.Binary.Bisimilarity.Type
open import FOT.FOTC.Program.ABP.StrongerInductionPrinciple.LemmaATP

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Data.Stream.Equality.PropertiesATP
open import FOTC.Program.ABP.ABP hiding ( B )
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
postulate
  helper :
    ∀ b i' is' os₁ os₂ →
    S b (i' ∷ is') os₁ os₂
      (has (send b) (ack b) (out b) (corrupt os₁) (corrupt os₂) (i' ∷ is'))
      (hbs (send b) (ack b) (out b) (corrupt os₁) (corrupt os₂) (i' ∷ is'))
      (hcs (send b) (ack b) (out b) (corrupt os₁) (corrupt os₂) (i' ∷ is'))
      (hds (send b) (ack b) (out b) (corrupt os₁) (corrupt os₂) (i' ∷ is'))
      (abpTransfer b os₁ os₂ (i' ∷ is'))
{-# ATP prove helper #-}

-- Main theorem.

-- See Issue https://github.com/asr/apia/issues/81 .
abpCorrectB : D → D → Set
abpCorrectB xs ys = xs ≡ xs
{-# ATP definition abpCorrectB #-}

abpCorrect : ∀ {b is os₁ os₂} → Bit b → Stream is → Fair os₁ → Fair os₂ →
             is ≈ abpTransfer b os₁ os₂ is
abpCorrect {b} {is} {os₁} {os₂} Bb Sis Fos₁ Fos₂ = ≈-stronger-coind abpCorrectB h refl
  where
  postulate
    h : abpCorrectB is (abpTransfer b os₁ os₂ is) →
        ∃[ i' ] ∃[ is' ] ∃[ js' ]
          is ≡ i' ∷ is' ∧ abpTransfer b os₁ os₂ is ≡ i' ∷ js' ∧ abpCorrectB is' js'
  {-# ATP prove h helper lemma #-}

------------------------------------------------------------------------------
-- abpTransfer produces a Stream.
postulate
  abpTransfer-Stream : ∀ {b is os₁ os₂} →
                       Bit b →
                       Stream is →
                       Fair os₁ →
                       Fair os₂ →
                       Stream (abpTransfer b os₁ os₂ is)
{-# ATP prove abpTransfer-Stream ≈→Stream₂ abpCorrect #-}

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.


text:
module Syntax where

open import Stack public

-- Abstract symbols, or atoms.

abstract
  Atom : Set
  Atom = Nat

-- Types, or propositions in constructive modal logic S4.

infixl 9 _⩕_
infixl 8 _⩖_
infixr 7 _⇒_
data Type : Set where
  α_   : Atom → Type
  _⇒_ : Type → Type → Type
  □_   : Type → Type
  _⩕_  : Type → Type → Type
  ⫪   : Type
  ⫫   : Type
  _⩖_  : Type → Type → Type

⫬_ : Type → Type
⫬ A = A ⇒ ⫫

-- Contexts, or stack pairs of types.

Context : Set
Context = Stack² Type Type

-- Derivations, or syntactic entailment.

infix 3 _⊢_
data _⊢_ : Context → Type → Set where
  var   : ∀ {A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ ⊢ A
  mvar  : ∀ {A Γ Δ}     → A ∈ Δ → Γ ⁏ Δ ⊢ A
  lam   : ∀ {A B Γ Δ}   → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⇒ B
  app   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ⇒ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
  box   : ∀ {A Γ Δ}     → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ □ A
  unbox : ∀ {A C Γ Δ}   → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ C → Γ ⁏ Δ ⊢ C
  pair  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⩕ B
  fst   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ⩕ B → Γ ⁏ Δ ⊢ A
  snd   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ⩕ B → Γ ⁏ Δ ⊢ B
  unit  : ∀ {Γ Δ}       → Γ ⁏ Δ ⊢ ⫪
  boom  : ∀ {C Γ Δ}     → Γ ⁏ Δ ⊢ ⫫ → Γ ⁏ Δ ⊢ C
  left  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A ⩖ B
  right : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ⩖ B
  case  : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ A ⩖ B → Γ , A ⁏ Δ ⊢ C → Γ , B ⁏ Δ ⊢ C → Γ ⁏ Δ ⊢ C

-- Shorthand for variables.

v₀ : ∀ {Γ Δ A} → Γ , A ⁏ Δ ⊢ A
v₀ = var i₀

v₁ : ∀ {Γ Δ A B} → Γ , A , B ⁏ Δ ⊢ A
v₁ = var i₁

v₂ : ∀ {Γ Δ A B C} → Γ , A , B , C ⁏ Δ ⊢ A
v₂ = var i₂

mv₀ : ∀ {Γ Δ A} → Γ ⁏ Δ , A ⊢ A
mv₀ = mvar i₀

mv₁ : ∀ {Γ Δ A B} → Γ ⁏ Δ , A , B ⊢ A
mv₁ = mvar i₁

mv₂ : ∀ {Γ Δ A B C} → Γ ⁏ Δ , A , B , C ⊢ A
mv₂ = mvar i₂

-- Stacks of derivations, or simultaneous syntactic entailment.

infix 3 _⊢⋆_
_⊢⋆_ : Context → Stack Type → Set
Γ ⁏ Δ ⊢⋆ ∅     = ⊤
Γ ⁏ Δ ⊢⋆ Ξ , A = Γ ⁏ Δ ⊢⋆ Ξ ∧ Γ ⁏ Δ ⊢ A

-- Monotonicity of syntactic entailment with respect to context inclusion.

mono⊢ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ′ ⊢ A
mono⊢ (η , ρ) (var i)      = var (mono∈ η i)
mono⊢ (η , ρ) (mvar i)     = mvar (mono∈ ρ i)
mono⊢ (η , ρ) (lam d)      = lam (mono⊢ (keep η , ρ) d)
mono⊢ ψ       (app d e)    = app (mono⊢ ψ d) (mono⊢ ψ e)
mono⊢ (η , ρ) (box d)      = box (mono⊢ (bot , ρ) d)
mono⊢ (η , ρ) (unbox d e)  = unbox (mono⊢ (η , ρ) d) (mono⊢ (η , keep ρ) e)
mono⊢ ψ       (pair d e)   = pair (mono⊢ ψ d) (mono⊢ ψ e)
mono⊢ ψ       (fst d)      = fst (mono⊢ ψ d)
mono⊢ ψ       (snd d)      = snd (mono⊢ ψ d)
mono⊢ ψ       unit         = unit
mono⊢ ψ       (boom d)     = boom (mono⊢ ψ d)
mono⊢ ψ       (left d)     = left (mono⊢ ψ d)
mono⊢ ψ       (right d)    = right (mono⊢ ψ d)
mono⊢ (η , ρ) (case d e f) = case (mono⊢ (η , ρ) d) (mono⊢ (keep η , ρ) e)
                                                      (mono⊢ (keep η , ρ) f)

mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ′ ⊢⋆ Ξ
mono⊢⋆ {∅}     ψ ∙       = ∙
mono⊢⋆ {Ξ , A} ψ (ξ , d) = mono⊢⋆ ψ ξ , mono⊢ ψ d

-- Reflexivity of simultaneous syntactic entailment.

refl⊢⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ (weak⊆ , refl⊆) refl⊢⋆ , v₀

mrefl⊢⋆ : ∀ {Δ Γ} → Γ ⁏ Δ ⊢⋆ Δ
mrefl⊢⋆ {∅}     = ∙
mrefl⊢⋆ {Δ , A} = mono⊢⋆ (refl⊆ , weak⊆) mrefl⊢⋆ , mv₀

-- Grafting of derivation trees, or simultaneous substitution, or cut.

graft∈ : ∀ {Ξ Γ Δ C} → Γ ⁏ Δ ⊢⋆ Ξ → C ∈ Ξ → Γ ⁏ Δ ⊢ C
graft∈ (ξ , d) top     = d
graft∈ (ξ , d) (pop i) = graft∈ ξ i

graft⊢ : ∀ {Γ Γ′ Δ Δ′ C} → Γ′ ⁏ Δ′ ⊢⋆ Γ → ∅ ⁏ Δ′ ⊢⋆ Δ → Γ ⁏ Δ ⊢ C → Γ′ ⁏ Δ′ ⊢ C
graft⊢ σ τ (var i)      = graft∈ σ i
graft⊢ σ τ (mvar i)     = mono⊢ (bot , refl⊆) (graft∈ τ i)
graft⊢ σ τ (lam d)      = lam (graft⊢ (mono⊢⋆ (weak⊆ , refl⊆) σ , v₀) τ d)
graft⊢ σ τ (app d e)    = app (graft⊢ σ τ d) (graft⊢ σ τ e)
graft⊢ σ τ (box d)      = box (graft⊢ ∙ τ d)
graft⊢ σ τ (unbox d e)  = unbox (graft⊢ σ τ d) (graft⊢ (mono⊢⋆ (refl⊆ , weak⊆) σ)
                                                          (mono⊢⋆ (refl⊆ , weak⊆) τ , mv₀) e)
graft⊢ σ τ (pair d e)   = pair (graft⊢ σ τ d) (graft⊢ σ τ e)
graft⊢ σ τ (fst d)      = fst (graft⊢ σ τ d)
graft⊢ σ τ (snd d)      = snd (graft⊢ σ τ d)
graft⊢ σ τ unit         = unit
graft⊢ σ τ (boom d)     = boom (graft⊢ σ τ d)
graft⊢ σ τ (left d)     = left (graft⊢ σ τ d)
graft⊢ σ τ (right d)    = right (graft⊢ σ τ d)
graft⊢ σ τ (case d e f) = case (graft⊢ σ τ d) (graft⊢ (mono⊢⋆ (weak⊆ , refl⊆) σ , v₀) τ e)
                                                (graft⊢ (mono⊢⋆ (weak⊆ , refl⊆) σ , v₀) τ f)

-- Derivations, or syntactic entailment, in normal form.

mutual
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ : Context → Type → Set where
    lamⁿᶠ   : ∀ {A B Γ Δ}   → Γ , A ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⇒ B
    boxⁿᶠ   : ∀ {A Γ Δ}     → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ⁿᶠ □ A
    pairⁿᶠ  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⩕ B
    unitⁿᶠ  : ∀ {Γ Δ}       → Γ ⁏ Δ ⊢ⁿᶠ ⫪
    leftⁿᶠ  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ A ⩖ B
    rightⁿᶠ : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ⩖ B
    neⁿᶠ    : ∀ {A Γ Δ}     → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ⁿᶠ A

  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ : Context → Type → Set where
    varⁿᵉ   : ∀ {A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ ⊢ⁿᵉ A
    mvarⁿᵉ  : ∀ {A Γ Δ}     → A ∈ Δ → Γ ⁏ Δ ⊢ⁿᵉ A
    appⁿᵉ   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᵉ A ⇒ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᵉ B
    unboxⁿᵉ : ∀ {A C Γ Δ}   → Γ ⁏ Δ ⊢ⁿᵉ □ A → Γ ⁏ Δ , A ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᵉ C
    fstⁿᵉ   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ⁿᵉ A
    sndⁿᵉ   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᵉ A ⩕ B → Γ ⁏ Δ ⊢ⁿᵉ B
    boomⁿᵉ  : ∀ {C Γ Δ}     → Γ ⁏ Δ ⊢ⁿᵉ ⫫ → Γ ⁏ Δ ⊢ⁿᵉ C
    caseⁿᵉ  : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A ⩖ B → Γ , A ⁏ Δ ⊢ⁿᶠ C → Γ , B ⁏ Δ ⊢ⁿᶠ C → Γ ⁏ Δ ⊢ⁿᵉ C

-- Shorthand for variables.

v₀ⁿᵉ : ∀ {Γ Δ A} → Γ , A ⁏ Δ ⊢ⁿᵉ A
v₀ⁿᵉ = varⁿᵉ top

mv₀ⁿᵉ : ∀ {Γ Δ A} → Γ ⁏ Δ , A ⊢ⁿᵉ A
mv₀ⁿᵉ = mvarⁿᵉ top

-- Stacks of derivations, or simultaneous syntactic entailment, in normal form.

infix 3 _⊢⋆ⁿᵉ_
_⊢⋆ⁿᵉ_ : Context → Stack Type → Set
Γ ⁏ Δ ⊢⋆ⁿᵉ ∅     = ⊤
Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ , A = Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ ∧ Γ ⁏ Δ ⊢ⁿᵉ A

-- Translation from normal form to arbitrary form.

mutual
  nf→af : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ A
  nf→af (neⁿᶠ d)       = ne→af d
  nf→af (lamⁿᶠ d)      = lam (nf→af d)
  nf→af (boxⁿᶠ d)      = box d
  nf→af (pairⁿᶠ d e)   = pair (nf→af d) (nf→af e)
  nf→af unitⁿᶠ         = unit
  nf→af (leftⁿᶠ d)     = left (nf→af d)
  nf→af (rightⁿᶠ d)    = right (nf→af d)

  ne→af : ∀ {Γ Δ A} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ A
  ne→af (varⁿᵉ i)      = var i
  ne→af (mvarⁿᵉ i)     = mvar i
  ne→af (appⁿᵉ d e)    = app (ne→af d) (nf→af e)
  ne→af (unboxⁿᵉ d e)  = unbox (ne→af d) (nf→af e)
  ne→af (fstⁿᵉ d)      = fst (ne→af d)
  ne→af (sndⁿᵉ d)      = snd (ne→af d)
  ne→af (boomⁿᵉ d)     = boom (ne→af d)
  ne→af (caseⁿᵉ d e f) = case (ne→af d) (nf→af e) (nf→af f)

-- Monotonicity of syntactic entailment with respect to context inclusion, in normal form.

mutual
  mono⊢ⁿᶠ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ′ ⁏ Δ′ ⊢ⁿᶠ A
  mono⊢ⁿᶠ (η , ρ) (lamⁿᶠ d)      = lamⁿᶠ (mono⊢ⁿᶠ (keep η , ρ) d)
  mono⊢ⁿᶠ (η , ρ) (boxⁿᶠ d)      = boxⁿᶠ (mono⊢ (bot , ρ) d)
  mono⊢ⁿᶠ ψ       (pairⁿᶠ d e)   = pairⁿᶠ (mono⊢ⁿᶠ ψ d) (mono⊢ⁿᶠ ψ e)
  mono⊢ⁿᶠ ψ       unitⁿᶠ         = unitⁿᶠ
  mono⊢ⁿᶠ ψ       (leftⁿᶠ d)     = leftⁿᶠ (mono⊢ⁿᶠ ψ d)
  mono⊢ⁿᶠ ψ       (rightⁿᶠ d)    = rightⁿᶠ (mono⊢ⁿᶠ ψ d)
  mono⊢ⁿᶠ ψ       (neⁿᶠ d)       = neⁿᶠ (mono⊢ⁿᵉ ψ d)

  mono⊢ⁿᵉ : ∀ {Γ Γ′ Δ Δ′ A} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ′ ⁏ Δ′ ⊢ⁿᵉ A
  mono⊢ⁿᵉ (η , ρ) (varⁿᵉ i)      = varⁿᵉ (mono∈ η i)
  mono⊢ⁿᵉ (η , ρ) (mvarⁿᵉ i)     = mvarⁿᵉ (mono∈ ρ i)
  mono⊢ⁿᵉ ψ       (appⁿᵉ d e)    = appⁿᵉ (mono⊢ⁿᵉ ψ d) (mono⊢ⁿᶠ ψ e)
  mono⊢ⁿᵉ (η , ρ) (unboxⁿᵉ d e)  = unboxⁿᵉ (mono⊢ⁿᵉ (η , ρ) d) (mono⊢ⁿᶠ (η , keep ρ) e)
  mono⊢ⁿᵉ ψ       (fstⁿᵉ d)      = fstⁿᵉ (mono⊢ⁿᵉ ψ d)
  mono⊢ⁿᵉ ψ       (sndⁿᵉ d)      = sndⁿᵉ (mono⊢ⁿᵉ ψ d)
  mono⊢ⁿᵉ ψ       (boomⁿᵉ d)     = boomⁿᵉ (mono⊢ⁿᵉ ψ d)
  mono⊢ⁿᵉ (η , ρ) (caseⁿᵉ d e f) = caseⁿᵉ (mono⊢ⁿᵉ (η , ρ) d) (mono⊢ⁿᶠ (keep η , ρ) e)
                                                                (mono⊢ⁿᶠ (keep η , ρ) f)

mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ′ ⁏ Δ′ ⊢⋆ⁿᵉ Ξ
mono⊢⋆ⁿᵉ {∅}     ψ ∙       = ∙
mono⊢⋆ⁿᵉ {Ξ , A} ψ (ξ , d) = mono⊢⋆ⁿᵉ ψ ξ , mono⊢ⁿᵉ ψ d

-- Reflexivity of simultaneous syntactic entailment, in normal form.

refl⊢⋆ⁿᵉ : ∀ {Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Γ
refl⊢⋆ⁿᵉ {∅}     = ∙
refl⊢⋆ⁿᵉ {Γ , A} = mono⊢⋆ⁿᵉ (weak⊆ , refl⊆) refl⊢⋆ⁿᵉ , v₀ⁿᵉ

mrefl⊢⋆ⁿᵉ : ∀ {Δ Γ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Δ
mrefl⊢⋆ⁿᵉ {∅}     = ∙
mrefl⊢⋆ⁿᵉ {Δ , A} = mono⊢⋆ⁿᵉ (refl⊆ , weak⊆) mrefl⊢⋆ⁿᵉ , mv₀ⁿᵉ


text:
-- {-# OPTIONS -v tc.meta:20 #-}
-- Agdalist 2010-09-24 David Leduc
module Issue323 where

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

data Trivial {A : Set}(a : A) : Set where
  trivial : Trivial a

lemma : (A : Set)(x y : A) -> Trivial (x , y)
lemma A x y = trivial


text:
import      Lvl
open import Type

module Type.Functions.Inverse {ℓₗ : Lvl.Level}{ℓₒ₁}{ℓₒ₂} {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where

open import Function.Domains
open import Type.Functions {ℓₗ}{ℓₒ₁}{ℓₒ₂} {X}{Y}
open import Type.Properties.Empty
open import Type.Properties.Singleton {ℓₒ₁}{ℓₒ₂}

inv : (f : X → Y) → ⦃ _ : Bijective(f) ⦄ → (Y → X)
inv f ⦃ Bijective.intro(proof) ⦄ (y) with proof{y}
... | IsUnit.intro (Unapply.intro x) _ = x

invᵣ : (f : X → Y) → ⦃ _ : Surjective(f) ⦄ → (Y → X)
invᵣ f ⦃ Surjective.intro(proof) ⦄ (y) with proof{y}
... | ◊.intro ⦃ Unapply.intro x ⦄ = x

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Issue2486.HaskellB where

{-# FOREIGN GHC import qualified MAlonzo.Code.Issue2486.ImportB as B #-}

{-# FOREIGN GHC

data Test = Con B.BBool

#-}

max_forks_repo_name: Agda-zh/agda


text:
module FreeVarPresheaves where

open import Data.Nat as Nat
import Level
open import Categories.Category
open import Categories.Presheaf
open import Relation.Binary.Core
open import Relation.Binary
open import Function using (flip)

module DTO = DecTotalOrder Nat.decTotalOrder

data ℕ-≤-eq {n m : ℕ} : Rel (n ≤ m) Level.zero where
  triv-eq : ∀ {p q} → ℕ-≤-eq p q

ℕ-≤-eq-equivRel : ∀ {n m} → IsEquivalence (ℕ-≤-eq {n} {m})
ℕ-≤-eq-equivRel = record
  { refl = triv-eq
  ; sym = λ _ → triv-eq
  ; trans = λ _ _ → triv-eq
  }

{-
trans-assoc : ∀ {a ℓ} {A : Set a} →
  {_<_ : Rel A ℓ} →
  {trans : Transitive _<_} →
  ∀ {w x y z : A} → ∀{p : w < x} → ∀{q : x < y} → ∀{r : y < z} →
  (trans p (trans q r)) ≡ (trans (trans p q) r)
trans-assoc = {!!}
-}

ℕ-≤-eq-assoc : {m n k i : ℕ} {p : m ≤ n} {q : n ≤ k} {r : k ≤ i} →
  ℕ-≤-eq (DTO.trans p (DTO.trans q r)) (DTO.trans (DTO.trans p q) r)
ℕ-≤-eq-assoc = triv-eq

trans-resp-ℕ-≤-eq : {m n k : ℕ} {p r : n ≤ k} {q s : m ≤ n} →
  ℕ-≤-eq p r → ℕ-≤-eq q s → ℕ-≤-eq (DTO.trans q p) (DTO.trans s r)
trans-resp-ℕ-≤-eq _ _ = triv-eq

op : Category Level.zero Level.zero Level.zero
op = record
   { Obj = ℕ
   ; _⇒_ = Nat._≤_
   ; _≡_ = ℕ-≤-eq
   ; _∘_ = flip DTO.trans
   ; id = DTO.refl
   ; assoc = ℕ-≤-eq-assoc
   ; identityˡ = triv-eq
   ; identityʳ = triv-eq
   ; equiv = ℕ-≤-eq-equivRel
   ; ∘-resp-≡ = trans-resp-ℕ-≤-eq
   }

Ctx a = List (Var a)

data Var : (Γ : Ctx) → Set where
  zero : ∀{Γ}               → TyVar (Γ + 1)
  succ : ∀{Γ} (x : TyVar Γ) → TyVar (Γ + 1)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Andreas, 2015-08-27 Allow rewrite rules for symbols defined in other file

{-# OPTIONS --rewriting #-}

open import Common.Nat
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

x+0 : ∀ x → x + 0 ≡ x
x+0 zero = refl
x+0 (suc x) rewrite x+0 x = refl

{-# REWRITE x+0 #-}  -- adding rewrite rule for + is ok

x+0+0 : ∀{x} → (x + 0) + 0 ≡ x
x+0+0 = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
------------------------------------------------------------------------

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

module Function.Related where

open import Level
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq      using (Equivalence)
open import Function.Injection   as Inj     using (Injection; _↣_)
open import Function.Inverse     as Inv     using (Inverse; _↔_)
open import Function.LeftInverse as LeftInv using (LeftInverse)
open import Function.Surjection  as Surj    using (Surjection)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Wrapper types

-- Synonyms which are used to make _∼[_]_ below "constructor-headed"
-- (which implies that Agda can deduce the universe code from an
-- expression matching any of the right-hand sides).

record _←_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor lam
  field app-← : B → A

open _←_ public

record _↢_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor lam
  field app-↢ : B ↣ A

open _↢_ public

------------------------------------------------------------------------
-- Relatedness

-- There are several kinds of "relatedness".

-- The idea to include kinds other than equivalence and bijection came
-- from Simon Thompson and Bengt Nordström. /NAD

data Kind : Set where
  implication         : Kind
  reverse-implication : Kind
  equivalence         : Kind
  injection           : Kind
  reverse-injection   : Kind
  left-inverse        : Kind
  surjection          : Kind
  bijection           : Kind

-- Interpretation of the codes above. The code "bijection" is
-- interpreted as Inverse rather than Bijection; the two types are
-- equivalent.

infix 4 _∼[_]_

_∼[_]_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Kind → Set ℓ₂ → Set _
A ∼[ implication         ] B = A → B
A ∼[ reverse-implication ] B = A ← B
A ∼[ equivalence         ] B = Equivalence (P.setoid A) (P.setoid B)
A ∼[ injection           ] B = Injection   (P.setoid A) (P.setoid B)
A ∼[ reverse-injection   ] B = A ↢ B
A ∼[ left-inverse        ] B = LeftInverse (P.setoid A) (P.setoid B)
A ∼[ surjection          ] B = Surjection  (P.setoid A) (P.setoid B)
A ∼[ bijection           ] B = Inverse     (P.setoid A) (P.setoid B)

-- A non-infix synonym.

Related : Kind → ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set _
Related k A B = A ∼[ k ] B

-- The bijective equality implies any kind of relatedness.

↔⇒ : ∀ {k x y} {X : Set x} {Y : Set y} →
     X ∼[ bijection ] Y → X ∼[ k ] Y
↔⇒ {implication}         = _⟨$⟩_ ∘ Inverse.to
↔⇒ {reverse-implication} = lam ∘′ _⟨$⟩_ ∘ Inverse.from
↔⇒ {equivalence}         = Inverse.equivalence
↔⇒ {injection}           = Inverse.injection
↔⇒ {reverse-injection}   = lam ∘′ Inverse.injection ∘ Inv.sym
↔⇒ {left-inverse}        = Inverse.left-inverse
↔⇒ {surjection}          = Inverse.surjection
↔⇒ {bijection}           = id

-- Actual equality also implies any kind of relatedness.

≡⇒ : ∀ {k ℓ} {X Y : Set ℓ} → X ≡ Y → X ∼[ k ] Y
≡⇒ P.refl = ↔⇒ Inv.id

------------------------------------------------------------------------
-- Special kinds of kinds

-- Kinds whose interpretation is symmetric.

data Symmetric-kind : Set where
  equivalence : Symmetric-kind
  bijection   : Symmetric-kind

-- Forgetful map.

⌊_⌋ : Symmetric-kind → Kind
⌊ equivalence ⌋ = equivalence
⌊ bijection   ⌋ = bijection

-- The proof of symmetry can be found below.

-- Kinds whose interpretation include a function which "goes in the
-- forward direction".

data Forward-kind : Set where
  implication  : Forward-kind
  equivalence  : Forward-kind
  injection    : Forward-kind
  left-inverse : Forward-kind
  surjection   : Forward-kind
  bijection    : Forward-kind

-- Forgetful map.

⌊_⌋→ : Forward-kind → Kind
⌊ implication  ⌋→ = implication
⌊ equivalence  ⌋→ = equivalence
⌊ injection    ⌋→ = injection
⌊ left-inverse ⌋→ = left-inverse
⌊ surjection   ⌋→ = surjection
⌊ bijection    ⌋→ = bijection

-- The function.

⇒→ : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋→ ] Y → X → Y
⇒→ {implication}  = id
⇒→ {equivalence}  = _⟨$⟩_ ∘ Equivalence.to
⇒→ {injection}    = _⟨$⟩_ ∘ Injection.to
⇒→ {left-inverse} = _⟨$⟩_ ∘ LeftInverse.to
⇒→ {surjection}   = _⟨$⟩_ ∘ Surjection.to
⇒→ {bijection}    = _⟨$⟩_ ∘ Inverse.to

-- Kinds whose interpretation include a function which "goes backwards".

data Backward-kind : Set where
  reverse-implication : Backward-kind
  equivalence         : Backward-kind
  reverse-injection   : Backward-kind
  left-inverse        : Backward-kind
  surjection          : Backward-kind
  bijection           : Backward-kind

-- Forgetful map.

⌊_⌋← : Backward-kind → Kind
⌊ reverse-implication ⌋← = reverse-implication
⌊ equivalence         ⌋← = equivalence
⌊ reverse-injection   ⌋← = reverse-injection
⌊ left-inverse        ⌋← = left-inverse
⌊ surjection          ⌋← = surjection
⌊ bijection           ⌋← = bijection

-- The function.

⇒← : ∀ {k x y} {X : Set x} {Y : Set y} → X ∼[ ⌊ k ⌋← ] Y → Y → X
⇒← {reverse-implication} = app-←
⇒← {equivalence}         = _⟨$⟩_ ∘ Equivalence.from
⇒← {reverse-injection}   = _⟨$⟩_ ∘ Injection.to ∘ app-↢
⇒← {left-inverse}        = _⟨$⟩_ ∘ LeftInverse.from
⇒← {surjection}          = _⟨$⟩_ ∘ Surjection.from
⇒← {bijection}           = _⟨$⟩_ ∘ Inverse.from

-- Kinds whose interpretation include functions going in both
-- directions.

data Equivalence-kind : Set where
    equivalence  : Equivalence-kind
    left-inverse : Equivalence-kind
    surjection   : Equivalence-kind
    bijection    : Equivalence-kind

-- Forgetful map.

⌊_⌋⇔ : Equivalence-kind → Kind
⌊ equivalence  ⌋⇔ = equivalence
⌊ left-inverse ⌋⇔ = left-inverse
⌊ surjection   ⌋⇔ = surjection
⌊ bijection    ⌋⇔ = bijection

-- The functions.

⇒⇔ : ∀ {k x y} {X : Set x} {Y : Set y} →
     X ∼[ ⌊ k ⌋⇔ ] Y → X ∼[ equivalence ] Y
⇒⇔ {equivalence}  = id
⇒⇔ {left-inverse} = LeftInverse.equivalence
⇒⇔ {surjection}   = Surjection.equivalence
⇒⇔ {bijection}    = Inverse.equivalence

-- Conversions between special kinds.

⇔⌊_⌋ : Symmetric-kind → Equivalence-kind
⇔⌊ equivalence ⌋ = equivalence
⇔⌊ bijection   ⌋ = bijection

→⌊_⌋ : Equivalence-kind → Forward-kind
→⌊ equivalence  ⌋ = equivalence
→⌊ left-inverse ⌋ = left-inverse
→⌊ surjection   ⌋ = surjection
→⌊ bijection    ⌋ = bijection

←⌊_⌋ : Equivalence-kind → Backward-kind
←⌊ equivalence  ⌋ = equivalence
←⌊ left-inverse ⌋ = left-inverse
←⌊ surjection   ⌋ = surjection
←⌊ bijection    ⌋ = bijection

------------------------------------------------------------------------
-- Opposites

-- For every kind there is an opposite kind.

_op : Kind → Kind
implication         op = reverse-implication
reverse-implication op = implication
equivalence         op = equivalence
injection           op = reverse-injection
reverse-injection   op = injection
left-inverse        op = surjection
surjection          op = left-inverse
bijection           op = bijection

-- For every morphism there is a corresponding reverse morphism of the
-- opposite kind.

reverse : ∀ {k a b} {A : Set a} {B : Set b} →
          A ∼[ k ] B → B ∼[ k op ] A
reverse {implication}         = lam
reverse {reverse-implication} = app-←
reverse {equivalence}         = Eq.sym
reverse {injection}           = lam
reverse {reverse-injection}   = app-↢
reverse {left-inverse}        = Surj.fromRightInverse
reverse {surjection}          = Surjection.right-inverse
reverse {bijection}           = Inv.sym

------------------------------------------------------------------------
-- For a fixed universe level every kind is a preorder and each
-- symmetric kind is an equivalence

K-refl : ∀ {k ℓ} → Reflexive (Related k {ℓ})
K-refl {implication}         = id
K-refl {reverse-implication} = lam id
K-refl {equivalence}         = Eq.id
K-refl {injection}           = Inj.id
K-refl {reverse-injection}   = lam Inj.id
K-refl {left-inverse}        = LeftInv.id
K-refl {surjection}          = Surj.id
K-refl {bijection}           = Inv.id

K-reflexive : ∀ {k ℓ} → _≡_ ⇒ Related k {ℓ}
K-reflexive P.refl = K-refl

K-trans : ∀ {k ℓ₁ ℓ₂ ℓ₃} → Trans (Related k {ℓ₁} {ℓ₂})
                                (Related k {ℓ₂} {ℓ₃})
                                (Related k {ℓ₁} {ℓ₃})
K-trans {implication}         = flip _∘′_
K-trans {reverse-implication} = λ f g → lam (app-← f ∘ app-← g)
K-trans {equivalence}         = flip Eq._∘_
K-trans {injection}           = flip Inj._∘_
K-trans {reverse-injection}   = λ f g → lam (Inj._∘_ (app-↢ f) (app-↢ g))
K-trans {left-inverse}        = flip LeftInv._∘_
K-trans {surjection}          = flip Surj._∘_
K-trans {bijection}           = flip Inv._∘_

SK-sym : ∀ {k ℓ₁ ℓ₂} → Sym (Related ⌊ k ⌋ {ℓ₁} {ℓ₂})
                          (Related ⌊ k ⌋ {ℓ₂} {ℓ₁})
SK-sym {equivalence} = Eq.sym
SK-sym {bijection}   = Inv.sym

SK-isEquivalence : ∀ k ℓ → IsEquivalence {ℓ = ℓ} (Related ⌊ k ⌋)
SK-isEquivalence k ℓ = record
  { refl  = K-refl
  ; sym   = SK-sym
  ; trans = K-trans
  }

SK-setoid : Symmetric-kind → (ℓ : Level) → Setoid _ _
SK-setoid k ℓ = record { isEquivalence = SK-isEquivalence k ℓ }

K-isPreorder : ∀ k ℓ → IsPreorder _↔_ (Related k)
K-isPreorder k ℓ = record
    { isEquivalence = SK-isEquivalence bijection ℓ
    ; reflexive     = ↔⇒
    ; trans         = K-trans
    }

K-preorder : Kind → (ℓ : Level) → Preorder _ _ _
K-preorder k ℓ = record { isPreorder = K-isPreorder k ℓ }

------------------------------------------------------------------------
-- Equational reasoning

-- Equational reasoning for related things.

module EquationalReasoning where

  infix  3 _∎
  infixr 2 _∼⟨_⟩_ _↔⟨_⟩_ _↔⟨⟩_ _≡⟨_⟩_

  _∼⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
           X ∼[ k ] Y → Y ∼[ k ] Z → X ∼[ k ] Z
  _ ∼⟨ X↝Y ⟩ Y↝Z = K-trans X↝Y Y↝Z

  -- Isomorphisms can be combined with any other kind of relatedness.

  _↔⟨_⟩_ : ∀ {k x y z} (X : Set x) {Y : Set y} {Z : Set z} →
           X ↔ Y → Y ∼[ k ] Z → X ∼[ k ] Z
  X ↔⟨ X↔Y ⟩ Y⇔Z = X ∼⟨ ↔⇒ X↔Y ⟩ Y⇔Z

  _↔⟨⟩_ : ∀ {k x y} (X : Set x) {Y : Set y} →
          X ∼[ k ] Y → X ∼[ k ] Y
  X ↔⟨⟩ X⇔Y = X⇔Y

  _≡⟨_⟩_ : ∀ {k ℓ z} (X : Set ℓ) {Y : Set ℓ} {Z : Set z} →
           X ≡ Y → Y ∼[ k ] Z → X ∼[ k ] Z
  X ≡⟨ X≡Y ⟩ Y⇔Z = X ∼⟨ ≡⇒ X≡Y ⟩ Y⇔Z

  _∎ : ∀ {k x} (X : Set x) → X ∼[ k ] X
  X ∎ = K-refl

  sym = SK-sym
  {-# WARNING_ON_USAGE sym
  "Warning: EquationalReasoning.sym was deprecated in v0.17.
  Please use SK-sym instead."
  #-}

------------------------------------------------------------------------
-- Every unary relation induces a preorder and, for symmetric kinds,
-- an equivalence. (No claim is made that these relations are unique.)

InducedRelation₁ : Kind → ∀ {a s} {A : Set a} →
                   (A → Set s) → A → A → Set _
InducedRelation₁ k S = λ x y → S x ∼[ k ] S y

InducedPreorder₁ : Kind → ∀ {a s} {A : Set a} →
                   (A → Set s) → Preorder _ _ _
InducedPreorder₁ k S = record
  { _≈_        = _≡_
  ; _∼_        = InducedRelation₁ k S
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = reflexive ∘
                      K-reflexive ∘
                      P.cong S
    ; trans         = K-trans
    }
  } where open Preorder (K-preorder _ _)

InducedEquivalence₁ : Symmetric-kind → ∀ {a s} {A : Set a} →
                      (A → Set s) → Setoid _ _
InducedEquivalence₁ k S = record
  { _≈_           = InducedRelation₁ ⌊ k ⌋ S
  ; isEquivalence = record
    { refl  = K-refl
    ; sym   = SK-sym
    ; trans = K-trans
    }
  }

------------------------------------------------------------------------
-- Every binary relation induces a preorder and, for symmetric kinds,
-- an equivalence. (No claim is made that these relations are unique.)

InducedRelation₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                   (A → B → Set s) → B → B → Set _
InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y)

InducedPreorder₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                   (A → B → Set s) → Preorder _ _ _
InducedPreorder₂ k _S_ = record
  { _≈_        = _≡_
  ; _∼_        = InducedRelation₂ k _S_
  ; isPreorder = record
    { isEquivalence = P.isEquivalence
    ; reflexive     = λ x≡y {z} →
                        reflexive $
                        K-reflexive $
                        P.cong (_S_ z) x≡y

    ; trans         = λ i↝j j↝k → K-trans i↝j j↝k
    }
  } where open Preorder (K-preorder _ _)

InducedEquivalence₂ : Symmetric-kind →
                      ∀ {a b s} {A : Set a} {B : Set b} →
                      (A → B → Set s) → Setoid _ _
InducedEquivalence₂ k _S_ = record
  { _≈_           = InducedRelation₂ ⌊ k ⌋ _S_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = λ i↝j → sym i↝j
    ; trans = λ i↝j j↝k → trans i↝j j↝k
    }
  } where open Setoid (SK-setoid _ _)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

preorder = K-preorder
{-# WARNING_ON_USAGE preorder
"Warning: preorder was deprecated in v0.17.
Please use K-preorder instead."
#-}
setoid = SK-setoid
{-# WARNING_ON_USAGE setoid
"Warning: setoid was deprecated in v0.17.
Please use SK-setoid instead."
#-}


text:
{-

An experiment of transporting rev-++-distr from lists to lists where
the arguments to cons have been flipped inspired by section 2 of
https://arxiv.org/abs/2010.00774

Note that Agda doesn't care about the order of constructors so we
can't do exactly the same example.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Experiments.List where

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

open import Cubical.Data.Sigma

infixr 5 _∷_
infixl 5 _∷'_
infixr 5 _++_

-- Normal lists
data List (A : Type) : Type where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

-- Lists where the arguments to cons have been flipped
data List' (A : Type) : Type where
  []  : List' A
  _∷'_ : (xs : List' A) (x : A) → List' A

variable
  A : Type

-- Some operations and properties for List

_++_ : List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

rev : List A → List A
rev [] = []
rev (x ∷ xs) = rev xs ++ (x ∷ [])

++-unit-r : (xs : List A) → xs ++ [] ≡ xs
++-unit-r [] = refl
++-unit-r (x ∷ xs) = cong (_∷_ x) (++-unit-r xs)

++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

rev-++-distr : (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
rev-++-distr [] ys       = sym (++-unit-r (rev ys))
rev-++-distr (x ∷ xs) ys = cong (_++ _) (rev-++-distr xs ys) ∙ ++-assoc (rev ys) (rev xs) (x ∷ [])

-- We now want to transport this to List'. For this we first establish
-- an isomorphism of the types.

toList' : List A → List' A
toList' []       = []
toList' (x ∷ xs) = toList' xs ∷' x

fromList' : List' A → List A
fromList' []        = []
fromList' (xs ∷' x) =  x ∷ fromList' xs

toFrom : (xs : List' A) → toList' (fromList' xs) ≡ xs
toFrom []          = refl
toFrom (xs ∷' x) i = toFrom xs i ∷' x

fromTo : (xs : List A) → fromList' (toList' xs) ≡ xs
fromTo []          = refl
fromTo (x ∷ xs) i =  x ∷ fromTo xs i

ListIso : Iso (List A) (List' A)
ListIso = iso toList' fromList' toFrom fromTo

ListEquiv : List A ≃ List' A
ListEquiv = isoToEquiv ListIso

-- We then use univalence to turn this into a path
ListPath : (A : Type) → List A ≡ List' A
ListPath A = isoToPath (ListIso {A = A})

-- We can now use this path to transport the operations and properties
-- from List to List'
module transport where

  -- First make a suitable Σ-type packaging what we need for the
  -- transport (note that _++_ and rev here are part of the Σ-type).
  -- It should be possible to automatically generate this given a module/file.
  T : Type → Type
  T X = Σ[ _++_ ∈ (X → X → X) ] Σ[ rev ∈ (X → X) ] ((xs ys : X) → rev (xs ++ ys) ≡ rev ys ++ rev xs)

  -- We can now transport the instance of T for List to List'
  T-List' : T (List' A)
  T-List' {A = A} = transport (λ i → T (ListPath A i)) (_++_ , rev , rev-++-distr)

  -- Getting the operations and property for List' is then just a matter of projecting them out
  _++'_ : List' A → List' A → List' A
  _++'_ = T-List' .fst

  rev' : List' A → List' A
  rev' = T-List' .snd .fst

  rev-++-distr' : (xs ys : List' A) → rev' (xs ++' ys) ≡ rev' ys ++' rev' xs
  rev-++-distr' = T-List' .snd .snd

-- To connect this with the Cubical Agda paper consider the following
-- (painfully) manual transport. This is really what the above code
-- unfolds to.
module manualtransport where

  _++'_ : List' A → List' A → List' A
  _++'_ {A = A} = transport (λ i → ListPath A i → ListPath A i → ListPath A i) _++_

  rev' : List' A → List' A
  rev' {A = A} = transport (λ i → ListPath A i → ListPath A i) rev

  rev-++-distr' : (xs ys : List' A) → rev' (xs ++' ys) ≡ rev' ys ++' rev' xs
  rev-++-distr' {A = A} = transport (λ i → (xs ys : ListPath A i)
                                         → revP i (appP i xs ys) ≡ appP i (revP i ys) (revP i xs))
                                    rev-++-distr
    where
    appP : PathP (λ i → ListPath A i → ListPath A i → ListPath A i) _++_ _++'_
    appP i = transp (λ j → ListPath A (i ∧ j) → ListPath A (i ∧ j) → ListPath A (i ∧ j)) (~ i) _++_

    revP : PathP (λ i → ListPath A i → ListPath A i) rev rev'
    revP i = transp (λ j → ListPath A (i ∧ j) → ListPath A (i ∧ j)) (~ i) rev

-- The above operations for List' are derived by going back and
-- forth. With the SIP we can do better and transport properties for
-- user defined operations (assuming that the operations are
-- well-defined wrt to the forward direction of the equivalence).
open import Cubical.Foundations.SIP
open import Cubical.Structures.Axioms
open import Cubical.Structures.Product
open import Cubical.Structures.Pointed
open import Cubical.Structures.Function

-- For illustrative purposes we first apply the SIP manually. This
-- requires quite a bit of boilerplate code which is automated in the
-- next module.
module manualSIP (A : Type) where

  -- First define the raw structure without axioms. This is just the
  -- signature of _++_ and rev.
  RawStruct : Type → Type
  RawStruct X = (X → X → X) × (X → X)

  -- Some boilerplate code which can be automated
  e1 : StrEquiv (λ x → x → x → x) ℓ-zero
  e1 = FunctionEquivStr+ pointedEquivAction
                         (FunctionEquivStr+ pointedEquivAction PointedEquivStr)

  e2 : StrEquiv (λ x → x → x) ℓ-zero
  e2 = FunctionEquivStr+ pointedEquivAction PointedEquivStr

  RawEquivStr : StrEquiv RawStruct _
  RawEquivStr = ProductEquivStr e1 e2

  rawUnivalentStr : UnivalentStr _ RawEquivStr
  rawUnivalentStr = productUnivalentStr e1 he1 e2 he2
    where
    he2 : UnivalentStr (λ z → z → z) e2
    he2 = functionUnivalentStr+ pointedEquivAction pointedTransportStr
                                PointedEquivStr pointedUnivalentStr

    he1 : UnivalentStr (λ z → z → z → z) e1
    he1 = functionUnivalentStr+ pointedEquivAction pointedTransportStr e2 he2

  -- Now the property that we want to transport
  P : (X : Type) → RawStruct X → Type
  P X (_++_ , rev) = ((xs ys : X) → rev (xs ++ ys) ≡ rev ys ++ rev xs)

  -- Package things up for List
  List-Struct : Σ[ X ∈ Type ] (Σ[ s ∈ RawStruct X ] (P X s))
  List-Struct = List A , (_++_ , rev) , rev-++-distr

  -- We now give direct definitions of ++' and rev' for List'
  _++'_ : List' A → List' A → List' A
  [] ++' ys        = ys
  (xs ∷' x) ++' ys = (xs ++' ys) ∷' x

  rev' : List' A → List' A
  rev' [] = []
  rev' (xs ∷' x) = rev' xs ++' ([] ∷' x)

  -- We then package this up into a raw structure on List'
  List'-RawStruct : Σ[ X ∈ Type ] (RawStruct X)
  List'-RawStruct = List' A , (_++'_ , rev')

  -- Finally we prove that toList' commutes with _++_ and rev. Note
  -- that this could be a lot more complex, see for example the Matrix
  -- example (Cubical.Algebra.Matrix).
  toList'-++ : (xs ys : List A) → toList' (xs ++ ys) ≡ toList' xs ++' toList' ys
  toList'-++ [] ys = refl
  toList'-++ (x ∷ xs) ys i = toList'-++ xs ys i ∷' x

  toList'-rev : (xs : List A) → toList' (rev xs) ≡ rev' (toList' xs)
  toList'-rev [] = refl
  toList'-rev (x ∷ xs) = toList'-++ (rev xs) (x ∷ []) ∙ cong (_++' ([] ∷' x)) (toList'-rev xs)

  -- We can now get the property for ++' and rev' via the SIP
  rev-++-distr' : (xs ys : List' A) → rev' (xs ++' ys) ≡ rev' ys ++' rev' xs
  rev-++-distr' = transferAxioms rawUnivalentStr List-Struct List'-RawStruct
                        (ListEquiv , toList'-++ , toList'-rev)

  -- Note that rev-++-distr' is really talking about the direct
  -- definitions of ++' and rev', not the transported operations as in
  -- the previous attempt.

-- We now automate parts of the above construction
open import Cubical.Structures.Auto

module SIP-auto (A : Type) where

  -- First define the raw structure without axioms. This is just the
  -- signature of _++_ and rev.
  RawStruct : Type → Type
  RawStruct X = (X → X → X) × (X → X)

  -- Some automated SIP magic
  RawEquivStr : _
  RawEquivStr = AutoEquivStr RawStruct

  rawUnivalentStr : UnivalentStr _ RawEquivStr
  rawUnivalentStr = autoUnivalentStr RawStruct

  -- Now the property that we want to transport
  P : (X : Type) → RawStruct X → Type
  P X (_++_ , rev) = ((xs ys : X) → rev (xs ++ ys) ≡ rev ys ++ rev xs)

  -- Package things up for List
  List-Struct : Σ[ X ∈ Type ] (Σ[ s ∈ RawStruct X ] (P X s))
  List-Struct = List A , (_++_ , rev) , rev-++-distr

  -- We now give direct definitions of ++' and rev' for List'
  _++'_ : List' A → List' A → List' A
  [] ++' ys        = ys
  (xs ∷' x) ++' ys = (xs ++' ys) ∷' x

  rev' : List' A → List' A
  rev' [] = []
  rev' (xs ∷' x) = rev' xs ++' ([] ∷' x)

  -- We then package this up into a raw structure on List'
  List'-RawStruct : Σ[ X ∈ Type ] (RawStruct X)
  List'-RawStruct = List' A , (_++'_ , rev')

  -- Finally we prove that toList' commutes with _++_ and rev. Note
  -- that this could be a lot more complex, see for example the Matrix
  -- example (Cubical.Algebra.Matrix).
  toList'-++ : (xs ys : List A) → toList' (xs ++ ys) ≡ toList' xs ++' toList' ys
  toList'-++ [] ys = refl
  toList'-++ (x ∷ xs) ys i = toList'-++ xs ys i ∷' x

  toList'-rev : (xs : List A) → toList' (rev xs) ≡ rev' (toList' xs)
  toList'-rev [] = refl
  toList'-rev (x ∷ xs) = toList'-++ (rev xs) (x ∷ []) ∙ cong (_++' ([] ∷' x)) (toList'-rev xs)

  -- We can now get the property for ++' and rev' via the SIP
  rev-++-distr' : (xs ys : List' A) → rev' (xs ++' ys) ≡ rev' ys ++' rev' xs
  rev-++-distr' = transferAxioms rawUnivalentStr List-Struct List'-RawStruct
                        (ListEquiv , toList'-++ , toList'-rev)

  -- Note that rev-++-distr' is really talking about the direct
  -- definitions of ++' and rev', not the transported operations as in
  -- the previous attempt.


text:
-- {-# OPTIONS -v tc.meta:100 #-}
-- Andreas, 2011-04-20
-- see Abel Pientka TLCA 2011
module PruningNonMillerPattern where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

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

-- bad variable y in head position
test : let X : Nat -> Nat -> Nat
           X = _
           Y : Nat -> Nat -> Nat
           Y = _
       in  (C : Set) ->
           (({x y : Nat} -> X x x ≡ suc (Y x y)) ->
            ({x y : Nat} -> Y x x ≡ x)           ->
            ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
test C k = k refl refl refl
{- none of these equations is immediately solvable.  However,
   from 1. we deduce that Y does not depend on its second argument, thus
   from 2. we solve Y x y = x, and then
   eqn. 3. simplifies to X x y = X x x, thus, X does not depend on its second arg,
   we can then solve using 1.  X x y = suc x
-}

-- a variant, where pruning is even triggered from a non-pattern
test' : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat -> Nat -> Nat
            Y = _
        in  (C : Set) ->
            (({x y : Nat} -> X x (suc x) ≡ suc (Y x y)) ->  -- non-pattern lhs
             ({x y : Nat} -> Y x x ≡ x)           ->
             ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
test' C k = k refl refl refl

-- another variant, where the pruned argument does not have an offending
-- variable in the head, but in a non-eliminateable position
-- (argument to a datatype)

data Sing {A : Set} : A → Set where
  sing : (x : A) -> Sing x

-- bad rigid under a data type constructor
test2 : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat → Set -> Nat
            Y = _
        in  (C : Set) ->
            (({x y : Nat} -> X x x ≡ suc (Y x (Sing (suc y)))) ->
             ({x y : Nat} -> Y x (Sing x) ≡ x)           ->
             ({x y : Nat} -> X (Y x (Sing y)) y ≡ X x x) -> C) -> C
test2 C k = k refl refl refl

T : Nat → Set
T zero    = Nat
T (suc _) = Nat → Nat

-- bad rigid y under a Pi type constructor
test3 : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat → Set -> Nat
            Y = _
        in  (C : Set) ->
            (({x y : Nat} -> X x x ≡ suc (Y x (T y -> T y))) ->
             ({x y : Nat} -> Y x (Sing x) ≡ x)           ->
             ({x y : Nat} -> X (Y x (Sing y)) y ≡ X x x) -> C) -> C
test3 C k = k refl refl refl

-- bad rigid y in head position under a lambda
test4 : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat → (Nat → Nat) -> Nat
            Y = _
        in  (C : Set) ->
            ((∀ {x : Nat} {y : Nat → Nat} -> X x x ≡ suc (Y x (λ k → y zero))) ->
             (∀ {x : Nat} {y : Nat → Nat} -> Y x (λ k → y zero) ≡ x)           ->
             (∀ {x : Nat} {y : Nat } -> X (Y x (λ k → y)) y ≡ X x x) -> C) -> C
test4 C k = k refl refl refl

-- bad variable in irrelevant position
test5 : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat -> .Nat -> Nat
            Y = _
        in  (C : Set) ->
            (({x y : Nat} -> X x (suc x) ≡ suc (Y x (suc y))) ->  -- non-pattern lhs
             ({x y : Nat} -> Y x x ≡ x)           ->
             ({x y : Nat} -> X (Y x (suc y)) y ≡ X x x) -> C) -> C
test5 C k = k refl refl refl

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module BTree.Equality.Properties {A : Set} where

open import BTree {A}
open import BTree.Equality {A}
open import Relation.Binary.Core

trans≃ : Transitive _≃_
trans≃ ≃lf ≃lf = ≃lf
trans≃ (≃nd x x' l≃r l≃l' l'≃r') (≃nd .x' x'' _ l'≃l'' l''≃r'') = ≃nd x x'' l≃r (trans≃ l≃l' l'≃l'')  l''≃r''

symm≃ : Symmetric _≃_
symm≃ ≃lf = ≃lf
symm≃ (≃nd x x' l≃r l≃l' l'≃r') = ≃nd x' x l'≃r' (symm≃ l≃l') l≃r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Cubical.Algebra.Ring.Base public
open import Cubical.Algebra.Ring.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical