text:
{-# OPTIONS --postfix-projections #-}
{-# OPTIONS --allow-unsolved-metas #-}

module StateSizedIO.writingOOsUsingIOVers4ReaderMethods where

open import StateSizedIO.RObject
open import StateSizedIO.Object
open import StateSizedIO.Base
open import Data.Product
open import Data.Nat
open import Data.Fin
open import Data.Bool
open import Function
open import Data.Unit
open import Data.String
open import Unit
open import Data.Bool.Base
open import Relation.Binary.PropositionalEquality
open import SizedIO.Console
open import Size
open import SizedIO.Base
open import Data.Sum
open import Data.Empty

-- ### new imports
--
open import StateSizedIO.cellStateDependent using (CellInterfaceˢ; empty; cellPempty')
open import NativeIO

objectInterfToIOInterfˢ : RInterfaceˢ → IOInterfaceˢ
objectInterfToIOInterfˢ I .IOStateˢ = I .Stateˢ
objectInterfToIOInterfˢ I .Commandˢ s = I .Methodˢ s ⊎ I .RMethodˢ s
objectInterfToIOInterfˢ I .Responseˢ s (inj₁ c) = I .Resultˢ s c
objectInterfToIOInterfˢ I .Responseˢ s (inj₂ c) = I .RResultˢ s c -- I .Resultˢ
objectInterfToIOInterfˢ I .IOnextˢ s (inj₁ c) r = I .nextˢ s c r
objectInterfToIOInterfˢ I .IOnextˢ s (inj₂ c) r = s -- I .nextˢ

ioInterfToObjectInterfˢ : IOInterfaceˢ → RInterfaceˢ
ioInterfToObjectInterfˢ I .Stateˢ = I .IOStateˢ
ioInterfToObjectInterfˢ I .Methodˢ = I .Commandˢ
ioInterfToObjectInterfˢ I .Resultˢ = I .Responseˢ --
ioInterfToObjectInterfˢ I .nextˢ = I .IOnextˢ
ioInterfToObjectInterfˢ I .RMethodˢ s = ⊥
ioInterfToObjectInterfˢ I .RResultˢ s ()

data DecSets : Set where
  fin : ℕ → DecSets

TDecSets : DecSets → Set
TDecSets (fin n) = Fin n

toDecSets : ∀{n} → (x : Fin n) → DecSets
toDecSets x = fin (toℕ x)

_==fin_ : {n : ℕ} → Fin n → Fin n → Bool
_==fin_ {zero} () t
_==fin_ {suc _} zero zero = true
_==fin_ {suc _} zero (suc _) = false
_==fin_ {suc _} (suc _) zero = false
_==fin_ {suc _} (suc s) (suc t) = s ==fin t

transferFin : {n : ℕ} → (P : Fin n → Set) →
              (i j : Fin n) → T (i ==fin j) →
              P i → P j
transferFin {zero} P () j q p
transferFin {suc n} P zero zero q p = p
transferFin {suc n} P zero (suc j) () p
transferFin {suc n} P (suc i) zero () p
transferFin {suc n} P (suc i) (suc j) q p = transferFin {n} (P ∘ suc) i j q p

_==DecSets_ : {d : DecSets} → TDecSets d → TDecSets d  → Bool
_==DecSets_ {fin n} = _==fin_

transferFin' : {n : ℕ} → (P : Fin n → Set) →
              (i j : Fin n) → ((i ==fin j) ≡ true) →
              P i → P j
transferFin' {zero} P () j q p
transferFin' {suc n} P zero zero q p = p
transferFin' {suc n} P zero (suc j) () p
transferFin' {suc n} P (suc i) zero () p
transferFin' {suc n} P (suc i) (suc j) q p = transferFin' {n} (P ∘ suc) i j q p

transferDecSets : {J : DecSets} → (P : TDecSets J → Set) →
              (i j : TDecSets J) → ((i ==DecSets j) ≡ true) →
              P i → P j
transferDecSets {(fin n)} P i j q p = transferFin' {n} P i j q p

{-
transferDec : {J : DecSets} → (P : TDecSets J  → Set) →
              (i j : TDecSets) → ((i ==DecSets j) ≡ true) →
              P i → P j
-}

--with {!!} inspect {!!} --(_==DecSets_ j j')
--... | x = {!!}

{-
... | true = {!!} -- {!(I j).nextˢ (f j) m ?!}
... | false = {!!}
-}

{-
    = if (j ==DecSets j') then  else {!!}
-}

module _ (I : IOInterfaceˢ )
         (let S = IOStateˢ I) (let C = Commandˢ I)
         (let R = Responseˢ I) (let n = IOnextˢ I)
           where

  mutual

-- \writingOOsUsingIOVersFourReaderMethodsIOind
    data IOˢind (A : S → Set) (s : S) : Set where
      doˢ''      :  (c : C s) (f : (r : R s c) → IOˢind A (n s c r)) → IOˢind A s
      returnˢ''  :  (a : A s) → IOˢind A s

    IOˢindₚ : (A : Set)(s s' : S) → Set
    IOˢindₚ A s s' = IOˢind (λ s'' → (s'' ≡ s) × A) s

module _ {I : RInterfaceˢ } (let S = Stateˢ I) (let n = nextˢ I)
           where

-- \writingOOsUsingIOVersFourReaderMethodstranslateIOind
  translateˢ : {A : S → Set} (s : S) (obj : RObjectˢ I s) (p : IOˢind (objectInterfToIOInterfˢ I) A s)
               → Σ[ s′ ∈ S ]  (A s′ × RObjectˢ I s′)
  translateˢ s obj (returnˢ'' x)       =  s , (x , obj)
  translateˢ s obj (doˢ'' (inj₁ c) p)  = obj .objectMethod c ▹ λ {(x , o′) → translateˢ (n s c x) o′ (p x)  }
  translateˢ s obj (doˢ'' (inj₂ c) p)  = obj .readerMethod c ▹ λ x → translateˢ s obj (p x)
-- obj .objectMethod c ▹ λ {(x , o′)
--                                      → translateˢ {A} {n s c x} o′ (p x)  }

module _ {I : RInterfaceˢ }   (let S = Stateˢ I)
           where

  getAˢ : ∀{A : S → Set} (s : S)
               → RObjectˢ I s
               → IOˢind (objectInterfToIOInterfˢ I) A s
               → Σ[ s′ ∈ S ]  A s′
  getAˢ s obj (returnˢ'' x) =  s , x
  getAˢ s obj p             =  let  res = translateˢ s obj p
                               in   proj₁ res , proj₁ (proj₂ res)

module _ (I : IOInterfaceˢ )
         (let S = IOStateˢ I) (let C = Commandˢ I)
         (let R = Responseˢ I) (let n = IOnextˢ I)
           where

  mutual
    -- IOˢind' A sbegin send
    -- are programs which start in state sbegin and end in state send

    data IOˢind' (A : S → Set) (sbegin : S) : (send : S) → Set where

      doˢ'''     : {send : S} → (c : C sbegin)  →
                   (f : (r : R sbegin c) → IOˢind' A (n sbegin c r) send)
                  → IOˢind' A sbegin send
      returnˢ''' : (a : A sbegin) → IOˢind' A sbegin sbegin

module _ {I : RInterfaceˢ } (let S = Stateˢ I) (let n = nextˢ I)
           where

  translateˢ' : ∀{A : S → Set}{sbegin : S}{send : S}
               → RObjectˢ I sbegin
               → IOˢind' (objectInterfToIOInterfˢ I) A sbegin send
               → (A send × RObjectˢ I send)
  translateˢ' {A} {sbegin} {send} obj (returnˢ''' x) = x , obj
  translateˢ' {A} {sbegin} {send} obj (doˢ''' (inj₁ c) p) =
                   obj .objectMethod c ▹ λ {(x , o')
                   → translateˢ' {A} {n sbegin c x} {send} o' (p x)  }
  translateˢ' {A} {sbegin} {send} obj (doˢ''' (inj₂ c) p) =
                   obj .readerMethod c ▹ λ x
                   → translateˢ' {A} {sbegin} {send} obj (p x)

--                   obj .objectMethod c ▹ λ {(x , o')
--                   → translateˢ' {A} {n sbegin c x} {send} o' (p x)  }

module _ {I : RInterfaceˢ }   (let S = Stateˢ I)
           where

  getAˢ' : ∀{A : S → Set}{sbegin : S}{send : S}
               → RObjectˢ I sbegin
               → IOˢind' (objectInterfToIOInterfˢ I) A sbegin send
               → A send
  getAˢ' {A} {sbegin} {send} obj (returnˢ''' x) = x
  getAˢ' {A} {sbegin} {send} obj p = let res = translateˢ' {I} {A} {sbegin} {send} obj p
                        in proj₁ res

updateFinFunction : {n : ℕ} → (P : Fin n → Set)
                    → (f : (k : Fin n) → P k)
                    → (l : Fin n)
                    → (b : P l)
                    → (k : Fin n) → P k
updateFinFunction {zero} P f () b k
updateFinFunction {suc n} P f zero b zero = b
updateFinFunction {suc n} P f zero b (suc k) = f (suc k)
updateFinFunction {suc n} P f (suc l) b zero = f zero
updateFinFunction {suc n} P f (suc l) b (suc k) = updateFinFunction {n} (P ∘ suc)  (f ∘ suc) l b k

updateDecSetsFunction : {J : DecSets} → (P : TDecSets J → Set)
                    → (f : (k : TDecSets J) → P k)
                    → (l : TDecSets J)
                    → (b : P l)
                    → (k : TDecSets J) → P k
updateDecSetsFunction {fin n} P f l b k = updateFinFunction {n} P f l b k

updateFinFunctionStateChange : {n : ℕ}
                    → (P : Fin n → Set)
                    → (f : (k : Fin n) → P k)
                    → (Q : (k : Fin n) → P k → Set)
                    → (g : (k : Fin n) → Q k (f k) )
                    → (l : Fin n)
                    → (newP : P l)
                    → (newQ : Q l newP)
                    → (k : Fin n)
                    → Q k (updateFinFunction {n} P f l newP k)
updateFinFunctionStateChange {zero} P f Q g () newP newQ k
updateFinFunctionStateChange {suc n} P f Q g zero newP newQ zero = newQ
updateFinFunctionStateChange {suc n} P f Q g zero newP newQ (suc k) = g (suc k)
updateFinFunctionStateChange {suc n} P f Q g (suc l) newP newQ zero = g zero
updateFinFunctionStateChange {suc n} P f Q g (suc l) newP newQ (suc k) =
   updateFinFunctionStateChange {n} (P ∘ suc) (f ∘ suc)
                                (λ k p → Q (suc k) p)
                                (g ∘ suc) l newP newQ k

updateDecSetsFunctionStateChange : {J : DecSets}
                    → (P : TDecSets J → Set)
                    → (f : (k : TDecSets J) → P k)
                    → (Q : (k : TDecSets J) → P k → Set)
                    → (g : (k : TDecSets J) → Q k (f k) )
                    → (l : TDecSets J)
                    → (newP : P l)
                    → (newQ : Q l newP)
                    → (k : TDecSets J)
                    → Q k (updateDecSetsFunction {J} P f l newP k)
updateDecSetsFunctionStateChange {fin n} P f Q g l newP newQ k = updateFinFunctionStateChange {n} P f Q g l newP newQ k

objectInterfMultiToIOInterfˢ : (J : DecSets) → (TDecSets J → Interfaceˢ) → IOInterfaceˢ
objectInterfMultiToIOInterfˢ J I .IOStateˢ = (j : TDecSets J) →  (I j).Stateˢ
objectInterfMultiToIOInterfˢ J I .Commandˢ f  = Σ[ j ∈ TDecSets J ] (I j).Methodˢ (f j)
objectInterfMultiToIOInterfˢ J I .Responseˢ f (j , m) = (I j).Resultˢ (f j) m
objectInterfMultiToIOInterfˢ J I .IOnextˢ f (j , m) r =
   updateDecSetsFunction {J} (λ j₁ → I j₁ .Stateˢ) f j (I j .nextˢ (f j) m r)

{-
objectInterfMultiToIOInterfˢ J I .IOnextˢ f (j , m) r j' with (_==DecSets_ j j') | inspect (_==DecSets_ j) j'
... | true | [ eq ] = transferDecSets {J} (λ j'' → I j'' .Stateˢ) j j' eq ((I j).nextˢ (f j) m r)
... | false | [ eq ] = f j'
-}

translateMultiˢ : (J : DecSets) → (I : TDecSets J → Interfaceˢ) →
            (A : ((j : TDecSets J) →  (I j).Stateˢ) → Set)
            (f : (j : TDecSets J) →  (I j).Stateˢ)
            (obj : (j : TDecSets J) →  Objectˢ (I j) (f j))
             → IOˢind (objectInterfMultiToIOInterfˢ J I) A f
             → Σ[ s' ∈ ((j : TDecSets J) →  (I j).Stateˢ) ]
                (A s' × ( (j : TDecSets J) → Objectˢ (I j) (s' j)))
translateMultiˢ J I A f obj (doˢ'' (j , m) p) = (obj j) .objectMethod m ▹ λ {(r , o')
     → translateMultiˢ J I A (IOnextˢ (objectInterfMultiToIOInterfˢ J I) f (j , m) r)
        (updateDecSetsFunctionStateChange {J}
          (λ j₁ → I j₁ .Stateˢ)
          f
          (λ j₁ state → Objectˢ (I j₁) state)
          obj j
          (I j .nextˢ (f j) m r) o')
          (p r)}
translateMultiˢ J I A f obj (returnˢ'' a) = f , a , obj

module _ (I₁ : IOInterfaceˢ )
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         (I₂ : IOInterfaceˢ )
         (let S₂ = IOStateˢ I₂)
         (let C₂ = Commandˢ I₂)
         (let R₂ = Responseˢ I₂)
         (let n₂ = IOnextˢ I₂)
           where

  mutual

    record  IOˢindcoind (i : Size)(A : S₁ → S₂ → Set) (s₁ : S₁)(s₂ : S₂) : Set where
      coinductive
      field
            forceIC : {j : Size< i} → IOˢindcoind+ j A s₁ s₂

    data IOˢindcoind+ (i : Size)(A : S₁ → S₂ → Set) (s₁ : S₁)(s₂ : S₂) : Set where
       doˢIO      :  (c₁ : C₁ s₁) (f : (r₁ : R₁ s₁ c₁) → IOˢindcoind i A (n₁ s₁ c₁ r₁) s₂)
                     → IOˢindcoind+ i A s₁ s₂
       doˢobj     :  (c₂ : C₂ s₂)(f : (r₂ : R₂ s₂ c₂) → IOˢindcoind+ i A s₁ (n₂ s₂ c₂ r₂))
                     → IOˢindcoind+ i A s₁ s₂
       returnˢic  :  A s₁ s₂
                     → IOˢindcoind+ i A s₁ s₂
open IOˢindcoind public

module _ (I₁ : IOInterfaceˢ )
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         (I₂ : IOInterfaceˢ )
         (let S₂ = IOStateˢ I₂)
         (let C₂ = Commandˢ I₂)
         (let R₂ = Responseˢ I₂)
         (let n₂ = IOnextˢ I₂) where

  ioˢind2IOˢindcoind+ : (A : S₁ → S₂ → Set) (s₁ : S₁)(s₂ : S₂)
                        (p : IOˢind I₂ (λ s₂' → A s₁ s₂') s₂)
                        → IOˢindcoind+ I₁ I₂ ∞ A s₁ s₂
  ioˢind2IOˢindcoind+ A s₁ s₂ (doˢ'' c f) = doˢobj c λ r →
                                            ioˢind2IOˢindcoind+ A s₁ (IOnextˢ I₂ s₂ c r) (f r)
  ioˢind2IOˢindcoind+ A s₁ s₂ (returnˢ'' a) = returnˢic a

  ioˢind2IOˢindcoind : (A : S₁ → S₂ → Set) (s₁ : S₁)(s₂ : S₂)
                        (p : IOˢind I₂ (λ s₂' → A s₁ s₂') s₂)
                        → IOˢindcoind I₁ I₂ ∞ A s₁ s₂

  ioˢind2IOˢindcoind A s₁ s₂ p .forceIC = ioˢind2IOˢindcoind+ A s₁ s₂ p

{-
    translateˢ : ∀{A : S → Set}{s : S}
                 → Objectˢ I s
                 → IOˢindcoind+ (objectInterfToIOInterfˢ I) A s
                 → Σ[ s' ∈ S ]  (A s' × Objectˢ I s')
    translateˢ {A} {s} obj (returnˢ'' x) = s , (x , obj)
    translateˢ {A} {s} obj (doˢobj c p) = obj .objectMethod c ▹ λ {(x , o')
                                        → translateˢ {A} {n s c x} o' (p x)  }
-}

{-
  delayˢic : {i : Size}{A : S₁ → S₂ → Set}{s₁ : S₁}{s₂ : S₂}
           → IOˢindcoindShape i A s₁ s₂
           → IOˢindcoind (↑ i) A s₁ s₂
  delayˢic {i} {A} {s₁} {s₂} P .IOˢindcoind.forceIC {j} = P
-}

module _ {I : IOInterfaceˢ } (let S = IOStateˢ I)
           where
   _>>=ind_ : {A :  S → Set}{B : S → Set}{s : S}
              (m : IOˢind I A s)
              (f : (s' : S) (a : A s') → IOˢind I B s')
              → IOˢind I B s
   _>>=ind_  (doˢ'' c f₁) f = doˢ'' c (λ r → f₁ r >>=ind f)
   _>>=ind_  {s = s} (returnˢ'' a) f = f s a

module _ {I₁ : IOInterfaceˢ }
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         {I₂ : IOInterfaceˢ }
         (let S₂ = IOStateˢ I₂)
         (let C₂ = Commandˢ I₂)
         (let R₂ = Responseˢ I₂)
         (let n₂ = IOnextˢ I₂)
           where
   mutual
     _>>=indcoind+_ : {i : Size}{A : S₁ → S₂ → Set}
                      {B : S₁ → S₂ → Set}
                      {s₁ : S₁}{s₂ : S₂}
                      (p : IOˢindcoind+ I₁ I₂ i A s₁ s₂)
                      (f : {s₁' : S₁}{s₂' : S₂}(a : A s₁' s₂') → IOˢindcoind+ I₁ I₂ i B s₁' s₂')
                      → IOˢindcoind+ I₁ I₂ i B s₁ s₂
     doˢobj c f₁ >>=indcoind+ f = doˢobj c (λ r → f₁ r >>=indcoind+ f)
     doˢIO c f₁  >>=indcoind+ f = doˢIO c  (λ r → f₁ r >>=indcoind f)
     returnˢic x >>=indcoind+ f = f x

{-
     _>>=indcoindShape_ : {i : Size}{A : S₁ → S₂ → Set}
                      {B : S₁ → S₂ → Set}
                      {s₁ : S₁}{s₂ : S₂}
                      (p : IOˢindcoindShape I₁ I₂ i A s₁ s₂)
                      (f : (s₁' : S₁)(s₂' : S₂)(a : A s₁' s₂') → IOˢindcoind+ I₁ I₂ i B s₁' s₂')
                      → IOˢindcoind+ I₁ I₂ i B s₁ s₂
     doˢIO c₁ f₁ >>=indcoindShape f = returnˢ'' (doˢIO c₁ (λ r → f₁ r >>=indcoind f))
     _>>=indcoindShape_ {s₁ = s₁} {s₂ = s₂} (returnˢic x) f = x >>=indcoindaux' f
-}
     _>>=indcoind_ : {i : Size}{A : S₁ → S₂ → Set}
                      {B : S₁ → S₂ → Set}
                      {s₁ : S₁}{s₂ : S₂}
                      (p : IOˢindcoind I₁ I₂ i A s₁ s₂)
                      (f : {s₁' : S₁}{s₂' : S₂}(a : A s₁' s₂') → IOˢindcoind+ I₁ I₂ i B s₁' s₂')
                      → IOˢindcoind I₁ I₂ i B s₁ s₂
     (p >>=indcoind f) .forceIC {j} = p .forceIC >>=indcoind+ f

{-
     _>>=indcoindaux'_ : {i : Size}{A : S₁ → S₂ → Set}
                      {B : S₁ → S₂ → Set}
                      {s₁ : S₁}{s₂ : S₂}
                      (p : IOˢ' I₁ i (λ s₁' → A s₁' s₂) s₁)
                      (f : {s₁' : S₁}{s₂' : S₂}(a : A s₁' s₂') → IOˢindcoind+ I₁ I₂ i B s₁' s₂')
                      → IOˢindcoind+ I₁ I₂ i B s₁ s₂
     doˢ' c f₁ >>=indcoindaux' f = {!!} -- returnˢ'' (returnˢic (doˢ' c λ r → {!returnˢic!})) -- doˢ' c λ r → f₁ r >>=indcoindaux f
     _>>=indcoindaux'_ {s₁ = s₁}{s₂ = s₂} (returnˢ' a)  f = f {s₁} {s₂} a -- doˢobj {!inj₂ c!} {!!}
-}

{-
     _>>=indcoindaux_ : {i : Size}{A : S₁ → S₂ → Set}
                      {B : S₁ → S₂ → Set}
                      {s₁ : S₁}{s₂ : S₂}
                      (p : IOˢ I₁ i (λ s₁' → A s₁' s₂) s₁)
                      (f : (s₁' : S₁)(s₂' : S₂)(a : A s₁' s₂') → IOˢindcoind+ I₁ I₂ i B s₁' s₂')
                      → IOˢindcoind+ I₁ I₂ i B s₁ s₂
     p >>=indcoindaux f = {!!}
-}

module _ {I₁ : IOInterfaceˢ }
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         {I₂ : IOInterfaceˢ }
         (let S₂ = IOStateˢ I₂)
           where
  open IOˢindcoind

  delayˢic : {i : Size}{A : S₁ → S₂ → Set}{s₁ : S₁}{s₂ : S₂}
           → IOˢindcoind+ I₁ I₂ i A s₁ s₂
           → IOˢindcoind I₁ I₂ (↑ i) A s₁ s₂
  delayˢic {i} {A} {s₁} {s₂} P .forceIC {j} = P

--Σ (Stateˢ I₂) (λ s₄ → Σ (A s₃ s₄) (λ x → Objectˢ I₂ s₄))) s₁

--→ IOˢind I₂ (λ s₂ → A s₁ s₂) s₂

open IOˢindcoind public

module _ (I₁ : IOInterfaceˢ )
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         (I₂ : RInterfaceˢ )
         (let I₂′ = objectInterfToIOInterfˢ I₂)
         (let S₂ = Stateˢ I₂)(let n₂ = IOnextˢ I₂′)
           where
  mutual
    translateˢIndCoind : ∀ {i A s₁ s₂} (obj : RObjectˢ I₂ s₂) (p : IOˢindcoind I₁ I₂′ i A s₁ s₂)
                       → IOˢ I₁ i (λ s₁ → Σ[ s₂ ∈ S₂ ] (A s₁ s₂ × RObjectˢ I₂ s₂)) s₁
    translateˢIndCoind obj p .forceˢ = translateˢIndCoind+ obj (p .forceIC)

    translateˢIndCoind+ : ∀{i A s₁ s₂} (obj : RObjectˢ  I₂ s₂) (p : IOˢindcoind+ I₁ I₂′ i A s₁ s₂)
                          → IOˢ' I₁ i (λ s₁ → Σ[ s₂ ∈ S₂ ] (A s₁ s₂ × RObjectˢ I₂ s₂)) s₁
    translateˢIndCoind+ obj (doˢobj (inj₁ c) f) = obj .objectMethod c ▹ λ { (x , obj′) →
      translateˢIndCoind+ obj′ (f x)}
    translateˢIndCoind+ obj (doˢobj (inj₂ c) f) = obj .readerMethod c ▹ λ x  →
      translateˢIndCoind+ obj (f x)
    translateˢIndCoind+ obj (doˢIO c₁ f) = doˢ' c₁ λ r₁ →
      translateˢIndCoind obj (f r₁)
    translateˢIndCoind+ {i} {A} {s₁} {s₂} obj (returnˢic a) = returnˢ' (s₂ , a , obj)
{-
    translateˢIndCoindShape : ∀{i} → {A : S₁ → S₂ → Set}{s₁ : S₁}{s₂ : S₂}
                 → RObjectˢ  I₂ s₂
                 → IOˢindcoindShape I₁ I₂′ i A s₁ s₂
                 → IOˢ' I₁ i ((λ s₁ → Σ[ s₂ ∈ S₂ ]  (A s₁ s₂ × RObjectˢ I₂ s₂))) s₁
    translateˢIndCoindShape {i} {A} {.s₁} {.s₂} obj (doˢIO {s₁} {s₂} c₁ p)
           = doˢ' c₁ (λ r₁ → translateˢIndCoind {i} {A} {n₁ s₁ c₁ r₁} {s₂} obj (p r₁))
    translateˢIndCoindShape {i} {A} {.s₁} {.s₂} obj (returnˢic {s₁} {s₂} p)
           = fmapˢ' i (λ s a → ( s₂ , a , obj)) s₁ p
-}

---
--- ### file content of writingOOsUsingIO
---

{-
objectInterfMultiToIOInterfˢ J I .IOnextˢ f (j , m) r j' with (_==DecSets_ j j') | inspect (_==DecSets_ j) j'
... | true | [ eq ] = transferDecSets {J} (λ j'' → I j'' .Stateˢ) j j' eq ((I j).nextˢ (f j) m r)
... | false | [ eq ] = f j'
-}

module _ (I₁ : IOInterfaceˢ )
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         (I₂ : IOInterfaceˢ )
         (let S₂ = IOStateˢ I₂)
           where

unsizedIOInterfToIOInterfˢ : IOInterface → IOInterfaceˢ
unsizedIOInterfToIOInterfˢ x .IOStateˢ  = Unit
unsizedIOInterfToIOInterfˢ x .Commandˢ  = λ _ → x .Command
unsizedIOInterfToIOInterfˢ x .Responseˢ = λ _ → x .Response
unsizedIOInterfToIOInterfˢ x .IOnextˢ   _ _ _ =  unit

ConsoleInterfaceˢ : IOInterfaceˢ
ConsoleInterfaceˢ = unsizedIOInterfToIOInterfˢ consoleI

data RCellStateˢ  : Set where
  empty full  : RCellStateˢ

data RCellMethodEmpty (A : Set) : Set where
    put : A → RCellMethodEmpty A

data RCellMethodFull (A : Set)  : Set where
    put : A → RCellMethodFull A

data RRCellMethodEmpty (A : Set) : Set where

data RRCellMethodFull (A : Set)  : Set where
    get : RRCellMethodFull A

RCellMethodˢ : (A : Set) → RCellStateˢ → Set
RCellMethodˢ A empty = RCellMethodEmpty A
RCellMethodˢ A full = RCellMethodFull A

RRCellMethodˢ : (A : Set) → RCellStateˢ → Set
RRCellMethodˢ A empty = RRCellMethodEmpty A
RRCellMethodˢ A full = RRCellMethodFull A

putGen : {A : Set} → {i : RCellStateˢ} → A → RCellMethodˢ A i
putGen {A} {empty} = put
putGen {A} {full} = put

RCellResultFull : ∀{A} → RCellMethodFull A → Set
RCellResultFull (put _) = Unit

RCellResultEmpty : ∀{A} → RCellMethodEmpty A → Set
RCellResultEmpty (put _) = Unit

RRCellResultFull : ∀{A} → RRCellMethodFull A → Set
RRCellResultFull {A} get = A

RRCellResultEmpty : ∀{A} → RRCellMethodEmpty A → Set
RRCellResultEmpty ()

RCellResultˢ : (A : Set) → (s : RCellStateˢ) → RCellMethodˢ A s → Set
RCellResultˢ A empty = RCellResultEmpty{A}
RCellResultˢ A full = RCellResultFull{A}

RRCellResultˢ : (A : Set) → (s : RCellStateˢ) → RRCellMethodˢ A s → Set
RRCellResultˢ A empty = RRCellResultEmpty{A}
RRCellResultˢ A full = RRCellResultFull{A}

nˢ : ∀{A} → (s : RCellStateˢ) → (c : RCellMethodˢ A s) → (RCellResultˢ A s c) → RCellStateˢ
nˢ _ _ _ = full

RCellInterfaceˢ : (A : Set) → RInterfaceˢ
Stateˢ (RCellInterfaceˢ A)  = RCellStateˢ
Methodˢ (RCellInterfaceˢ A)  = RCellMethodˢ A
Resultˢ (RCellInterfaceˢ A)  = RCellResultˢ A
RMethodˢ (RCellInterfaceˢ A)  = RRCellMethodˢ A
RResultˢ (RCellInterfaceˢ A)  = RRCellResultˢ A
nextˢ (RCellInterfaceˢ A)  = nˢ

{-
mutual
   RcellPempty : (i : Size) → IOObject consoleI (RCellInterfaceˢ String) i empty
   method (cellPempty i) {j} (put str) = do (putStrLn ("put (" ++ str ++ ")")) λ _ →
                                         return (unit , cellPfull j str)

   cellPfull : (i : Size) → (str : String) → IOObject consoleI (CellInterfaceˢ String) i full
   method (cellPfull i str) {j} get        = do (putStrLn ("get (" ++ str ++ ")")) λ _ →
                                             return (str , cellPfull j str)
   method (cellPfull i str) {j} (put str') = do (putStrLn ("put (" ++ str' ++ ")")) λ _ →
                                             return (unit , cellPfull j str')
-}

-- UNSIZED Version, without IO
mutual
   RcellPempty' : ∀{A} → RObjectˢ (RCellInterfaceˢ A) empty
   RcellPempty' .objectMethod (put a)     =  (_ , RcellPfull' a)
   RcellPempty' .readerMethod ()

   RcellPfull' : ∀{A} → A → RObjectˢ (RCellInterfaceˢ A) full
   RcellPfull' a .readerMethod get         = a
   RcellPfull' a .objectMethod (put a')  = (_ , RcellPfull' a')

RCellInterfaceˢIO : IOInterfaceˢ
RCellInterfaceˢIO = objectInterfToIOInterfˢ (RCellInterfaceˢ String)

module _ (I : IOInterface)
       (let C = I .Command)
       (let R = I .Response)
       (let I' = unsizedIOInterfToIOInterfˢ I)
       (let C' = I' .Commandˢ)
       (let R' = I' .Responseˢ)
       (convertC : C' _ → C)
       (convertR : ∀{c : C} → Response I (convertC c)  →  I .Response c)

       where
  mutual

    flatternIOˢ : ∀ {A : Set}
                 → IOˢ (unsizedIOInterfToIOInterfˢ I) ∞ (λ _ → A) unit
                 → IO I ∞ A
    flatternIOˢ {A} p .force  = flatternIOˢ' (forceˢ p)

    flatternIOˢ' : {A : Set}
                 → IOˢ' (unsizedIOInterfToIOInterfˢ I) ∞ (λ _ → A) unit
                 → IO' I ∞ A
    flatternIOˢ' {A} (doˢ' cˢ f) = do' (convertC cˢ) (λ rˢ →
                    flatternIOˢ (f (convertR {cˢ} rˢ)))
    flatternIOˢ' {A} (returnˢ' a) = return' a

{-
doIOShape : {i : Size}
       {I₁ :  IOInterfaceˢ} {I₂ :  IOInterfaceˢ}
       {A : I₁ .IOStateˢ → I₂ .IOStateˢ → Set}
       {s₁ : I₁ .IOStateˢ}
       {s₂ : I₂ .IOStateˢ}
      (c₁ : I₁ .Commandˢ s₁) →
         ((r₁ : I₁ .Responseˢ s₁ c₁) →
          IOˢindcoind I₁ I₂ i  A (IOnextˢ I₁ s₁ c₁ r₁) s₂)
        →  IOˢindcoindShape I₁ I₂ i A  s₁ s₂
doIOShape  = doˢIO
-}

{-
callMethod'' : {I₂ :  IOInterfaceˢ}
             {A : I₂ .IOStateˢ → Set}
             {s₂ : I₂ .IOStateˢ}
             (c : Commandˢ I₂ s₂) →
             ((r : Responseˢ I₂ s₂ c) → IOˢind I₂ A (IOnextˢ I₂ s₂ c r))
             → IOˢind I₂ A s₂
callMethod'' = doˢobj
-}

doˢobj∞ : {I₁ : IOInterfaceˢ }{I₂ :  IOInterfaceˢ}
             {A : IOStateˢ I₁ → I₂ .IOStateˢ → Set}
             {s₁ : IOStateˢ I₁}
             {s₂ : I₂ .IOStateˢ}
             (c : Commandˢ I₂ s₂) →
             ((r : Responseˢ I₂ s₂ c) → IOˢindcoind+ I₁ I₂ ∞ A s₁ (IOnextˢ I₂ s₂ c r) )
             → IOˢindcoind I₁ I₂ ∞ A s₁ s₂
doˢobj∞ {I₁} {I₂} {A} {s₁} {s₂} c f .forceIC {j} = doˢobj c  f

{-
callMethod+ : {I₁ : IOInterfaceˢ }{I₂ :  IOInterfaceˢ}
             {A : IOStateˢ I₁ → I₂ .IOStateˢ → Set}
             {s₁ : IOStateˢ I₁}
             {s₂ : I₂ .IOStateˢ}
             (c : Commandˢ I₂ s₂) →
             ((r : Responseˢ I₂ s₂ c) → IOˢindcoind+ I₁ I₂ ∞ A s₁ (IOnextˢ I₂ s₂ c r) )
             → IOˢindcoind+ I₁ I₂ ∞ A s₁ s₂
callMethod+ {I₁} {I₂} {A} {s₁} {s₂} = doˢobj
-}

{-
we think not needed anymore
endIO : {I₁ :  IOInterfaceˢ} {I₂ :  IOInterfaceˢ}
--      {A : I₁ .IOStateˢ → I₂ .IOStateˢ → Set}
       {s₁ : I₁ .IOStateˢ}
       {s₂ : I₂ .IOStateˢ}
       → IOˢind I₂ (λ s → IOˢindcoind I₁ I₂ ∞ (λ _ _ → Unit) s₁ s) s₂
endIO {I₁} {I₂} {s₁} {s₂} = returnˢ'' (delayˢic (returnˢ'' (returnˢic (returnˢ' unit)))) -- (delayˢic (returnˢic (returnˢ' unit)))
--                returnˢ'' {I₂}
--             {!!} -- (delayˢic {!returnˢ''!} ) -- (returnˢ'' (returnˢic (returnˢ' unit))))   --(returnˢic (returnˢ' unit)))
-}

endIO+ : {I₁ :  IOInterfaceˢ} {I₂ :  IOInterfaceˢ}
       {s₁ : I₁ .IOStateˢ}
       {s₂ : I₂ .IOStateˢ}
       → IOˢindcoind+ I₁ I₂ ∞ (λ _ _ → Unit) s₁ s₂
endIO+ = returnˢic unit

endIO∞ : {I₁ :  IOInterfaceˢ} {I₂ :  IOInterfaceˢ}
       {s₁ : I₁ .IOStateˢ}
       {s₂ : I₂ .IOStateˢ}
       → IOˢindcoind I₁ I₂ ∞ (λ _ _ → Unit) s₁ s₂
endIO∞ .forceIC {j} = endIO+

doˢIO∞ : {i : Size}
        {I₁ :  IOInterfaceˢ} {I₂ :  IOInterfaceˢ}
       {s₁ : I₁ .IOStateˢ}
       {s₂ : I₂ .IOStateˢ}
       (c₁ : I₁ .Commandˢ s₁) →
       ((r₁ : I₁ .Responseˢ s₁ c₁) →
        IOˢindcoind I₁ I₂ i (λ _ _ → Unit) (IOnextˢ I₁ s₁ c₁ r₁) s₂)
       → IOˢindcoind I₁ I₂ i (λ _ _ → Unit) s₁ s₂
doˢIO∞ {i} c p .forceIC {j} = doˢIO c p

callProg : {I : IOInterfaceˢ }{A : I .IOStateˢ → Set}{s : I .IOStateˢ} (a : A s) → IOˢind I A s
callProg = returnˢ''

run' : IOˢindcoind ConsoleInterfaceˢ RCellInterfaceˢIO ∞ (λ x y → Unit)
          unit empty
       → NativeIO Unit
run' prog = translateIOConsole
               (flatternIOˢ  consoleI (λ c → c) (λ r → r)
              (fmapˢ ∞ (λ x y → unit) unit
                (translateˢIndCoind ConsoleInterfaceˢ
                                    (RCellInterfaceˢ String) RcellPempty' (prog))))

module _ {objInf : RInterfaceˢ}
         (let objIOInf = objectInterfToIOInterfˢ objInf)
         {objState : objIOInf .IOStateˢ }
           where
        run_startingWith_ :  IOˢindcoind ConsoleInterfaceˢ objIOInf ∞ (λ x y → Unit) unit objState
                             → RObjectˢ objInf objState → NativeIO Unit
        run prog startingWith obj = translateIOConsole
           (flatternIOˢ  consoleI (λ c → c) (λ r → r) (fmapˢ ∞ (λ x y → unit) unit
                                    (translateˢIndCoind ConsoleInterfaceˢ objInf obj prog)))

        run+_startingWith_ : IOˢindcoind+ ConsoleInterfaceˢ objIOInf ∞ (λ _ _ → Unit) unit objState
              → RObjectˢ objInf objState
              → NativeIO Unit
        run+ prog startingWith obj = translateIOConsole
                         (flatternIOˢ consoleI id id (fmapˢ ∞  (λ _ _ → unit) unit
                              (delayˢ (translateˢIndCoind+ ConsoleInterfaceˢ  objInf obj prog))))
-- (ioInterfToObjectInterfˢ objIOInf)
--- ### END of file content of writingOOsUsingIO
---

{-

obj .objectMethod c ▹ λ {(x , o')
                                      → translateˢ {A} {n s c x} o' (p x)  }

                              let q : Σ[ s' ∈ S₂ ]
                                        (IOˢindcoindShape I₁ I₂′ i A s₁ s'
                                         × Objectˢ I₂ s')
                                  q = translateˢ obj p
                              in translateˢIndCoindShape (proj₂ (proj₂ q)) (proj₁ (proj₂ q)) -}

module _ (I₁ : IOInterfaceˢ )
         (let S₁ = IOStateˢ I₁) (let C₁ = Commandˢ I₁)
         (let R₁ = Responseˢ I₁) (let n₁ = IOnextˢ I₁)
         (I₂ : IOInterfaceˢ )
         (let S₂ = IOStateˢ I₂)
         (let C₂ = Commandˢ I₂)
         (let R₂ = Responseˢ I₂)
         (let n₂ = IOnextˢ I₂)
         (I₂' : IOInterface)
         (let C₂' = I₂' .Command)
         (let R₂' = I₂' .Response)
         (let I₂'' = unsizedIOInterfToIOInterfˢ I₂')
         (let C₂'' = I₂'' .Commandˢ)
         (let R₂'' = I₂'' .Responseˢ)
         (convertC : (s₂ : S₂)(c₂ : C₂ s₂) → C₂')
         (convertR : (s₂ : S₂)(c₂ : C₂ s₂)(r₂ : R₂' (convertC s₂ c₂)) → R₂ s₂ c₂)
         (A : Set)
           where

   mutual
    translateIndCoindFlatteningObj : ∀{i} (s₁ : S₁) (s₂ : S₂)
                                       → IOˢindcoind I₁ I₂ i (λ _ _ →  A) s₁ s₂
                                       → IOˢindcoind I₁ I₂'' i (λ _ _ →  A) s₁ _
    translateIndCoindFlatteningObj {i} s₁ s₂ p .forceIC {j} = translateIndCoindFlatteningObj+ {j} s₁ s₂ (p .forceIC {j})

    translateIndCoindFlatteningObj+ : ∀{i} (s₁ : S₁) (s₂ : S₂)
                                       → IOˢindcoind+ I₁ I₂ i (λ _ _ →  A) s₁ s₂
                                       → IOˢindcoind+ I₁ I₂'' i (λ _ _ →  A) s₁ _
    translateIndCoindFlatteningObj+ {i} s₁ s₂ (doˢIO c₁ f) = doˢIO c₁ λ r₁ → translateIndCoindFlatteningObj (n₁ s₁ c₁ r₁) s₂ (f r₁)
    translateIndCoindFlatteningObj+ {i} s₁ s₂ (doˢobj c₂ f) = doˢobj (convertC s₂ c₂) λ r₂ →
                                                              translateIndCoindFlatteningObj+ s₁ (n₂ s₂ c₂ (convertR s₂ c₂ r₂)) (f (convertR s₂ c₂ r₂))
    translateIndCoindFlatteningObj+ {i} s₁ s₂ (returnˢic x) = returnˢic x

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
module Issue1436-1 where

module A where

  infixl 20 _↑_
  infixl  1 _↓_

  data D : Set where
    ●       : D
    _↓_ _↑_ : D → D → D

module B where

  infix -1000000 _↓_

  data D : Set where
    _↓_ : D → D → D

open A
open B

-- The expression below is not parsed. If the number 20 above is
-- replaced by 19, then it is parsed…

rejected = ● ↑ ● ↓ ● ↑ ● ↓ ● ↑ ●

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2016-07-29, issue #717
-- reported by LarryTheLiquid on 2012-10-28

data Foo (A : Set) : Set where
  foo : Foo A

data Bar : Set where
  bar baz : Foo {!Bar!} → Bar  -- previously, this IP got duplicated internally

fun : (x : Bar) → Foo Bar
fun (bar y) = {!y!} -- WAS: goal is "Set" (incorrect, should be "Foo Bar")
fun (baz z) = {!z!} -- goal is "Foo Bar" (correct)

-- Works now, after fix for #1720!

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category
open import Categories.Category.Complete

module Categories.Category.Complete.Properties.SolutionSet where

open import Level

open import Categories.Functor
open import Categories.Object.Initial
open import Categories.Object.Product.Indexed
open import Categories.Object.Product.Indexed.Properties
open import Categories.Diagram.Equalizer
open import Categories.Diagram.Equalizer.Limit
open import Categories.Diagram.Equalizer.Properties

import Categories.Diagram.Limit as Lim
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    o′ ℓ′ e′ : Level
    J : Category o ℓ e

module _ (C : Category o ℓ e) where
  open Category C

  record SolutionSet : Set (o ⊔ ℓ) where
    field
      D : Obj → Obj
      arr : ∀ X → D X ⇒ X

module _ {C : Category o ℓ e} (Com : Complete (o ⊔ ℓ ⊔ o′) (o ⊔ ℓ ⊔ ℓ′) (o ⊔ ℓ ⊔ e′) C) (S : SolutionSet C) where
  private
    module S = SolutionSet S
    module C = Category C

    open S
    open Category C
    open HomReasoning
    open MR C

    W : IndexedProductOf C D
    W = Complete⇒IndexedProductOf C {o′ = ℓ ⊔ o′} {ℓ′ = ℓ ⊔ ℓ′} {e′ = ℓ ⊔ e′} Com D
    module W = IndexedProductOf W

    W⇒W : Set ℓ
    W⇒W = W.X ⇒ W.X

    Warr : IndexedProductOf C {I = W⇒W} λ _ → W.X
    Warr = Complete⇒IndexedProductOf C {o′ = o ⊔ o′} {ℓ′ = o ⊔ ℓ′} {e′ = o ⊔ e′} Com _
    module Warr = IndexedProductOf Warr

    Δ : W.X ⇒ Warr.X
    Δ = Warr.⟨ (λ _ → C.id) ⟩

    Γ : W.X ⇒ Warr.X
    Γ = Warr.⟨ (λ f → f) ⟩

    equalizer : Equalizer C Δ Γ
    equalizer = complete⇒equalizer C Com Δ Γ
    module equalizer = Equalizer equalizer

    prop : (f : W.X ⇒ W.X) → f ∘ equalizer.arr ≈ equalizer.arr
    prop f = begin
      f ∘ equalizer.arr            ≈˘⟨ pullˡ (Warr.commute _ f) ⟩
      Warr.π f ∘ Γ ∘ equalizer.arr ≈˘⟨ refl⟩∘⟨ equalizer.equality ⟩
      Warr.π f ∘ Δ ∘ equalizer.arr ≈⟨ cancelˡ (Warr.commute _ f) ⟩
      equalizer.arr                ∎

    ! : ∀ A → equalizer.obj ⇒ A
    ! A = arr A ∘ W.π A ∘ equalizer.arr

    module _ {A} (f : equalizer.obj ⇒ A) where

      equalizer′ : Equalizer C (! A) f
      equalizer′ = complete⇒equalizer C Com (! A) f
      module equalizer′ = Equalizer equalizer′

      s : W.X ⇒ equalizer′.obj
      s = arr _ ∘ W.π (equalizer′.obj)

      t : W.X ⇒ W.X
      t = equalizer.arr ∘ equalizer′.arr ∘ s

      t′ : equalizer.obj ⇒ equalizer.obj
      t′ = equalizer′.arr ∘ s ∘ equalizer.arr

      t∘eq≈eq∘1 : equalizer.arr ∘ t′ ≈ equalizer.arr ∘ C.id
      t∘eq≈eq∘1 = begin
        equalizer.arr ∘ t′                                   ≈⟨ refl⟩∘⟨ sym-assoc ⟩
        equalizer.arr ∘ (equalizer′.arr ∘ s) ∘ equalizer.arr ≈⟨ sym-assoc ⟩
        t ∘ equalizer.arr                                    ≈⟨ prop _ ⟩
        equalizer.arr                                        ≈˘⟨ identityʳ ⟩
        equalizer.arr ∘ C.id                                 ∎

      t′≈id : t′ ≈ C.id
      t′≈id = Equalizer⇒Mono C equalizer _ _ t∘eq≈eq∘1

      !-unique : ! A ≈ f
      !-unique = equalizer-≈⇒≈ C equalizer′ t′≈id

  SolutionSet⇒Initial : Initial C
  SolutionSet⇒Initial = record
    { ⊥            = equalizer.obj
    ; ⊥-is-initial = record
      { !        = ! _
      ; !-unique = !-unique
      }
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- examples for termination with tupled arguments

module Tuple where

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

data Pair (A : Set) (B : Set) : Set where
  pair : A -> B -> Pair A B

-- uncurried addition
add : Pair Nat Nat -> Nat
add (pair x (succ y)) = succ (add (pair x y))
add (pair x zero)     = x

data T (A : Set) (B : Set) : Set where
  c1 : A -> B -> T A B
  c2 : A -> B -> T A B

{-
-- constructor names do not matter
add' : T Nat Nat -> Nat
add' (c1 x (succ y)) = succ (add' (c2 x y))
add' (c2 x (succ y)) = succ (add' (c1 x y))
add' (c1 x zero) = x
add' (c2 x zero) = x

-- additionally: permutation of arguments
add'' : T Nat Nat -> Nat
add'' (c1 x (succ y)) = succ (add'' (c2 y x))
add'' (c2 (succ y) x) = succ (add'' (c1 x y))
add'' (c1 x zero) = x
add'' (c2 zero x) = x
-}


text:
-- Andreas, 2016-08-01, issue #2125, qualified names in pragmas

{-# OPTIONS --rewriting #-}

import Common.Equality as Eq

{-# BUILTIN REWRITE Eq._≡_ #-} -- qualified name, should be accepted

postulate
  A : Set
  a b : A

module M where
  open Eq
  postulate
    rule : a ≡ b

{-# REWRITE M.rule #-}  -- qualified name, should be accepted

-- ERROR WAS: in the name M.rule, the part M.rule is not valid
-- NOW: works

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Object.Products

module Categories.Object.Products.N-ary {o ℓ e}
  (C : Category o ℓ e)
  (P : Products C)
  where

open Category C
open Products P
open Equiv

import Categories.Object.Product
open Categories.Object.Product C

import Categories.Object.BinaryProducts
open Categories.Object.BinaryProducts C

import Categories.Object.BinaryProducts.N-ary

import Categories.Object.Terminal
open Categories.Object.Terminal C

open import Data.Nat
open import Data.Vec
open import Data.Vec.Properties
open import Data.Product.N-ary hiding ([])

import Level

open import Relation.Binary.PropositionalEquality as PropEq
  using ()
  renaming (_≡_ to _≣_
           ; refl to ≣-refl
           ; sym  to ≣-sym
           ; cong to ≣-cong
           )

open BinaryProducts binary
module NonEmpty = Categories.Object.BinaryProducts.N-ary C binary
open Terminal terminal

Prod : {n : ℕ} → Vec Obj n → Obj
Prod { zero} [] = ⊤
Prod {suc n} As = NonEmpty.Prod As

-- This whole module is made a great deal more heinous than it should be
-- by the fact that "xs ++ [] ≣ xs" is ill-typed, so I have to repeatedly
-- prove trivial corrolaries of that fact without using it directly.
-- I don't really know how to deal with that in a sane way.

πˡ : {n m : ℕ}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → Prod (As ++ Bs) ⇒ Prod As
πˡ {       zero}      []       Bs  = !
πˡ {      suc n} (A ∷ As) (B ∷ Bs) = NonEmpty.πˡ (A ∷ As) (B ∷ Bs)
πˡ {   suc zero} (A ∷ [])      []  = id
πˡ {suc (suc n)} (A ∷ As)      []  = ⟨ π₁ , πˡ As [] ∘ π₂ ⟩

πʳ : {n m : ℕ}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → Prod (As ++ Bs) ⇒ Prod Bs
πʳ [] Bs = id
πʳ (A ∷ As) (B ∷ Bs) = NonEmpty.πʳ (A ∷ As) (B ∷ Bs)
πʳ As [] = !

glue : {n m : ℕ}{X : Obj}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → (f : X ⇒ Prod As)
  → (g : X ⇒ Prod Bs)
  → X ⇒ Prod (As ++ Bs)
glue {       zero}      []       Bs  f g = g
glue {      suc n} (A ∷ As) (B ∷ Bs) f g = NonEmpty.glue (A ∷ As) (B ∷ Bs) f g
glue {   suc zero} (A ∷ [])      []  f g = f
glue {suc (suc n)} (A ∷ As)      []  f g = ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩

open HomReasoning

.commuteˡ : {n m : ℕ}{X : Obj}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → πˡ As Bs ∘ glue As Bs f g ≡ f
commuteˡ {       zero}      []       Bs  {f}{g} = !-unique₂ (! ∘ g) f
commuteˡ {      suc n} (A ∷ As) (B ∷ Bs) {f}{g} = NonEmpty.commuteˡ (A ∷ As) (B ∷ Bs)
commuteˡ {   suc zero} (A ∷ [])      []  {f}{g} = identityˡ
commuteˡ {suc (suc n)} (A ∷ As)      []  {f}{g} =
  begin
    ⟨ π₁ , πˡ As [] ∘ π₂ ⟩ ∘ ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩∘ ⟩
    ⟨ π₁              ∘ ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
    , (πˡ As [] ∘ π₂) ∘ ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
    ⟩
  ↓⟨ ⟨⟩-congʳ assoc ⟩
    ⟨ π₁            ∘ ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
    , πˡ As [] ∘ π₂ ∘ ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
    ⟩
  ↓⟨ ⟨⟩-cong₂ commute₁ (∘-resp-≡ʳ commute₂) ⟩
    ⟨ π₁ ∘ f , πˡ As [] ∘ glue As [] (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩-congʳ (commuteˡ As []) ⟩
    ⟨ π₁ ∘ f , π₂ ∘ f ⟩
  ↓⟨ g-η ⟩
      f
  ∎

.commuteʳ : {n m : ℕ}{X : Obj}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → πʳ As Bs ∘ glue As Bs f g ≡ g
commuteʳ {       zero}      []       Bs  {f}{g} = identityˡ
commuteʳ {      suc n} (A ∷ As) (B ∷ Bs) {f}{g} = NonEmpty.commuteʳ (A ∷ As) (B ∷ Bs)
commuteʳ {   suc zero} (A ∷ [])      []  {f}{g} = !-unique₂ (! ∘ f) g
commuteʳ {suc (suc n)} (A ∷ As)      []  {f}{g} = !-unique₂ (! ∘ glue (A ∷ As) [] f g) g

.N-universal : {n m : ℕ}{X : Obj}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → {f : X ⇒ Prod As}
  → {g : X ⇒ Prod Bs}
  → {h : X ⇒ Prod (As ++ Bs) }
  → πˡ As Bs ∘ h ≡ f
  → πʳ As Bs ∘ h ≡ g
  → glue As Bs f g ≡ h
N-universal {       zero}      []       Bs  {f}{g}{h} h-commuteˡ h-commuteʳ = trans (sym h-commuteʳ) identityˡ
N-universal {      suc n} (A ∷ As) (B ∷ Bs) {f}{g}{h} h-commuteˡ h-commuteʳ = NonEmpty.N-universal (A ∷ As) (B ∷ Bs) h-commuteˡ h-commuteʳ
N-universal {   suc zero} (A ∷ [])      []  {f}{g}{h} h-commuteˡ h-commuteʳ = trans (sym h-commuteˡ) identityˡ
N-universal {suc (suc n)} (A ∷ As)      []  {f}{g}{h} h-commuteˡ h-commuteʳ =
  begin
    ⟨ π₁ ∘ f , glue As [] (π₂ ∘ f) g ⟩
  ↓⟨ ⟨⟩-congʳ (N-universal As [] π₂∘h-commuteˡ π₂∘h-commuteʳ) ⟩
    ⟨ π₁ ∘ f , π₂ ∘ h ⟩
  ↑⟨ ⟨⟩-congˡ π₁∘h-commuteˡ ⟩
    ⟨ π₁ ∘ h , π₂ ∘ h ⟩
  ↓⟨ g-η ⟩
    h
  ∎

  where
    -- h-commuteˡ : ⟨ π₁ , πˡ As [] ∘ π₂ ⟩ ∘ h ≡ f
    -- h-commuteʳ : (πʳ As [] ∘ π₂) ∘ h ≡ g

    π₁∘h-commuteˡ : π₁ ∘ h ≡ π₁ ∘ f
    π₁∘h-commuteˡ =
      begin
        π₁ ∘ h
      ↑⟨ commute₁ ⟩∘⟨ refl ⟩
        (π₁ ∘ ⟨ π₁ , πˡ As [] ∘ π₂ ⟩) ∘ h
      ↓⟨ assoc ⟩
        π₁ ∘ ⟨ π₁ , πˡ As [] ∘ π₂ ⟩ ∘ h
      ↓⟨ refl ⟩∘⟨ h-commuteˡ ⟩
        π₁ ∘ f
      ∎

    π₂∘h-commuteˡ :  πˡ As [] ∘ π₂ ∘ h ≡ π₂ ∘ f
    π₂∘h-commuteˡ =
      begin
        πˡ As [] ∘ π₂ ∘ h
      ↑⟨ assoc ⟩
        (πˡ As [] ∘ π₂) ∘ h
      ↑⟨ commute₂ ⟩∘⟨ refl ⟩
        (π₂ ∘ ⟨ π₁ , πˡ As [] ∘ π₂ ⟩) ∘ h
      ↓⟨ assoc ⟩
        π₂ ∘ ⟨ π₁ , πˡ As [] ∘ π₂ ⟩ ∘ h
      ↓⟨ refl ⟩∘⟨ h-commuteˡ ⟩
        π₂ ∘ f
      ∎

    π₂∘h-commuteʳ : πʳ As [] ∘ π₂ ∘ h ≡ g
    π₂∘h-commuteʳ = !-unique₂ (πʳ As [] ∘ π₂ ∘ h) g

isProduct : {n m : ℕ}
  → (As : Vec Obj n)
  → (Bs : Vec Obj m)
  → Product (Prod As) (Prod Bs)
isProduct {n}{m} As Bs = record
  { A×B   = Prod (As ++ Bs)
  ; π₁    = πˡ As Bs
  ; π₂    = πʳ As Bs
  ; ⟨_,_⟩ = glue As Bs
  ; commute₁ = commuteˡ As Bs
  ; commute₂ = commuteʳ As Bs
  ; universal = N-universal As Bs
  }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- {-# OPTIONS -v tc.term.args:30 -v tc.meta:50 #-}
module Issue795 where

data Q (A : Set) : Set where

F : (N : Set → Set) → Set₁
F N = (A : Set) → N (Q A) → N A

postulate
   N : Set → Set
   f : F N
   R : (N : Set → Set) → Set
   funny-term : ∀ N → (f : F N) → R N

-- This should work now:  WAS: "Refuse to construct infinite term".
thing : R N
thing = funny-term _ (λ A → f _)
  -- funny-term ?N : F ?N -> R ?N
  -- funny-term ?N : ((A : Set) -> ?N (Q A) -> ?N A) -> R ?N
  -- A : F ?N |- f (?A A) :=> ?N (Q (?A A)) -> ?N (?A A)
  --   |- λ A → f (?A A) <=:  (A : Set) -> N (Q A) -> N A

{- What is happening here?

Agda first creates a (closed) meta variable

  ?N : Set -> Set

Then it checks

  λ A → f ?   against type F ?N = (A : Set) -> ?N (Q A) -> ?N A

(After what it does now, it still needs to check that

  R ?N  is a subtype of R N

It would be smart if that was done first.)

In context A : Set, continues to check

  f ?  against type  ?N (Q A) -> ?N A

Since the type of f is F N = (A : Set) -> N (Q A) -> N A, the created meta,
dependent on A : Set is

  ?A : Set -> Set

and we are left with checking that the inferred type of f (?A A),

  N (Q (?A A)) -> N (?A A)

is a subtype of

  ?N (Q A) -> ?N A

This yields two equations

  ?N (Q A) = N (Q (?A A))

  ?N A     = N (?A A)

The second one is solved as

  ?N = λ z → N (?A z)

simpliying the remaining equation to

  N (?A (Q A)) = N (Q (?A A))

and further to

  ?A (Q A) = Q (?A A)

The expected solution is, of course, the identity, but it cannot be
found mechanically from this equation.

At this point, another solution is ?A = Q.
In general, any power of Q is a solution.

If Agda postponed here, it would come to the problem

  R ?N  =  R N

simplified to ?N = N and instantiated to

  λ z → N (?A z)  =  N

This would solve ?A to be the identity.
-}


text:
module Examples where

open import Prelude
open import Sessions.Syntax

module _ where
  open import Relation.Ternary.Separation.Construct.List Type

  lets : ∀[ Exp a ⇒ (a ∷_) ⊢ Exp b ─✴ Exp b ]
  app (lets e₁) e₂ σ = ap (lam _ e₂ ×⟨ ⊎-comm σ ⟩ e₁)

  -- The example from section 2.1 of the paper
  ex₁ : Exp unit ε
  ex₁ =
    letpair (mkchan (unit ! end) ×⟨ ⊎-idʳ ⟩ (
    lets (fork
      (lam unit
        (letpair (recv (var refl) ×⟨ consʳ (consˡ []) ⟩
          letunit (letunit (var refl ×⟨ ⊎-∙ ⟩ var refl) ×⟨ consʳ ⊎-idʳ ⟩
            (terminate (var refl))))))) $⟨ consʳ (consˡ []) ⟩
    (lets (send (unit ×⟨ ⊎-idˡ ⟩ var refl)) $⟨ ⊎-comm ⊎-∙ ⟩
      letunit (var refl ×⟨ consʳ ⊎-∙ ⟩ terminate (var refl)))))

module _ where
  open import Sessions.Semantics.Expr
  open import Sessions.Semantics.Process as P hiding (main)
  open import Relation.Ternary.Separation.Construct.Market
  open import Relation.Ternary.Separation.Monad.Error

  pool₁ : ∃ λ Φ → Except Exc (● St) Φ
  pool₁ = start 1000 (P.main comp)
    where
      comp = app (runReader nil) (eval 1000 ex₁) ⊎-idˡ

open import IO
open import Data.String.Base using (_++_)
open import Codata.Musical.Notation
open import Debug.Trace
open import Data.Sum
open import Relation.Ternary.Separation.Monad.Error

-- to run the main and see the program trace,
-- run 'make examples'
main = run $ ♯ (putStrLn "Hello, World!")
    >> ♯ (♯ putStrLn result
    >> ♯ putStrLn "done")
  where
  result = case pool₁ of λ where
             (ty , ExceptT.partial (inj₁ e)) → "fail"
             (ty , ExceptT.partial (inj₂ v)) → "ok"


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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)

-- The tensor product of certain monoidal categories is a monoidal functor.

module Categories.Functor.Monoidal.Tensor {o ℓ e} {C : Category o ℓ e}
  {M : Monoidal C} where

open import Data.Product using (_,_)

open import Categories.Category.Product using (Product)
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Category.Monoidal.Construction.Product hiding (⊗)
open import Categories.Category.Monoidal.Interchange
open import Categories.Category.Monoidal.Structure
open import Categories.Morphism using (module ≅)
open import Categories.Functor.Monoidal
import Categories.Functor.Monoidal.Braided as BMF
import Categories.Functor.Monoidal.Symmetric as SMF
open import Categories.NaturalTransformation.NaturalIsomorphism
   using (NaturalIsomorphism)

open NaturalIsomorphism
private
  C-monoidal : MonoidalCategory o ℓ e
  C-monoidal = record { U = C; monoidal = M }

  C×C          = Product C C
  C×C-monoidal = Product-MonoidalCategory C-monoidal C-monoidal

open MonoidalCategory C-monoidal

-- By definition, the tensor product ⊗ of a monoidal category C is a
-- binary functor ⊗ : C × C → C.  The product category C × C of a
-- monoidal category C is again monoidal.  Thus we may ask:
--
--   Is the functor ⊗ a monoidal functor, i.e. does it preserve the
--   monoidal structure in a suitable way (lax or strong)?
--
-- The answer is "yes", provided ⊗ comes equipped with a (coherent)
-- interchange map, aka a "four-middle interchange", which is the case
-- e.g. when C is braided.

module Lax (hasInterchange : HasInterchange M) where
  private module interchange = HasInterchange hasInterchange

  ⊗-isMonoidalFunctor : IsMonoidalFunctor C×C-monoidal C-monoidal ⊗
  ⊗-isMonoidalFunctor = record
    { ε             = unitorˡ.to
    ; ⊗-homo        = F⇒G interchange.naturalIso
    ; associativity = interchange.assoc
    ; unitaryˡ      = interchange.unitˡ
    ; unitaryʳ      = interchange.unitʳ
    }

  ⊗-MonoidalFunctor : MonoidalFunctor C×C-monoidal C-monoidal
  ⊗-MonoidalFunctor = record { F = ⊗ ; isMonoidal = ⊗-isMonoidalFunctor }

module LaxBraided (B : Braided M) where
  open Lax (BraidedInterchange.hasInterchange B) public

module LaxSymmetric (S : Symmetric M) where
  open SymmetricInterchange S
  open Lax hasInterchange public
  open SymmetricMonoidalCategory using ()
    renaming (braidedMonoidalCategory to bmc)
  private
    C-symmetric : SymmetricMonoidalCategory o ℓ e
    C-symmetric = record { symmetric = S }

    C×C-symmetric = Product-SymmetricMonoidalCategory C-symmetric C-symmetric

  open BMF.Lax (bmc C×C-symmetric) (bmc C-symmetric)
  open SMF.Lax C×C-symmetric C-symmetric

  ⊗-isBraidedMonoidalFunctor : IsBraidedMonoidalFunctor ⊗
  ⊗-isBraidedMonoidalFunctor = record
    { isMonoidal      = ⊗-isMonoidalFunctor
    ; braiding-compat = swapInner-braiding′
    }

  ⊗-SymmetricMonoidalFunctor : SymmetricMonoidalFunctor
  ⊗-SymmetricMonoidalFunctor = record
    { isBraidedMonoidal = ⊗-isBraidedMonoidalFunctor }

module Strong (hasInterchange : HasInterchange M) where
  private module interchange = HasInterchange hasInterchange

  ⊗-isMonoidalFunctor : IsStrongMonoidalFunctor C×C-monoidal C-monoidal ⊗
  ⊗-isMonoidalFunctor = record
    { ε             = ≅.sym C unitorˡ
    ; ⊗-homo        = interchange.naturalIso
    ; associativity = interchange.assoc
    ; unitaryˡ      = interchange.unitˡ
    ; unitaryʳ      = interchange.unitʳ
    }

  ⊗-MonoidalFunctor : StrongMonoidalFunctor C×C-monoidal C-monoidal
  ⊗-MonoidalFunctor = record { isStrongMonoidal = ⊗-isMonoidalFunctor }

-- TODO: implement the missing bits in Categories.Category.Monoidal.Interchange.

module StrongBraided (B : Braided M) where
  open Strong (BraidedInterchange.hasInterchange B) public

module StrongSymmetric (S : Symmetric M) where
  open SymmetricInterchange S
  open Strong hasInterchange public
  open SymmetricMonoidalCategory using ()
    renaming (braidedMonoidalCategory to bmc)
  private
    C-symmetric : SymmetricMonoidalCategory o ℓ e
    C-symmetric = record { symmetric = S }

    C×C-symmetric = Product-SymmetricMonoidalCategory C-symmetric C-symmetric

  open BMF.Strong (bmc C×C-symmetric) (bmc C-symmetric)
  open SMF.Strong C×C-symmetric C-symmetric

  ⊗-isBraidedMonoidalFunctor : IsBraidedMonoidalFunctor ⊗
  ⊗-isBraidedMonoidalFunctor = record
    { isStrongMonoidal = ⊗-isMonoidalFunctor
    ; braiding-compat  = swapInner-braiding′
    }

  ⊗-SymmetricMonoidalFunctor : SymmetricMonoidalFunctor
  ⊗-SymmetricMonoidalFunctor = record
    { isBraidedMonoidal = ⊗-isBraidedMonoidalFunctor }

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
{-# OPTIONS --cubical #-}
open import Agda.Builtin.Cubical.Path

data PushOut {A B C : Set} (f : C → A) (g : C → B) : Set where
  inl : A → PushOut f g
  inr : B → PushOut f g
  push : ∀ c → inl (f c) ≡ inr (g c)
  squash : ∀ a b → a ≡ b

data ∥_∥₀ (A : Set) : Set where
  ∣_∣    : A → ∥ A ∥₀
  squash : ∀ (x y : ∥ A ∥₀) → (p q : x ≡ y) → p ≡ q

data Segment : Set where
  start end : Segment
  line      : start ≡ end

-- prop truncation
data ∥_∥ (A : Set) : Set where
  ∣_∣ : A → ∥ A ∥
  squash : ∀ (x y : ∥ A ∥) → x ≡ y

elim : ∀ {A : Set} (P : Set) → ((x y : P) → x ≡ y) → (A → P) → ∥ A ∥ → P
elim P Pprop f ∣ x ∣          = f x
elim P Pprop f (squash x y i) = Pprop (elim P Pprop f x) (elim P Pprop f y) i


text:
-- Andreas, 2014-05-17

open import Common.Prelude
open import Common.Equality

postulate
  bla : ∀ x → x ≡ zero
  P   : Nat → Set
  p   : P zero
  K   : ∀{A B : Set} → A → B → A

f : ∀ x → P x
f x rewrite K {x ≡ x} {Nat} refl {!!} = {!!}

-- Expected: two interaction points!


text:
------------------------------------------------------------------------
-- Equivalences with erased "proofs", defined in terms of partly
-- erased contractible fibres
------------------------------------------------------------------------

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

open import Equality

module Equivalence.Erased.Contractible-preimages
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Prelude

open import Bijection eq using (_↔_)
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Contractible-preimages eq as CP
open import Erased.Level-1 eq as Erased
  hiding (module []-cong; module []-cong₁; module []-cong₂)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_; Split-surjective)

private
  variable
    a b ℓ ℓ₁ ℓ₂      : Level
    A B              : Type a
    c ext k k′ p x y : A
    P                : A → Type p
    f                : (x : A) → P x

------------------------------------------------------------------------
-- Some basic types

-- "Preimages" with erased proofs.

infix 5 _⁻¹ᴱ_

_⁻¹ᴱ_ : {A : Type a} {@0 B : Type b} → @0 (A → B) → @0 B → Type (a ⊔ b)
f ⁻¹ᴱ y = ∃ λ x → Erased (f x ≡ y)

-- Contractibility with an erased proof.

Contractibleᴱ : Type ℓ → Type ℓ
Contractibleᴱ A = ∃ λ (x : A) → Erased (∀ y → x ≡ y)

-- The property of being an equivalence (with erased proofs).

Is-equivalenceᴱ : {A : Type a} {B : Type b} → @0 (A → B) → Type (a ⊔ b)
Is-equivalenceᴱ f = ∀ y → Contractibleᴱ (f ⁻¹ᴱ y)

-- Equivalences with erased proofs.

_≃ᴱ_ : Type a → Type b → Type (a ⊔ b)
A ≃ᴱ B = ∃ λ (f : A → B) → Is-equivalenceᴱ f

------------------------------------------------------------------------
-- Some conversion lemmas

-- Conversions between _⁻¹_ and _⁻¹ᴱ_.

⁻¹→⁻¹ᴱ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} {@0 y : B} →
  f ⁻¹ y → f ⁻¹ᴱ y
⁻¹→⁻¹ᴱ = Σ-map id [_]→

@0 ⁻¹ᴱ→⁻¹ : f ⁻¹ᴱ x → f ⁻¹ x
⁻¹ᴱ→⁻¹ = Σ-map id erased

@0 ⁻¹≃⁻¹ᴱ : f ⁻¹ y ≃ f ⁻¹ᴱ y
⁻¹≃⁻¹ᴱ {f = f} {y = y} =
  (∃ λ x → f x ≡ y)           ↝⟨ (∃-cong λ _ → Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
  (∃ λ x → Erased (f x ≡ y))  □

_ : _≃_.to ⁻¹≃⁻¹ᴱ p ≡ ⁻¹→⁻¹ᴱ p
_ = refl _

@0 _ : _≃_.from ⁻¹≃⁻¹ᴱ p ≡ ⁻¹ᴱ→⁻¹ p
_ = refl _

-- Conversions between Contractible and Contractibleᴱ.

Contractible→Contractibleᴱ :
  {@0 A : Type a} →
  Contractible A → Contractibleᴱ A
Contractible→Contractibleᴱ = Σ-map id [_]→

@0 Contractibleᴱ→Contractible : Contractibleᴱ A → Contractible A
Contractibleᴱ→Contractible = Σ-map id erased

@0 Contractible≃Contractibleᴱ :
  Contractible A ≃ Contractibleᴱ A
Contractible≃Contractibleᴱ =
  (∃ λ x → ∀ y → x ≡ y)           ↝⟨ (∃-cong λ _ → Eq.inverse $ Eq.↔⇒≃ $ erased Erased↔) ⟩□
  (∃ λ x → Erased (∀ y → x ≡ y))  □

_ :
  _≃_.to Contractible≃Contractibleᴱ c ≡ Contractible→Contractibleᴱ c
_ = refl _

@0 _ :
  _≃_.from Contractible≃Contractibleᴱ c ≡ Contractibleᴱ→Contractible c
_ = refl _

-- Conversions between CP.Is-equivalence and Is-equivalenceᴱ.

Is-equivalence→Is-equivalenceᴱ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} →
  CP.Is-equivalence f → Is-equivalenceᴱ f
Is-equivalence→Is-equivalenceᴱ eq y =
    ⁻¹→⁻¹ᴱ (proj₁₀ (eq y))
  , [ cong ⁻¹→⁻¹ᴱ ∘ proj₂ (eq y) ∘ ⁻¹ᴱ→⁻¹ ]

@0 Is-equivalenceᴱ→Is-equivalence :
  Is-equivalenceᴱ f → CP.Is-equivalence f
Is-equivalenceᴱ→Is-equivalence eq y =
    ⁻¹ᴱ→⁻¹ (proj₁ (eq y))
  , cong ⁻¹ᴱ→⁻¹ ∘ erased (proj₂ (eq y)) ∘ ⁻¹→⁻¹ᴱ

private

  -- In an erased context CP.Is-equivalence and Is-equivalenceᴱ are
  -- pointwise equivalent (assuming extensionality).
  --
  -- This lemma is not exported. See Is-equivalence≃Is-equivalenceᴱ
  -- below, which computes in a different way.

  @0 Is-equivalence≃Is-equivalenceᴱ′ :
    {A : Type a} {B : Type b} {f : A → B} →
    CP.Is-equivalence f ↝[ a ⊔ b ∣ a ⊔ b ] Is-equivalenceᴱ f
  Is-equivalence≃Is-equivalenceᴱ′ {a = a} {f = f} {k = k} ext =
    (∀ y → Contractible (f ⁻¹ y))    ↝⟨ (∀-cong ext′ λ _ → H-level-cong ext 0 ⁻¹≃⁻¹ᴱ) ⟩
    (∀ y → Contractible (f ⁻¹ᴱ y))   ↝⟨ (∀-cong ext′ λ _ → from-isomorphism Contractible≃Contractibleᴱ) ⟩□
    (∀ y → Contractibleᴱ (f ⁻¹ᴱ y))  □
    where
    ext′ = lower-extensionality? k a lzero ext

------------------------------------------------------------------------
-- Some type formers are propositional in erased contexts

-- In an erased context Contractibleᴱ is propositional (assuming
-- extensionality).

@0 Contractibleᴱ-propositional :
  {A : Type a} →
  Extensionality a a →
  Is-proposition (Contractibleᴱ A)
Contractibleᴱ-propositional ext =
  H-level.respects-surjection
    (_≃_.surjection Contractible≃Contractibleᴱ)
    1
    (Contractible-propositional ext)

-- In an erased context Is-equivalenceᴱ f is a proposition (assuming
-- extensionality).
--
-- See also Is-equivalenceᴱ-propositional-for-Erased below.

@0 Is-equivalenceᴱ-propositional :
  {A : Type a} {B : Type b} →
  Extensionality (a ⊔ b) (a ⊔ b) →
  (f : A → B) → Is-proposition (Is-equivalenceᴱ f)
Is-equivalenceᴱ-propositional ext f =
  H-level.respects-surjection
    (_≃_.surjection $ Is-equivalence≃Is-equivalenceᴱ′ ext)
    1
    (CP.propositional ext f)

------------------------------------------------------------------------
-- More conversion lemmas

-- In an erased context CP.Is-equivalence and Is-equivalenceᴱ are
-- pointwise equivalent (assuming extensionality).

@0 Is-equivalence≃Is-equivalenceᴱ :
  {A : Type a} {B : Type b} {f : A → B} →
  CP.Is-equivalence f ↝[ a ⊔ b ∣ a ⊔ b ] Is-equivalenceᴱ f
Is-equivalence≃Is-equivalenceᴱ {k = equivalence} ext =
  Eq.with-other-function
    (Eq.with-other-inverse
       (Is-equivalence≃Is-equivalenceᴱ′ ext)
       Is-equivalenceᴱ→Is-equivalence
       (λ _ → CP.propositional ext _ _ _))
    Is-equivalence→Is-equivalenceᴱ
    (λ _ → Is-equivalenceᴱ-propositional ext _ _ _)
Is-equivalence≃Is-equivalenceᴱ = Is-equivalence≃Is-equivalenceᴱ′

_ :
  _≃_.to (Is-equivalence≃Is-equivalenceᴱ ext) p ≡
  Is-equivalence→Is-equivalenceᴱ p
_ = refl _

@0 _ :
  _≃_.from (Is-equivalence≃Is-equivalenceᴱ ext) p ≡
  Is-equivalenceᴱ→Is-equivalence p
_ = refl _

-- Conversions between CP._≃_ and _≃ᴱ_.

≃→≃ᴱ :
  {@0 A : Type a} {@0 B : Type b} →
  A CP.≃ B → A ≃ᴱ B
≃→≃ᴱ = Σ-map id Is-equivalence→Is-equivalenceᴱ

@0 ≃ᴱ→≃ : A ≃ᴱ B → A CP.≃ B
≃ᴱ→≃ = Σ-map id Is-equivalenceᴱ→Is-equivalence

-- In an erased context CP._≃_ and _≃ᴱ_ are pointwise equivalent
-- (assuming extensionality).

@0 ≃≃≃ᴱ :
  {A : Type a} {B : Type b} →
  (A CP.≃ B) ↝[ a ⊔ b ∣ a ⊔ b ] (A ≃ᴱ B)
≃≃≃ᴱ {A = A} {B = B} ext =
  A CP.≃ B                       ↔⟨⟩
  (∃ λ f → CP.Is-equivalence f)  ↝⟨ (∃-cong λ _ → Is-equivalence≃Is-equivalenceᴱ ext) ⟩
  (∃ λ f → Is-equivalenceᴱ f)    ↔⟨⟩
  A ≃ᴱ B                         □

_ : _≃_.to (≃≃≃ᴱ ext) p ≡ ≃→≃ᴱ p
_ = refl _

@0 _ : _≃_.from (≃≃≃ᴱ ext) p ≡ ≃ᴱ→≃ p
_ = refl _

-- An isomorphism relating _⁻¹ᴱ_ to _⁻¹_.

Erased-⁻¹ᴱ↔Erased-⁻¹ :
  {@0 A : Type a} {@0 B : Type b} {@0 f : A → B} {@0 y : B} →
  Erased (f ⁻¹ᴱ y) ↔ Erased (f ⁻¹ y)
Erased-⁻¹ᴱ↔Erased-⁻¹ {f = f} {y = y} =
  Erased (∃ λ x → Erased (f x ≡ y))             ↝⟨ Erased-Σ↔Σ ⟩
  (∃ λ x → Erased (Erased (f (erased x) ≡ y)))  ↝⟨ (∃-cong λ _ → Erased-Erased↔Erased) ⟩
  (∃ λ x → Erased (f (erased x) ≡ y))           ↝⟨ inverse Erased-Σ↔Σ ⟩□
  Erased (∃ λ x → f x ≡ y)                      □

-- An isomorphism relating Contractibleᴱ to Contractible.

Erased-Contractibleᴱ↔Erased-Contractible :
  {@0 A : Type a} →
  Erased (Contractibleᴱ A) ↔ Erased (Contractible A)
Erased-Contractibleᴱ↔Erased-Contractible =
  Erased (∃ λ x → Erased (∀ y → x ≡ y))           ↝⟨ Erased-Σ↔Σ ⟩
  (∃ λ x → Erased (Erased (∀ y → erased x ≡ y)))  ↝⟨ (∃-cong λ _ → Erased-Erased↔Erased) ⟩
  (∃ λ x → Erased (∀ y → erased x ≡ y))           ↝⟨ inverse Erased-Σ↔Σ ⟩□
  Erased (∃ λ x → ∀ y → x ≡ y)                    □

------------------------------------------------------------------------
-- Some results related to Contractibleᴱ

-- Contractibleᴱ respects split surjections with erased proofs.

Contractibleᴱ-respects-surjection :
  {@0 A : Type a} {@0 B : Type b}
  (f : A → B) → @0 Split-surjective f →
  Contractibleᴱ A → Contractibleᴱ B
Contractibleᴱ-respects-surjection {A = A} {B = B} f s h@(x , _) =
    f x
  , [ proj₂ (H-level.respects-surjection surj 0
               (Contractibleᴱ→Contractible h))
    ]
  where
  @0 surj : A ↠ B
  surj = record
    { logical-equivalence = record
      { to   = f
      ; from = proj₁ ∘ s
      }
    ; right-inverse-of = proj₂ ∘ s
    }

-- "Preimages" (with erased proofs) of an erased function with a
-- quasi-inverse with erased proofs are contractible.

Contractibleᴱ-⁻¹ᴱ :
  {@0 A : Type a} {@0 B : Type b}
  (@0 f : A → B)
  (g : B → A)
  (@0 f∘g : ∀ x → f (g x) ≡ x)
  (@0 g∘f : ∀ x → g (f x) ≡ x) →
  ∀ y → Contractibleᴱ (f ⁻¹ᴱ y)
Contractibleᴱ-⁻¹ᴱ {A = A} {B = B} f g f∘g g∘f y =
    (g y , [ proj₂ (proj₁ c′) ])
  , [ cong ⁻¹→⁻¹ᴱ ∘ proj₂ c′ ∘ ⁻¹ᴱ→⁻¹ ]
  where
  @0 A↔B : A ↔ B
  A↔B = record
    { surjection = record
      { logical-equivalence = record
        { to   = f
        ; from = g
        }
      ; right-inverse-of = f∘g
      }
    ; left-inverse-of = g∘f
    }

  @0 c′ : Contractible (f ⁻¹ y)
  c′ = Preimage.bijection⁻¹-contractible A↔B y

-- If an inhabited type comes with an erased proof of
-- propositionality, then it is contractible (with erased proofs).

inhabited→Is-proposition→Contractibleᴱ :
  {@0 A : Type a} →
  A → @0 Is-proposition A → Contractibleᴱ A
inhabited→Is-proposition→Contractibleᴱ x prop = (x , [ prop x ])

-- Some closure properties.

Contractibleᴱ-Σ :
  {@0 A : Type a} {@0 P : A → Type p} →
  Contractibleᴱ A → (∀ x → Contractibleᴱ (P x)) → Contractibleᴱ (Σ A P)
Contractibleᴱ-Σ cA@(a , _) cP =
    (a , proj₁₀ (cP a))
  , [ proj₂ $ Σ-closure 0 (Contractibleᴱ→Contractible cA)
                          (Contractibleᴱ→Contractible ∘ cP)
    ]

Contractibleᴱ-× :
  {@0 A : Type a} {@0 B : Type b} →
  Contractibleᴱ A → Contractibleᴱ B → Contractibleᴱ (A × B)
Contractibleᴱ-× cA cB = Contractibleᴱ-Σ cA (λ _ → cB)

Contractibleᴱ-Π :
  {@0 A : Type a} {@0 P : A → Type p} →
  @0 Extensionality a p →
  (∀ x → Contractibleᴱ (P x)) → Contractibleᴱ ((x : A) → P x)
Contractibleᴱ-Π ext c =
    proj₁₀ ∘ c
  , [ proj₂ $ Π-closure ext 0 (Contractibleᴱ→Contractible ∘ c)
    ]

Contractibleᴱ-↑ :
  {@0 A : Type a} →
  Contractibleᴱ A → Contractibleᴱ (↑ ℓ A)
Contractibleᴱ-↑ c@(a , _) =
    lift a
  , [ proj₂ $ ↑-closure 0 (Contractibleᴱ→Contractible c)
    ]

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for one universe
-- level

module []-cong₁ (ax : []-cong-axiomatisation ℓ) where

  open Erased-cong ax ax
  open Erased.[]-cong₁ ax

  ----------------------------------------------------------------------
  -- Some results related to _⁻¹ᴱ_

  -- The function _⁻¹ᴱ y respects erased extensional equality.

  ⁻¹ᴱ-respects-extensional-equality :
    {@0 B : Type ℓ} {@0 f g : A → B} {@0 y : B} →
    @0 (∀ x → f x ≡ g x) → f ⁻¹ᴱ y ≃ g ⁻¹ᴱ y
  ⁻¹ᴱ-respects-extensional-equality {f = f} {g = g} {y = y} f≡g =
    (∃ λ x → Erased (f x ≡ y))  ↝⟨ (∃-cong λ _ → Erased-cong-≃ (≡⇒↝ _ (cong (_≡ _) $ f≡g _))) ⟩□
    (∃ λ x → Erased (g x ≡ y))  □

  -- An isomorphism relating _⁻¹ᴱ_ to _⁻¹_.

  ⁻¹ᴱ[]↔⁻¹[] :
    {@0 B : Type ℓ} {f : A → Erased B} {@0 y : B} →
    f ⁻¹ᴱ [ y ] ↔ f ⁻¹ [ y ]
  ⁻¹ᴱ[]↔⁻¹[] {f = f} {y = y} =
    (∃ λ x → Erased (f x ≡ [ y ]))       ↔⟨ (∃-cong λ _ → Erased-cong-≃ (Eq.≃-≡ $ Eq.↔⇒≃ $ inverse $ erased Erased↔)) ⟩
    (∃ λ x → Erased (erased (f x) ≡ y))  ↝⟨ (∃-cong λ _ → Erased-≡↔[]≡[]) ⟩□
    (∃ λ x → f x ≡ [ y ])                □

  -- Erased "commutes" with _⁻¹ᴱ_.

  Erased-⁻¹ᴱ :
    {@0 A : Type a} {@0 B : Type ℓ} {@0 f : A → B} {@0 y : B} →
    Erased (f ⁻¹ᴱ y) ↔ map f ⁻¹ᴱ [ y ]
  Erased-⁻¹ᴱ {f = f} {y = y} =
    Erased (f ⁻¹ᴱ y)  ↝⟨ Erased-⁻¹ᴱ↔Erased-⁻¹ ⟩
    Erased (f ⁻¹ y)   ↝⟨ Erased-⁻¹ ⟩
    map f ⁻¹ [ y ]    ↝⟨ inverse ⁻¹ᴱ[]↔⁻¹[] ⟩□
    map f ⁻¹ᴱ [ y ]   □

  ----------------------------------------------------------------------
  -- Some results related to Contractibleᴱ

  -- Erased commutes with Contractibleᴱ.

  Erased-Contractibleᴱ↔Contractibleᴱ-Erased :
    {@0 A : Type ℓ} →
    Erased (Contractibleᴱ A) ↝[ ℓ ∣ ℓ ]ᴱ Contractibleᴱ (Erased A)
  Erased-Contractibleᴱ↔Contractibleᴱ-Erased {A = A} ext =
    Erased (∃ λ x → Erased ((y : A) → x ≡ y))           ↔⟨ Erased-cong-↔ (∃-cong λ _ → erased Erased↔) ⟩
    Erased (∃ λ x → (y : A) → x ≡ y)                    ↔⟨ Erased-Σ↔Σ ⟩
    (∃ λ x → Erased ((y : A) → erased x ≡ y))           ↝⟨ (∃-cong λ _ →
                                                            Erased-cong?
                                                              (λ ext → ∀-cong ext λ _ →
                                                                         from-isomorphism (inverse $ erased Erased↔))
                                                              ext) ⟩
    (∃ λ x → Erased ((y : A) → Erased (erased x ≡ y)))  ↝⟨ (∃-cong λ _ →
                                                            Erased-cong?
                                                              (λ ext → Π-cong ext (inverse $ erased Erased↔) λ _ →
                                                                         from-isomorphism Erased-≡↔[]≡[])
                                                              ext) ⟩□
    (∃ λ x → Erased ((y : Erased A) → x ≡ y))           □

  -- An isomorphism relating Contractibleᴱ to Contractible.

  Contractibleᴱ-Erased↔Contractible-Erased :
    {@0 A : Type ℓ} →
    Contractibleᴱ (Erased A) ↝[ ℓ ∣ ℓ ] Contractible (Erased A)
  Contractibleᴱ-Erased↔Contractible-Erased {A = A} ext =
    Contractibleᴱ (Erased A)  ↝⟨ inverse-erased-ext? Erased-Contractibleᴱ↔Contractibleᴱ-Erased ext ⟩
    Erased (Contractibleᴱ A)  ↔⟨ Erased-Contractibleᴱ↔Erased-Contractible ⟩
    Erased (Contractible A)   ↝⟨ Erased-H-level↔H-level 0 ext ⟩□
    Contractible (Erased A)   □

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for two universe
-- levels

module []-cong₂
  (ax₁ : []-cong-axiomatisation ℓ₁)
  (ax₂ : []-cong-axiomatisation ℓ₂)
  where

  open Erased-cong ax₁ ax₂

  ----------------------------------------------------------------------
  -- A result related to Contractibleᴱ

  -- Contractibleᴱ preserves isomorphisms (assuming extensionality).

  Contractibleᴱ-cong :
    {A : Type ℓ₁} {B : Type ℓ₂} →
    @0 Extensionality? k′ (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
    A ↔[ k ] B → Contractibleᴱ A ↝[ k′ ] Contractibleᴱ B
  Contractibleᴱ-cong {A = A} {B = B} ext A↔B =
    (∃ λ (x : A) → Erased ((y : A) → x ≡ y))  ↝⟨ (Σ-cong A≃B′ λ _ →
                                                  Erased-cong?
                                                    (λ ext → Π-cong ext A≃B′ λ _ →
                                                             from-isomorphism $ inverse $ Eq.≃-≡ A≃B′)
                                                    ext) ⟩□
    (∃ λ (x : B) → Erased ((y : B) → x ≡ y))  □
    where
    A≃B′ = from-isomorphism A↔B

------------------------------------------------------------------------
-- Results that follow if the []-cong axioms hold for all universe
-- levels

module []-cong (ax : ∀ {ℓ} → []-cong-axiomatisation ℓ) where

  private
    open module BC₁ {ℓ} =
      []-cong₁ (ax {ℓ = ℓ})
      public
    open module BC₂ {ℓ₁ ℓ₂} =
      []-cong₂ (ax {ℓ = ℓ₁}) (ax {ℓ = ℓ₂})
      public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------------
-- Testing the translation of the propositional functions
------------------------------------------------------------------------------

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

module PropositionalFunction4 where

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

postulate
  D   : Set
  f   : D → D
  a   : D
  _≡_ : D → D → Set

A : D → Set
A x = f x ≡ f x
{-# ATP definition A #-}

-- In this case the propositional function uses functions.
postulate foo : A a → A a
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical --no-import-sorts --safe --guardedness #-}
module Cubical.DStructures.Experiments where

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

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Maybe

open import Cubical.Relation.Binary

open import Cubical.Structures.Subtype
open import Cubical.Structures.LeftAction

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Semidirect

-- this file also serves as Everything.agda
open import Cubical.DStructures.Base

open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Meta.Isomorphism

open import Cubical.DStructures.Structures.Action
open import Cubical.DStructures.Structures.Category
open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Group
-- open import Cubical.DStructures.Structures.Higher
open import Cubical.DStructures.Structures.Nat
open import Cubical.DStructures.Structures.PeifferGraph
open import Cubical.DStructures.Structures.ReflGraph
open import Cubical.DStructures.Structures.SplitEpi
open import Cubical.DStructures.Structures.Strict2Group
open import Cubical.DStructures.Structures.Type
-- open import Cubical.DStructures.Structures.Universe
open import Cubical.DStructures.Structures.VertComp
open import Cubical.DStructures.Structures.XModule
open import Cubical.DStructures.Equivalences.GroupSplitEpiAction
open import Cubical.DStructures.Equivalences.PreXModReflGraph
open import Cubical.DStructures.Equivalences.XModPeifferGraph
open import Cubical.DStructures.Equivalences.PeifferGraphS2G

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' ℓ≅B' : Level

open Kernel
open GroupHom -- such .fun!
open GroupLemmas
open MorphismLemmas

{-

record Hom-𝒮 {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : URGStr A ℓ≅A)
             {B : Type ℓB} {ℓ≅B : Level} (𝒮-B : URGStr B ℓ≅B)
             : Type (ℓ-max (ℓ-max ℓA ℓB) (ℓ-max ℓ≅A ℓ≅B)) where
  constructor hom-𝒮
  open URGStr
  field
    fun : A → B
    fun-≅ : {a a' : A} → (p : _≅_ 𝒮-A a a') → _≅_ 𝒮-B (fun a) (fun a')
    fun-ρ : {a : A} → fun-≅ (ρ 𝒮-A a) ≡ ρ 𝒮-B (fun a)

∫𝒮ᴰ-π₁ : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
         {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
         → Hom-𝒮 (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) 𝒮-A
Hom-𝒮.fun (∫𝒮ᴰ-π₁ 𝒮ᴰ-B) = fst
Hom-𝒮.fun-≅ (∫𝒮ᴰ-π₁ 𝒮ᴰ-B) = fst
Hom-𝒮.fun-ρ (∫𝒮ᴰ-π₁ 𝒮ᴰ-B) = refl

module _ {ℓ : Level} {A : Type ℓ} (𝒮-A : URGStr A ℓ) where
  𝒮ᴰ-toHom : Iso (Σ[ B ∈ (A → Type ℓ) ] (URGStrᴰ 𝒮-A B ℓ)) (Σ[ B ∈ (Type ℓ) ] Σ[ 𝒮-B ∈ (URGStr B ℓ) ] (Hom-𝒮 𝒮-B 𝒮-A))
  Iso.fun 𝒮ᴰ-toHom (B , 𝒮ᴰ-B) = (Σ[ a ∈ A ] B a) , {!!} , {!!}
  Iso.inv 𝒮ᴰ-toHom (B , 𝒮ᴰ-B , F) = (λ a → Σ[ b ∈ B ] F .fun b ≡ a) , {!!}
    where
      open Hom-𝒮
  Iso.leftInv 𝒮ᴰ-toHom (B , 𝒮ᴰ-B) = ΣPathP ((funExt (λ a → {!!})) , {!!})
  Iso.rightInv 𝒮ᴰ-toHom (B , 𝒮ᴰ-B , F) = {!!}
-}

-- Older Experiments --

-- needs --guardedness flag

module _ where
  record Hierarchy {A : Type ℓ} (𝒮-A : URGStr A ℓ) : Type (ℓ-suc ℓ) where
    coinductive
    field
      B : A → Type ℓ
      𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ
      ℋ : Maybe (Hierarchy {A = Σ A B} (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Issue357 where

module M (X : Set) where

  data R : Set where
    r : X → R

postulate
  P Q : Set
  q   : Q

open M P
open M.R

works : M.R Q
works = M.R.r q

fails : M.R Q
fails = r q


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

open import lib.Basics
open import lib.types.Coproduct
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.PushoutFmap
open import lib.types.Span
open import lib.types.Unit

-- Wedge of two pointed types is defined as a particular case of pushout

module lib.types.Wedge where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  wedge-span : Span
  wedge-span = span (de⊙ X) (de⊙ Y) Unit (λ _ → pt X) (λ _ → pt Y)

  Wedge : Type (lmax i j)
  Wedge = Pushout wedge-span

  infix 80 _∨_
  _∨_ = Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  winl : de⊙ X → X ∨ Y
  winl x = left x

  winr : de⊙ Y → X ∨ Y
  winr y = right y

  wglue : winl (pt X) == winr (pt Y)
  wglue = glue tt

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙Wedge : Ptd (lmax i j)
  ⊙Wedge = ⊙[ Wedge X Y , winl (pt X) ]

  infix 80 _⊙∨_
  _⊙∨_ = ⊙Wedge

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙winl : X ⊙→ X ⊙∨ Y
  ⊙winl = (winl , idp)

  ⊙winr : Y ⊙→ X ⊙∨ Y
  ⊙winr = (winr , ! wglue)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  module WedgeElim {k} {P : X ∨ Y → Type k}
    (inl* : (x : de⊙ X) → P (winl x)) (inr* : (y : de⊙ Y) → P (winr y))
    (glue* : inl* (pt X) == inr* (pt Y) [ P ↓ wglue ]) where

    private
      module M = PushoutElim inl* inr* (λ _ → glue*)

    f = M.f
    glue-β = M.glue-β unit

  open WedgeElim public using () renaming (f to Wedge-elim)

  module WedgeRec {k} {C : Type k} (inl* : de⊙ X → C) (inr* : de⊙ Y → C)
    (glue* : inl* (pt X) == inr* (pt Y)) where

    private
      module M = PushoutRec {d = wedge-span X Y} inl* inr* (λ _ → glue*)

    f = M.f
    glue-β = M.glue-β unit

  open WedgeRec public using () renaming (f to Wedge-rec)

module ⊙WedgeRec {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : X ⊙→ Z) (h : Y ⊙→ Z) where

  open WedgeRec (fst g) (fst h) (snd g ∙ ! (snd h)) public

  ⊙f : X ⊙∨ Y ⊙→ Z
  ⊙f = (f , snd g)

  ⊙winl-β : ⊙f ⊙∘ ⊙winl == g
  ⊙winl-β = idp

  ⊙winr-β : ⊙f ⊙∘ ⊙winr == h
  ⊙winr-β = ⊙λ= (λ _ → idp) $
    ap (_∙ snd g)
       (ap-! f wglue ∙ ap ! glue-β ∙ !-∙ (snd g) (! (snd h)))
    ∙ ∙-assoc (! (! (snd h))) (! (snd g)) (snd g)
    ∙ ap (! (! (snd h)) ∙_) (!-inv-l (snd g))
    ∙ ∙-unit-r (! (! (snd h)))
    ∙ !-! (snd h)

⊙Wedge-rec = ⊙WedgeRec.⊙f

⊙Wedge-rec-post∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (k : Z ⊙→ W) (g : X ⊙→ Z) (h : Y ⊙→ Z)
  → k ⊙∘ ⊙Wedge-rec g h == ⊙Wedge-rec (k ⊙∘ g) (k ⊙∘ h)
⊙Wedge-rec-post∘ k g h = ⊙λ=
  (Wedge-elim (λ _ → idp) (λ _ → idp)
    (↓-='-in' $ ⊙WedgeRec.glue-β (k ⊙∘ g) (k ⊙∘ h)
               ∙ lemma (fst k) (snd g) (snd h) (snd k)
               ∙ ! (ap (ap (fst k)) (⊙WedgeRec.glue-β g h))
               ∙ ∘-ap (fst k) (fst (⊙Wedge-rec g h)) wglue))
  idp
  where
  lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y z : A} {w : B}
    (p : x == z) (q : y == z) (r : f z == w)
    → (ap f p ∙ r) ∙ ! (ap f q ∙ r) == ap f (p ∙ ! q)
  lemma f idp idp idp = idp

⊙Wedge-rec-η : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙Wedge-rec ⊙winl ⊙winr == ⊙idf (X ⊙∨ Y)
⊙Wedge-rec-η = ⊙λ=
  (Wedge-elim (λ _ → idp) (λ _ → idp)
    (↓-='-in' $ ap-idf wglue
               ∙ ! (!-! wglue)
               ∙ ! (⊙WedgeRec.glue-β ⊙winl ⊙winr)))
  idp

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  add-wglue : de⊙ (X ⊙⊔ Y) → X ∨ Y
  add-wglue (inl x) = winl x
  add-wglue (inr y) = winr y

  ⊙add-wglue : X ⊙⊔ Y ⊙→ X ⊙∨ Y
  ⊙add-wglue = add-wglue , idp

module Fold {i} {X : Ptd i} = ⊙WedgeRec (⊙idf X) (⊙idf X)
fold = Fold.f
⊙fold = Fold.⊙f

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  module Projl = ⊙WedgeRec (⊙idf X) (⊙cst {X = Y})
  module Projr = ⊙WedgeRec (⊙cst {X = X}) (⊙idf Y)

  projl = Projl.f
  projr = Projr.f
  ⊙projl = Projl.⊙f
  ⊙projr = Projr.⊙f

module _ {i i' j j'} {X : Ptd i} {X' : Ptd i'} {Y : Ptd j} {Y' : Ptd j'}
  (eqX : X ⊙≃ X') (eqY : Y ⊙≃ Y') where

  wedge-span-emap : SpanEquiv (wedge-span X Y) (wedge-span X' Y')
  wedge-span-emap = ( span-map (fst (fst eqX)) (fst (fst eqY)) (idf _)
                        (comm-sqr λ _ → snd (fst eqX))
                        (comm-sqr λ _ → snd (fst eqY))
                    , snd eqX , snd eqY , idf-is-equiv _)

  ∨-emap : X ∨ Y ≃ X' ∨ Y'
  ∨-emap = Pushout-emap wedge-span-emap

  ⊙∨-emap : X ⊙∨ Y ⊙≃ X' ⊙∨ Y'
  ⊙∨-emap = ≃-to-⊙≃ ∨-emap (ap winl (snd (fst eqX)))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module _ where

infix  -1 _■
infixr -2 step-∼

postulate
  Transitive : {A : Set} (P Q : A → A → Set) → Set

  step-∼ : ∀ {A} {P Q : A → A → Set}
             ⦃ t : Transitive P Q ⦄ x {y z} →
             Q y z → P x y → Q x z

syntax step-∼ x Qyz Pxy = x ∼⟨ Pxy ⟩ Qyz

infix 4 _≈_
postulate
  Proc  : Set
  _≈_   : Proc → Proc → Set
  _■    : ∀ x → x ≈ x
  instance trans : Transitive  _≈_ _≈_

module DummyInstances where

  postulate
    R₁ R₂ R₃ R₄ R₅ : Proc → Proc → Set

  postulate
    instance
      transitive₁₁ : Transitive R₁ R₁
      transitive₁₂ : Transitive R₁ R₂
      transitive₁₃ : Transitive R₁ R₃
      transitive₁₄ : Transitive R₁ R₄
      transitive₁₅ : Transitive R₁ R₅
      transitive₂₁ : Transitive R₂ R₁
      transitive₂₂ : Transitive R₂ R₂
      transitive₂₃ : Transitive R₂ R₃
      transitive₂₄ : Transitive R₂ R₄
      transitive₂₅ : Transitive R₂ R₅
      transitive₃₁ : Transitive R₃ R₁
      transitive₃₂ : Transitive R₃ R₂
      transitive₃₃ : Transitive R₃ R₃
      transitive₃₄ : Transitive R₃ R₄
      transitive₃₅ : Transitive R₃ R₅
      transitive₄₁ : Transitive R₄ R₁
      transitive₄₂ : Transitive R₄ R₂
      transitive₄₃ : Transitive R₄ R₃
      transitive₄₄ : Transitive R₄ R₄
      transitive₄₅ : Transitive R₄ R₅
      transitive₅₁ : Transitive R₅ R₁
      transitive₅₂ : Transitive R₅ R₂
      transitive₅₃ : Transitive R₅ R₃
      transitive₅₄ : Transitive R₅ R₄
      transitive₅₅ : Transitive R₅ R₅

postulate
  comm : ∀ {P} → P ≈ P
  P    : Proc

cong : P ≈ P
cong =
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ∼⟨ comm ⟩
  P ■


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

-- Syntax

open import Library

module Derivations (Base : Set) where

import Formulas; private open module Form = Formulas Base
-- open import Formulas Base public

-- Derivations

infix 2 _⊢_

data _⊢_ (Γ : Cxt) : (A : Form) → Set where
  hyp    : ∀{A} (x : Hyp A Γ) → Γ ⊢ A
  impI   : ∀{A B} (t : Γ ∙ A ⊢ B) → Γ ⊢ A ⇒ B
  impE   : ∀{A B} (t : Γ ⊢ A ⇒ B) (u : Γ ⊢ A) → Γ ⊢ B
  andI   : ∀{A B} (t : Γ ⊢ A) (u : Γ ⊢ B) → Γ ⊢ A ∧ B
  andE₁  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ A
  andE₂  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ B
  orI₁   : ∀{A B} (t : Γ ⊢ A) → Γ ⊢ A ∨ B
  orI₂   : ∀{A B} (t : Γ ⊢ B) → Γ ⊢ A ∨ B
  orE    : ∀{A B C} (t : Γ ⊢ A ∨ B) (u : Γ ∙ A ⊢ C) (v : Γ ∙ B ⊢ C) → Γ ⊢ C
  falseE : ∀{C} (t : Γ ⊢ False) → Γ ⊢ C
  trueI  : Γ ⊢ True

-- Example derivation

andComm : ∀{A B} → ε ⊢ A ∧ B ⇒ B ∧ A
andComm = impI (andI (andE₂ (hyp top)) (andE₁ (hyp top)))

-- Weakening

Tm = λ A Γ → Γ ⊢ A

monD : ∀{A} → Mon (Tm A)
monD τ (hyp x)     = hyp (monH τ x)
monD τ (impI t)    = impI (monD (lift τ) t)
monD τ (impE t u)  = impE (monD τ t) (monD τ u)
monD τ (andI t u)  = andI (monD τ t) (monD τ u)
monD τ (andE₁ t)   = andE₁ (monD τ t)
monD τ (andE₂ t)   = andE₂ (monD τ t)
monD τ (orI₁ t)    = orI₁ (monD τ t)
monD τ (orI₂ t)    = orI₂ (monD τ t)
monD τ (orE t u v) = orE (monD τ t) (monD (lift τ) u) (monD (lift τ) v)
monD τ (falseE t)  = falseE (monD τ t)
monD τ trueI       = trueI

monD-id : ∀{Γ A} (t : Γ ⊢ A) → monD id≤ t ≡ t
monD-id (hyp x) = refl
monD-id (impI t) = cong impI (monD-id t)  -- REWRITE lift-id≤
monD-id (impE t u) = cong₂ impE (monD-id t) (monD-id u)
monD-id (andI t u) = cong₂ andI (monD-id t) (monD-id u)
monD-id (andE₁ t) = cong andE₁ (monD-id t)
monD-id (andE₂ t) = cong andE₂ (monD-id t)
monD-id (orI₁ t) = cong orI₁ (monD-id t)
monD-id (orI₂ t) = cong orI₂ (monD-id t)
monD-id (orE t u v) = cong₃ orE (monD-id t) (monD-id u) (monD-id v)
monD-id (falseE t) = cong falseE (monD-id t)
monD-id trueI = refl

-- For normal forms, we use the standard presentation.
-- Normal forms are not unique.

-- Normality as predicate

mutual
  data Neutral {Γ} {A} : (t : Γ ⊢ A) → Set where
    hyp : (x : Hyp A Γ) → Neutral (hyp x)
    impE : ∀{B} {t : Γ ⊢ B ⇒ A} {u : Γ ⊢ B} (ne : Neutral t) (nf : Normal u) → Neutral (impE t u)
    andE₁ : ∀{B} {t : Γ ⊢ A ∧ B} (ne : Neutral t) → Neutral (andE₁ t)
    andE₂ : ∀{B} {t : Γ ⊢ B ∧ A} (ne : Neutral t) → Neutral (andE₂ t)

  data Normal {Γ} : ∀{A} (t : Γ ⊢ A) → Set where
    ne     : ∀{A} {t : Γ ⊢ A} (ne : Neutral t) → Normal t
    impI   : ∀{A B} (t : Γ ∙ A ⊢ B) (nf : Normal t) → Normal (impI t)
    andI   : ∀{A B} (t : Γ ⊢ A) (u : Γ ⊢ B) (nf₁ : Normal t) (nf₂ : Normal u) → Normal (andI t u)
    orI₁   : ∀{A B} {t : Γ ⊢ A} (nf : Normal t) → Normal (orI₁ {Γ} {A} {B} t)
    orI₂   : ∀{A B} {t : Γ ⊢ B} (nf : Normal t) → Normal (orI₂ {Γ} {A} {B} t)
    orE    : ∀{A B C} {t : Γ ⊢ A ∨ B} {u : Γ ∙ A ⊢ C} {v : Γ ∙ B ⊢ C}
             (ne : Neutral t) (nf₁ : Normal u) (nf₂ : Normal v) → Normal (orE t u v)
    falseE : ∀{A} {t : Γ ⊢ False} (ne : Neutral t) → Normal (falseE {Γ} {A} t)
    trueI  : Normal trueI

-- Intrinsic normality

mutual
  data Ne (Γ : Cxt) (A : Form) : Set where
    hyp    : ∀    (x : Hyp A Γ) → Ne Γ A
    impE   : ∀{B} (t : Ne Γ (B ⇒ A)) (u : Nf Γ B) → Ne Γ A
    andE₁  : ∀{B} (t : Ne Γ (A ∧ B)) → Ne Γ A
    andE₂  : ∀{B} (t : Ne Γ (B ∧ A)) → Ne Γ A

  data Nf (Γ : Cxt) : (A : Form) → Set where
    -- ne     : ∀{A} (t : Ne Γ A) → Nf Γ A   -- allows η-short nfs
    ne     : ∀{P} (t : Ne Γ (Atom P)) → Nf Γ (Atom P)
    impI   : ∀{A B} (t : Nf (Γ ∙ A) B) → Nf Γ (A ⇒ B)
    andI   : ∀{A B} (t : Nf Γ A) (u : Nf Γ B) → Nf Γ (A ∧ B)
    orI₁   : ∀{A B} (t : Nf Γ A) → Nf Γ (A ∨ B)
    orI₂   : ∀{A B} (t : Nf Γ B) → Nf Γ (A ∨ B)
    orE    : ∀{A B C} (t : Ne Γ (A ∨ B)) (u : Nf (Γ ∙ A) C) (v : Nf (Γ ∙ B) C) → Nf Γ C
    falseE : ∀{A} (t : Ne Γ False) → Nf Γ A
    trueI  : Nf Γ True

-- Presheaf-friendly argument order

Ne' = λ A Γ → Ne Γ A
Nf' = λ A Γ → Nf Γ A

-- Admissible false-Elimination from a normal proof of false (using case splits)

falseE! : ∀{A} → Nf' False →̇ Nf' A
-- falseE! (ne t)       = falseE t  -- only for η-short
falseE! (orE t t₁ t₂) = orE t (falseE! t₁) (falseE! t₂)
falseE! (falseE t)   = falseE t

-- Ne' and Nf' are presheaves over (Cxt, ≤)

mutual

  monNe : ∀{A} → Mon (Ne' A)
  monNe τ (hyp x)     = hyp (monH τ x)
  monNe τ (impE t u)  = impE (monNe τ t) (monNf τ u)
  monNe τ (andE₁ t)   = andE₁ (monNe τ t)
  monNe τ (andE₂ t)   = andE₂ (monNe τ t)

  monNf : ∀{A} → Mon (Nf' A)
  monNf τ (ne t)     = ne (monNe τ t)
  monNf τ (impI t)    = impI (monNf (lift τ) t)
  monNf τ (andI t u)  = andI (monNf τ t) (monNf τ u)
  monNf τ (orI₁ t)    = orI₁ (monNf τ t)
  monNf τ (orI₂ t)    = orI₂ (monNf τ t)
  monNf τ (orE t u v) = orE (monNe τ t) (monNf (lift τ) u) (monNf (lift τ) v)
  monNf τ (falseE t)  = falseE (monNe τ t)
  monNf τ trueI       = trueI

-- Forgetting normality

mutual
  ne[_] : ∀{Γ A} (t : Ne Γ A) → Γ ⊢ A
  ne[ hyp x ]     = hyp x
  ne[ impE t u ]  = impE ne[ t ] nf[ u ]
  ne[ andE₁ t ]   = andE₁ ne[ t ]
  ne[ andE₂ t ]   = andE₂ ne[ t ]

  nf[_] : ∀{Γ A} (t : Nf Γ A) → Γ ⊢ A
  nf[ ne t ]      = ne[ t ]
  nf[ impI t ]    = impI nf[ t ]
  nf[ andI t u ]  = andI nf[ t ] nf[ u ]
  nf[ orI₁ t ]    = orI₁ nf[ t ]
  nf[ orI₂ t ]    = orI₂ nf[ t ]
  nf[ orE t u v ] = orE ne[ t ] nf[ u ] nf[ v ]
  nf[ falseE t ]  = falseE ne[ t ]
  nf[ trueI ]     = trueI

mutual

  monD-ne : ∀{Γ Δ A} (τ : Δ ≤ Γ) (t : Ne Γ A) → ne[ monNe τ t ] ≡ monD τ ne[ t ]
  monD-ne τ (hyp x)     = refl
  monD-ne τ (impE t u)  = cong₂ impE (monD-ne τ t) (monD-nf τ u)
  monD-ne τ (andE₁ t)   = cong andE₁ (monD-ne τ t)
  monD-ne τ (andE₂ t)   = cong andE₂ (monD-ne τ t)

  monD-nf : ∀{Γ Δ A} (τ : Δ ≤ Γ) (t : Nf Γ A) → nf[ monNf τ t ] ≡ monD τ nf[ t ]
  monD-nf τ (ne t)      = monD-ne τ t
  monD-nf τ (impI t)    = cong impI (monD-nf (lift τ) t)
  monD-nf τ (andI t u)  = cong₂ andI (monD-nf τ t) (monD-nf τ u)
  monD-nf τ (orI₁ t)    = cong orI₁ (monD-nf τ t)
  monD-nf τ (orI₂ t)    = cong orI₂ (monD-nf τ t)
  monD-nf τ (orE t u v) = cong₃ orE (monD-ne τ t) (monD-nf (lift τ) u) (monD-nf (lift τ) v)
  monD-nf τ (falseE t)  = cong falseE (monD-ne τ t)
  monD-nf τ trueI       = refl

  -- monD-ne : ∀{Γ Δ A} (τ : Δ ≤ Γ) (t : Ne Γ A) → monD τ ne[ t ] ≡ ne[ monNe τ t ]
  -- monD-ne τ (hyp x)     = refl
  -- monD-ne τ (impE t u)  = cong₂ impE (monD-ne τ t) (monD-nf τ u)
  -- monD-ne τ (andE₁ t)   = cong andE₁ (monD-ne τ t)
  -- monD-ne τ (andE₂ t)   = cong andE₂ (monD-ne τ t)

  -- monD-nf : ∀{Γ Δ A} (τ : Δ ≤ Γ) (t : Nf Γ A) → monD τ nf[ t ] ≡ nf[ monNf τ t ]
  -- monD-nf τ (ne t)      = monD-ne τ t
  -- monD-nf τ (impI t)    = cong impI (monD-nf (lift τ) t)
  -- monD-nf τ (andI t u)  = cong₂ andI (monD-nf τ t) (monD-nf τ u)
  -- monD-nf τ (orI₁ t)    = cong orI₁ (monD-nf τ t)
  -- monD-nf τ (orI₂ t)    = cong orI₂ (monD-nf τ t)
  -- monD-nf τ (orE t u v) = cong₃ orE (monD-ne τ t) (monD-nf (lift τ) u) (monD-nf (lift τ) v)
  -- monD-nf τ (falseE t)  = cong falseE (monD-ne τ t)
  -- monD-nf τ trueI       = refl

{-# REWRITE monD-ne monD-nf #-}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
{-# OPTIONS --without-K #-}
open import Library

--------------------------------------------------------------------------------
-- Universes for a Category
--------------------------------------------------------------------------------

record CatLevel : Set where
  field
    Obj  : Level
    Hom  : Level

  Obj-Hom : Level
  Obj-Hom = ℓ-max Obj Hom

  Cat : Level
  Cat = ℓ-suc (ℓ-max Obj Hom)

--------------------------------------------------------------------------------
-- Definition of a Category
--------------------------------------------------------------------------------

module _ (ℓ : CatLevel) (let module ℓ = CatLevel ℓ) where
  record Category : Set ℓ.Cat where
    field
      Obj   : Set ℓ.Obj
      _⇒_   : Obj → Obj → Set ℓ.Hom
      id    : (X : Obj) → X ⇒ X
      _∘_   : ∀{X Y Z} → Y ⇒ Z → X ⇒ Y → X ⇒ Z

    infix 4 _⇒_
    infix 6 _∘_

    field
      idl   : ∀{X Y}{f : X ⇒ Y} → (id Y) ∘ f ≡ f
      idr   : ∀{X Y}{f : X ⇒ Y} → f ∘ (id X) ≡ f
      assoc : ∀{W X Y Z}{f : W ⇒ X}{g : X ⇒ Y}{h : Y ⇒ Z}
                → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)

--------------------------------------------------------------------------------
-- Dual Category
--------------------------------------------------------------------------------

    op : Category
    op = record { Obj    = Obj
                ; _⇒_    = λ-flip _⇒_
                ; id     = id
                ; _∘_    = λ-flip _∘_
                ; idl    = idr
                ; idr    = idl
                ; assoc  = ≡-sym assoc }

--------------------------------------------------------------------------------
-- Properties of Spacial Morphisms
--------------------------------------------------------------------------------

    record _≅_ (X Y : Obj) : Set ℓ.Cat where
      field
        f   : X ⇒ Y
        g   : Y ⇒ X
        g∘f : g ∘ f ≡ id X
        f∘g : f ∘ g ≡ id Y

    record _≾_ (X Y : Obj) : Set ℓ.Cat where
      field
        s   : X ⇒ Y
        r   : Y ⇒ X
        r∘s : r ∘ s ≡ id X

    module _ {X Y : Obj} (f : X ⇒ Y) where
      is-isomorphism  : Set ℓ.Hom
      is-isomorphism  = Σ[ g ∈ Y ⇒ X ] (g ∘ f ≡ id X) × (f ∘ g ≡ id Y)

      is-section      : Set ℓ.Hom
      is-section      = Σ[ g ∈ Y ⇒ X ] g ∘ f ≡ id X

      is-retraction   : Set ℓ.Hom
      is-retraction   = Σ[ g ∈ Y ⇒ X ] f ∘ g ≡ id Y

      is-monomorphism : Set ℓ.Obj-Hom
      is-monomorphism = ∀{Z}{g h : Z ⇒ X} → f ∘ g ≡ f ∘ h → g ≡ h

      is-epimorphism  : Set ℓ.Obj-Hom
      is-epimorphism  = ∀{Z}{g h : Y ⇒ Z} → g ∘ f ≡ h ∘ f → g ≡ h

      is-bimorphism   : Set ℓ.Obj-Hom
      is-bimorphism   = is-monomorphism × is-epimorphism

    module _ (X Y : Obj) where
      _iso⇒_  : Set ℓ.Hom
      _iso⇒_  = Σ (X ⇒ Y) is-isomorphism

      _mono⇒_ : Set ℓ.Obj-Hom
      _mono⇒_ = Σ (X ⇒ Y) is-monomorphism

      _epi⇒_  : Set ℓ.Obj-Hom
      _epi⇒_  = Σ (X ⇒ Y) is-epimorphism

--------------------------------------------------------------------------------
-- Category of Sets i.e. Types that has no non-trival equality
--------------------------------------------------------------------------------

SetCat : (ℓ : Level) → Category (record { Obj = ℓ-suc ℓ ; Hom = ℓ })
SetCat ℓ = record
  { Obj   = Object
  ; _⇒_   = λ (X Y : Object) → (X → Y)
  ; id    = λ (X : Object) → (λ x → x)
  ; _∘_   = λ {X Y Z : Object} (g : Y → Z) (f : X → Y) → (λ x → g (f x))
  ; idl   = ≡-refl
  ; idr   = ≡-refl
  ; assoc = ≡-refl
  } where Object = Set ℓ

SetCat₀ = SetCat ℓ-zero

max_stars_repo_name: gunpinyo/agda-cat

max_issues_repo_name: gunpinyo/agda-cat

max_forks_repo_name: gunpinyo/agda-cat


text:
module Luau.Value.ToString where

open import Agda.Builtin.String using (String)
open import Agda.Builtin.Float using (primShowFloat)
open import Luau.Value using (Value; nil; addr; number)
open import Luau.Addr.ToString using (addrToString)

valueToString : Value → String
valueToString nil = "nil"
valueToString (addr a) = addrToString a
valueToString (number x) = primShowFloat x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by lattices
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.Lattice
  {c ℓ₁ ℓ₂} (L : Lattice c ℓ₁ ℓ₂) where

open Lattice L

import Algebra as Alg
import Algebra.Structures as Alg
open import Algebra.FunctionProperties _≈_
open import Data.Product using (_,_)
open import Function using (flip)
open import Relation.Binary
open import Relation.Binary.Properties.Poset poset
import Relation.Binary.Properties.JoinSemilattice joinSemilattice as J
import Relation.Binary.Properties.MeetSemilattice meetSemilattice as M
import Relation.Binary.Reasoning.Setoid as EqReasoning
import Relation.Binary.Reasoning.PartialOrder as POR

∨-absorbs-∧ : _∨_ Absorbs _∧_
∨-absorbs-∧ x y =
  let x≤x∨[x∧y] , _ , least = supremum  x (x ∧ y)
      x∧y≤x     , _ , _     = infimum x y
  in antisym (least x refl x∧y≤x) x≤x∨[x∧y]

∧-absorbs-∨ : _∧_ Absorbs _∨_
∧-absorbs-∨ x y =
  let x∧[x∨y]≤x , _ , greatest = infimum  x (x ∨ y)
      x≤x∨y     , _ , _        = supremum x y
  in antisym x∧[x∨y]≤x (greatest x refl x≤x∨y)

absorptive : Absorptive _∨_ _∧_
absorptive = ∨-absorbs-∧ , ∧-absorbs-∨

∧≤∨ : ∀ {x y} → x ∧ y ≤ x ∨ y
∧≤∨ {x} {y} = begin
  x ∧ y ≤⟨ x∧y≤x x y ⟩
  x     ≤⟨ x≤x∨y x y ⟩
  x ∨ y ∎
  where open POR poset

-- two quadrilateral arguments

quadrilateral₁ : ∀ {x y} → x ∨ y ≈ x → x ∧ y ≈ y
quadrilateral₁ {x} {y} x∨y≈x = begin
  x ∧ y       ≈⟨ M.∧-cong (Eq.sym x∨y≈x) Eq.refl ⟩
  (x ∨ y) ∧ y ≈⟨ M.∧-comm _ _ ⟩
  y ∧ (x ∨ y) ≈⟨ M.∧-cong Eq.refl (J.∨-comm _ _) ⟩
  y ∧ (y ∨ x) ≈⟨ ∧-absorbs-∨ _ _ ⟩
  y           ∎
  where open EqReasoning setoid

quadrilateral₂ : ∀ {x y} → x ∧ y ≈ y → x ∨ y ≈ x
quadrilateral₂ {x} {y} x∧y≈y = begin
  x ∨ y       ≈⟨ J.∨-cong Eq.refl (Eq.sym x∧y≈y) ⟩
  x ∨ (x ∧ y) ≈⟨ ∨-absorbs-∧ _ _ ⟩
  x           ∎
  where open EqReasoning setoid

-- collapsing sublattice

collapse₁ : ∀ {x y} → x ≈ y → x ∧ y ≈ x ∨ y
collapse₁ {x} {y} x≈y = begin
  x ∧ y ≈⟨ M.y≤x⇒x∧y≈y y≤x ⟩
  y     ≈⟨ Eq.sym x≈y ⟩
  x     ≈⟨ Eq.sym (J.x≤y⇒x∨y≈y y≤x) ⟩
  y ∨ x ≈⟨ J.∨-comm _ _ ⟩
  x ∨ y ∎
  where
  y≤x = reflexive (Eq.sym x≈y)
  open EqReasoning setoid

-- this can also be proved by quadrilateral argument, but it's much less symmetric.
collapse₂ : ∀ {x y} → x ∨ y ≤ x ∧ y → x ≈ y
collapse₂ {x} {y} ∨≤∧ = antisym
  (begin x     ≤⟨ x≤x∨y _ _ ⟩
         x ∨ y ≤⟨ ∨≤∧ ⟩
         x ∧ y ≤⟨ x∧y≤y _ _ ⟩
         y     ∎)
  (begin y     ≤⟨ y≤x∨y _ _ ⟩
         x ∨ y ≤⟨ ∨≤∧ ⟩
         x ∧ y ≤⟨ x∧y≤x _ _ ⟩
         x     ∎)
  where open POR poset

------------------------------------------------------------------------
-- The dual construction is also a lattice.

∧-∨-isLattice : IsLattice _≈_ (flip _≤_) _∧_ _∨_
∧-∨-isLattice = record
  { isPartialOrder = invIsPartialOrder
  ; supremum       = infimum
  ; infimum        = supremum
  }

∧-∨-lattice : Lattice c ℓ₁ ℓ₂
∧-∨-lattice = record
  { _∧_       = _∨_
  ; _∨_       = _∧_
  ; isLattice = ∧-∨-isLattice
  }

------------------------------------------------------------------------
-- Every order-theoretic lattice can be turned into an algebraic one.

isAlgLattice : Alg.IsLattice _≈_ _∨_ _∧_
isAlgLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = J.∨-comm
  ; ∨-assoc       = J.∨-assoc
  ; ∨-cong        = J.∨-cong
  ; ∧-comm        = M.∧-comm
  ; ∧-assoc       = M.∧-assoc
  ; ∧-cong        = M.∧-cong
  ; absorptive    = absorptive
  }

algLattice : Alg.Lattice c ℓ₁
algLattice = record { isLattice = isAlgLattice }


text:
data Unit : Set where
  unit : Unit

data Builtin : Set where
  addInteger : Builtin

data SizedTermCon : Set where
  integer : (s : Unit) → SizedTermCon

data ScopedTm : Set where
  con : SizedTermCon → ScopedTm

data Value : ScopedTm → Set where
  V-con : (tcn : SizedTermCon) → Value (con tcn)

BUILTIN : Builtin → (t : ScopedTm) → Value t → Unit
BUILTIN addInteger _ (V-con (integer s)) = s


text:
-- The Berry majority function.

module Berry where

  data Bool : Set where
    F : Bool
    T : Bool

  maj : Bool -> Bool -> Bool -> Bool
  maj T T T = T
  maj T F x = x
  maj F x T = x
  maj x T F = x   -- doesn't hold definitionally
  maj F F F = F

  postulate
    z : Bool


text:
module Inductive.Examples.Nat where

open import Inductive
open import Tuple

import Data.Fin as Fin
open import Data.Product
open import Data.List
open import Data.Vec hiding (lookup)

Nat : Set
Nat = Inductive ( ([] , []) ∷ (([] , ([] ∷ [])) ∷ []))

zero : Nat
zero = construct Fin.zero [] []

suc : Nat → Nat
suc n = construct (Fin.suc Fin.zero) [] ((λ _ → n) ∷ [])

_+_ : Nat → Nat → Nat
n + m = rec (m ∷ ((λ x x₁ → suc x₁) ∷ [])) n

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


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

module Data.Binary.Proofs.Multiplication where

open import Relation.Binary.PropositionalEquality
open import Data.Binary.Operations.Unary
open import Data.Binary.Operations.Addition
open import Data.Binary.Operations.Multiplication
open import Data.Binary.Proofs.Unary
open import Data.Binary.Proofs.Addition
open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality.FasterReasoning
import Data.Nat.Properties as ℕ
open import Function
open import Data.Nat.Reasoning

mul-homo : ∀ xs ys → ⟦ mul xs ys ⇓⟧⁺ ≡ ⟦ xs ⇓⟧⁺ ℕ.* ⟦ ys ⇓⟧⁺
mul-homo 1ᵇ ys = sym (ℕ.+-identityʳ _)
mul-homo (O ∷ xs) ys = cong 2* (mul-homo xs ys) ⟨ trans ⟩ sym (ℕ.*-distribʳ-+ ⟦ ys ⇓⟧⁺ ⟦ xs ⇓⟧⁺ _)
mul-homo (I ∷ xs) ys =
  begin
    ⟦ add O (O ∷ mul ys xs) ys ⇓⟧⁺
  ≡⟨ add₀-homo (O ∷ mul ys xs) ys ⟩
    2* ⟦ mul ys xs ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺
  ≡⟨ ⟦ ys ⇓⟧⁺ ≪+ cong 2* (mul-homo ys xs) ⟩
    2* (⟦ ys ⇓⟧⁺ ℕ.* ⟦ xs ⇓⟧⁺) ℕ.+ ⟦ ys ⇓⟧⁺
  ≡⟨ ℕ.+-comm _ ⟦ ys ⇓⟧⁺ ⟩
    ⟦ ys ⇓⟧⁺ ℕ.+ 2* (⟦ ys ⇓⟧⁺ ℕ.* ⟦ xs ⇓⟧⁺)
  ≡˘⟨ ⟦ ys ⇓⟧⁺ +≫ ℕ.*-distribˡ-+ ⟦ ys ⇓⟧⁺ _ _ ⟩
    ⟦ ys ⇓⟧⁺ ℕ.+ ⟦ ys ⇓⟧⁺ ℕ.* (2* ⟦ xs ⇓⟧⁺)
  ≡⟨ ⟦ ys ⇓⟧⁺ +≫ ℕ.*-comm ⟦ ys ⇓⟧⁺ _ ⟩
    ⟦ ys ⇓⟧⁺ ℕ.+ (2* ⟦ xs ⇓⟧⁺) ℕ.* ⟦ ys ⇓⟧⁺
  ∎

*-homo : ∀ xs ys → ⟦ xs * ys ⇓⟧ ≡ ⟦ xs ⇓⟧ ℕ.* ⟦ ys ⇓⟧
*-homo 0ᵇ ys = refl
*-homo (0< x) 0ᵇ = sym (ℕ.*-zeroʳ ⟦ x ⇓⟧⁺)
*-homo (0< xs) (0< ys) = mul-homo xs ys

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
-- Copatterns disabled!
{-# OPTIONS --no-copatterns #-}

open import Common.Product

test : {A B : Set} (a : A) (b : B) → A × B
test a b = {!!}
-- Should give error when attempting to split.


text:
module bstd.belt where

open import Agda.Builtin.Nat using () renaming (Nat to ℕ)
-- open import Agda.Builtin.Word using (Word64)

record traits : Set₁ where
  infixl 5 _⊕_
  infixl 6 _⊞_ _⊟_
  field
    w : Set
    _⊟_ : w → w → w
    _⊞_ : w → w → w
    _⊕_ : w → w → w
    G_ : ℕ → w → w
    _⋘_ : w → ℕ → w

module prim (t : traits) where

  open traits t
  record block : Set where
    constructor _∶_∶_∶_
    field
      a b c d : w

  record key : Set where

  G₅ = G 5
  G₁₃ = G 13
  G₂₁ = G 21

  encᵢ : w → (ℕ → w) → block → block
  encᵢ i k (a ∶ b ∶ c ∶ d) = b‴ ∶ d′ ∶ a′ ∶ c‴ where
    b′ = b ⊕ G₅ (a ⊞ k 0)
    c′ = c ⊕ G₂₁ (d ⊞ k 1)
    a′ = a ⊟ G₁₃ (b ⊞ k 2)
    e = G₂₁ (b ⊞ c ⊞ k 3) ⊕ i
    b″ = b′ ⊞ e
    c″ = c′ ⊟ e
    d′ = d ⊞ G₁₃ (c ⊞ k 4)
    b‴ = b″ ⊕ G₂₁ (a ⊞ k 5)
    c‴ = c″ ⊕ G₅ (d ⊞ k 6)

  𝔼 : key → block → block
  𝔼 k b = {!encᵢ 2 k (encᵢ 1 k x))!}

{-
0 B1 94 BA C8 0A 08 F5 3B 36 6D 00 8E 58 4A 5D E4
1 85 04 FA 9D 1B B6 C7 AC 25 2E 72 C2 02 FD CE 0D
2 5B E3 D6 12 17 B9 61 81 FE 67 86 AD 71 6B 89 0B
3 5C B0 C0 FF 33 C3 56 B8 35 C4 05 AE D8 E0 7F 99
4 E1 2B DC 1A E2 82 57 EC 70 3F CC F0 95 EE 8D F1
5 C1 AB 76 38 9F E6 78 CA F7 C6 F8 60 D5 BB 9C 4F
6 F3 3C 65 7B 63 7C 30 6A DD 4E A7 79 9E B2 3D 31
7 3E 98 B5 6E 27 D3 BC CF 59 1E 18 1F 4C 5A B7 93
8 E9 DE E7 2C 8F 0C 0F A6 2D DB 49 F4 6F 73 96 47
9 06 07 53 16 ED 24 7A 37 39 CB A3 83 03 A9 8B F6
A 92 BD 9B 1C E5 D1 41 01 54 45 FB C9 5E 4D 0E F2
B 68 20 80 AA 22 7D 64 2F 26 87 F9 34 90 40 55 11
C BE 32 97 13 43 FC 9A 48 A0 2A 88 5F 19 4B 09 A1
D 7E CD A4 D0 15 44 AF 8C A5 84 50 BF 66 D2 E8 8A
E A2 D7 46 52 42 A8 DF B3 69 74 C5 51 EB 23 29 21
F D4 EF D9 B4 3A 62 28 75 91 14 10 EA 77 6C DA 1D
-}

max_stars_repo_name: semenov-vladyslav/bstd

max_issues_repo_name: semenov-vladyslav/bstd

max_forks_repo_name: semenov-vladyslav/bstd


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some simple binary relations
------------------------------------------------------------------------

module Relation.Binary.Simple where

open import Relation.Binary
open import Data.Unit
open import Data.Empty
open import Level

-- Constant relations.

Const : ∀ {a b c} {A : Set a} {B : Set b} → Set c → REL A B c
Const I = λ _ _ → I

-- The universally true relation.

Always : ∀ {a ℓ} {A : Set a} → Rel A ℓ
Always = Const (Lift ⊤)

Always-setoid : ∀ {a ℓ} (A : Set a) → Setoid a ℓ
Always-setoid A = record
  { Carrier       = A
  ; _≈_           = Always
  ; isEquivalence = record {}
  }

-- The universally false relation.

Never : ∀ {a ℓ} {A : Set a} → Rel A ℓ
Never = Const (Lift ⊥)


text:
module RandomAccessList.Redundant.Core where

open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)

open import Data.Num.Redundant
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Etc

infixr 2 0∷ _1∷_ _,_2∷_

data 0-2-RAL (A : Set) : ℕ → Set where
    []     : ∀ {n}                                                               → 0-2-RAL A n
    0∷     : ∀ {n}                                           → 0-2-RAL A (suc n) → 0-2-RAL A n
    _1∷_   : ∀ {n} → BinaryLeafTree A n                      → 0-2-RAL A (suc n) → 0-2-RAL A n
    _,_2∷_ : ∀ {n} → BinaryLeafTree A n → BinaryLeafTree A n → 0-2-RAL A (suc n) → 0-2-RAL A n

--------------------------------------------------------------------------------
-- to Redundant Binary Numeral System
--------------------------------------------------------------------------------

⟦_⟧ₙ : ∀ {n A} → 0-2-RAL A n → Redundant
⟦          [] ⟧ₙ = []
⟦       0∷ xs ⟧ₙ = zero ∷ ⟦ xs ⟧ₙ
⟦ x     1∷ xs ⟧ₙ = one  ∷ ⟦ xs ⟧ₙ
⟦ x , y 2∷ xs ⟧ₙ = two  ∷ ⟦ xs ⟧ₙ

⟦_⟧ : ∀ {n A} → 0-2-RAL A n → Redundant
⟦_⟧ {n} xs = n <<< ⟦ xs ⟧ₙ

--------------------------------------------------------------------------------
-- to ℕ
--------------------------------------------------------------------------------

{-
[_]ₙ : ∀ {A n} → 0-2-RAL A n → ℕ
[          [] ]ₙ = 0
[       0∷ xs ]ₙ = 0 + 2 * [ xs ]ₙ
[ x     1∷ xs ]ₙ = 1 + 2 * [ xs ]ₙ
[ x , y 2∷ xs ]ₙ = 2 + 2 * [ xs ]ₙ

[_] : ∀ {n A} → 0-2-RAL A n → ℕ
[_] {n} xs = 2 ^ n * [ xs ]ₙ
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral