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

open import Categories.Category

module Categories.Category.Closed {o ℓ e} (C : Category o ℓ e) where

private
  module C = Category C
  open C
  variable
    A B X X′ Y Y′ Z Z′ U V : Obj
    f g : A ⇒ B

  open Commutation

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Equality using (_⟶_)
open import Function.Inverse using (_InverseOf_; Inverse)

open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.NaturalTransformation.Dinatural

record Closed : Set (levelOfTerm C) where
  field
    -- internal hom
    [-,-] : Bifunctor C.op C C
    unit  : Obj

  [_,-] : Obj → Functor C C
  [_,-] = appˡ [-,-]

  [-,_] : Obj → Functor C.op C
  [-,_] = appʳ [-,-]

  module [-,-] = Functor [-,-]

  [_,_]₀ : Obj → Obj → Obj
  [ X , Y ]₀ = [-,-].F₀ (X , Y)

  [_,_]₁ : A ⇒ B → X ⇒ Y → [ B , X ]₀ ⇒ [ A , Y ]₀
  [ f , g ]₁ = [-,-].F₁ (f , g)

  field
    -- i
    identity : NaturalIsomorphism idF [ unit ,-]
    -- j
    diagonal : Extranaturalʳ unit [-,-]

  module identity = NaturalIsomorphism identity
  module diagonal = DinaturalTransformation diagonal

  [[X,-],[X,-]] : Obj → Bifunctor C.op C C
  [[X,-],[X,-]] X = [-,-] ∘F (Functor.op [ X ,-] ⁂ [ X ,-])

  [[-,Y],[-,Z]] : Obj → Obj → Bifunctor C C.op C
  [[-,Y],[-,Z]] Y Z = [-,-] ∘F ((Functor.op [-, Y ]) ⁂ [-, Z ])

  -- L needs to be natural in Y and Z while extranatural in Z.
  -- it is better to spell out the conditions and then prove that indeed
  -- the naturality conditions hold.
  field
    L : ∀ X Y Z → [ Y , Z ]₀ ⇒ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀
    L-natural-comm : [ [ Y , Z ]₀ ⇒  [ [ X , Y′ ]₀ , [ X , Z′ ]₀ ]₀ ]⟨
                       [ f , g ]₁                                   ⇒⟨ [ Y′ , Z′ ]₀ ⟩
                       L X Y′ Z′
                     ≈ L X Y Z                                      ⇒⟨ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀ ⟩
                       [ [ C.id , f ]₁ , [ C.id , g ]₁ ]₁
                     ⟩
    L-dinatural-comm : [ [ Y , Z ]₀ ⇒  [ [ X , Y ]₀ , [ X′ , Z ]₀ ]₀ ]⟨
                         L X′ Y Z                                      ⇒⟨ [ [ X′ , Y ]₀ , [ X′ , Z ]₀ ]₀ ⟩
                         [ [ f , C.id ]₁ , [ C.id , C.id ]₁ ]₁
                       ≈ L X Y Z                                       ⇒⟨ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀ ⟩
                         [ [ C.id , C.id ]₁ , [ f , C.id ]₁ ]₁
                       ⟩

  L-natural : NaturalTransformation [-,-] ([[X,-],[X,-]] X)
  L-natural {X} = ntHelper record
    { η       = λ where
      (Y , Z) → L X Y Z
    ; commute = λ _ → L-natural-comm
    }

  L-dinatural : Extranaturalʳ [ Y , Z ]₀ (flip-bifunctor ([[-,Y],[-,Z]] Y Z))
  L-dinatural {Y} {Z} = extranaturalʳ (λ X → L X Y Z) L-dinatural-comm

  module L-natural {X}     = NaturalTransformation (L-natural {X})
  module L-dinatural {Y Z} = DinaturalTransformation (L-dinatural {Y} {Z})

  -- other required diagrams
  field
    Lj≈j : [ unit ⇒ [ [ X , Y ]₀ , [ X , Y ]₀ ]₀ ]⟨
             diagonal.α Y                        ⇒⟨ [ Y , Y ]₀ ⟩
             L X Y Y
           ≈ diagonal.α [ X , Y ]₀
           ⟩
    jL≈i : [ [ X , Y ]₀ ⇒ [ unit , [ X , Y ]₀ ]₀ ]⟨
             L X X Y                             ⇒⟨ [ [ X , X ]₀ , [ X , Y ]₀ ]₀ ⟩
             [ diagonal.α X , C.id ]₁
           ≈ identity.⇒.η [ X , Y ]₀
           ⟩
    iL≈i : [ [ Y , Z ]₀ ⇒ [ Y , [ unit , Z ]₀ ]₀ ]⟨
             L unit Y Z                          ⇒⟨ [ [ unit , Y ]₀ , [ unit , Z ]₀ ]₀ ⟩
             [ identity.⇒.η Y , C.id ]₁
           ≈ [ C.id , identity.⇒.η Z ]₁
           ⟩

    pentagon : [ [ U , V ]₀ ⇒ [ [ Y , U ]₀ , [ [ X , Y ]₀ , [ X , V ]₀ ]₀ ]₀ ]⟨
                 L X U V                            ⇒⟨ [ [ X , U ]₀ , [ X , V ]₀ ]₀ ⟩
                 L [ X , Y ]₀ [ X , U ]₀ [ X , V ]₀ ⇒⟨ [ [ [ X , Y ]₀ , [ X , U ]₀ ]₀ , [ [ X , Y ]₀ , [ X , V ]₀ ]₀ ]₀ ⟩
                 [ L X Y U , C.id ]₁
               ≈ L Y U V                            ⇒⟨ [ [ Y , U ]₀ , [ Y , V ]₀ ]₀ ⟩
                 [ C.id , L X Y V ]₁
               ⟩

  open Functor

  γ : hom-setoid {X} {Y} ⟶ hom-setoid {unit} {[ X , Y ]₀}
  γ {X} = record
    { _⟨$⟩_ = λ f → [ C.id , f ]₁ ∘ diagonal.α _
    ; cong  = λ eq → ∘-resp-≈ˡ (F-resp-≈ [ X ,-] eq)
    }

  field
    γ⁻¹             : hom-setoid {unit} {[ X , Y ]₀} ⟶ hom-setoid {X} {Y}
    γ-inverseOf-γ⁻¹ : γ {X} {Y} InverseOf γ⁻¹

  γ-inverse : Inverse (hom-setoid {unit} {[ X , Y ]₀}) (hom-setoid {X} {Y})
  γ-inverse = record
    { to         = γ⁻¹
    ; from       = γ
    ; inverse-of = γ-inverseOf-γ⁻¹
    }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

module Examples.Gcd.Spec where

open import Calf.CostMonoid
import Calf.CostMonoids as CM

open import Calf CM.ℕ-CostMonoid
open import Calf.Types.Nat

open import Examples.Gcd.Euclid
open import Examples.Gcd.Clocked

open import Data.Nat.DivMod
open import Data.Nat
open import Relation.Binary.PropositionalEquality as P
open import Data.Nat.Properties
open import Data.Product

gcd/clocked≡spec/zero : ∀ k x h → k ≥ gcd/depth (x , ℕ.zero , h) →
  ◯ (gcd/clocked k (x , ℕ.zero , h) ≡ ret {nat} x)
gcd/clocked≡spec/zero ℕ.zero x h h1 u = refl
gcd/clocked≡spec/zero (suc k) x h h1 u = refl

suc-cancel-≤ : ∀ {m n} → suc m ≤ suc n → m ≤ n
suc-cancel-≤ (s≤s h) = h

gcd/clocked/mono : ∀ k x y h → k ≥ gcd/depth (x , y , h) →
  gcd/clocked k (x , y , h) ≡ gcd/clocked (suc k) (x , y , h)
gcd/clocked/mono ℕ.zero x ℕ.zero h h1 = refl
gcd/clocked/mono (suc k) x ℕ.zero h h1 = refl
gcd/clocked/mono (suc k) x (suc y) h h1 =
  begin
    gcd/clocked (suc k) (x , suc y , h) ≡⟨ refl ⟩
    step (F nat) 1 (gcd/clocked k (suc y , x % suc y , m%n<n x y)) ≡⟨
      P.cong (step (F nat) 1)
        (gcd/clocked/mono k (suc y) (x % suc y) (m%n<n x y)
          (suc-cancel-≤ (P.subst (λ r → suc k ≥ r) (gcd/depth-unfold-suc {x} {y} {h}) h1))) ⟩
    step (F nat) 1 (gcd/clocked (suc k) (suc y , x % suc y , m%n<n x y))
  ∎
  where open ≡-Reasoning

gcd/clocked≡spec/suc : ∀ k x y h → k ≥ gcd/depth (x , suc y , h) →
  ◯ (gcd/clocked k (x , suc y , h) ≡ gcd/clocked k (suc y , x % suc y , m%n<n x y))
gcd/clocked≡spec/suc (suc k) x y h h1 u =
  begin
  gcd/clocked (suc k) (x , suc y , h) ≡⟨ refl ⟩
  step (F nat) 1 (gcd/clocked k (suc y , x % suc y , m%n<n x y)) ≡⟨ step/ext (F nat) ((gcd/clocked k (suc y , x % suc y , m%n<n x y))) 1 u ⟩
  gcd/clocked k (suc y , x % suc y , m%n<n x y) ≡⟨ gcd/clocked/mono k (suc y) (x % suc y) (m%n<n x y)
    (suc-cancel-≤ (P.subst (λ r → suc k ≥ r) (gcd/depth-unfold-suc {x} {y} {h}) h1)) ⟩
  gcd/clocked (suc k) (suc y , x % suc y , m%n<n x y)
  ∎
  where open ≡-Reasoning

gcd≡spec/zero : ∀ x h → ◯ (gcd (x , 0 , h) ≡ ret {nat} x)
gcd≡spec/zero x h = gcd/clocked≡spec/zero (gcd/depth (x , 0 , h)) x h ≤-refl

gcd≡spec/suc : ∀ x y h → ◯ (gcd (x , suc y , h) ≡ gcd (suc y , x % suc y , m%n<n x y))
gcd≡spec/suc x y h u =
  begin
    gcd (x , suc y , h) ≡⟨ gcd/clocked≡spec/suc (gcd/depth (x , suc y , h)) x y h ≤-refl u ⟩
    gcd/clocked (gcd/depth (x , suc y , h)) (suc y , x % suc y , m%n<n x y) ≡⟨
      cong (λ k → gcd/clocked k (suc y , x % suc y , m%n<n x y))
      (gcd/depth-unfold-suc {x} {y} {h}) ⟩
    gcd/clocked (suc (gcd/depth (suc y , x % suc y , m%n<n x y))) (suc y , x % suc y , m%n<n x y) ≡⟨
      sym (gcd/clocked/mono
        (gcd/depth (suc y , x % suc y , m%n<n x y)) (suc y) (x % suc y) (m%n<n x y) ≤-refl) ⟩
    gcd/clocked (gcd/depth (suc y , x % suc y , m%n<n x y)) (suc y , x % suc y , m%n<n x y)
  ∎
  where open ≡-Reasoning

ext: agda

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on indexed containers
------------------------------------------------------------------------

module Data.Container.Indexed.FreeMonad where

open import Level
open import Function hiding (const)
open import Category.Monad.Predicate
open import Data.Container.Indexed hiding (_∈_)
open import Data.Container.Indexed.Combinator hiding (id; _∘_)
open import Data.Empty
open import Data.Sum using (inj₁; inj₂)
open import Data.Product
open import Data.W.Indexed
open import Relation.Unary
open import Relation.Unary.PredicateTransformer

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

infixl 9 _⋆C_
infix  9 _⋆_

_⋆C_ : ∀ {i o c r} {I : Set i} {O : Set o} →
       Container I O c r → Pred O c → Container I O _ _
C ⋆C X = const X ⊎ C

_⋆_ : ∀ {ℓ} {O : Set ℓ} → Container O O ℓ ℓ → Pt O ℓ
C ⋆ X = μ (C ⋆C X)

pattern returnP x = (inj₁ x , _)
pattern doP c k   = (inj₂ c , k)

do : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X} →
     ⟦ C ⟧ (C ⋆ X) ⊆ C ⋆ X
do (c , k) = sup (doP c k)

rawPMonad : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} →
            RawPMonad {ℓ = ℓ} (_⋆_ C)
rawPMonad {C = C} = record
  { return? = return
  ; _=<?_  = _=<<_
  }
  where
  return : ∀ {X} → X ⊆ C ⋆ X
  return x = sup (inj₁ x , ⊥-elim ∘ lower)

  _=<<_ : ∀ {X Y} → X ⊆ C ⋆ Y → C ⋆ X ⊆ C ⋆ Y
  f =<< sup (returnP x) = f x
  f =<< sup (doP c k)   = do (c , λ r → f =<< k r)

leaf : ∀ {ℓ} {O : Set ℓ} {C : Container O O ℓ ℓ} {X : Pred O ℓ} →
       ⟦ C ⟧ X ⊆ C ⋆ X
leaf (c , k) = do (c , return? ∘ k)
  where
  open RawPMonad rawPMonad


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

module Data1 where

_-_ : {A : Set}{B : A -> Set}{C : (a : A) -> B a -> Set} ->
      ({a : A}(b : B a) -> C a b) -> (f : (a : A) -> B a) ->
      (a : A) -> C a (f a)
f - g = \ x -> f (g x)

id : {X : Set} -> X -> X
id x = x

konst : {S : Set}{T : S -> Set} -> ({x : S} -> T x) -> (x : S) -> T x
konst c x = c

data Zero : Set where
record One : Set where

record Sig (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

open module Sig' {S : Set}{T : S -> Set} = Sig {S}{T}

_,_ : forall {S T}(s : S) -> T s -> Sig S T
s , t = record {fst = s; snd = t}

infixr 40 _,_

_*_ : Set -> Set -> Set
S * T = Sig S \ _ -> T

sig : forall {S T}{P : Sig S T -> Set} ->
      ((s : S)(t : T s) -> P (s , t)) -> (st : Sig S T) -> P st
sig f st = f (fst st) (snd st)

data Cx : Set where
  E : Cx
  _/_ : Cx -> Set -> Cx

data _:>_ : Cx -> Set -> Set where
  ze : {G : Cx}{S : Set} -> (G / S) :> S
  su : {G : Cx}{S T : Set} -> G :> T -> (G / S) :> T

data PROP : Set where
  Absu : PROP
  Triv : PROP
  _/\_ : PROP -> PROP -> PROP
  All : (S : Set) -> (S -> PROP) -> PROP

Prf : PROP -> Set
Prf Absu = Zero
Prf Triv = One
Prf (P /\ Q) = Prf P * Prf Q
Prf (All S P) = (x : S) -> Prf (P x)

data CON (G : Cx) : Set where
  ?? : {S : Set} -> G :> S -> S -> CON G
  PrfC : PROP -> CON G
  _*C_ : CON G -> CON G -> CON G
  PiC : (S : Set) -> (S -> CON G) -> CON G
  SiC : (S : Set) -> (S -> CON G) -> CON G
  MuC : (O : Set) -> (O -> CON (G / O)) -> O -> CON G
  NuC : (O : Set) -> (O -> CON (G / O)) -> O -> CON G

Box : (G : Cx) -> ((S : Set) -> (G :> S) -> Set) -> Set
Box E F = One
Box (G / S) F = Box G (\ S n -> F S (su n)) * F S ze

pr : {G : Cx}{S : Set}{F : (S : Set) -> (G :> S) -> Set} -> Box G F -> (n : G :> S) -> F S n
pr fsf ze = snd fsf
pr fsf (su n) = pr (fst fsf) n

Pay : Cx -> Set
Pay G = Box G (\ I _ -> I -> Set)

Arr : (G : Cx) -> Pay G -> Pay G -> Set
Arr G X Y = Box G (\ S n -> (s : S) -> pr X n s -> pr Y n s)

mutual
  [|_|] : {G : Cx} -> CON G -> Pay G -> Set
  [| ?? n i |]     X = pr X n i
  [| PrfC P |]     X = Prf P
  [| C *C D |]     X = [| C |] X * [| D |] X
  [| PiC S C |]    X = (s : S) -> [| C s |] X
  [| SiC S C |]    X = Sig S \ s -> [| C s |] X
  [| MuC O C o |]  X = Mu C X o
  [| NuC O C o |]  X = Nu C X o

  data Mu {G : Cx}{O : Set}(C : O -> CON (G / O))(X : Pay G)(o : O) : Set where
    con : [| C o |] ( X , Mu C X ) -> Mu C X o
  codata Nu {G : Cx}{O : Set}(C : O -> CON (G / O))(X : Pay G)(o : O) : Set where
    con : [| C o |] ( X , Nu C X ) -> Nu C X o

noc :  {G : Cx}{O : Set}{C : O -> CON (G / O)}{X : Pay G}{o : O} ->
       Nu C X o -> [| C o |] ( X , Nu C X )
noc (con xs) = xs

mutual
  map : {G : Cx}{X Y : Pay G} -> (C : CON G) ->
        Arr G X Y ->
        [| C |] X -> [| C |] Y
  map (?? n i)     f = pr f n i
  map (PrfC P)     f = id
  map (C *C D)     f = sig \ c d -> map C f c , map D f d
  map (PiC S C)    f = \ c s -> map (C s) f (c s)
  map (SiC S C)    f = sig \ s c -> s , map (C s) f c
  map (MuC O C o)  f = foldMap C (Mu C _) f (\ o -> con) o
  map (NuC O C o)  f = unfoldMap C (Nu C _) f (\ o -> noc) o

  foldMap :  {G : Cx}{O : Set}(C : O -> CON (G / O)){X Y : Pay G}(Z : O -> Set) ->
          Arr G X Y ->
          ((o : O) -> [| C o |] ( Y , Z ) -> Z o) ->
          (o : O) -> Mu C X o -> Z o
  foldMap C Z f alg o (con xs) = alg o (map (C o) (f , foldMap C Z f alg) xs)

  unfoldMap :  {G : Cx}{O : Set}(C : O -> CON (G / O)){X Y : Pay G}(Z : O -> Set) ->
            Arr G X Y ->
            ((o : O) -> Z o -> [| C o |] ( X , Z )) ->
            (o : O) -> Z o -> Nu C Y o
  unfoldMap C Z f coalg o y = con (map (C o) (f , unfoldMap C Z f coalg) (coalg o y))

ida : (G : Cx) -> (X : Pay G) -> Arr G X X
ida E = id
ida (G / S) = sig \ Xs X -> ida G Xs , \ s x -> x

compa : (G : Cx) -> (X Y Z : Pay G) -> Arr G Y Z -> Arr G X Y -> Arr G X Z
compa E = \ _ _ _ _ _ -> _
compa (G / S) = sig \ Xs X -> sig \ Ys Y -> sig \ Zs Z -> sig \ fs f -> sig \ gs g ->
  compa G Xs Ys Zs fs gs , \ s x -> f s (g s x)

data _==_ {X : Set}(x : X) : {Y : Set} -> Y -> Set where
  refl : x == x

subst : {X : Set}{P : X -> Set}{x y : X} -> x == y -> P x -> P y
subst refl p = p

_=,=_ : {S : Set}{T : S -> Set}
        {s0 : S}{s1 : S} -> s0 == s1 ->
        {t0 : T s0}{t1 : T s1} -> t0 == t1 ->
        _==_ {Sig S T} (s0 , t0) {Sig S T} (s1 , t1)
refl =,= refl = refl

mylem :  (G : Cx) -> (X : Pay G) -> compa G X X X (ida G X) (ida G X) == ida G X
mylem E X = refl
mylem (G / S) X = mylem G (fst X) =,= refl

claim : (G : Cx){O : Set}(C : O -> CON (G / O))(X : Pay G)
        (P : (o : O) -> Mu C X o -> Set) -> (p : (o : O)(y : Mu C X o) -> P o y)
        (o : O) ->
        compa (G / O) (X , Mu C X) (X , (\ o -> Sig (Mu C X o) (P o))) (X , Mu C X)
         (ida G X , konst fst) (ida G X , (\ o y -> (y , p o y)))
        == ida (G / O) (X , Mu C X)
claim G C X P p o = mylem G X =,= refl

idLem : {G : Cx}{S : Set}{X : Pay G}(n : G :> S) ->
        pr (ida G X) n == (\ (s : S)(x : pr X n s) -> x)
idLem ze = refl
idLem (su y) = idLem y

_=$_ : {S : Set}{T : S -> Set}{f g : (s : S) -> T s} ->
        f == g -> (s : S) -> f s == g s
refl =$ s = refl

mutual  -- and too intensional
  mapId : {G : Cx}{X : Pay G} -> (C : CON G) -> (xs : [| C |] X) ->
          map C (ida G X) xs == xs
  mapId (?? y y') xs = (idLem y =$ y') =$ xs
  mapId (PrfC y) xs = refl
  mapId (y *C y') xs = mapId y (fst xs) =,= mapId y' (snd xs)
  mapId (PiC S y) xs = {!!} -- no chance
  mapId (SiC S y) xs = refl =,= mapId (y (fst xs)) (snd xs)
  mapId (MuC O y y') xs = foldMapId y y' xs
  mapId (NuC O y y') xs = {!!}

  foldMapId : {G : Cx}{O : Set}(C : O -> CON (G / O)){X : Pay G}
              (o : O)(z : Mu C X o) ->
              foldMap C (Mu C X) (ida G X) (\ o -> con) o z == z
  foldMapId C o (con xzs) = {!!} -- close but no banana

mapComp :  {G : Cx}{X Y Z : Pay G} (f : Arr G Y Z)(g : Arr G X Y)
           (C : CON G) -> (xs : [| C |] X) ->
           map C f (map C g xs) == map C (compa G X Y Z f g) xs
mapComp = {!!}

_-=-_ : {X : Set}{x y z : X} -> x == y -> y == z -> x == z
refl -=- refl = refl

induction : {G : Cx}{O : Set}(C : O -> CON (G / O)){X : Pay G}
            (P : (o : O) -> Mu C X o -> Set) ->
            ((o : O)(xyps : [| C o |] (X , (\ o -> Sig (Mu C X o) (P o)))) ->
             P o (con (map (C o) (ida G X , konst fst) xyps))) ->
            (o : O)(y : Mu C X o) -> P o y
induction {G} C {X} P p o (con xys) =
  subst {P = \ xys -> P o (con xys)}{y = xys}
    ((mapComp
     (ida G X , konst fst) (ida G X , (\ o y -> (y , induction C P p o y))) (C o) xys
     -=- {!!})
      -=- mapId (C o) xys)
    (p o (map (C o) (ida G X , (\ o y -> (y , induction C P p o y))) xys))

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


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

module Generics where

data Zero : Set where
data One  : Set where
  ∙ : One

data _+_ (A B : Set) : Set where
  inl : A -> A + B
  inr : B -> A + B

data _×_ (A : Set)(B : A -> Set) : Set where
  <_,_> : (x : A) -> B x -> A × B

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

data Shape (I : Set) : Set where
  ι : Shape I
  σ : Shape I -> Shape I
  δ : Shape I -> Shape I

data Tel {I : Set} : Shape I -> Set1 where
  empty	  : Tel ι
  non-rec : {s : Shape I}(A : Set) -> (A -> Tel s) -> Tel (σ s)
  rec	  : {s : Shape I}(H : Set) -> (H -> I) -> Tel s -> Tel (δ s)

Index : {I : Set}(E : Set){s : Shape I} -> Tel s -> Set
Index E  empty	      = E
Index E (non-rec A f) = (x : A) -> Index E (f x)
Index E (rec H i s)   = Index E s

data Con (I E : Set) : Set1 where
  con : {s : Shape I}(tel : Tel s) -> Index E tel -> Con I E

infixr 40 _|_

data OP (I E : Set) : Set1 where
  ∅   : OP I E
  _|_ : Con I E -> OP I E -> OP I E

Args-tel : {I : Set}(U : I -> Set){s : Shape I} -> Tel s -> Set
Args-tel U empty	 = One
Args-tel U (non-rec A s) = A × \a -> Args-tel U (s a)
Args-tel U (rec H i s)   = ((x : H) -> U (i x)) × \_ -> Args-tel U s

Args : {I E : Set}(U : I -> Set) -> OP I E -> Set
Args U ∅	       = Zero
Args U (con tel _ | γ) = Args-tel U tel + Args U γ

index-tel : {I E : Set}{s : Shape I}(U : I -> Set)(tel : Tel s) -> Index E tel -> Args-tel U tel -> E
index-tel U  empty	  i ∙		= i
index-tel U (non-rec A s) i < a , arg > = index-tel U (s a) (i a) arg
index-tel U (rec H di s)  i < d , arg > = index-tel U s i arg

index : {I E : Set}(U : I -> Set)(γ : OP I E) -> Args U γ -> E
index U ∅		()
index U (con tel i | _) (inl x) = index-tel U tel i x
index U (con _ _   | γ) (inr y) = index U γ y

OPr : Set -> Set1
OPr I = I -> OP I One

data Ur {I : Set}(γ : OPr I)(i : I) : Set where
  intror : Args (Ur γ) (γ i) -> Ur γ i

OPg : Set -> Set1
OPg I = OP I I

const-index : {I E : Set}{s : Shape I} -> E -> (tel : Tel s) -> Index E tel
const-index i  empty	   = i
const-index i (non-rec _ s)   = \a -> const-index i (s a)
const-index i (rec _ _ s) = const-index i s

ε-shape : {I : Set} -> Shape I -> Shape I
ε-shape  ι    = σ ι
ε-shape (σ s) = σ (ε-shape s)
ε-shape (δ s) = δ (ε-shape s)

ε-tel : {I : Set}{s : Shape I} -> I -> (tel : Tel s) -> Index I tel -> Tel (ε-shape s)
ε-tel i  empty		j = non-rec (j == i) \_ -> empty
ε-tel i (non-rec A arg) j = non-rec A \a -> ε-tel i (arg a) (j a)
ε-tel i (rec H di arg)  j = rec H di (ε-tel i arg j)

ε-con : {I : Set} -> I -> Con I I -> Con I One
ε-con j (con tel i) = con args' (const-index ∙ args')
  where
    args' = ε-tel j tel i

ε : {I : Set} -> OPg I -> OPr I
ε  ∅	  _ = ∅
ε (c | γ) j = ε-con j c | ε γ j

Ug : {I : Set} -> OPg I -> I -> Set
Ug γ = Ur (ε γ)

g→rArgs-tel : {I : Set}(U : I -> Set){s : Shape I}
	      (tel : Tel s)(i : Index I tel)(arg : Args-tel U tel) ->
	      Args-tel U (ε-tel (index-tel U tel i arg) tel i)
g→rArgs-tel U  empty	      i ∙	    = < refl , ∙ >
g→rArgs-tel U (non-rec A tel) i < a , arg > = < a , g→rArgs-tel U (tel a) (i a) arg >
g→rArgs-tel U (rec H di tel)  i < d , arg > = < d , g→rArgs-tel U tel i arg >

g→rArgs : {I : Set}(U : I -> Set)(γ : OPg I)(a : Args U γ) -> Args U (ε γ (index U γ a))
g→rArgs U ∅		  ()
g→rArgs U (con tel i | _) (inl arg) = inl (g→rArgs-tel U tel i arg)
g→rArgs U (con _   _ | γ) (inr arg) = inr (g→rArgs U γ arg)

introg : {I : Set}(γ : OPg I)(a : Args (Ug γ) γ) -> Ug γ (index (Ug γ) γ a)
introg γ a = intror (g→rArgs (Ug γ) γ a)

r→gArgs-tel : {I : Set}(U : I -> Set){s : Shape I}(tel : Tel s)(ind : Index I tel)
	      (i : I) -> Args-tel U (ε-tel i tel ind) -> Args-tel U tel
r→gArgs-tel U  empty	      ind i < p , ∙ >	= ∙
r→gArgs-tel U (non-rec A tel) ind i < a , arg > = < a , r→gArgs-tel U (tel a) (ind a) i arg >
r→gArgs-tel U (rec H di tel)  ind i < d , arg > = < d , r→gArgs-tel U tel ind i arg >

r→gArgs : {I : Set}(U : I -> Set)(γ : OPg I)(i : I)(a : Args U (ε γ i)) -> Args U γ
r→gArgs U  ∅		  _ ()
r→gArgs U (con tel ind | _) i (inl arg) = inl (r→gArgs-tel U tel ind i arg)
r→gArgs U (con _   _   | γ) i (inr arg) = inr (r→gArgs U γ i arg)

-- Elimination rules

IndArg-tel : {I : Set}(U : I -> Set){s : Shape I}(tel : Tel s) -> Args-tel U tel -> Set
IndArg-tel U  empty	     ∙		 = Zero
IndArg-tel U (non-rec A tel) < a , arg > = IndArg-tel U (tel a) arg
IndArg-tel U (rec H di tel)  < d , arg > = H + IndArg-tel U tel arg

IndArg : {I E : Set}(U : I -> Set)(γ : OP I E) -> Args U γ -> Set
IndArg U  ∅		 ()
IndArg U (con tel _ | _) (inl arg) = IndArg-tel U tel arg
IndArg U (con _   _ | γ) (inr arg) = IndArg U γ arg

-- Examples

nat : OPr One
nat = \i -> con empty ∙ | con (rec One (\_ -> ∙) empty) ∙ | ∅

N : Set
N = Ur nat ∙

z : N
z = intror (inl ∙)

s : N -> N
s n = intror (inr (inl < (\_ -> n) , ∙ >))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical-compatible --guardedness #-}
module Common.Coinduction where

open import Agda.Builtin.Coinduction public

private
  my-♯ : ∀ {a} {A : Set a} → A → ∞ A
  my-♯ x = ♯ x


text:
module New.Changes where

open import Data.Product public hiding (map)
open import Data.Sum public hiding (map)
open import Data.Unit.Base public

open import Relation.Binary.PropositionalEquality public hiding ([_])
open import Postulate.Extensionality public
open import Level

open import Theorem.Groups-Nehemiah public

record IsChAlg {ℓ : Level} (A : Set ℓ) (Ch : Set ℓ) : Set (suc ℓ) where
  field
    _⊕_ : A → Ch → A
    _⊝_ : A → A → Ch
    valid : A → Ch → Set ℓ
    _⊚[_]_ : Ch → A → Ch → Ch
    ⊝-valid : ∀ (a b : A) → valid a (b ⊝ a)
    ⊕-⊝ : (b a : A) → a ⊕ (b ⊝ a) ≡ b
    ⊚-correct : ∀ (a : A) → (da1 : Ch) → valid a da1 → (da2 : Ch) → valid (a ⊕ da1) da2 →
      a ⊕ da1 ⊚[ a ] da2 ≡ a ⊕ da1 ⊕ da2
    ⊚-valid : (a : A) → (da1 : Ch) → valid a da1 → (da2 : Ch) → valid (a ⊕ da1) da2 → valid a (da1 ⊚[ a ] da2)
  infixl 6 _⊕_ _⊝_

  Δ : A → Set ℓ
  Δ a = Σ[ da ∈ Ch ] (valid a da)

  update-diff = ⊕-⊝

  nil : A → Ch
  nil a = a ⊝ a
  nil-valid : (a : A) → valid a (nil a)
  nil-valid a = ⊝-valid a a
  update-nil : (a : A) → a ⊕ nil a ≡ a
  update-nil a = update-diff a a

  default-⊚ : Ch → A → Ch → Ch
  default-⊚ da1 a da2 = a ⊕ da1 ⊕ da2 ⊝ a
  default-⊚-valid : (a : A) → (da1 : Ch) → valid a da1 → (da2 : Ch) → valid (a ⊕ da1) da2 → valid a (default-⊚ da1 a da2)
  default-⊚-valid a da1 ada1 da2 ada2 = ⊝-valid a (a ⊕ da1 ⊕ da2)
  default-⊚-correct : ∀ (a : A) → (da1 : Ch) → valid a da1 → (da2 : Ch) → valid (a ⊕ da1) da2 →
      a ⊕ default-⊚ da1 a da2 ≡ a ⊕ da1 ⊕ da2
  default-⊚-correct a da1 ada1 da2 ada2 = update-diff (a ⊕ da1 ⊕ da2) a

record ChAlg {ℓ : Level} (A : Set ℓ) : Set (suc ℓ) where
  field
    Ch : Set ℓ
    isChAlg : IsChAlg A Ch
  open IsChAlg isChAlg public

open ChAlg {{...}} public hiding (Ch)
Ch : ∀ {ℓ} (A : Set ℓ) → {{CA : ChAlg A}} → Set ℓ
Ch A {{CA}} = ChAlg.Ch CA

-- Huge hack, but it does gives the output you want to see in all cases I've seen.

{-# DISPLAY IsChAlg.valid x = valid #-}
{-# DISPLAY ChAlg.valid x = valid #-}
{-# DISPLAY IsChAlg._⊕_ x = _⊕_ #-}
{-# DISPLAY ChAlg._⊕_ x = _⊕_ #-}
{-# DISPLAY IsChAlg.nil x = nil #-}
{-# DISPLAY ChAlg.nil x = nil #-}
{-# DISPLAY IsChAlg._⊝_ x = _⊝_ #-}
{-# DISPLAY ChAlg._⊝_ x = _⊝_ #-}

module _ {ℓ₁} {ℓ₂}
  {A : Set ℓ₁} {B : Set ℓ₂} {{CA : ChAlg A}} {{CB : ChAlg B}} where
  open ≡-Reasoning
  open import Postulate.Extensionality
  instance
    funCA : ChAlg (A → B)
  private
    fCh = A → Ch A → Ch B
    _f⊕_ : (A → B) → fCh → A → B
    _f⊕_ = λ f df a → f a ⊕ df a (nil a)
    _f⊝_ : (g f : A → B) → fCh
    _f⊝_ = λ g f a da → g (a ⊕ da) ⊝ f a

  IsDerivative : ∀ (f : A → B) → (df : fCh) → Set (ℓ₁ ⊔ ℓ₂)
  IsDerivative f df = ∀ a da (v : valid a da) → f (a ⊕ da) ≡ f a ⊕ df a da

  WellDefinedFunChangePoint : ∀ (f : A → B) → (df : fCh) → ∀ a da → Set ℓ₂
  WellDefinedFunChangePoint f df a da = (f f⊕ df) (a ⊕ da) ≡ f a ⊕ df a da

  WellDefinedFunChange : ∀ (f : A → B) → (df : fCh) → Set (ℓ₁ ⊔ ℓ₂)
  WellDefinedFunChange f df = ∀ a da (ada : valid a da) → WellDefinedFunChangePoint f df a da

  private
    fvalid : (A → B) → fCh → Set (ℓ₁ ⊔ ℓ₂)
    fvalid =  λ f df → ∀ a da (ada : valid a da) →
        valid (f a) (df a da) ×
        WellDefinedFunChangePoint f df a da
    f⊝-valid : ∀ (f g : A → B) → fvalid f (g f⊝ f)
    f⊝-valid = λ f g a da (v : valid a da) →
         ⊝-valid (f a) (g (a ⊕ da))
        , ( begin
          f (a ⊕ da) ⊕ (g (a ⊕ da ⊕ nil (a ⊕ da)) ⊝ f (a ⊕ da))
        ≡⟨ cong (λ □ → f (a ⊕ da) ⊕ (g □ ⊝ f (a ⊕ da)))
             (update-nil (a ⊕ da)) ⟩
          f (a ⊕ da) ⊕ (g (a ⊕ da) ⊝ f (a ⊕ da))
        ≡⟨ update-diff (g (a ⊕ da)) (f (a ⊕ da)) ⟩
          g (a ⊕ da)
        ≡⟨ sym (update-diff (g (a ⊕ da)) (f a)) ⟩
          f a ⊕ (g (a ⊕ da) ⊝ f a)
        ∎)

    -- Two alternatives. Proofs on f⊚ are a bit easier.
    -- f⊚ is optimized relying on the incrementalization property for df2.
    f⊚ f⊚2 : fCh → (A → B) → fCh → fCh
    f⊚ df1 f df2 = λ a da → (df1 a (nil a)) ⊚[ f a ] (df2 a da)
    f⊚-valid : (f : A → B) → (df1 : fCh) → fvalid f df1 → (df2 : fCh) → fvalid (f f⊕ df1) df2 → fvalid f (f⊚ df1 f df2)
    f⊚-valid f df1 fdf1 df2 fdf2 a da ada
      rewrite ⊚-correct (f a) (df1 a (nil a)) (proj₁ (fdf1 a (nil a) (nil-valid a))) (df2 a da) (proj₁ (fdf2 a da ada))
      | ⊚-correct
        (f (a ⊕ da))
        (df1 (a ⊕ da) (nil (a ⊕ da))) (proj₁ (fdf1 (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da))))
        (df2 (a ⊕ da) (nil (a ⊕ da))) (proj₁ (fdf2 (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da))))
      =
        ⊚-valid (f a) (df1 a (nil a)) (proj₁ (fdf1 a (nil a) (nil-valid a))) (df2 a da) (proj₁ (fdf2 a da ada))
      , proj₂ (fdf2 a da ada)

    -- f⊚2 is optimized relying on the incrementalization property for df1, so we need to use that property to rewrite some goals.
    f⊚2 df1 f df2 = λ a da → df1 a da ⊚[ f a ] df2 (a ⊕ da) (nil (a ⊕ da))
    f⊚-valid2 : (f : A → B) → (df1 : fCh) → fvalid f df1 → (df2 : fCh) → fvalid (f f⊕ df1) df2 → fvalid f (f⊚2 df1 f df2)
    f⊚-valid2 f df1 fdf1 df2 fdf2 = lemma
      where
        -- Prove that (df2 (a ⊕ da) (nil (a ⊕ da))) is valid for (f a ⊕ df1 a da).
        -- Using the incrementalization property for df1, that becomes (f ⊕ df1) (a ⊕ da).
        --
        -- Since df2 is valid for f ⊕ df1, it follows that (df2 (a ⊕ da) (nil (a ⊕ da)))
        -- is indeed valid for (f ⊕ df1) (a ⊕ da).
        valid-df2-a2-nila2 : ∀ a da → (valid a da) → valid (f a ⊕ df1 a da) (df2 (a ⊕ da) (nil (a ⊕ da)))
        valid-df2-a2-nila2 a da ada rewrite sym (proj₂ (fdf1 a da ada)) = proj₁ (fdf2 (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da)))

        lemma : fvalid f (f⊚2 df1 f df2)
        lemma a da ada
          rewrite ⊚-correct
            (f a)
            (df1 a da) (proj₁ (fdf1 a da ada))
            (df2 (a ⊕ da) (nil (a ⊕ da))) (valid-df2-a2-nila2 a da ada)
          | update-nil (a ⊕ da)
          | ⊚-correct
            (f (a ⊕ da))
            (df1 (a ⊕ da) (nil (a ⊕ da))) (proj₁ (fdf1 (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da))))
            (df2 (a ⊕ da) (nil (a ⊕ da))) (proj₁ (fdf2 (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da))))
          | proj₂ (fdf1 a da ada)
          = ⊚-valid (f a) (df1 a da) (proj₁ (fdf1 a da ada)) (df2 (a ⊕ da) (nil (a ⊕ da))) (valid-df2-a2-nila2 a da ada)
          , refl

    f⊚-correct : ∀ (f : A → B) → (df1 : fCh) → fvalid f df1 → (df2 : fCh) → fvalid (f f⊕ df1) df2 → (a : A) →
      (f f⊕ f⊚ df1 f df2) a ≡ ((f f⊕ df1) f⊕ df2) a
    f⊚-correct f df1 fdf1 df2 fdf2 a = ⊚-correct (f a) (df1 a (nil a)) (proj₁ (fdf1 a (nil a) (nil-valid a))) (df2 a (nil a)) (proj₁ (fdf2 a (nil a) (nil-valid a)))

  private
    funUpdateDiff : ∀ g f a → (f f⊕ (g f⊝ f)) a ≡ g a
  funUpdateDiff g f a rewrite update-nil a = update-diff (g a) (f a)
  funCA = record
    { Ch = A → Ch A → Ch B
    ; isChAlg = record
      { _⊕_ = _f⊕_
      ; _⊝_ = _f⊝_
      ; valid = fvalid
      ; _⊚[_]_ = f⊚
      ; ⊝-valid = f⊝-valid
      ; ⊕-⊝ = λ g f → ext (funUpdateDiff g f)
      ; ⊚-correct = λ f df1 fdf1 df2 fdf2 → ext (f⊚-correct f df1 fdf1 df2 fdf2)
      ; ⊚-valid = f⊚-valid
      } }

  private
    pCh = Ch A × Ch B
    _p⊕_ : A × B → Ch A × Ch B → A × B
    _p⊕_ (a , b) (da , db) = a ⊕ da , b ⊕ db
    _p⊝_ : A × B → A × B → pCh
    _p⊝_ (a2 , b2) (a1 , b1) = a2 ⊝ a1 , b2 ⊝ b1
    pvalid : A × B → pCh → Set (ℓ₂ ⊔ ℓ₁)
    pvalid (a , b) (da , db) = valid a da × valid b db
    p⊝-valid : (p1 p2 : A × B) → pvalid p1 (p2 p⊝ p1)
    p⊝-valid (a1 , b1) (a2 , b2) = ⊝-valid a1 a2 , ⊝-valid b1 b2
    p⊕-⊝ : (p2 p1 : A × B) → p1 p⊕ (p2 p⊝ p1) ≡ p2
    p⊕-⊝ (a2 , b2) (a1 , b1) = cong₂ _,_ (⊕-⊝ a2 a1) (⊕-⊝ b2 b1)
    _p⊚[_]_ : pCh → A × B → pCh → pCh
    (da1 , db1) p⊚[ a , b ] (da2 , db2) = da1 ⊚[ a ] da2 , db1 ⊚[ b ] db2
    p⊚-valid : (p : A × B) (dp1 : pCh) →
      pvalid p dp1 →
      (dp2 : pCh) → pvalid (p p⊕ dp1) dp2 → pvalid p (dp1 p⊚[ p ] dp2)
    p⊚-valid (a , b) (da1 , db1) (ada1 , bdb1) (da2 , db2) (ada2 , bdb2) = ⊚-valid a da1 ada1 da2 ada2 , ⊚-valid b db1 bdb1 db2 bdb2
    p⊚-correct : (p : A × B) (dp1 : pCh) →
      pvalid p dp1 →
      (dp2 : pCh) → pvalid (p p⊕ dp1) dp2 → p p⊕ (dp1 p⊚[ p ] dp2) ≡ (p p⊕ dp1) p⊕ dp2
    p⊚-correct (a , b) (da1 , db1) (ada1 , bdb1) (da2 , db2) (ada2 , bdb2) rewrite ⊚-correct a da1 ada1 da2 ada2 | ⊚-correct b db1 bdb1 db2 bdb2 = refl
  instance
    pairCA : ChAlg (A × B)
  pairCA = record
    { Ch = pCh
    ; isChAlg = record
    { _⊕_ = _p⊕_
    ; _⊝_ = _p⊝_
    ; valid = pvalid
    ; ⊝-valid = p⊝-valid
    ; ⊕-⊝ = p⊕-⊝
    ; _⊚[_]_ = _p⊚[_]_
    ; ⊚-valid = p⊚-valid
    ; ⊚-correct = p⊚-correct
    } }

  private
    SumChange = (Ch A ⊎ Ch B) ⊎ (A ⊎ B)

  data SumChange2 : Set (ℓ₁ ⊔ ℓ₂) where
    ch₁ : (da : Ch A) → SumChange2
    ch₂ : (db : Ch B) → SumChange2
    rp : (s : A ⊎ B) → SumChange2

  convert : SumChange → SumChange2
  convert (inj₁ (inj₁ da)) = ch₁ da
  convert (inj₁ (inj₂ db)) = ch₂ db
  convert (inj₂ s) = rp s
  convert₁ : SumChange2 → SumChange
  convert₁ (ch₁ da) = inj₁ (inj₁ da)
  convert₁ (ch₂ db) = inj₁ (inj₂ db)
  convert₁ (rp s) = inj₂ s

  data SValid : A ⊎ B → SumChange → Set (ℓ₁ ⊔ ℓ₂) where
    sv₁ : ∀ (a : A) (da : Ch A) (ada : valid a da) → SValid (inj₁ a) (convert₁ (ch₁ da))
    sv₂ : ∀ (b : B) (db : Ch B) (bdb : valid b db) → SValid (inj₂ b) (convert₁ (ch₂ db))
    svrp₁ : ∀ a1 b2 → SValid (inj₁ a1) (convert₁ (rp (inj₂ b2)))
    svrp₂ : ∀ b1 a2 → SValid (inj₂ b1) (convert₁ (rp (inj₁ a2)))

  inv1 : ∀ ds → convert₁ (convert ds) ≡ ds
  inv1 (inj₁ (inj₁ da)) = refl
  inv1 (inj₁ (inj₂ db)) = refl
  inv1 (inj₂ s) = refl
  inv2 : ∀ ds → convert (convert₁ ds) ≡ ds
  inv2 (ch₁ da) = refl
  inv2 (ch₂ db) = refl
  inv2 (rp s) = refl

  private
    s⊕2 : A ⊎ B → SumChange2 → A ⊎ B
    s⊕2 (inj₁ a) (ch₁ da) = inj₁ (a ⊕ da)
    s⊕2 (inj₂ b) (ch₂ db) = inj₂ (b ⊕ db)
    s⊕2 (inj₂ b) (ch₁ da) = inj₂ b -- invalid
    s⊕2 (inj₁ a) (ch₂ db) = inj₁ a -- invalid
    s⊕2 s (rp s₁) = s₁

    s⊕ : A ⊎ B → SumChange → A ⊎ B
    s⊕ s ds = s⊕2 s (convert ds)

    s⊝2 : A ⊎ B → A ⊎ B → SumChange2
    s⊝2 (inj₁ x2) (inj₁ x1) = ch₁ (x2 ⊝ x1)
    s⊝2 (inj₂ y2) (inj₂ y1) = ch₂ (y2 ⊝ y1)
    s⊝2 s2 s1 = rp s2

    s⊝ : A ⊎ B → A ⊎ B → SumChange
    s⊝ s2 s1 = convert₁ (s⊝2 s2 s1)

    s⊝-valid : (a b : A ⊎ B) → SValid a (s⊝ b a)
    s⊝-valid (inj₁ x1) (inj₁ x2) = sv₁ x1 (x2 ⊝ x1) (⊝-valid x1 x2)
    s⊝-valid (inj₂ y1) (inj₂ y2) = sv₂ y1 (y2 ⊝ y1) (⊝-valid y1 y2)
    s⊝-valid s1@(inj₁ x) s2@(inj₂ y) = svrp₁ x y
    s⊝-valid s1@(inj₂ y) s2@(inj₁ x) = svrp₂ y x

    s⊕-⊝ : (b a : A ⊎ B) → s⊕ a (s⊝ b a) ≡ b
    s⊕-⊝ (inj₁ x2) (inj₁ x1) rewrite ⊕-⊝ x2 x1 = refl
    s⊕-⊝ (inj₁ x2) (inj₂ y1) = refl
    s⊕-⊝ (inj₂ y2) (inj₁ x1) = refl
    s⊕-⊝ (inj₂ y2) (inj₂ y1) rewrite ⊕-⊝ y2 y1 = refl
    {-# TERMINATING #-}
    isSumCA : IsChAlg (A ⊎ B) SumChange
    s⊚-valid : (a : A ⊎ B) (da1 : SumChange) →
      SValid a da1 →
      (da2 : SumChange) →
      SValid (s⊕ a da1) da2 →
      SValid a (IsChAlg.default-⊚ isSumCA da1 a da2)
    s⊚-correct : (a : A ⊎ B) (da1 : SumChange) →
      SValid a da1 →
      (da2 : SumChange) →
      SValid (s⊕ a da1) da2 →
      s⊕ a (IsChAlg.default-⊚ isSumCA da1 a da2) ≡
      s⊕ (s⊕ a da1) da2

  instance
    sumCA : ChAlg (A ⊎ B)
  isSumCA = record
    { _⊕_ = s⊕
    ; _⊝_ = s⊝
    ; valid = SValid
    ; ⊝-valid = s⊝-valid
    ; ⊕-⊝ = s⊕-⊝
    ; _⊚[_]_ = IsChAlg.default-⊚ isSumCA
    ; ⊚-valid = s⊚-valid
    ; ⊚-correct = s⊚-correct
    }

  s⊚-valid = IsChAlg.default-⊚-valid isSumCA
  s⊚-correct = IsChAlg.default-⊚-correct isSumCA

  sumCA = record
    { Ch = SumChange
    ; isChAlg = isSumCA }

open import Data.Integer

instance
  intCA : ChAlg ℤ
intCA = record
  { Ch = ℤ
  ; isChAlg = record
  { _⊕_ = _+_
  ; _⊝_ = _-_
  ; valid = λ a b → ⊤
  ; ⊝-valid = λ a b → tt
  ; ⊕-⊝ = λ b a → n+[m-n]=m {a} {b}
  ; ⊚-valid = λ a da1 _ da2 _ → tt
  ; _⊚[_]_ = λ da1 a da2 → da1 + da2
  ; ⊚-correct = λ a da1 _ da2 _ → sym (associative-int a da1 da2)
  } }

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Issue620 where

module A where
  postulate _+_*_ : Set → Set → Set → Set

postulate X : Set

2X : Set
2X = X A.+ X * X

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

module Categories.Category.Complete.Properties {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Product
open import Relation.Binary

open import Categories.Category.Complete
open import Categories.Category.Complete.Finitely
open import Categories.Category.Construction.Functors
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Limit.Properties
open import Categories.Diagram.Equalizer.Limit C
open import Categories.Diagram.Cone.Properties
open import Categories.Object.Terminal
open import Categories.Object.Product.Limit C
open import Categories.Object.Terminal.Limit C
open import Categories.Functor
open import Categories.Functor.Limits
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)

import Categories.Category.Construction.Cones as Co
import Categories.Morphism.Reasoning as MR
import Categories.Morphism as Mor

-- exports
open import Categories.Category.Complete.Properties.Construction public
open import Categories.Category.Complete.Properties.SolutionSet public

private
  variable
    o′ ℓ′ e′ o″ ℓ″ e″ : Level
  module C = Category C

module _ (Com : Complete o′ ℓ′ e′ C) where

  Complete⇒FinitelyComplete : FinitelyComplete C
  Complete⇒FinitelyComplete = record
    { cartesian = record
      { terminal = limit⇒⊥ (Com (⊥⇒limit-F _ _ _))
      ; products = record
        { product = λ {A B} → limit⇒product (Com (product⇒limit-F _ _ _ A B))
        }
      }
    ; equalizer = complete⇒equalizer Com
    }

-- if the base category is complete, then the functor category is complete.
-- in addition, the evaluation functor is continuous.
--
--     Functors-Complete : Complete o″ ℓ″ e″ D^C
--     evalF-Continuous : ∀ X → Continuous o″ ℓ″ e″ (evalF C D X)

module _ {D : Category o′ ℓ′ e′} (Com : Complete o″ ℓ″ e″ D) where
  private
    D^C = Functors C D
    module D^C = Category D^C
    module D   = Category D

    module _ {J : Category o″ ℓ″ e″} (F : Functor J D^C) where
      private
        module J = Category J
        module F = Functor F
        open F
        module F₀ j = Functor (F₀ j)
        module F₁ {a b} (f : a J.⇒ b) = NaturalTransformation (F₁ f)

      ev : C.Obj → Functor D^C D
      ev = evalF C D

      F[-,_] : C.Obj → Functor J D
      F[-, X ] = ev X ∘F F

      F[-,-] : Functor C (Functors J D)
      F[-,-] = record
        { F₀           = F[-,_]
        ; F₁           = λ {A B} f → ntHelper record
          { η       = λ j → F₀.₁ j f
          ; commute = λ {j k} g → begin
            F₀.₁ k f D.∘ F₁.η g A D.∘ F₀.₁ j C.id   ≈⟨ pullˡ (F₁.sym-commute g f) ⟩
            (F₁.η g B D.∘ F₀.₁ j f) D.∘ F₀.₁ j C.id ≈⟨ elimʳ (F₀.identity _) ⟩
            F₁.η g B D.∘ F₀.₁ j f                   ≈⟨ introʳ (F₀.identity _) ⟩∘⟨refl ⟩
            (F₁.η g B D.∘ F₀.₁ j C.id) D.∘ F₀.₁ j f ∎
          }
        ; identity     = F₀.identity _
        ; homomorphism = F₀.homomorphism _
        ; F-resp-≈     = λ eq → F₀.F-resp-≈ _ eq
        }
        where open D.HomReasoning
              open MR D

      module F[-,-] = Functor F[-,-]

      module LimFX X = Limit (Com F[-, X ])
      open LimFX hiding (commute)

      K⇒lim : ∀ {X Y} (f : X C.⇒ Y) K → Co.Cones F[-, Y ] [ nat-map-Cone (F[-,-].₁ f) K , limit Y ]
      K⇒lim f K = rep-cone _ (nat-map-Cone (F[-,-].₁ f) K)

      lim⇒lim : ∀ {X Y} (f : X C.⇒ Y) → Co.Cones F[-, Y ] [ nat-map-Cone (F[-,-].₁ f) (limit X) , limit Y ]
      lim⇒lim f = K⇒lim f (limit _)

      module lim⇒lim {X Y} (f : X C.⇒ Y) = Co.Cone⇒ F[-, Y ] (lim⇒lim f)

      module FCone (K : Co.Cone F) where
        open Co.Cone F K public
        module N   = Functor N
        module ψ j = NaturalTransformation (ψ j)

      module FCone⇒ {K K′ : Co.Cone F} (K⇒K′ : Co.Cone⇒ F K K′) where
        open Co.Cone⇒ F K⇒K′ public
        module arr = NaturalTransformation arr

      FXcone : ∀ X → (K : Co.Cone F) → Co.Cone F[-, X ]
      FXcone X K = record
        { N    = N.₀ X
        ; apex = record
          { ψ       = λ j → ψ.η j X
          ; commute = λ f → D.∘-resp-≈ˡ (elimʳ (F₀.identity _)) ○ commute f
          }
        }
        where open FCone K
              open D.HomReasoning
              open MR D

      ⊤ : Co.Cone F
      ⊤ = record
        { N    = record
          { F₀           = λ X → apex X
          ; F₁           = λ {A B} f → lim⇒lim.arr f
          ; identity     = λ {X} →
            terminal.!-unique X record
            { arr     = D.id
            ; commute = D.identityʳ ○ ⟺ (elimˡ (F₀.identity _))
            }
          ; homomorphism = λ {X Y Z} {f g} →
            terminal.!-unique₂ Z
              {nat-map-Cone (F[-,-].₁ (g C.∘ f)) (limit X)}
              {terminal.! Z}
              {record { commute = λ {j} →
              begin
                proj Z j ∘ lim⇒lim.arr g ∘ lim⇒lim.arr f
                  ≈⟨ pullˡ (lim⇒lim.commute g) ⟩
                (F₀.₁ j g ∘ proj Y j) ∘ lim⇒lim.arr f
                  ≈⟨ pullʳ (lim⇒lim.commute f) ⟩
                F₀.₁ j g ∘ F₀.₁ j f ∘ proj X j
                  ≈˘⟨ pushˡ (F₀.homomorphism j) ⟩
                F₀.₁ j (g C.∘ f) ∘ proj X j
                  ∎ }}
          ; F-resp-≈     = λ {A B} {f g} eq → terminal.!-unique B record
            { commute = lim⇒lim.commute g ○ ∘-resp-≈ˡ (F₀.F-resp-≈ _ (C.Equiv.sym eq)) }
          }
        ; apex = record
          { ψ       = λ j → ntHelper record
            { η       = λ X → proj X j
            ; commute = λ _ → LimFX.commute _
            }
          ; commute = λ f {X} → ∘-resp-≈ˡ (introʳ (F₀.identity _)) ○ limit-commute X f
          }
        }
        where open D
              open D.HomReasoning
              open MR D

      K⇒⊤′ : ∀ X {K} → Co.Cones F [ K , ⊤ ] → Co.Cones F[-, X ] [ FXcone X K , LimFX.limit X ]
      K⇒⊤′ X {K} K⇒⊤ = record
        { arr     = arr.η X
        ; commute = comm
        }
        where open FCone⇒ K⇒⊤ renaming (commute to comm)

      complete : Limit F
      complete = record
        { terminal = record
          { ⊤             = ⊤
          ; ⊤-is-terminal = record
            { !        = λ {K} →
              let module K = FCone K
              in record
              { arr     = ntHelper record
                { η       = λ X → rep X (FXcone X K)
                ; commute = λ {X Y} f →
                  terminal.!-unique₂ Y
                    {nat-map-Cone (F[-,-].₁ f) (FXcone X K)}
                    {record { commute = λ {j} →
                    begin
                      proj Y j ∘ rep Y (FXcone Y K) ∘ K.N.₁ f ≈⟨ pullˡ (LimFX.commute Y) ⟩
                      K.ψ.η j Y ∘ K.N.F₁ f                    ≈⟨ K.ψ.commute j f ⟩
                      F₀.₁ j f ∘ K.ψ.η j X                    ∎ }}
                    {record { commute = λ {j} →
                    begin
                      proj Y j ∘ lim⇒lim.arr f ∘ rep X (FXcone X K) ≈⟨ pullˡ (lim⇒lim.commute f) ⟩
                      (F₀.₁ j f ∘ proj X j) ∘ rep X (FXcone X K)    ≈⟨ pullʳ (LimFX.commute X) ⟩
                      F₀.₁ j f ∘ K.ψ.η j X                          ∎ }}
                }
              ; commute = λ {_} {X} → LimFX.commute X
              }
            ; !-unique = λ K⇒⊤ {X} → terminal.!-unique X (K⇒⊤′ X K⇒⊤)
            }
          }
        }
        where open D
              open D.HomReasoning
              open MR D

      module _ (L : Limit F) (X : C.Obj) where
        module LimExpanded (L : Limit F) where
          private
            module L = Limit L
          open L public
          module apex   = Functor L.apex
          module proj j = NaturalTransformation (L.proj j)

        module L = LimExpanded L
        module complete = LimExpanded complete

        open MR D
        open D.HomReasoning

        cone-iso :  Mor._≅_ (Co.Cones F) complete.limit L.limit
        cone-iso = up-to-iso-cone F complete L
        module cone-iso where
          open Mor._≅_ cone-iso public
          module from where
            open Co.Cone⇒ F from public
            module arr = NaturalTransformation arr
          module to where
            open Co.Cone⇒ F to public
            module arr = NaturalTransformation arr

          ft-iso : Mor._≅_ D^C complete.apex L.apex
          ft-iso = Lim.up-to-iso F complete L
          module ft-iso = Mor._≅_ ft-iso

          apex-iso : ∀ X → Mor._≅_ D (complete.apex.₀ X) (L.apex.₀ X)
          apex-iso X = record
            { from = NaturalTransformation.η ft-iso.from X
            ; to   = NaturalTransformation.η ft-iso.to X
            ; iso  = record
              { isoˡ = ft-iso.isoˡ
              ; isoʳ = ft-iso.isoʳ
              }
            }

        ! : {K : Co.Cone F[-, X ]} → Co.Cone⇒ F[-, X ] K (F-map-Coneˡ (ev X) L.limit)
        ! {K} = record
          { arr     = cone-iso.from.arr.η X D.∘ rep X K
          ; commute = λ {j} → begin
            (L.proj.η j X D.∘ L.apex.₁ C.id) D.∘ cone-iso.from.arr.η X D.∘ rep X K
              ≈⟨ elimʳ L.apex.identity ⟩∘⟨refl ⟩
            L.proj.η j X D.∘ cone-iso.from.arr.η X D.∘ rep X K
              ≈⟨ pullˡ cone-iso.from.commute ⟩
            complete.proj.η j X D.∘ rep X K
              ≈⟨ LimFX.commute X {_} {K} ⟩
            ψ j
              ∎
          }
          where open Co.Cone _ K
        module ! K = Co.Cone⇒ _ (! {K})

        !-unique : {K : Co.Cone F[-, X ]} (f : Co.Cone⇒ F[-, X ] K (F-map-Coneˡ (ev X) L.limit)) →
                   !.arr K D.≈ Co.Cone⇒.arr f
        !-unique {K} f = ⟺ (switch-tofromˡ (cone-iso.apex-iso X) target)
          where open Co.Cone _ K
                module f = Co.Cone⇒ _ f
                target : cone-iso.to.arr.η X D.∘ f.arr D.≈ rep X K
                target = terminal.!-unique₂ X {K}
                         {record
                           { arr     = cone-iso.to.arr.η X D.∘ f.arr
                           ; commute = λ {j} → begin
                             proj X j D.∘ cone-iso.to.arr.η X D.∘ f.arr ≈⟨ pullˡ cone-iso.to.commute ⟩
                             L.proj.η j X D.∘ f.arr                     ≈⟨ introʳ L.apex.identity ⟩∘⟨refl ⟩
                             (L.proj.η j X D.∘ L.apex.₁ C.id) D.∘ f.arr ≈⟨ f.commute ⟩
                             ψ j                                        ∎
                           }}
                         {record
                           { arr     = rep X K
                           ; commute = λ {j} → begin
                             proj X j D.∘ rep X K                       ≈⟨ LimFX.commute X ⟩
                             ψ j                                        ∎
                           }}

        preserves : IsTerminal (Co.Cones F[-, X ]) (F-map-Coneˡ (ev X) L.limit)
        preserves = record
          { !        = !
          ; !-unique = !-unique
          }

  Functors-Complete : Complete o″ ℓ″ e″ D^C
  Functors-Complete = complete

  evalF-Continuous : ∀ X → Continuous o″ ℓ″ e″ (evalF C D X)
  evalF-Continuous X {J} {F} L = preserves F L X

max_stars_repo_name: turion/agda-categories

max_issues_repo_name: turion/agda-categories

max_forks_repo_name: turion/agda-categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Papers.Synthetic where

-- Cubical synthetic homotopy theory
-- Mörtberg and Pujet, „Cubical synthetic homotopy theory“.
-- https://dl.acm.org/doi/abs/10.1145/3372885.3373825

-- 2.1
import Agda.Builtin.Cubical.Path              as Path
import Cubical.Foundations.Prelude            as Prelude
-- 2.2
import Agda.Primitive.Cubical                 as PrimitiveCubical
import Cubical.Data.Bool                      as Bool
import Cubical.Core.Primitives                as CorePrimitives
-- 2.3
import Cubical.HITs.S1                        as S1
-- 2.4
import Cubical.Foundations.Equiv              as Equiv
import Cubical.Core.Glue                      as CoreGlue
import Cubical.Foundations.Univalence         as Univalence
-- 3.
import Cubical.HITs.Torus                     as T2
-- 3.1
import Cubical.Data.Int                       as Int
import Cubical.Data.Int.Properties            as IntProp
import Cubical.Foundations.Isomorphism        as Isomorphism
-- 4.1
import Cubical.HITs.Susp                      as Suspension
import Cubical.HITs.Sn                        as Sn
import Agda.Builtin.Nat                       as BNat
import Agda.Builtin.Bool                      as BBool
import Cubical.Foundations.GroupoidLaws       as GroupoidLaws
import Cubical.HITs.S2                        as S2
import Cubical.HITs.S3                        as S3
-- 4.2
import Cubical.HITs.Pushout                   as Push
import Cubical.HITs.Pushout.Properties        as PushProp
-- 4.3
import Cubical.HITs.Join                      as Join
import Cubical.HITs.Join.Properties           as JoinProp
-- 5.
import Cubical.HITs.Hopf                      as Hopf

--------------------------------------------------------------------------------
-- 2.  Cubical Agda
-- 2.1 The Interval and Path Types
-- 2.2 Transport and Composition
-- 2.3 Higher Inductive Types
-- 2.4 Glue Types and Univalence
--------------------------------------------------------------------------------

-- 2.1 The Interval and Path Types
open Path using (PathP) public
open Prelude using (_≡_ ; refl ; funExt) public
open Prelude renaming (sym to _⁻¹) public

-- 2.2 Transport and Composition
open Prelude using (transport ; subst ; J ; JRefl) public
open PrimitiveCubical using (Partial) public
open Bool using (Bool ; true ; false) public

partialBool : ∀ i → Partial (i ∨ ~ i) Bool
partialBool i = λ {(i = i1) → true
                 ; (i = i0) → false}

open CorePrimitives using (inS ; outS ; hcomp) public
open Prelude using (_∙_) public

-- 2.3 Higher Inductive Types
open S1 using (S¹ ; base ; loop) public

double : S¹ → S¹
double base = base
double (loop i) = (loop ∙ loop) i

-- 2.4 Glue Types and Univalence
open Equiv using (idEquiv) public
open CoreGlue using (Glue) public
open Univalence using (ua) public

--------------------------------------------------------------------------------
-- 3.  The Circle and Torus
-- 3.1 The Loop Spaces of the Circle and Torus
--------------------------------------------------------------------------------

open T2 using ( Torus ; point ; line1 ; line2 ; square
              ; t2c ; c2t ; c2t-t2c ; t2c-c2t ; Torus≡S¹×S¹)

-- 3.1 The Loop Spaces of the Circle and Torus
open S1 using (ΩS¹) public
open T2 using (ΩTorus) public
open Int using (Int ; pos ; negsuc) public
open IntProp using (sucPathInt) public
open S1 using (helix ; winding) public

-- Examples computing the winding numbers of the circle
_ : winding (loop ∙ loop ∙ loop) ≡ pos 3
_ = refl

_ : winding ((loop ⁻¹) ∙ loop ∙ (loop ⁻¹)) ≡ negsuc 0
_ = refl

open S1 renaming (intLoop to loopn) public
open S1 renaming (windingIntLoop to winding-loopn) public
open S1 using (encode ; decode ; decodeEncode ; ΩS¹≡Int) public
open Isomorphism using (isoToPath ; iso) public

-- Notation of the paper, current notation under ΩS¹≡Int
ΩS¹≡Int' : ΩS¹ ≡ Int
ΩS¹≡Int' = isoToPath (iso winding loopn
                      winding-loopn (decodeEncode base))

open T2 using (ΩTorus≡Int×Int ; windingTorus) public

-- Examples at the end of section 3.
_ : windingTorus (line1 ∙ line2) ≡ (pos 1 , pos 1)
_ = refl

_ : windingTorus ((line1 ⁻¹) ∙ line2 ∙ line1) ≡ (pos 0 , pos 1)
_ = refl

--------------------------------------------------------------------------------
-- 4.  Suspension, Spheres and Pushouts
-- 4.1 Suspension
-- 4.2 Pushouts and the 3 × 3 Lemma
-- 4.3 The Join and S³
--------------------------------------------------------------------------------

-- 4.1 Suspension
open Suspension using (Susp ; north ; south ; merid) public
open Sn using (S₊) public
open Suspension using ( SuspBool→S¹ ; S¹→SuspBool
                      ; SuspBool→S¹→SuspBool
                      ; S¹→SuspBool→S¹) public

-- Deprecated version of S₊
open BNat renaming (Nat to ℕ) hiding (_*_) public
open CorePrimitives renaming (Type to Set) public
open BBool using (Bool) public
-- At the time the paper was published, Set was used instead of Type
_-sphere : ℕ → Set
0 -sphere = Bool
(suc n) -sphere = Susp (n -sphere)

-- Lemma 4.1. The (1)-sphere is equal to the circle S1.

open BBool using (true ; false) public
-- Deprecated version of SuspBool→S¹
s2c : 1 -sphere → S¹
s2c north = base
s2c south = base
s2c (merid true i) = loop i
s2c (merid false i) = base -- (loop ⁻¹) i

-- Deprecated version of S¹→SuspBool
c2s : S¹ → 1 -sphere
c2s base = north
c2s (loop i) = (merid true ∙ (merid false ⁻¹)) i

open GroupoidLaws using (rUnit) public
-- Deprecated version of SuspBool→S¹→SuspBool
s2c-c2s : ∀ (p : S¹) → s2c (c2s p) ≡ p
s2c-c2s base = refl
s2c-c2s (loop i) j = rUnit loop (~ j) i

h1 : I → I → 1 -sphere
h1 i j = merid false (i ∧ j)

h2 : I → I → 1 -sphere
h2 i j = hcomp (λ k → λ { (i = i0) → north
                        ; (i = i1) → merid false (j ∨ ~ k)
                        ; (j = i1) → merid true i })
               (merid true i)

-- Deprecated version of S¹→SuspBool→S¹
c2s-s2c : ∀ (t : 1 -sphere) → c2s (s2c t) ≡ t
c2s-s2c north j = north
c2s-s2c south j = merid false j
c2s-s2c (merid true i) j = h2 i j
c2s-s2c (merid false i) j = merid false (i ∧ j)

-- Notation of the paper, current notation under S¹≡SuspBool
-- Proof of Lemma 4.1
1-sphere≡S¹ : 1 -sphere ≡ S¹
1-sphere≡S¹ = isoToPath (iso s2c c2s s2c-c2s c2s-s2c)

-- Definitions of S2 and S3
open S2 using (S²) public
open S3 using (S³) public

-- 4.2 Pushouts and the 3 × 3 Lemma
open Push using (Pushout) public
-- 3x3-span is implemented as a record
open PushProp using (3x3-span) public
open 3x3-span using (f□1) public
-- The rest of the definitions inside the 3x3-lemma
-- A□0-A○□ , A□○-A○□ ...
open 3x3-span using (3x3-lemma) public

-- 4.3 The Join and S³
open Join renaming (join to Join) using (S³≡joinS¹S¹) public
open JoinProp using (join-assoc) public

--------------------------------------------------------------------------------
-- 5.  The Hopf Fibration
--------------------------------------------------------------------------------

-- rot (denoted by _·_ here) in the paper is substituted by a rot and rotLoop in S1
open S1 using (_·_ ; rotLoop) public
open Hopf renaming ( HopfSuspS¹ to Hopf
                   ; JoinS¹S¹→TotalHopf to j2h
                   ; TotalHopf→JoinS¹S¹ to h2j)
          using (HopfS²) public
open S1 renaming (rotInv-1 to lem-rot-inv) public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-interpreter-full where
open import common public
open import well-typed-syntax
open import well-typed-syntax-interpreter

Contextε⇓ : Context⇓ ε
Contextε⇓ = tt

Typε⇓ : Typ ε → Set max-level
Typε⇓ T = Typ⇓ T Contextε⇓

Termε⇓ : {T : Typ ε} → Term T → Typε⇓ T
Termε⇓ t = Term⇓ t Contextε⇓

Typε▻⇓ : ∀ {A} → Typ (ε ▻ A) → Typε⇓ A → Set max-level
Typε▻⇓ T A⇓ = Typ⇓ T (Contextε⇓ , A⇓)

Termε▻⇓ : ∀ {A} → {T : Typ (ε ▻ A)} → Term T → (x : Typε⇓ A) → Typε▻⇓ T x
Termε▻⇓ t x = Term⇓ t (Contextε⇓ , x)

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


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

open import HoTT

open import stash.modalities.Orthogonality

module stash.modalities.Nullification where

module _ {i} where

  postulate -- HIT
    P⟨_⟩ : (A X : Type i) → Type i
    p[_] : {A X : Type i} → X → P⟨ A ⟩ X
    is-orth : {A X : Type i} → ⟦ A ⊥ P⟨ A ⟩ X ⟧

  module NullElim {A X : Type i} {Q : P⟨ A ⟩ X → Type i}
    (p : (x : P⟨ A ⟩ X) → ⟦ A ⊥ Q x ⟧) (d : (x : X) → Q p[ x ]) where

    postulate
      f : Π (P⟨ A ⟩ X) Q
      p[_]-β : ∀ x → f p[ x ] ↦ d x
    {-# REWRITE p[_]-β #-}

open NullElim public renaming (f to Null-elim)

module _ {i} (A : Type i) where

  NullModality : Modality i
  Modality.is-local NullModality X = ⟦ A ⊥ X ⟧
  Modality.is-local-is-prop NullModality = is-equiv-is-prop
  Modality.◯ NullModality = P⟨ A ⟩
  Modality.◯-is-local NullModality = is-orth
  Modality.η NullModality = p[_]
  Modality.◯-elim NullModality = Null-elim
  Modality.◯-elim-β NullModality _ _ _ = idp
  Modality.◯-=-is-local NullModality x y = pths-orth is-orth

module _ {i} (A X : Type i) where

  f-aux : (x : P⟨ Susp A ⟩ X) → P⟨ A ⟩ (x == x)
  f-aux = Null-elim (λ x → susp-≻ A (P⟨ A ⟩ (x == x)) is-orth) (λ x → p[ idp ])

  f : (x y : P⟨ Susp A ⟩ X) → x == y → P⟨ A ⟩ (x == y)
  f x .x idp = f-aux x

module _ {i} {A B : Type i} (f : A → B) where

  ap-fib-to : {a₀ a₁ : A} (p : f a₀ == f a₁) → hfiber (ap f) p
    → Σ (hfiber f (f a₀)) (λ α →
       Σ (hfiber f (f a₁)) (λ β →
       Σ (fst α == fst β) (λ q →
       ap f q == snd α ∙ p ∙ ! (snd β))))
  ap-fib-to {a₀} {a₁} .(ap f q) (q , idp) = (a₀ , idp) , (a₁ , idp) , q , ! (∙-unit-r (ap f q))

  postulate
    ap-fib : {a₀ a₁ : A} (p : f a₀ == f a₁) → is-equiv (ap-fib-to p)

  new-ap-fib : {a₀ a₁ : A} (p : f a₀ == f a₁) → hfiber (ap f) p
    → Σ (hfiber f (f a₀)) (λ α →
       Σ (hfiber f (f a₁)) (λ β →
       α == β [ (λ z → hfiber f z) ↓ p ]))
  new-ap-fib = {!!}

module _ {i} (A X : Type i) (x y : X) where

  module NMA = Modality (NullModality A)
  module NMSA = Modality (NullModality (Susp A))

  -- Okay.  Here is the map in question:
  pΣ : x == y → Path {A = P⟨ Susp A ⟩ X} p[ x ] p[ y ]
  pΣ = ap p[_]

  lemma : NMSA.is-◯-equiv pΣ
  lemma p = NMSA.equiv-preserves-◯-conn ((ap-fib-to p[_] p , ap-fib p[_] p) ⁻¹)
              {!!}

  thm : NMA.is-◯-equiv pΣ
  thm p = {!!}

  -- equiv-preserves-◯-conn : {A B : Type ℓ} → A ≃ B → is-◯-connected A → is-◯-connected B
  -- equiv-preserves-◯-conn e c = equiv-preserves-level (◯-emap e) c

  -- Okay, here's a better explanation: you are simply applying the
  -- full fledged join adjunction formula to the p[_].  I think
  -- the diagonal of this map will have fibers which are exactly
  -- the PathOver description you give above.  Or something
  -- very close to this.  That's the main idea.

  -- Theorem 19.1 of CwA and PA asserts that this map
  -- is A-connected.  Have to trace through the argument.
  -- So we don't contruct a direct inverse ...

  -- He starts by observing that it is ΣA-connected.
  -- Do you have a proof of this?  It should be obvious ...

  -- So by adjuction, loops on this fiber is A-connected.

  -- Then the claim is that you can commute with limits, i.e.
  -- that this is the fiber on loops of the canoncial map.

  -- Right.  This is much clearer.  We'll need some preparation,
  -- but I think this should be quite doable.

  -- this map is fairly easy by adjunction ...
  to : P⟨ A ⟩ (x == y) → (Path {A = P⟨ Susp A ⟩ X} p[ x ] p[ y ])
  to = Null-elim (λ p → adj-orth A (P⟨ Susp A ⟩ X) is-orth p[ x ] p[ y ]) (λ p → ap p[_] p)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Categories where

open import Library

record Cat {a b} : Set (lsuc (a ⊔ b)) where
  field Obj  : Set a
        Hom  : Obj → Obj → Set b
        iden : ∀{X} → Hom X X
        comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
        idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≅ f
        idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≅ f
        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
               comp (comp f g) h ≅ comp f (comp g h)
open Cat

_Op : ∀{a b} →  Cat {a}{b} → Cat
C Op = record{
  Obj  = Obj C;
  Hom  = λ X Y → Hom C Y X;
  iden = iden C;
  comp = λ f g → comp C g f;
  idl  = idr C;
  idr  = idl C;
  ass  = sym (ass C)}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module list where

module List (A : Set) where

  data List : Set where
    nil  : List
    _::_ : A -> List -> List

  _++_ : List -> List -> List
  nil       ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)


text:
module x01-842Naturals-hc-2 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

one : ℕ
one = suc zero

two : ℕ
two = suc (suc zero)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

_ : seven ≡ 7
_ = refl

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

_ : 2 + 3 ≡ 5
_ = refl

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- many steps condensed
    5
  ∎

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

_ =
  begin
    2 * 3
  ≡⟨⟩    -- many steps condensed
    6
  ∎

_ : 3 * 4 ≡ 12
_ = refl

_^_ : ℕ → ℕ → ℕ
m ^ zero  = suc zero
m ^ suc n = m * (m ^ n)

_ : 2 ^ 0 ≡ 1
_ = refl

_ : 2 ^ 1 ≡ 2
_ = refl

_ : 2 ^ 2 ≡ 4
_ = refl

_ : 2 ^ 3 ≡ 8
_ = refl

_ : 3 ^ 3 ≡ 27
_ = refl

_∸_ : ℕ → ℕ → ℕ
zero  ∸     n = zero
m     ∸  zero = m
suc m ∸ suc n = m ∸ n

_ : 3 ∸ 2 ≡ 1
_ = refl

_ : 2 ∸ 3 ≡ 0
_ = refl

infixl 6  _+_  _∸_
infixl 7  _*_

{-# BUILTIN NATPLUS  _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

-- Binary representation.

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

-- Our representation of zero is different from PLFA.
-- We use the empty sequence of bits (more consistent).

bin-zero : Bin-ℕ
bin-zero = bits

bin-one : Bin-ℕ
bin-one = bits x1     -- 1 in binary

bin-two : Bin-ℕ
bin-two = bits x1 x0  -- 10 in binary

-- 842 exercise: Increment (1 point)
-- Define increment (add one).

inc : Bin-ℕ → Bin-ℕ
inc  bits  = bits x1
inc (m x0) = m    x1
inc (m x1) = (inc m) x0

_ : inc (bits) ≡ bits x1
_ = refl
_ : inc (bits          x1) ≡ bits       x1 x0
_ = refl
_ : inc (bits       x1 x0) ≡ bits       x1 x1
_ = refl
_ : inc (bits       x1 x1) ≡ bits    x1 x0 x0
_ = refl
_ : inc (bits    x1 x0 x0) ≡ bits    x1 x0 x1
_ = refl
_ : inc (bits    x1 x0 x1) ≡ bits    x1 x1 x0
_ = refl
_ : inc (bits    x1 x1 x0) ≡ bits    x1 x1 x1
_ = refl
_ : inc (bits    x1 x1 x1) ≡ bits x1 x0 x0 x0
_ = refl
_ : inc (bits x1 x0 x1 x1) ≡ bits x1 x1 x0 x0
_ = refl

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc m) = suc (suc (dbl m))

tob : ℕ → Bin-ℕ
tob  zero   = bits
tob (suc m) = inc (tob m)

fromb : Bin-ℕ → ℕ
fromb  bits  = zero
fromb (n x0) =      dbl (fromb n)
fromb (n x1) = suc (dbl (fromb n))

_ : tob 6 ≡ bits x1 x1 x0
_ = refl

_ : fromb  bits           ≡ 0
_ = refl
_ : fromb (bits       x0) ≡ 0
_ = refl
_ : fromb (bits       x1) ≡ 1
_ = refl
_ : fromb (bits    x1 x0) ≡ 2
_ = refl
_ : fromb (bits    x1 x1) ≡ 3
_ = refl
_ : fromb (bits x1 x1 x0) ≡ 6
_ = refl
_ : fromb (bits x1 x1 x0) ≡ 6
_ = refl

-- Do NOT use 'to' and 'from'. Work with Bin-ℕ as if ℕ did not exist.
_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
bits   bin-+     n  =                    n
m      bin-+  bits  =            m
(m x0) bin-+ (n x0) =           (m bin-+ n) x0
(m x0) bin-+ (n x1) =      inc ((m bin-+ n) x0)
(m x1) bin-+ (n x0) =      inc ((m bin-+ n) x0)
(m x1) bin-+ (n x1) = inc (inc ((m bin-+ n) x0))

_ : (bits x1 x0 x0 x0) bin-+ (bits x1) ≡ (bits x1 x0 x0 x1)
_ = refl
_ : (bits x1 x0 x0 x1) bin-+ (bits x1) ≡ (bits x1 x0 x1 x0)
_ = refl
_ : (bits x1 x0 x0 x0) bin-+ (bits x1 x1 x1) ≡ (bits x1 x1 x1 x1)
_ = refl
_ : (tob 6) bin-+ (tob 2) ≡ (tob 8)
_ = refl
_ : (bits x1 x0) bin-+ (bits x1 x1) ≡ (bits x1 x0 x1)
_ = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-

A simpler definition of truncation ∥ A ∥ n from n ≥ -1

Note that this uses the HoTT book's indexing, so it will be off
 from `∥_∥_` in HITs.Truncation.Base by -2

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Truncation.Base where

open import Cubical.Data.NatMinusOne renaming (suc₋₁ to suc)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.Sn.Base
open import Cubical.Data.Nat.Base renaming (suc to sucℕ)
open import Cubical.Data.Unit.Base
open import Cubical.Data.Empty

-- this definition is off by one. Use hLevelTrunc or ∥_∥ for truncations
-- (off by 2 w.r.t. the HoTT-book)
data HubAndSpoke {ℓ} (A : Type ℓ) (n : ℕ) : Type ℓ where
  ∣_∣ : A  → HubAndSpoke A n
  hub : (f : S₊ n → HubAndSpoke A n) → HubAndSpoke A n
  spoke : (f : S₊ n → HubAndSpoke A n) (x : S₊ n) → hub f ≡ f x

hLevelTrunc : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → Type ℓ
hLevelTrunc zero A = Unit*
hLevelTrunc (sucℕ n) A = HubAndSpoke A n

∥_∥_ : ∀ {ℓ} (A : Type ℓ) (n : ℕ) → Type ℓ
∥ A ∥ n = hLevelTrunc n A

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --guardedness-preserving-type-constructors #-}

open import Agda.Builtin.Coinduction
open import Agda.Builtin.IO
open import Agda.Builtin.Unit

data Rec (A : ∞ Set) : Set where
  fold : ♭ A → Rec A

D : Set
D = Rec (♯ (∞ D))

d : D
d = fold (♯ d)

postulate
  seq    : {A B : Set} → A → B → B
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \_   -> return #-}
{-# COMPILE GHC seq    = \_ _ -> seq    #-}

main : IO ⊤
main = seq d (return tt)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module FlatDomInequality-2 where

postulate
  A : Set

h : (@♭ x : A) → A
h x = x

q : A → A
q = h

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module thms where

open import bool-thms public
open import bool-thms2 public
open import list-thms public
open import list-thms2 public
open import maybe-thms public
open import product-thms public
open import string-thms public
open import sum-thms public
open import nat-thms public
open import trie-thms public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --no-positivity-check #-}
open import Prelude hiding (id; Bool; _∷_; [])

module Examples.Bad where

data TC : Set where
  tc-int : TC
  tc-bool : TC
  tc-char : TC

_tc≟_ : (a b : TC) → Dec (a ≡ b)
tc-int tc≟ tc-int = yes refl
tc-int tc≟ tc-bool = no (λ ())
tc-bool tc≟ tc-int = no (λ ())
tc-bool tc≟ tc-bool = yes refl
tc-int tc≟ tc-char = no (λ ())
tc-bool tc≟ tc-char = no (λ ())
tc-char tc≟ tc-int = no (λ ())
tc-char tc≟ tc-bool = no (λ ())
tc-char tc≟ tc-char = yes refl

open import Implicits.Oliveira.Types TC _tc≟_
open import Implicits.Oliveira.Terms TC _tc≟_
open import Implicits.Oliveira.Contexts TC _tc≟_
open import Implicits.Oliveira.WellTyped TC _tc≟_
open import Implicits.Oliveira.Substitutions TC _tc≟_
open import Implicits.Oliveira.Types.Unification TC _tc≟_
open import Implicits.Improved.Undecidable.Resolution TC _tc≟_
open import Data.Maybe
open import Data.List
open import Extensions.ListFirst

Bool : ∀ {n} → Type n
Bool = simpl (tc tc-bool)

Int : ∀ {n} → Type n
Int = simpl (tc tc-int)

Char : ∀ {n} → Type n
Char = simpl (tc tc-char)

module Ex₀ where

  data Bad : Set where
    bad : ¬ Bad → Bad

  getFun : Bad → ¬ Bad
  getFun (bad x) = x

  omega : Bad → ⊥
  omega b = getFun b b

  loop : ⊥
  loop = omega (bad omega)

module Ex₁ where

  Δ : ICtx zero
  Δ = Bool ⇒ Bool ∷ Bool ∷ []

  Bad : Set
  Bad = Δ ⊢ (Bool ⇒ Bool ) ↓ (tc tc-bool)

  getFun : Bad → ¬ Bad
  getFun (i-iabs (r-simp (here p ._)) x₁) = {!!}
  getFun (i-iabs (r-simp (there ._ f x)) y) = f

  omega : Bad → ⊥
  omega b = getFun b b

  bad : ¬ Bad → Bad
  bad ¬x = i-iabs (r-simp (there _ ¬x (here (i-simp (tc tc-bool)) []))) (i-simp (tc tc-bool))

  loop : ⊥
  loop = omega (bad omega)


text:
module nouse_CollatzProof where

open import Data.Nat

-- 偽
data ⊥ : Set where
-- 真
record ⊤ : Set where

-- 選言
data _∨_ (P Q : Set) : Set where
  ∨Intro1 : P → P ∨ Q
  ∨Intro2 : Q → P ∨ Q
∨Elim : {P Q R : Set} → P ∨ Q  →  (P → R) → (Q → R) → R
∨Elim (∨Intro1 a) prfP _ = prfP a
∨Elim (∨Intro2 b) _ prfQ = prfQ b

-- 否定
¬ : Set → Set
¬ p = p → ⊥
⊥Elim : {P : Set} → ⊥ → P
⊥Elim ()

postulate
  LEM : (P : Set) → (P ∨ ¬ P)
  smaller : ℕ → Set
  -- n:左端からの連続するビット1
  -- k+2で小さくならない→k+1で小さくならない
  lemma1-3 : (k : ℕ) → ¬ (smaller (suc (suc k))) → ¬ (smaller (suc k))
  lemma2   : smaller 0 -- evenは小さくなる
  lemma3   : smaller 1 -- 4x+1は小さくなる

-- 二重否定除去
DNE1 : {p : Set} → p → ¬ (¬ p)
DNE1 p q = q p
DNE2 : {p : Set} → ¬ (¬ p) → p
DNE2 {p0} p1 = ∨Elim (LEM p0) (λ y → y) (λ z → ⊥Elim (p1 z))

-- 対偶
contraposition : {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition = λ f g x → g (f x)
contraposition2 : {A B : Set} → (¬ B → ¬ A) → (A → B)
contraposition2 p a =
  let t = (contraposition p) (DNE1 a) in DNE2 t

-- 本論
-- n:最下位からの連続するビット1
proof : (n : ℕ) → smaller n
proof zero          = lemma2 -- even
proof (suc zero)    = lemma3 -- 4x+1
proof (suc (suc n)) = part n (proof (suc n))
  where
    -- （k+2で小さくならない→k+1で小さくならない）→（k+1で小さくなる→k+2で小さくなる）
    part : (k : ℕ) → smaller (suc k) → smaller (suc (suc k))
    part k = contraposition2 (lemma1-3 k)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definition of and lemmas related to "true infinitely often"
------------------------------------------------------------------------

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

module Data.Nat.InfinitelyOften where

open import Category.Monad using (RawMonad)
open import Level using (0ℓ)
open import Data.Empty using (⊥-elim)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map)
open import Data.Sum hiding (map)
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
open import Relation.Unary using (Pred; _∪_; _⊆_)
open RawMonad (¬¬-Monad {p = 0ℓ})

-- Only true finitely often.

Fin : ∀ {ℓ} → Pred ℕ ℓ → Set ℓ
Fin P = ∃ λ i → ∀ j → i ≤ j → ¬ P j

-- A non-constructive definition of "true infinitely often".

Inf : ∀ {ℓ} → Pred ℕ ℓ → Set ℓ
Inf P = ¬ Fin P

-- Fin is preserved by binary sums.

_∪-Fin_ : ∀ {ℓp ℓq P Q} → Fin {ℓp} P → Fin {ℓq} Q → Fin (P ∪ Q)
_∪-Fin_ {P = P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
  where
  open ≤-Reasoning

  helper : ∀ k → i ⊔ j ≤ k → ¬ (P ∪ Q) k
  helper k i⊔j≤k (inj₁ p) = ¬p k (begin
    i      ≤⟨ m≤m⊔n i j ⟩
    i ⊔ j  ≤⟨ i⊔j≤k ⟩
    k      ∎) p
  helper k i⊔j≤k (inj₂ q) = ¬q k (begin
    j      ≤⟨ m≤m⊔n j i ⟩
    j ⊔ i  ≡⟨ ⊔-comm j i ⟩
    i ⊔ j  ≤⟨ i⊔j≤k ⟩
    k      ∎) q

-- Inf commutes with binary sums (in the double-negation monad).

commutes-with-∪ : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
commutes-with-∪ p∪q =
  call/cc λ ¬[p⊎q] →
  (λ ¬p ¬q → ⊥-elim (p∪q (¬p ∪-Fin ¬q)))
    <$> ¬[p⊎q] ∘ inj₁ ⊛ ¬[p⊎q] ∘ inj₂

-- Inf is functorial.

map : ∀ {ℓp ℓq P Q} → P ⊆ Q → Inf {ℓp} P → Inf {ℓq} Q
map P⊆Q ¬fin = ¬fin ∘ Prod.map id (λ fin j i≤j → fin j i≤j ∘ P⊆Q)

-- Inf is upwards closed.

up : ∀ {ℓ P} n → Inf {ℓ} P → Inf (P ∘ _+_ n)
up     zero    = id
up {P = P} (suc n) = up n ∘ up₁
  where
  up₁ : Inf P → Inf (P ∘ suc)
  up₁ ¬fin (i , fin) = ¬fin (suc i , helper)
    where
    helper : ∀ j → 1 + i ≤ j → ¬ P j
    helper ._ (s≤s i≤j) = fin _ i≤j

-- A witness.

witness : ∀ {ℓ P} → Inf {ℓ} P → ¬ ¬ ∃ P
witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))

-- Two different witnesses.

twoDifferentWitnesses
  : ∀ {P} → Inf P → ¬ ¬ ∃₂ λ m n → m ≢ n × P m × P n
twoDifferentWitnesses inf =
  witness inf                     >>= λ w₁ →
  witness (up (1 + proj₁ w₁) inf) >>= λ w₂ →
  return (_ , _ , m≢1+m+n (proj₁ w₁) , proj₂ w₁ , proj₂ w₂)


text:
-- 2010-10-14

{-# OPTIONS --universe-polymorphism #-}

module FakeProjectionsDoNotPreserveGuardedness where

-- Coinduction is only available with universe polymorphism

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

infixl 6 _⊔_

-- Coinduction

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

-- Products

infixr 4 _,_
infixr 2 _×_

-- fake product with projections
postulate
  _×_   : (A B : Set) → Set
  _,_   : {A B : Set}(a : A)(b : B) → A × B
  proj₁ : {A B : Set}(p : A × B) → A
  proj₂ : {A B : Set}(p : A × B) → B

-- Streams

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

mutual

  repeat : {A : Set}(a : A) → Stream A
  repeat a = a ∷ proj₂ (repeat' a)

  repeat' : {A : Set}(a : A) → A × ∞ (Stream A)
  repeat' a = a , ♯ repeat a

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout

module lib.types.Join  where

module _ {i j} (A : Type i) (B : Type j) where

  *-span : Span
  *-span = span A B (A × B) fst snd

  _*_ : Type _
  _*_ = Pushout *-span

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

  *-⊙span : ⊙Span
  *-⊙span = ⊙span X Y (X ⊙× Y) ⊙fst ⊙snd

  _⊙*_ : Ptd _
  _⊙*_ = ⊙Pushout *-⊙span

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module RandomAccessList.Redundant.Core.Properties where

open import BuildingBlock
open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)
open import RandomAccessList.Redundant.Core

open import Data.Num.Redundant
open import Data.Num.Redundant.Properties

open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Etc
open import Data.Nat.Properties.Simple
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

⟦[]⟧≈zero∷[] : ∀ {n A} → (xs : 0-2-RAL A n) → {xs≣[] : xs ≡ []} → ⟦ xs ⟧ ≈ zero ∷ []
⟦[]⟧≈zero∷[] {n} {A} [] = <<<-zero n [] {eq refl}
⟦[]⟧≈zero∷[] (      0∷ xs) {()}
⟦[]⟧≈zero∷[] (x     1∷ xs) {()}
⟦[]⟧≈zero∷[] (x , y 2∷ xs) {()}

--------------------------------------------------------------------------------
-- On ⟦_⟧ and ⟦_⟧ₙ

{-
⟦[]⟧ₙ≡0 : ∀ {A n} → (xs : 0-2-RAL A n) → {xs≣[] : xs ≡ []} → ⟦ xs ⟧ₙ ≡ zero ∷ []
⟦[]⟧ₙ≡0 []                 = refl
⟦[]⟧ₙ≡0 (      0∷ xs) {()}
⟦[]⟧ₙ≡0 (x     1∷ xs) {()}
⟦[]⟧ₙ≡0 (x , y 2∷ xs) {()}

⟦[]⟧≡0 : ∀ {n A} → (xs : 0-2-RAL A n) → {xs≣[] : xs ≡ []} → ⟦ xs ⟧ ≡ zero ∷ []
⟦[]⟧≡0 {n}    []     {p}  =
    begin
        n <<< (zero ∷ [])
    ≡⟨ {!   !} ⟩
        zero ∷ []
    ∎
⟦[]⟧≡0 (      0∷ xs) {()}
⟦[]⟧≡0 (x     1∷ xs) {()}
⟦[]⟧≡0 (x , y 2∷ xs) {()}
-- identity
⟦[]⟧ₙ≡0 : ∀ {A n} → (xs : 0-2-RAL A n) → xs ≡ [] → ⟦ xs ⟧ₙ ≡ zero
⟦[]⟧ₙ≡0 []            p  = refl
⟦[]⟧ₙ≡0 (      0∷ xs) ()
⟦[]⟧ₙ≡0 (x     1∷ xs) ()
⟦[]⟧ₙ≡0 (x , y 2∷ xs) ()

⟦[]⟧≡0 : ∀ {n A} → (xs : 0-2-RAL A n) → xs ≡ [] → ⟦ xs ⟧ ≡ 0
⟦[]⟧≡0 {zero }    [] p  = refl
⟦[]⟧≡0 {suc n}    [] p  = *-right-zero (2 * 2 ^ n)
⟦[]⟧≡0 (      0∷ xs) ()
⟦[]⟧≡0 (x     1∷ xs) ()
⟦[]⟧≡0 (x , y 2∷ xs) ()

⟦0∷xs⟧≡⟦xs⟧ : ∀ {n A} → (xs : 0-2-RAL A (suc n)) → ⟦ 0∷ xs ⟧ ≡ ⟦ xs ⟧
⟦0∷xs⟧≡⟦xs⟧ {zero} xs = +-right-identity (2 * ⟦ xs ⟧ₙ)
⟦0∷xs⟧≡⟦xs⟧ {suc n} xs =
    begin
        2 * 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ sym (*-assoc (2 * 2 ^ n) 2 ⟦ xs ⟧ₙ) ⟩
        ((2 * 2 ^ n) * 2) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ x → x * ⟦ xs ⟧ₙ) (*-comm (2 * 2 ^ n) 2) ⟩
        (2 * (2 * 2 ^ n)) * ⟦ xs ⟧ₙ
    ∎

⟦[]⟧≡⟦[]⟧ : ∀ {m n A} → ⟦ [] {A} {m} ⟧ ≡ ⟦ [] {A} {n} ⟧
⟦[]⟧≡⟦[]⟧ {m} {n} =
    begin
        2 ^ m * 0
    ≡⟨ *-right-zero (2 ^ m) ⟩
        0
    ≡⟨ sym (*-right-zero (2 ^ n)) ⟩
        2 ^ n * 0
    ∎

splitIndex : ∀ {n A} → (x : BinaryLeafTree A n) → (xs : 0-2-RAL A (suc n)) → ⟦ x 1∷ xs ⟧ ≡ 1 * (2 ^ n) + ⟦ xs ⟧
splitIndex {n} x xs =
    begin
        2 ^ n * suc (2 * ⟦ xs ⟧ₙ)
    ≡⟨ +-*-suc (2 ^ n) (2 * ⟦ xs ⟧ₙ) ⟩
        2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (λ w → 2 ^ n + w) (sym (*-assoc (2 ^ n) 2 ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + (2 ^ n * 2) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + w * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        2 ^ n + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → w + (2 * 2 ^ n) * ⟦ xs ⟧ₙ) (sym (+-right-identity (2 ^ n))) ⟩
        2 ^ n + 0 + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ∎

splitIndex2 : ∀ {n A} → (x : BinaryLeafTree A n) → (y : BinaryLeafTree A n) → (xs : 0-2-RAL A (suc n)) → ⟦ x , y 2∷ xs ⟧ ≡ 2 * (2 ^ n) + ⟦ xs ⟧
splitIndex2 {n} x y xs =
    begin
        2 ^ n * (1 + (1 + (2 * ⟦ xs ⟧ₙ)))
    ≡⟨ +-*-suc (2 ^ n) ((1 + (2 * ⟦ xs ⟧ₙ))) ⟩
        2 ^ n + 2 ^ n * (1 + (2 * ⟦ xs ⟧ₙ))
    ≡⟨ cong (λ w → 2 ^ n + w) (+-*-suc (2 ^ n) (2 * ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + (2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ))
    ≡⟨ sym (+-assoc (2 ^ n) (2 ^ n) (2 ^ n * (2 * ⟦ xs ⟧ₙ))) ⟩
        2 ^ n + 2 ^ n + 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ cong (λ w → 2 ^ n + 2 ^ n + w) (sym (*-assoc (2 ^ n) 2 ⟦ xs ⟧ₙ)) ⟩
        2 ^ n + 2 ^ n + (2 ^ n * 2) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + 2 ^ n + w * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        2 ^ n + 2 ^ n + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ w → 2 ^ n + w + (2 * 2 ^ n) * ⟦ xs ⟧ₙ) (sym (+-right-identity (2 ^ n))) ⟩
        2 ^ n + (2 ^ n + 0) + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ≡⟨ refl ⟩
        2 * 2 ^ n + (2 * 2 ^ n) * ⟦ xs ⟧ₙ
    ∎

    begin
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ≡⟨ {!   !} ⟩
        {!   !}
    ∎
-}

{-
⟦[]⟧≡⟦[]⟧ : ∀ {n A} → ⟦ [] {A} {suc n} ⟧ ≡ ⟦ [] {A} {n} ⟧
⟦[]⟧≡⟦[]⟧ {n} =
    begin
        (2 * 2 ^ n) * 0
    ≡⟨ *-right-zero (2 * 2 ^ n) ⟩
        0
    ≡⟨ sym (*-right-zero (2 ^ n)) ⟩
        2 ^ n * 0
    ∎

⟦0∷xs⟧≡⟦xs⟧ {zero} xs = +-right-identity (2 * ⟦ xs ⟧ₙ)
⟦0∷xs⟧≡⟦xs⟧ {suc n} xs =
    begin
        2 * 2 ^ n * (2 * ⟦ xs ⟧ₙ)
    ≡⟨ sym (*-assoc (2 * 2 ^ n) 2 ⟦ xs ⟧ₙ) ⟩
        2 * 2 ^ n * 2 * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ x → x * ⟦ xs ⟧ₙ) (*-assoc 2 (2 ^ n) 2) ⟩
        2 * (2 ^ n * 2) * ⟦ xs ⟧ₙ
    ≡⟨ cong (λ x → 2 * x * ⟦ xs ⟧ₙ) (*-comm (2 ^ n) 2) ⟩
        (2 * (2 * 2 ^ n)) * ⟦ xs ⟧ₙ
    ∎

⟦0∷xs⟧≢0⇒⟦xs⟧≢0  : ∀ {n A}
                → (xs : 0-1-RAL A (suc n))
                → ⟦ 0∷ xs ⟧ ≢ 0
                → ⟦ xs ⟧ ≢ 0
⟦0∷xs⟧≢0⇒⟦xs⟧≢0 xs p = contraposition (trans (⟦0∷xs⟧≡⟦xs⟧ xs)) p
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

open import Fragment.Equational.Theory

module Fragment.Equational.Model.Synthetic (Θ : Theory) where

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Algebra (Σ Θ)
open import Fragment.Algebra.Free (Σ Θ)
open import Fragment.Algebra.Homomorphism (Σ Θ)
open import Fragment.Algebra.Quotient (Σ Θ)
open import Fragment.Equational.Model.Base Θ
  using (Model; IsModel; Models)
open import Fragment.Setoid.Morphism using (_·_)

open import Level using (Level; _⊔_)
open import Function using (_∘_)

open import Data.Empty using (⊥)
open import Data.Nat using (ℕ)
open import Data.Product using (proj₁; proj₂)
open import Data.Vec using (map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid; IsEquivalence)
import Relation.Binary.PropositionalEquality as PE

private
  variable
    a ℓ : Level

module _ (A : Algebra {a} {ℓ}) where

  infix 4 _≊_

  data _≊_ : ∥ A ∥ → ∥ A ∥ → Set (a ⊔ ℓ) where
    refl    : ∀ {x} → x ≊ x
    sym     : ∀ {x y} → x ≊ y → y ≊ x
    trans   : ∀ {x y z} → x ≊ y → y ≊ z → x ≊ z
    inherit : ∀ {x y} → x =[ A ] y → x ≊ y
    cong    : ∀ {n} → (f : ops (Σ Θ) n)
              → ∀ {xs ys} → Pointwise _≊_ xs ys
              → A ⟦ f ⟧ xs ≊ A ⟦ f ⟧ ys
    axiom   : ∀ {n} → (eq : eqs Θ n) → (θ : Env A n)
              → ∣ inst A θ ∣ (proj₁ (Θ ⟦ eq ⟧ₑ))
                ≊ ∣ inst A θ ∣ (proj₂ (Θ ⟦ eq ⟧ₑ))

  private

    ≊-isEquivalence : IsEquivalence _≊_
    ≊-isEquivalence = record { refl  = refl
                             ; sym   = sym
                             ; trans = trans
                             }

  instance
    ≊-isDenom : IsDenominator A _≊_
    ≊-isDenom = record { isEquivalence = ≊-isEquivalence
                       ; isCompatible  = cong
                       ; isCoarser     = inherit
                       }

  Synthetic : Model
  Synthetic = record { ∥_∥/≈   = ∥ A ∥/ _≊_
                     ; isModel = isModel
                     }
    where open module T = Setoid (∥ A ∥/ _≊_)
          open import Relation.Binary.Reasoning.Setoid (∥ A ∥/ _≊_)

          models : Models (A / _≊_)
          models eq θ = begin
              ∣ inst (A / _≊_) θ ∣ lhs
            ≈⟨ T.sym (lemma {x = lhs}) ⟩
              ∣ (inc A _≊_) ⊙ (inst A θ) ∣ lhs
            ≈⟨ axiom eq θ ⟩
              ∣ (inc A _≊_) ⊙ (inst A θ) ∣ rhs
            ≈⟨ lemma {x = rhs} ⟩
              ∣ inst (A / _≊_) θ ∣ rhs
            ∎
            where lhs = proj₁ (Θ ⟦ eq ⟧ₑ)
                  rhs = proj₂ (Θ ⟦ eq ⟧ₑ)
                  lemma = inst-universal (A / _≊_) θ
                              {h = (inc A _≊_) ⊙ (inst A θ) }
                              (λ x → PE.refl)

          isModel : IsModel (∥ A ∥/ _≊_)
          isModel = record { isAlgebra = A / _≊_ -isAlgebra
                           ; models    = models
                           }

J : ℕ → Model
J = Synthetic ∘ F

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------------
-- Simple example of a nested recursive function
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. Vol. 2152 of LNCS. 2001.

module FOTC.Program.Nest.Nest where

open import FOTC.Base

------------------------------------------------------------------------------
-- The nest function.
postulate
  nest   : D → D
  nest-0 : nest zero            ≡ zero
  nest-S : ∀ n → nest (succ₁ n) ≡ nest (nest n)
{-# ATP axioms nest-0 nest-S #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Jesper, 2015-12-18: the helper function shouldn't be accepted, since it
-- matches on a heterogeneous equality and the equation between the types
-- Box A and Box B cannot be solved without injective type constructors.

data Box (A : Set) : Set where
  [_] : A → Box A

data _≡_ (A : Set) : Set → Set₁ where
  refl : A ≡ A

data _≅_ {A : Set₁} (x : A) : {B : Set₁} → B → Set₂ where
  refl : x ≅ x

data C : Set → Set₁ where
  c₁ c₂ : (A : Set) → C (Box A)

data D : {A : Set} → C A → Set₂ where
  d₁ : (A : Set) → D (c₁ A)
  d₂ : (A : Set) → D (c₂ A)

D-elim-c₁-helper :
  (P : {A B : Set} {c : C A} →
       D c → A ≡ Box B → c ≅ c₁ B → Set₂) →
  ((A : Set) → P (d₁ A) refl refl) →
  {A B : Set} {c : C A}
  (x : D c) (eq₂ : c ≅ c₁ B) (eq₁ : A ≡ Box B) → P x eq₁ eq₂
D-elim-c₁-helper P p (d₂ A) ()   _
D-elim-c₁-helper P p (d₁ A) refl refl = p A


text:
module sum-downFrom where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (*-suc; *-identityʳ; *-distribʳ-+; *-distribˡ-∸; +-∸-assoc; +-∸-comm; m+n∸m≡n; m≤m*n)

open import lists using (List; []; _∷_; [_,_,_]; sum)

-- (n - 1), ⋯ , 0 を返す
downFrom : ℕ → List ℕ
downFrom zero    = []
downFrom (suc n) = n ∷ downFrom n

_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
_ = refl

-- n ≤ n * n の証明
n≤n*n : ∀ (n : ℕ) → n ≤ n * n
n≤n*n zero    = z≤n
n≤n*n (suc n) = m≤m*n (suc n) (s≤s z≤n)

-- n ≤ n * 2 の証明
n≤n*2 : ∀ (n : ℕ) → n ≤ n * 2
n≤n*2 n = m≤m*n n (s≤s z≤n)

-- n * 2 ∸ n = n の証明
n*2∸n≡n : ∀ (n : ℕ) → n * 2 ∸ n ≡ n
n*2∸n≡n n =
  begin
    n * 2 ∸ n
  ≡⟨ cong (_∸ n) (*-suc n 1) ⟩ -- 積の展開
    n + n * 1 ∸ n
  ≡⟨ m+n∸m≡n n (n * 1) ⟩ -- n ∸ n の除去
    n * 1
  ≡⟨ *-identityʳ n ⟩ -- * 1 の除去
    n
  ∎

-- m * (n ∸ 1) = m * n ∸ m の証明
m*[n∸1]≡m*n∸m : ∀ (m n : ℕ) → m * (n ∸ 1) ≡ m * n ∸ m
m*[n∸1]≡m*n∸m m n =
  begin
    m * (n ∸ 1)
  ≡⟨ *-distribˡ-∸ m n 1 ⟩ -- n * の分配
    m * n ∸ m * 1
  ≡⟨ cong (m * n ∸_) (*-identityʳ m) ⟩ -- * 1 の除去
    m * n ∸ m
  ∎

-- (n - 1) + ⋯ + 0 と n * (n ∸ 1) / 2 が等しいことの証明
sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
sum-downFrom zero =
  begin
    sum (downFrom zero) * 2
  ≡⟨⟩
    sum [] * 2
  ≡⟨⟩
    zero
    -- = zero * (zero ∸ 1)
  ∎
sum-downFrom (suc n) =
  begin
    sum (downFrom (suc n)) * 2
  ≡⟨⟩
    sum (n ∷ downFrom n) * 2
  ≡⟨⟩
    (n + sum (downFrom n)) * 2
  ≡⟨ *-distribʳ-+ 2 n (sum (downFrom n)) ⟩ -- * 2 の分配
    (n * 2) + (sum (downFrom n)) * 2
  ≡⟨ cong (n * 2 +_) (sum-downFrom n) ⟩ -- 帰納法
    (n * 2) + (n * (n ∸ 1))
  ≡⟨ cong (n * 2 +_) (m*[n∸1]≡m*n∸m n n) ⟩ -- n * の分配
    (n * 2) + (n * n ∸ n)
  ≡⟨ sym (+-∸-assoc (n * 2) (n≤n*n n)) ⟩ -- 結合法則
    (n * 2) + n * n ∸ n
  ≡⟨ +-∸-comm (n * n) (n≤n*2 n) ⟩ -- 交換法則
    (n * 2) ∸ n + n * n
  ≡⟨ cong (_+ n * n) (n*2∸n≡n n) ⟩ -- n ∸ n の除去
    n + n * n
    -- = n * (suc n)
    -- = (suc n) * n
    -- = (suc n) * ((suc n) ∸ 1)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
open import Categories
open import Functors
open import RMonads

module RMonads.REM {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
                   (M : RMonad J) where
open import Library
open RMonad M
open Fun

record RAlg : Set (a ⊔ c ⊔ d) where
  constructor ralg
  open Cat D
  field acar  : Obj
        astr  : ∀ {Z} → Hom (OMap J Z) acar → Hom (T Z) acar
        alaw1 : ∀ {Z}{f : Hom (OMap J Z) acar} →
                f ≅ comp (astr f) η
        alaw2 : ∀{Z}{W}{k : Hom (OMap J Z) (T W)}
                {f : Hom (OMap J W) acar} →
                astr (comp (astr f) k) ≅ comp (astr f) (bind k)

AlgEq : {X Y : RAlg} → RAlg.acar X ≅ RAlg.acar Y →
  ((λ {Z} → RAlg.astr X {Z}) ≅ (λ {Z} → RAlg.astr Y {Z})) →
        X ≅ Y
AlgEq {ralg acar astr _ _}{ralg .acar .astr _ _} refl refl = let open Cat in
  cong₂ (ralg acar astr)
        (iext λ _ → iext λ _ → ir _ _)
        (iext λ _ → iext λ _ → iext λ _ → iext λ _ → ir _ _)

astrnat : ∀(alg : RAlg){X Y}
          (f : Cat.Hom C X Y) →
          (g : Cat.Hom D (OMap J X) (RAlg.acar alg))
          (g' : Cat.Hom D (OMap J Y) (RAlg.acar alg)) →
          Cat.comp D g' (HMap J f) ≅ g →
          Cat.comp D (RAlg.astr alg g')
                     (RMonad.bind M (Cat.comp D (RMonad.η M) (HMap J f)))
          ≅
          RAlg.astr alg g
astrnat alg f g g' p = let
  open RAlg alg; open Cat D in
  proof
  comp (astr g') (bind (comp η (HMap J f)))
  ≅⟨ sym alaw2 ⟩
  astr (comp (astr g') (comp η (HMap J f)))
  ≅⟨ cong astr (sym ass) ⟩
  astr (comp (comp (astr g') η) (HMap J f))
  ≅⟨ cong (λ g₁ → astr (comp g₁ (HMap J f))) (sym alaw1) ⟩
  astr (comp g' (HMap J f))
  ≅⟨ cong astr p ⟩
  astr g ∎

record RAlgMorph (A B : RAlg) : Set (a ⊔ c ⊔ d)
  where
  constructor ralgmorph
  open Cat D
  open RAlg
  field amor : Hom (acar A) (acar B)
        ahom : ∀{Z}{f : Hom (OMap J Z) (acar A)} →
               comp amor (astr A f) ≅ astr B (comp amor f)
open RAlgMorph

RAlgMorphEq : ∀{X Y : RAlg}{f g : RAlgMorph X Y} → amor f ≅ amor g → f ≅ g
RAlgMorphEq {X}{Y}{ralgmorph amor _}{ralgmorph .amor _} refl =
  cong (ralgmorph amor) (iext λ _ → iext λ _ → ir _ _)

lemZ : ∀{X X' Y Y' : RAlg}
       {f : RAlgMorph X Y}{g : RAlgMorph X' Y'} → X ≅ X' → Y ≅ Y' →
             amor f ≅ amor g → f ≅ g
lemZ refl refl = RAlgMorphEq

IdMorph : ∀{A : RAlg} → RAlgMorph A A
IdMorph {A} = let open Cat D; open RAlg A in record {
  amor = iden;
  ahom = λ {_ f} →
    proof
    comp iden (astr f)
    ≅⟨ idl ⟩
    astr f
    ≅⟨ cong astr (sym idl) ⟩
    astr (comp iden f)
    ∎}

CompMorph : ∀{X Y Z : RAlg} →
            RAlgMorph Y Z → RAlgMorph X Y → RAlgMorph X Z
CompMorph {X}{Y}{Z} f g = let open Cat D; open RAlg in record {
  amor = comp (amor f) (amor g);
  ahom = λ {_ f'} →
    proof
    comp (comp (amor f) (amor g)) (astr X f')
    ≅⟨ ass ⟩
    comp (amor f) (comp (amor g) (astr X f'))
    ≅⟨ cong (comp (amor f)) (ahom g) ⟩
    comp (amor f) (astr Y (comp (amor g) f'))
    ≅⟨ ahom f ⟩
    astr Z (comp (amor f) (comp (amor g) f'))
    ≅⟨ cong (astr Z) (sym ass) ⟩
    astr Z (comp (comp (amor f) (amor g)) f')
    ∎}

idlMorph : {X Y : RAlg}{f : RAlgMorph X Y} →
           CompMorph IdMorph f ≅ f
idlMorph = RAlgMorphEq (Cat.idl D)

idrMorph : ∀{X Y : RAlg}{f : RAlgMorph X Y} →
           CompMorph f IdMorph ≅ f
idrMorph = RAlgMorphEq (Cat.idr D)

assMorph : ∀{W X Y Z : RAlg}
           {f : RAlgMorph Y Z}{g : RAlgMorph X Y}{h : RAlgMorph W X} →
           CompMorph (CompMorph f g) h ≅ CompMorph f (CompMorph g h)
assMorph = RAlgMorphEq (Cat.ass D)

EM : Cat
EM = record{
  Obj  = RAlg;
  Hom  = RAlgMorph;
  iden = IdMorph;
  comp = CompMorph;
  idl  = idlMorph;
  idr  = idrMorph;
  ass  = λ{_ _ _ _ f g h} → assMorph {f = f}{g}{h}}


text:
module Data.Bool.Instance where

open import Class.Equality
open import Class.Show
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

instance
  Bool-Eq : Eq Bool
  Bool-Eq = record { _≟_ = helper }
    where
      helper : ∀ (x y : Bool) → Dec (x ≡ y)
      helper false false = yes refl
      helper false true = no (λ ())
      helper true false = no (λ ())
      helper true true = yes refl

  Bool-Show : Show Bool
  Bool-Show = record { show = λ { false → "false" ; true → "true" } }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module Type.Properties.Empty{ℓ} where

import      Lvl
open import Type

-- A type is empty when "empty functions" exists for it, which essentially means that there are no objects with this type.
-- This is an useful definition because the empty type is not unique (There are an infinite number of "empty types").
-- An explanation for why there are an infinite number of them:
-- · Types are not equal to each other extensionally (unlike sets, type equality is not based on their inhabitants (set equality is based on which elements that the set contains)).
-- An alternative explanation:
-- · Type equality is nominal (loosely: based on its name (assuming no other type could be named the same)), and not representional.
-- Or more simply by an example:
-- · `data Empty : Type where` defines an empty type.
--   `data Empty2 : Type where` also defines an empty type.
--   Now, `Empty` is not type equal to `Empty2` because the terms does not normalize further (by the rules of the language).
-- So by proving IsEmpty(T), it means that the type T is empty, because empty types are the only types that has the property of having empty functions.
record IsEmpty (T : Type{ℓ}) : Type{Lvl.𝐒(ℓ)} where
  constructor intro
  field
    -- Empty functions for an empty type
    -- For any type U, it is always possible to construct a function from T to U if T is empty
    empty : ∀{U : Type{ℓ}} → T → U

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Fragment.Equational.Theory where

open import Fragment.Equational.Theory.Base public


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Limit where

open import Level

open import Cats.Category.Base
open import Cats.Category.Cones as Cones using
  (Cone ; Cones ; ConesF ; cone-iso→obj-iso)
open import Cats.Category.Constructions.Terminal using (HasTerminal)
open import Cats.Category.Constructions.Unique using (∃!′)
open import Cats.Category.Fun as Fun using (Trans ; _↝_)
open import Cats.Functor using (Functor)
open import Cats.Util.Conv

import Cats.Category.Constructions.Terminal as Terminal
import Cats.Category.Constructions.Iso as Iso

open Cone
open Cones._⇒_
open Functor
open Fun._≈_
open Trans

private
  module Cs {lo la l≈ lo′ la′ l≈′} {C : Category lo la l≈}
    {D : Category lo′ la′ l≈′} {F : Functor C D} = Category (Cones F)

module _ {lo la l≈ lo′ la′ l≈′}
  {J : Category lo la l≈}
  {Z : Category lo′ la′ l≈′}
  where

  private
    module J = Category J
    module Z = Category Z

  IsLimit : {D : Functor J Z} → Cone D → Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′)
  IsLimit {D} = Terminal.IsTerminal {C = Cones D}

  record Limit (D : Functor J Z) : Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) where
    field
      cone : Cone D
      isLimit : IsLimit cone

    open Cone cone using () renaming (arr to proj)

    private
      hasTerminal : HasTerminal (Cones D)
      hasTerminal = record { ⊤ = cone ; isTerminal = isLimit }

    open HasTerminal hasTerminal public using
      ( ! ; !-unique ) renaming
      ( ⊤-unique to cone-unique
      ; ⇒⊤-unique to ⇒cone-unique )

    !! : (cone′ : Cone D) → cone′ .Cone.Apex Z.⇒ cone .Cone.Apex
    !! cone′ = ! cone′ .arr

    !!-unique : {cone′ : Cone D} (f : cone′ Cs.⇒ cone)
      → !! cone′ Z.≈ f .arr
    !!-unique f = !-unique f

    arr∘!! : ∀ cone′ {j} → proj j Z.∘ !! cone′ Z.≈ cone′ .Cone.arr j
    arr∘!! cone′ = ! cone′ .commute _

    !!∘ : ∀ {C D} (f : C Cs.⇒ D)
      → !! D Z.∘ f .arr Z.≈ !! C
    !!∘ {C} {D} f = Z.≈.sym (!!-unique record
      { commute = λ j →
        let open Z.≈-Reasoning in
        begin
          proj j Z.∘ !! D Z.∘ f .arr
        ≈⟨ Z.unassoc ⟩
          (proj j Z.∘ !! D) Z.∘ f .arr
        ≈⟨ Z.∘-resp-l (arr∘!! D) ⟩
          D .arr j Z.∘ f .arr
        ≈⟨ f .commute j ⟩
          C .arr j
        ∎
      })

    open Cone cone public

  open Limit public

  instance
    HasObj-Limit : ∀ {D} → HasObj (Limit D) _ _ _
    HasObj-Limit {D} = record { Cat = Cones D ; _ᴼ = cone }

  module _ {D : Functor J Z} where

    unique : (l m : Limit D) → Iso.Build._≅_ (Cones D) (l ᴼ) (m ᴼ)
    unique l m = Terminal.terminal-unique (isLimit l) (isLimit m)

    obj-unique : (l m : Limit D) → Iso.Build._≅_ Z (l ᴼ ᴼ) (m ᴼ ᴼ)
    obj-unique l m = cone-iso→obj-iso _ (unique l m)

  module _ {F G : Functor J Z} where

    trans : (ϑ : Trans F G) (l : Limit F) (m : Limit G)
      → l .Apex Z.⇒ m .Apex
    trans ϑ l m = !! m (ConesF .fmap ϑ .fobj (l .cone))

    arr∘trans : ∀ ϑ l m c
      →   m .arr c Z.∘ trans ϑ l m
      Z.≈ ϑ .component c Z.∘ l .arr c
    arr∘trans ϑ l m c = arr∘!! m (ConesF .fmap ϑ .fobj (l .cone))

    trans-resp : ∀ {ϑ ι} l m
      → ϑ Fun.≈ ι
      → trans ϑ l m Z.≈ trans ι l m
    trans-resp {ϑ} {ι} l m ϑ≈ι = !!-unique m record
      { commute = λ j → Z.≈.trans (arr∘trans ι l m j)
          (Z.∘-resp-l (Z.≈.sym (≈-elim ϑ≈ι)))
      }

  trans-id : {F : Functor J Z} (l : Limit F)
    → trans Fun.id l l Z.≈ Z.id
  trans-id l = !!-unique l record
    { commute = λ j → Z.≈.trans Z.id-r (Z.≈.sym Z.id-l)
    }

  trans-∘ : {F G H : Functor J Z} (ϑ : Trans G H) (ι : Trans F G)
    → ∀ l m n
    → trans ϑ m n Z.∘ trans ι l m Z.≈ trans (ϑ Fun.∘ ι) l n
  trans-∘ {F} {G} {H} ϑ ι l m n = Z.≈.sym (!!-unique n record
      { commute = λ j → let open Z.≈-Reasoning in
        begin
          n .arr j Z.∘ trans ϑ m n Z.∘ trans ι l m
        ≈⟨ Z.unassoc ⟩
          (n .arr j Z.∘ trans ϑ m n) Z.∘ trans ι l m
        ≈⟨ Z.∘-resp-l (arr∘trans ϑ m n j ) ⟩
          (ϑ .component j Z.∘ m .arr j) Z.∘ trans ι l m
        ≈⟨ Z.assoc ⟩
          ϑ .component j Z.∘ m .arr j Z.∘ trans ι l m
        ≈⟨ Z.∘-resp-r (arr∘trans ι l m j) ⟩
          ϑ .component j Z.∘ ι .component j Z.∘ l .arr j
        ≈⟨ Z.unassoc ⟩
          (ϑ Fun.∘ ι) .component j Z.∘ l .arr j
        ∎
      })

record _HasLimitsOf_
  {lo la l≈} (C : Category lo la l≈) {lo′ la′ l≈′} (J : Category lo′ la′ l≈′)
  : Set (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′ )
  where
  private
    module C = Category C
    module J↝C = Category (J ↝ C)

  field
    lim′ : (F : Functor J C) → Limit F

  lim : Functor J C → C.Obj
  lim F = lim′ F .cone .Apex

  limF : Functor (J ↝ C) C
  limF = record
    { fobj = λ F → lim F
    ; fmap = λ {F} {G} ϑ → trans ϑ (lim′ _) (lim′ _)
    ; fmap-resp = λ ϑ≈ι → trans-resp (lim′ _) (lim′ _) ϑ≈ι
    ; fmap-id = trans-id (lim′ _)
    ; fmap-∘ = trans-∘ _ _ (lim′ _) (lim′ _) (lim′ _)
    }

record Complete {lo la l≈} (C : Category lo la l≈) lo′ la′ l≈′
  : Set (lo ⊔ la ⊔ l≈ ⊔ suc (lo′ ⊔ la′ ⊔ l≈′))
  where
  field
    lim′ : ∀ {J : Category lo′ la′ l≈′} (F : Functor J C) → Limit F

  hasLimitsOf : (J : Category lo′ la′ l≈′) → C HasLimitsOf J
  hasLimitsOf J ._HasLimitsOf_.lim′ = lim′

  private
    open module HasLimitsOf {J} = _HasLimitsOf_ (hasLimitsOf J) public hiding (lim′)

preservesLimits : ∀ {lo la l≈ lo′ la′ l≈′}
  → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  → Functor C D
  → (lo″ la″ l≈″ : Level)
  → Set _
preservesLimits {C = C} F lo″ la″ l≈″
    = {J : Category lo″ la″ l≈″}
    → {D : Functor J C}
    → {c : Cone D}
    → IsLimit c
    → IsLimit (Cones.apFunctor F c)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module Generic.Lib.Equality.Congn where

open import Generic.Lib.Intro
open import Generic.Lib.Equality.Propositional
open import Generic.Lib.Data.Product
open import Generic.Lib.Data.Nat
open import Generic.Lib.Data.Pow
open import Generic.Lib.Data.Sets

zip≡ : ∀ {n αs} {As : Sets {n} αs} -> HList As -> HList As -> Sets (replicatePow n lzero)
zip≡ {0}      tt       tt      = tt
zip≡ {suc _} (x , xs) (y , ys) = (x ≡ y) , zip≡ xs ys

congn : ∀ {β} {B : Set β} n {αs} {As : Sets {n} αs} {xs ys : HList As}
      -> (f : FoldSets As B) -> FoldSets (zip≡ xs ys) (applyFoldSets f xs ≡ applyFoldSets f ys)
congn  0      y      = refl
congn (suc n) f refl = congn n (f _)

private
  module Test where
    cong′ : ∀ {α β} {A : Set α} {B : Set β} {x y} -> (f : A -> B) -> x ≡ y -> f x ≡ f y
    cong′ = congn 1

    cong₂′ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x₁ x₂ y₁ y₂}
           -> (g : A -> B -> C) -> x₁ ≡ x₂ -> y₁ ≡ y₂ -> g x₁ y₁ ≡ g x₂ y₂
    cong₂′ = congn 2

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
postulate
  A : Set
  a : A

data D : A → Set where
  d : (a : A) → D a

f : A → (D a → Set) → Set
f a f = f (d a)

-- Bad error:
-- a != a of type A
-- when checking that the pattern d a has type D a

-- Better error:
-- a != a of type A
-- (because one is a variable and one a defined identifier)
-- when checking that the pattern d a has type D a