text:
module SizedIO.IOGraphicsLib where

{-# FOREIGN GHC import qualified Graphics.SOE #-}
{-# FOREIGN GHC import qualified Graphics.Rendering.OpenGL #-}
{-# FOREIGN GHC import qualified GHC.Int #-}
{-# FOREIGN GHC import qualified Foreign.C.Types #-}

open import Data.Bool.Base
open import Data.Char.Base
open import Data.Nat.Base hiding (_+_)
open import Data.List.Base as L
open import Data.Integer.Base
open import Data.Product

open import Data.Maybe.Base

open import Size renaming (Size to AgdaSize)

open import SizedIO.Base

open import NativeIO
open import NativeInt

AgdaPoint = (ℤ × ℤ)

postulate Window : Set
-- {-# COMPILED_TYPE Window Graphics.SOE.Window #-}

postulate Size : Set
-- {-# COMPILED_TYPE Size Graphics.SOE.Size #-}

postulate size : ℤ → ℤ → Size
-- {-# COMPILED size (\ x y -> ( (fromInteger x) :: Int, (fromInteger y) :: Int) :: Graphics.SOE.Size) #-}

postulate Point : Set
-- {-# COMPILED_TYPE Point Graphics.SOE.Point #-}

postulate nativePoint : ℤ → ℤ → Point
-- {-# COMPILED nativePoint (\ x y -> (fromInteger x, fromInteger y)::Graphics.SOE.Point) #-}

postulate nativeProj1Point : Point → ℤ
postulate nativeProj2Point : Point → ℤ
-- {-# COMPILED nativeProj1Point (\(x, y) -> toInteger x) #-}
-- {-# COMPILED nativeProj2Point (\(x, y) -> toInteger y) #-}

{-
toNativePoint : Point → NativePoint
toNativePoint (x , y) = nativePoint x y
-}

data Event : Set where
   Key : Char → Bool → Event
   Button : Point → Bool → Bool → Event
   MouseMove : Point → Event
   Resize : Event
   Closed : Event

-- {-# COMPILED_DATA Event Graphics.SOE.Event Graphics.SOE.Key Graphics.SOE.Button Graphics.SOE.MouseMove Graphics.SOE.Resize Graphics.SOE.Closed #-}

postulate nativeMaybeGetWindowEvent : Window → NativeIO (Maybe Event)
-- {-# COMPILED nativeMaybeGetWindowEvent Graphics.SOE.maybeGetWindowEvent #-}

postulate nativeGetWindowEvent : Window → NativeIO (Event)
-- {-# COMPILED nativeGetWindowEvent Graphics.SOE.getWindowEvent #-}

postulate Graphic : Set
-- {-# COMPILED_TYPE Graphic Graphics.SOE.Graphic #-}

postulate nativeDrawInWindow : Window → Graphic → NativeIO Unit
-- {-# COMPILED nativeDrawInWindow Graphics.SOE.drawInWindow #-}

postulate Word32 : Set
-- {-# COMPILED_TYPE Word32 Graphics.SOE.Word32 #-}

postulate text : Point → String → Graphic
-- {-# COMPILED text (\ p s -> Graphics.SOE.text p (Data.Text.unpack s)) #-}

data RedrawMode : Set where
-- (removed from lib where: DoubleBuffered : RedrawMode, Unbuffered : RedrawMode)

-- {-# COMPILED_DATA RedrawMode Graphics.SOE.RedrawMode #-}

postulate nativeDrawGraphic : RedrawMode
-- {-# COMPILED nativeDrawGraphic Graphics.SOE.drawGraphic #-}

postulate nativeDrawBufferedGraphic : RedrawMode
-- {-# COMPILED nativeDrawBufferedGraphic Graphics.SOE.drawBufferedGraphic #-}

postulate nativeOpenWindow : String → Size → NativeIO Window
-- {-# COMPILED nativeOpenWindow (\ s -> Graphics.SOE.openWindow (Data.Text.unpack s)) #-}

postulate nativeOpenWindowEx : String → (Maybe Point) → (Maybe Size) → RedrawMode → (Maybe Word32) → NativeIO Window
-- {-# COMPILED nativeOpenWindowEx (\s -> Graphics.SOE.openWindowEx (Data.Text.unpack s)) #-}

nativeOpenWindowExNat : String → (Maybe Point) → ℕ → ℕ → RedrawMode → (Maybe Word32) → NativeIO Window
nativeOpenWindowExNat s p n1 n2 a b = nativeOpenWindowEx s p (just (size (+ n1) (+ n2))) a b

postulate nativeCloseWindow : Window → NativeIO Unit
-- {-# COMPILED nativeCloseWindow Graphics.SOE.closeWindow #-}

postulate nativeRunGraphics :  NativeIO Unit → NativeIO Unit
-- {-#  COMPILED nativeRunGraphics Graphics.SOE.runGraphics #-}

postulate word32ToInteger : Word32 → ℤ
-- {-#  COMPILED word32ToInteger (\w -> toInteger (Graphics.SOE.word32ToInt w)) #-}

postulate nativeTimeGetTime : NativeIO Word32
-- {-#  COMPILED nativeTimeGetTime Graphics.SOE.timeGetTime #-}

data Color : Set where
  black   : Color
  blue    : Color
  green   : Color
  cyan    : Color
  red     : Color
  magenta : Color
  yellow  : Color
  white   : Color
-- {-#  COMPILED_DATA Color Graphics.SOE.Color Graphics.SOE.Black Graphics.SOE.Blue Graphics.SOE.Green Graphics.SOE.Cyan Graphics.SOE.Red Graphics.SOE.Magenta Graphics.SOE.Yellow Graphics.SOE.White #-}

postulate withColor : Color → Graphic → Graphic
-- {-#  COMPILED withColor Graphics.SOE.withColor #-}

postulate polygon : List Point → Graphic
-- {-#  COMPILED polygon Graphics.SOE.polygon #-}

{-
polygon : List Point → Graphic
polygon l = nativePolygon (L.map toNativePoint l)
-}

data GraphicsCommands : Set where
  closeWindow         : Window            → GraphicsCommands
  maybeGetWindowEvent : Window            → GraphicsCommands
  getWindowEvent      : Window            → GraphicsCommands
  openWindowNotEx     : String → Size    → GraphicsCommands
  openWindow          : String → (Maybe Point) → ℕ → ℕ
                        → RedrawMode → (Maybe Word32) → GraphicsCommands
  timeGetTime         :                      GraphicsCommands
  drawInWindow        : Window → Graphic → GraphicsCommands
  print               : String →             GraphicsCommands

GraphicsResponses : GraphicsCommands → Set
GraphicsResponses (maybeGetWindowEvent w) = Maybe Event
GraphicsResponses (getWindowEvent w)      = Event
GraphicsResponses (closeWindow w)         = Unit
GraphicsResponses (openWindowNotEx s s')  = Window
GraphicsResponses (openWindow s n1 n2 s' r w) = Window
GraphicsResponses timeGetTime             = Word32
GraphicsResponses _                       = Unit

GraphicsInterface : IOInterface
Command  GraphicsInterface = GraphicsCommands
Response GraphicsInterface = GraphicsResponses

IOGraphics : AgdaSize → Set → Set
IOGraphics i = IO GraphicsInterface i

IOGraphics+ : AgdaSize → Set → Set
IOGraphics+ i = IO+ GraphicsInterface i

translateIOGraphicsLocal : (c : GraphicsCommands) → NativeIO (GraphicsResponses c)
translateIOGraphicsLocal (maybeGetWindowEvent w) = nativeMaybeGetWindowEvent w
translateIOGraphicsLocal (getWindowEvent w)      = nativeGetWindowEvent w
translateIOGraphicsLocal (closeWindow w)         = nativeCloseWindow w
translateIOGraphicsLocal (openWindowNotEx str size)   = nativeOpenWindow str size
translateIOGraphicsLocal (openWindow str point n1 n2 mode word) = nativeOpenWindowExNat str point n1 n2 mode word
translateIOGraphicsLocal timeGetTime             = nativeTimeGetTime
translateIOGraphicsLocal (drawInWindow w g)      = nativeDrawInWindow w g
translateIOGraphicsLocal (print s)             = nativePutStrLn s

translateIOGraphics : {A : Set} → IOGraphics ∞ A → NativeIO A
translateIOGraphics = translateIO translateIOGraphicsLocal

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Reasoning.PartialOrder module directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.PartialOrderReasoning
         {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where

open import Relation.Binary.Reasoning.PartialOrder P public

ext: agda


text:
module Category.Profunctor.Star where
open import Agda.Primitive using (_⊔_)
open import Category.Functor     using (RawFunctor    ; module RawFunctor)
open import Category.Functor.Lawful
open import Category.Applicative using (RawApplicative; module RawApplicative)
open import Data.Product using (_,_)
open import Data.Sum using (inj₁; inj₂)
open import Category.Profunctor
open import Category.Strong
open import Category.Choice
open import Relation.Binary.PropositionalEquality using (refl)
open import Axiom.Extensionality.Propositional using (Extensionality)

Star : ∀ {l₁ l₂ l₃} (F : Set l₂ → Set l₃) (A : Set l₁) (B : Set l₂) → Set (l₁ ⊔ l₃)
Star F A B = (A → F B)

starProfunctor : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} → RawFunctor F → ProfunctorImp (Star F)
starProfunctor f = record
  { dimap = λ f h g z → h <$> (g (f z))
  ; lmap  = λ f g z → g (f z)
  ; rmap  = λ h g z → h <$> (g z)
  } where open RawFunctor f

starLawfulProfunctor : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} {Func : RawFunctor F} → Extensionality l₁ l₂ → LawfulFunctorImp Func → LawfulProfunctorImp (starProfunctor Func)
starLawfulProfunctor ext f = record
  { lmapId = refl
  ; rmapId = ext (λ _ → <$>-identity)
  ; dimapLmapRmap = refl
  } where open LawfulFunctor f

starStrong : ∀ {l₁ l₂} {F : Set l₁ → Set l₂} → RawFunctor F → StrongImp (Star F)
starStrong f = record
  { first'  = λ { f → λ { (x , z) → (_, z) <$> f x } }
  ; second' = λ { f → λ { (z , x) → (z ,_) <$> f x } }
  ; isProfunctor = starProfunctor f
  } where open RawFunctor f

starChoice : ∀ {l} {F : Set l → Set l} → RawApplicative F → ChoiceImp (Star F)
starChoice f = record
  { left'  = λ { f → λ { (inj₁ x) → inj₁ <$> f x ; (inj₂ z) → pure (inj₂ z) } }
  ; right' = λ { f → λ { (inj₁ z) → pure (inj₁ z) ; (inj₂ x) → inj₂ <$> f x } }
  ; isProfunctor = starProfunctor rawFunctor
  } where open RawApplicative f

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


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

open import lib.Basics
open import lib.cubical.Square
open import lib.types.Bool
open import lib.types.Cofiber
open import lib.types.Lift
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.PushoutFmap
open import lib.types.Sigma
open import lib.types.Span
open import lib.types.Suspension
open import lib.types.Wedge

module lib.types.BigWedge where

module _ {i j} {A : Type i} where

  {- the function for cofiber -}
  bigwedge-f : (X : A → Ptd j) → A → Σ A (de⊙ ∘ X)
  bigwedge-f X a = a , pt (X a)

  bigwedge-span : (A → Ptd j) → Span
  bigwedge-span X = cofiber-span (bigwedge-f X)

  BigWedge : (A → Ptd j) → Type (lmax i j)
  BigWedge X = Cofiber (bigwedge-f X)

  bwbase : {X : A → Ptd j} → BigWedge X
  bwbase = cfbase

  bwin : {X : A → Ptd j} → (a : A) → de⊙ (X a) → BigWedge X
  bwin = curry cfcod

  ⊙BigWedge : (A → Ptd j) → Ptd (lmax i j)
  ⊙BigWedge X = ⊙[ BigWedge X , bwbase ]

  bwglue : {X : A → Ptd j} → (a : A) → bwbase {X} == bwin a (pt (X a))
  bwglue = cfglue

  ⊙bwin : {X : A → Ptd j} → (a : A) → X a ⊙→ ⊙BigWedge X
  ⊙bwin a = (bwin a , ! (bwglue a))

  module BigWedgeElim {X : A → Ptd j} {k} {P : BigWedge X → Type k}
    (base* : P bwbase) (in* : (a : A) (x : de⊙ (X a)) → P (bwin a x))
    (glue* : (a : A) → base* == in* a (pt (X a)) [ P ↓ bwglue a ])
    = CofiberElim {f = bigwedge-f X} {P = P} base* (uncurry in*) glue*

  BigWedge-elim = BigWedgeElim.f

  module BigWedgeRec {X : A → Ptd j} {k} {C : Type k}
    (base* : C) (in* : (a : A) → de⊙ (X a) → C)
    (glue* : (a : A) → base* == in* a (pt (X a)))
    = CofiberRec {f = bigwedge-f X} {C = C} base* (uncurry in*) glue*

module _ {i j₀ j₁} {A : Type i} {X₀ : A → Ptd j₀} {X₁ : A → Ptd j₁}
  (Xeq : ∀ a → X₀ a ⊙≃ X₁ a) where

  bigwedge-span-emap-r : SpanEquiv (cofiber-span (bigwedge-f X₀)) (cofiber-span (bigwedge-f X₁))
  bigwedge-span-emap-r = span-map (idf _) (Σ-fmap-r λ a → fst (⊙–> (Xeq a))) (idf _)
    (comm-sqr λ _ → idp) (comm-sqr λ a → pair= idp (⊙–>-pt (Xeq a))) ,
    idf-is-equiv _ , Σ-isemap-r (λ a → snd (Xeq a)) , idf-is-equiv _

  BigWedge-emap-r : BigWedge X₀ ≃ BigWedge X₁
  BigWedge-emap-r = Pushout-emap bigwedge-span-emap-r

  ⊙BigWedge-emap-r : ⊙BigWedge X₀ ⊙≃ ⊙BigWedge X₁
  ⊙BigWedge-emap-r = ≃-to-⊙≃ BigWedge-emap-r idp

module _ {i₀ i₁ j} {A₀ : Type i₀} {A₁ : Type i₁}
  (X : A₁ → Ptd j) (Aeq : A₀ ≃ A₁) where

  bigwedge-span-emap-l : SpanEquiv (cofiber-span (bigwedge-f (X ∘ –> Aeq))) (cofiber-span (bigwedge-f X))
  bigwedge-span-emap-l = span-map (idf _) (Σ-fmap-l (de⊙ ∘ X) (–> Aeq)) (–> Aeq)
    (comm-sqr λ _ → idp) (comm-sqr λ _ → idp) ,
    idf-is-equiv _ , Σ-isemap-l (de⊙ ∘ X) (snd Aeq) , snd Aeq

  BigWedge-emap-l : BigWedge (X ∘ –> Aeq) ≃ BigWedge X
  BigWedge-emap-l = Pushout-emap bigwedge-span-emap-l

  ⊙BigWedge-emap-l : ⊙BigWedge (X ∘ –> Aeq) ⊙≃ ⊙BigWedge X
  ⊙BigWedge-emap-l = ≃-to-⊙≃ BigWedge-emap-l idp

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

  extract-glue-from-BigWedge-is-const :
    ∀ bw → extract-glue {s = bigwedge-span X} bw == north
  extract-glue-from-BigWedge-is-const = BigWedge-elim
    idp
    (λ x y → ! (merid x))
    (↓-='-from-square ∘ λ x →
      ExtractGlue.glue-β x ∙v⊡
        tr-square (merid x)
      ⊡v∙ ! (ap-cst north (cfglue x)))

{- A BigWedge indexed by Bool is just a binary Wedge -}
module _ {i} (Pick : Bool → Ptd i) where

  BigWedge-Bool-equiv-Wedge : BigWedge Pick ≃ Wedge (Pick true) (Pick false)
  BigWedge-Bool-equiv-Wedge = equiv f g f-g g-f
    where
    module F = BigWedgeRec {X = Pick}
      {C = Wedge (Pick true) (Pick false)}
      (winl (pt (Pick true)))
      (λ {true → winl; false → winr})
      (λ {true → idp; false → wglue})

    module G = WedgeRec {X = Pick true} {Y = Pick false}
      {C = BigWedge Pick}
      (bwin true)
      (bwin false)
      (! (bwglue true) ∙ bwglue false)

    f = F.f
    g = G.f

    abstract
      f-g : ∀ w → f (g w) == w
      f-g = Wedge-elim
        (λ _ → idp)
        (λ _ → idp)
        (↓-∘=idf-in' f g $
          ap f (ap g wglue)
            =⟨ ap (ap f) G.glue-β ⟩
          ap f (! (bwglue true) ∙ bwglue false)
            =⟨ ap-∙ f (! (bwglue true)) (bwglue false) ⟩
          ap f (! (bwglue true)) ∙ ap f (bwglue false)
            =⟨ ap-! f (bwglue true)
               |in-ctx (λ w → w ∙ ap f (bwglue false)) ⟩
          ! (ap f (bwglue true)) ∙ ap f (bwglue false)
            =⟨ F.glue-β true
               |in-ctx (λ w → ! w ∙ ap f (bwglue false)) ⟩
          ap f (bwglue false)
            =⟨ F.glue-β false ⟩
          wglue =∎)

      g-f : ∀ bw → g (f bw) == bw
      g-f = BigWedge-elim
        (! (bwglue true))
        (λ {true → λ _ → idp; false → λ _ → idp})
        (λ {true → ↓-∘=idf-from-square g f $
              ap (ap g) (F.glue-β true) ∙v⊡
              bl-square (bwglue true);
            false → ↓-∘=idf-from-square g f $
              (ap (ap g) (F.glue-β false) ∙ G.glue-β) ∙v⊡
              lt-square (! (bwglue true)) ⊡h vid-square})

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed containers aka interaction structures aka polynomial
-- functors. The notation and presentation here is closest to that of
-- Hancock and Hyvernat in "Programming interfaces and basic topology"
-- (2006/9).
--
------------------------------------------------------------------------

module Data.Container.Indexed where

open import Level
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
open import Data.Product as Prod hiding (map)
open import Relation.Unary using (Pred; _⊆_)
open import Relation.Binary as B using (Preorder; module Preorder)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
open import Relation.Binary.Indexed
open import Data.W.Indexed
open import Data.M.Indexed

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

-- The type and its semantics ("extension").

open import Data.Container.Indexed.Core public
open Container public

-- Abbreviation for the commonly used level one version of indexed
-- containers.

_▷_ : Set → Set → Set₁
I ▷ O = Container I O zero zero

-- The least and greatest fixpoint.

μ ν : ∀ {o c r} {O : Set o} → Container O O c r → Pred O _
μ = W
ν = M

-- Equality, parametrised on an underlying relation.

Eq : ∀ {i o c r ℓ} {I : Set i} {O : Set o} (C : Container I O c r)
     (X Y : Pred I ℓ) → REL X Y ℓ → REL (⟦ C ⟧ X) (⟦ C ⟧ Y) _
Eq C _ _ _≈_ {o₁} {o₂} (c , k) (c′ , k′) =
  o₁ ≡ o₂ × c ≅ c′ × (∀ r r′ → r ≅ r′ → k r ≈ k′ r′)

private

  -- Note that, if propositional equality were extensional, then Eq _≅_
  -- and _≅_ would coincide.

  Eq⇒≅ : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
         {C : Container I O c r} {X : Pred I ℓ} {o₁ o₂ : O}
         {xs : ⟦ C ⟧ X o₁} {ys : ⟦ C ⟧ X o₂} → H.Extensionality r ℓ →
         Eq C X X (λ x₁ x₂ → x₁ ≅ x₂) xs ys → xs ≅ ys
  Eq⇒≅ {xs = c , k} {.c , k′} ext (refl , refl , k≈k′) =
    H.cong (_,_ c) (ext (λ _ → refl) (λ r → k≈k′ r r refl))

setoid : ∀ {i o c r} {I : Set i} {O : Set o} →
         Container I O c r → Setoid I (c ⊔ r) _ → Setoid O _ _
setoid C X = record
  { Carrier       = ⟦ C ⟧ X.Carrier
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl , refl , λ { r .r refl → X.refl }
    ; sym   = sym
    ; trans = λ { {_} {i = xs} {ys} {zs} → trans {_} {i = xs} {ys} {zs}  }
    }
  }
  where
  module X = Setoid X

  _≈_ : Rel (⟦ C ⟧ X.Carrier) _
  _≈_ = Eq C X.Carrier X.Carrier X._≈_

  sym : Symmetric (⟦ C ⟧ X.Carrier) _≈_
  sym {_} {._} {_ , _} {._ , _} (refl , refl , k) =
    refl , refl , λ { r .r refl → X.sym (k r r refl) }

  trans : Transitive (⟦ C ⟧ X.Carrier) _≈_
  trans {._} {_} {._} {_ , _} {._ , _} {._ , _}
    (refl , refl , k) (refl , refl , k′) =
      refl , refl , λ { r .r refl → X.trans (k r r refl) (k′ r r refl) }

------------------------------------------------------------------------
-- Functoriality

-- Indexed containers are functors.

map : ∀ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o}
      (C : Container I O c r) {X : Pred I ℓ₁} {Y : Pred I ℓ₂} →
      X ⊆ Y → ⟦ C ⟧ X ⊆ ⟦ C ⟧ Y
map _ f = Prod.map ⟨id⟩ (λ g → f ⟨∘⟩ g)

module Map where

  identity : ∀ {i o c r} {I : Set i} {O : Set o} (C : Container I O c r)
             (X : Setoid I _ _) → let module X = Setoid X in
             ∀ {o} {xs : ⟦ C ⟧ X.Carrier o} → Eq C X.Carrier X.Carrier
             X._≈_ xs (map C {X.Carrier} ⟨id⟩ xs)
  identity C X = Setoid.refl (setoid C X)

  composition : ∀ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o}
                (C : Container I O c r) {X : Pred I ℓ₁} {Y : Pred I ℓ₂}
                (Z : Setoid I _ _) → let module Z = Setoid Z in
                {f : Y ⊆ Z.Carrier} {g : X ⊆ Y} {o : O} {xs : ⟦ C ⟧ X o} →
                Eq C Z.Carrier Z.Carrier Z._≈_
                  (map C {Y} f (map C {X} g xs))
                  (map C {X} (f ⟨∘⟩ g) xs)
  composition C Z = Setoid.refl (setoid C Z)

------------------------------------------------------------------------
-- Container morphisms

module _ {i₁ i₂ o₁ o₂}
         {I₁ : Set i₁} {I₂ : Set i₂} {O₁ : Set o₁} {O₂ : Set o₂} where

  -- General container morphism.

  record ContainerMorphism {c₁ c₂ r₁ r₂ ℓ₁ ℓ₂}
         (C₁ : Container I₁ O₁ c₁ r₁) (C₂ : Container I₂ O₂ c₂ r₂)
         (f : I₁ → I₂) (g : O₁ → O₂)
         (_∼_ : B.Rel I₂ ℓ₁) (_≈_ : B.REL (Set r₂) (Set r₁) ℓ₂)
         (_·_ : ∀ {A B} → A ≈ B → A → B) :
         Set (i₁ ⊔ i₂ ⊔ o₁ ⊔ o₂ ⊔ c₁ ⊔ c₂ ⊔ r₁ ⊔ r₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      command   : Command C₁ ⊆ Command C₂ ⟨∘⟩ g
      response  : ∀ {o} {c₁ : Command C₁ o} →
                  Response C₂ (command c₁) ≈ Response C₁ c₁
      coherent  : ∀ {o} {c₁ : Command C₁ o} {r₂ : Response C₂ (command c₁)} →
                  f (next C₁ c₁ (response · r₂)) ∼ next C₂ (command c₁) r₂

  open ContainerMorphism public

  -- Plain container morphism.

  _⇒[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
             Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
             Container I₂ O₂ c₂ r₂ → Set _
  C₁ ⇒[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ → R₁) _$_

  -- Linear container morphism.

  _⊸[_/_]_ : ∀ {c₁ c₂ r₁ r₂} →
             Container I₁ O₁ c₁ r₁ → (I₁ → I₂) → (O₁ → O₂) →
             Container I₂ O₂ c₂ r₂ → Set _
  C₁ ⊸[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ _↔_
                                       (λ r₂↔r₁ r₂ → Inverse.to r₂↔r₁ ⟨$⟩ r₂)

  -- Cartesian container morphism.

  _⇒C[_/_]_ : ∀ {c₁ c₂ r} →
              Container I₁ O₁ c₁ r → (I₁ → I₂) → (O₁ → O₂) →
              Container I₂ O₂ c₂ r → Set _
  C₁ ⇒C[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ ≡ R₁)
                                        (λ r₂≡r₁ r₂ → P.subst ⟨id⟩ r₂≡r₁ r₂)

-- Degenerate cases where no reindexing is performed.

module _ {i o c r} {I : Set i} {O : Set o} where

  _⇒_ : B.Rel (Container I O c r) _
  C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂

  _⊸_ : B.Rel (Container I O c r) _
  C₁ ⊸ C₂ = C₁ ⊸[ ⟨id⟩ / ⟨id⟩ ] C₂

  _⇒C_ : B.Rel (Container I O c r) _
  C₁ ⇒C C₂ = C₁ ⇒C[ ⟨id⟩ / ⟨id⟩ ] C₂

------------------------------------------------------------------------
-- Plain morphisms

-- Interpretation of _⇒_.

⟪_⟫ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r} →
      C₁ ⇒ C₂ → (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
⟪ m ⟫ X (c , k) = command m c , λ r₂ →
  P.subst X (coherent m) (k (response m r₂))

module PlainMorphism {i o c r} {I : Set i} {O : Set o} where

  -- Naturality.

  Natural : ∀ {ℓ} {C₁ C₂ : Container I O c r} →
            ((X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X) → Set _
  Natural {C₁ = C₁} {C₂} m =
    ∀ {X} Y → let module Y = Setoid Y in (f : X ⊆ Y.Carrier) →
    ∀ {o} (xs : ⟦ C₁ ⟧ X o) →
      Eq C₂ Y.Carrier Y.Carrier Y._≈_
        (m Y.Carrier $ map C₁ {X} f xs) (map C₂ {X} f $ m X xs)

  -- Natural transformations.

  NT : ∀ {ℓ} (C₁ C₂ : Container I O c r) → Set _
  NT {ℓ} C₁ C₂ = ∃ λ (m : (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X) →
                 Natural m

  -- Container morphisms are natural.

  natural : ∀ {ℓ} (C₁ C₂ : Container I O c r) (m : C₁ ⇒ C₂) → Natural {ℓ} ⟪ m ⟫
  natural _ _ m {X} Y f _ = refl , refl , λ { r .r refl → lemma (coherent m) }
    where
    module Y = Setoid Y

    lemma : ∀ {i j} (eq : i ≡ j) {x} →
            P.subst Y.Carrier eq (f x) Y.≈ f (P.subst X eq x)
    lemma refl = Y.refl

  -- In fact, all natural functions of the right type are container
  -- morphisms.

  complete : ∀ {C₁ C₂ : Container I O c r} (nt : NT C₁ C₂) →
             ∃ λ m → (X : Setoid I _ _) →
                     let module X = Setoid X in
                     ∀ {o} (xs : ⟦ C₁ ⟧ X.Carrier o) →
                     Eq C₂ X.Carrier X.Carrier X._≈_
                       (proj₁ nt X.Carrier xs) (⟪ m ⟫ X.Carrier {o} xs)
  complete {C₁} {C₂} (nt , nat) = m , (λ X xs → nat X
    (λ { (r , eq) → P.subst (Setoid.Carrier X) eq (proj₂ xs r) })
    (proj₁ xs , (λ r → r , refl)))
    where

    m : C₁ ⇒ C₂
    m = record
      { command  = λ      c₁       → proj₁        (lemma c₁)
      ; response = λ {_} {c₁}  r₂  → proj₁ (proj₂ (lemma c₁) r₂)
      ; coherent = λ {_} {c₁} {r₂} → proj₂ (proj₂ (lemma c₁) r₂)
      }
      where
      lemma : ∀ {o} (c₁ : Command C₁ o) → Σ[ c₂ ∈ Command C₂ o ]
              ((r₂ : Response C₂ c₂) → Σ[ r₁ ∈ Response C₁ c₁ ]
              next C₁ c₁ r₁ ≡ next C₂ c₂ r₂)
      lemma c₁ = nt (λ i → Σ[ r₁ ∈ Response C₁ c₁ ] next C₁ c₁ r₁ ≡ i)
                    (c₁ , λ r₁ → r₁ , refl)

  -- Identity.

  id : (C : Container I O c r) → C ⇒ C
  id _ = record
    { command  = ⟨id⟩
    ; response = ⟨id⟩
    ; coherent = refl
    }

  -- Composition.

  infixr 9 _∘_

  _∘_ : {C₁ C₂ C₃ : Container I O c r} →
        C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
  f ∘ g = record
    { command  = command  f ⟨∘⟩ command g
    ; response = response g ⟨∘⟩ response f
    ; coherent = coherent g ⟨ P.trans ⟩ coherent f
    }

  -- Identity and composition commute with ⟪_⟫.

  id-correct : ∀ {ℓ} {C : Container I O c r} → ∀ {X : Pred I ℓ} {o} →
               ⟪ id C ⟫ X {o} ≗ ⟨id⟩
  id-correct _ = refl

  ∘-correct : {C₁ C₂ C₃ : Container I O c r}
              (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) (X : Setoid I (c ⊔ r) _) →
              let module X = Setoid X in
              ∀ {o} {xs : ⟦ C₁ ⟧ X.Carrier o} →
              Eq C₃ X.Carrier X.Carrier X._≈_
                (⟪ f ∘ g ⟫ X.Carrier xs)
                (⟪ f ⟫ X.Carrier (⟪ g ⟫ X.Carrier xs))
  ∘-correct f g X = refl , refl , λ { r .r refl → lemma (coherent g)
                                                        (coherent f) }
    where
    module X = Setoid X

    lemma : ∀ {i j k} (eq₁ : i ≡ j) (eq₂ : j ≡ k) {x} →
      P.subst X.Carrier (P.trans eq₁ eq₂) x
      X.≈
      P.subst X.Carrier eq₂ (P.subst X.Carrier eq₁ x)
    lemma refl refl = X.refl

------------------------------------------------------------------------
-- Linear container morphisms

module LinearMorphism
  {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
  (m : C₁ ⊸ C₂)
  where

  morphism : C₁ ⇒ C₂
  morphism = record
    { command  = command m
    ; response = _⟨$⟩_ (Inverse.to (response m))
    ; coherent = coherent m
    }

  ⟪_⟫⊸ : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
  ⟪_⟫⊸ = ⟪ morphism ⟫

open LinearMorphism public using (⟪_⟫⊸)

------------------------------------------------------------------------
-- Cartesian morphisms

module CartesianMorphism
  {i o c r} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r}
  (m : C₁ ⇒C C₂)
  where

  morphism : C₁ ⇒ C₂
  morphism = record
    { command  = command m
    ; response = P.subst ⟨id⟩ (response m)
    ; coherent = coherent m
    }

  ⟪_⟫C : ∀ {ℓ} (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
  ⟪_⟫C = ⟪ morphism ⟫

open CartesianMorphism public using (⟪_⟫C)

------------------------------------------------------------------------
-- All and any

-- □ and ◇ are defined in the core module.

module _ {i o c r ℓ₁ ℓ₂} {I : Set i} {O : Set o} (C : Container I O c r)
         {X : Pred I ℓ₁} {P Q : Pred (Σ I X) ℓ₂} where

  -- All.

  □-map : P ⊆ Q → □ C P ⊆ □ C Q
  □-map P⊆Q = _⟨∘⟩_ P⊆Q

  -- Any.

  ◇-map : P ⊆ Q → ◇ C P ⊆ ◇ C Q
  ◇-map P⊆Q = Prod.map ⟨id⟩ P⊆Q

-- Membership.

infix 4 _∈_

_∈_ : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
      {C : Container I O c r} {X : Pred I (i ⊔ ℓ)} → REL X (⟦ C ⟧ X) _
_∈_ {C = C} {X} x xs = ◇ C {X = X} (_≅_ x) (, xs)


text:
-- Andreas, 2017-02-13, issue #2456 reported by identicalsnowflake
-- Introduced by fix for #1698

record Class (t : Set) : Set where

postulate
  t : Set

  instance Class t

-- Should give error, but not internal error.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed containers core
------------------------------------------------------------------------

module Data.Container.Indexed.Core where

open import Level
open import Data.Product
open import Relation.Unary

infix 5 _◃_/_

record Container {i o} (I : Set i) (O : Set o) (c r : Level) :
                 Set (i ⊔ o ⊔ suc c ⊔ suc r) where
  constructor _◃_/_
  field
    Command  : (o : O) → Set c
    Response : ∀ {o} → Command o → Set r
    next     : ∀ {o} (c : Command o) → Response c → I

-- The semantics ("extension") of an indexed container.

⟦_⟧ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} → Container I O c r →
      Pred I ℓ → Pred O _
⟦ C ◃ R / n ⟧ X o = Σ[ c ∈ C o ] ((r : R c) → X (n c r))

------------------------------------------------------------------------
-- All and any

module _ {i o c r ℓ} {I : Set i} {O : Set o}
         (C : Container I O c r) {X : Pred I ℓ} where

  -- All.

  □ : ∀ {ℓ′} → Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _
  □ P (_ , _ , k) = ∀ r → P (_ , k r)

  -- Any.

  ◇ : ∀ {ℓ′} → Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _
  ◇ P (_ , _ , k) = ∃ λ r → P (_ , k r)


text:
-- Andreas, 2018-10-15, issue #3264 reported by Guillaume Brunerie

-- Refine should not say "cannot refine" just because of a termination error.

f : Set → Set
f A = {!f!}  -- C-c C-r

-- EXPECTED ANSWER:
--
-- ?1 : Set
-- ———— Errors ————————————————————————————————————————————————
-- Termination checking failed for the following functions:
--   f
-- Problematic calls:
--   f (?1 (A = A))
-- when checking that the expression f ? has type Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of < to ≤, along with a number of properties
------------------------------------------------------------------------

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

open import Relation.Binary

module Relation.Binary.StrictToNonStrict
         {a ℓ₁ ℓ₂} {A : Set a}
         (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
         where

open import Relation.Nullary
open import Relation.Binary.Consequences
open import Function
open import Data.Product
open import Data.Sum
open import Data.Empty

------------------------------------------------------------------------
-- Conversion

-- _<_ can be turned into _≤_ as follows:

_≤_ : Rel A _
x ≤ y = (x < y) ⊎ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

reflexive : _≈_ ⇒ _≤_
reflexive = inj₂

antisym : IsEquivalence _≈_ →
          Transitive _<_ →
          Irreflexive _≈_ _<_ →
          Antisymmetric _≈_ _≤_
antisym eq trans irrefl = as
  where
  module Eq = IsEquivalence eq

  as : Antisymmetric _≈_ _≤_
  as (inj₂ x≈y) _          = x≈y
  as (inj₁ _)   (inj₂ y≈x) = Eq.sym y≈x
  as (inj₁ x<y) (inj₁ y<x) =
    ⊥-elim (trans∧irr⟶asym {_≈_ = _≈_} Eq.refl trans irrefl x<y y<x)

trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ →
        Transitive _<_ → Transitive _≤_
trans eq <-resp-≈ <-trans = tr
  where
  module Eq = IsEquivalence eq

  tr : Transitive _≤_
  tr (inj₁ x<y) (inj₁ y<z) = inj₁ $ <-trans x<y y<z
  tr (inj₁ x<y) (inj₂ y≈z) = inj₁ $ proj₁ <-resp-≈ y≈z x<y
  tr (inj₂ x≈y) (inj₁ y<z) = inj₁ $ proj₂ <-resp-≈ (Eq.sym x≈y) y<z
  tr (inj₂ x≈y) (inj₂ y≈z) = inj₂ $ Eq.trans x≈y y≈z

≤-resp-≈ : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → _≤_ Respects₂ _≈_
≤-resp-≈ eq <-resp-≈ = ((λ {_ _ _} → resp₁) , (λ {_ _ _} → resp₂))
  where
  module Eq = IsEquivalence eq

  resp₁ : ∀ {x y' y} → y' ≈ y → x  ≤ y' → x ≤ y
  resp₁ y'≈y (inj₁ x<y') = inj₁ (proj₁ <-resp-≈ y'≈y x<y')
  resp₁ y'≈y (inj₂ x≈y') = inj₂ (Eq.trans x≈y' y'≈y)

  resp₂ : ∀ {y x' x} → x' ≈ x → x' ≤ y  → x ≤ y
  resp₂ x'≈x (inj₁ x'<y) = inj₁ (proj₂ <-resp-≈ x'≈x x'<y)
  resp₂ x'≈x (inj₂ x'≈y) = inj₂ (Eq.trans (Eq.sym x'≈x) x'≈y)

total : Trichotomous _≈_ _<_ → Total _≤_
total <-tri x y with <-tri x y
... | tri< x<y x≉y x≯y = inj₁ (inj₁ x<y)
... | tri≈ x≮y x≈y x≯y = inj₁ (inj₂ x≈y)
... | tri> x≮y x≉y x>y = inj₂ (inj₁ x>y)

decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
decidable ≈-dec <-dec x y with ≈-dec x y | <-dec x y
... | yes x≈y | _       = yes (inj₂ x≈y)
... | no  x≉y | yes x<y = yes (inj₁ x<y)
... | no  x≉y | no  x≮y = no helper
  where
  helper : x ≤ y → ⊥
  helper (inj₁ x<y) = x≮y x<y
  helper (inj₂ x≈y) = x≉y x≈y

decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
decidable' compare x y with compare x y
... | tri< x<y _   _ = yes (inj₁ x<y)
... | tri≈ _   x≈y _ = yes (inj₂ x≈y)
... | tri> x≮y x≉y _ = no helper
  where
  helper : x ≤ y → ⊥
  helper (inj₁ x<y) = x≮y x<y
  helper (inj₂ x≈y) = x≉y x≈y


text:
module Prelude.Fin where

open import Prelude.Nat
open import Prelude.Equality
open import Prelude.Decidable
open import Prelude.Ord
open import Prelude.Bool
open import Prelude.Function
open import Prelude.Number
open import Prelude.Nat.Properties using (suc-inj)

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} (i : Fin n) → Fin (suc n)

finToNat : ∀ {@erased n} → Fin n → Nat
finToNat  zero   = zero
finToNat (suc i) = suc (finToNat i)

finToNat-inj : ∀ {@erased n} {i j : Fin n} → finToNat i ≡ finToNat j → i ≡ j
finToNat-inj {i = zero } {zero } p = refl
finToNat-inj {i = zero } {suc j} ()
finToNat-inj {i = suc i} {zero } ()
finToNat-inj {i = suc i} {suc j} p rewrite finToNat-inj (suc-inj p) = refl

natToFin : ∀ {n} (m : Nat) {{m<n : IsTrue (lessNat m n)}} → Fin n
natToFin {zero }  _   {{}}
natToFin {suc n}  zero   = zero
natToFin {suc n} (suc m) = suc (natToFin m)

instance
  NumberFin : ∀ {n} → Number (Fin n)
  Number.Constraint (NumberFin {n}) k = IsTrue (lessNat k n)
  fromNat {{NumberFin}} = natToFin

--- Equality ---

fsuc-inj : ∀ {@erased n} {i j : Fin n} → Fin.suc i ≡ suc j → i ≡ j
fsuc-inj refl = refl

private
  eqFin : ∀ {@erased n} (i j : Fin n) → Dec (i ≡ j)
  eqFin  zero    zero    = yes refl
  eqFin  zero   (suc  j) = no λ ()
  eqFin (suc i)  zero    = no λ ()
  eqFin (suc i) (suc  j) with eqFin i j
  eqFin (suc i) (suc .i) | yes refl = yes refl
  eqFin (suc i) (suc  j) | no neq   = no λ eq → neq (fsuc-inj eq)

instance
  EqFin : ∀ {n} → Eq (Fin n)
  _==_ {{EqFin}} = eqFin

--- Ord ---

instance
  OrdFin : ∀ {n} → Ord (Fin n)
  OrdFin = OrdBy finToNat-inj

  OrdLawsFin : ∀ {n} → Ord/Laws (Fin n)
  OrdLawsFin = OrdLawsBy finToNat-inj

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

open import Level
open import Data.Product using (Σ; _,_; Σ-syntax; uncurry; proj₂)

open import Categories.Support.PropositionalEquality

open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.Cones
open import Categories.Object.Terminal as T using (Terminal; module Terminal)
import Categories.Morphisms as Mor
open import Categories.Cone using (module Cone; module ConeOver)

module LimitsOf {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

  private module L = Terminal

  open Category C
  open Category J using () renaming (Obj to Dot)
  open Functor F
  open Mor C using (_≅_; _≡ⁱ_)
  open Mor (Cones F) using () renaming (_≅_ to _⇿_; _≡ⁱ_ to _≜ⁱ_)
  open Category (Cones F) using () renaming (Obj to Cone; _≡_ to _≜₁_; _∘_ to _▵_; _⇒_ to _⇾_; id to id▵)
  open ConeOver F using (_≜_; ≜-refl; ≜-sym; ≜-trans; heterogenize; homogenize; ConeUnder; tether; untether; _≜′_) renaming (module _≜_ to ≜; module _≜′_ to ≜′)
  open Heterogeneous C

  -- Isomorphic to an terminal object, but worth keeping distinct in case we change its definition
  record Limit : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    field
      terminal : Terminal (Cones F)

    private module terminal = Terminal terminal
    module Fl = Float F

    {-
    vertex : Obj
    vertex = Cone.N terminal.⊤

    proj : ∀ j → vertex ⇒ F₀ j
    proj = Cone.ψ terminal.⊤

    proj-cone : Cone
    proj-cone = terminal.⊤
    -}

    open terminal public using () renaming (⊤ to proj-cone)
    open Cone proj-cone public using () renaming (N to vertex; ψ to proj)

    rep-cone : (K : Cone) → (K ⇾ proj-cone)
    rep-cone K = terminal.! {K}

    rep : (K : Cone) → (Cone.N K ⇒ vertex)
    rep K = ConeMorphism.f (terminal.! {K})

    unrep : ∀ {X} → (X ⇒ vertex) → Cone
    unrep f = record
      { N = domain f
      ; ψ = λ j → proj j ∘ f
      ; commute = λ l → Equiv.trans (Equiv.sym assoc) (∘-resp-≡ˡ (commute l))
      }
      where
      open Cone proj-cone

    conify : ∀ {X} (f : X ⇒ vertex) → (unrep f ⇾ proj-cone)
    conify f = record { f = f; commute = Equiv.refl }

    unrep-cone : ∀ {K : Cone} → (K ⇾ proj-cone) → Cone
    unrep-cone κ = unrep (ConeMorphism.f κ)

    commute-cone : ∀ {K : Cone} → unrep-cone (rep-cone K) ≜ K
    commute-cone {K} = record
      { N-≣ = ≣-refl
      ; ψ-≡ = λ j → ≡⇒∼ (Equiv.sym (ConeMorphism.commute (rep-cone K)))
      }

    .commute : ∀ K j → proj j ∘ rep K ≡ Cone.ψ K j
    commute K = λ j → Equiv.sym (ConeMorphism.commute (rep-cone K))

    private
      domain▵ : ∀ {X Y} → X ⇾ Y → Cone
      domain▵ {X} _ = X

    .universal-cone : ∀ {K : Cone} {i : K ⇾ proj-cone} → unrep-cone i ≜ K → Cones F [ rep-cone K ≡ i ]
    universal-cone {K} {i} pf = terminal.!-unique i

    .universal : ∀ {K : Cone} {i : Cone.N K ⇒ vertex} → unrep i ≜ K → rep K ≡ i
    universal {K} {i} pf = terminal.!-unique (Fl.floatʳ (heterogenize (homogenize pf ≣-refl)) (conify i))
    -- complicated, isn't it?  but it's necessary in order to make the float
    --   compute enough for the !-unique to typecheck.  by replacing the
    --   N-≣ in pf with ≣-refl we can make it happen!

    g-η-cone₀ : ∀ {K} {κ : K ⇾ proj-cone} → K ≜ unrep-cone κ
    g-η-cone₀ {K} {κ} = record { N-≣ = ≣-refl; ψ-≡ = λ j → ≡⇒∼ (ConeMorphism.commute κ) }

    .g-η-cone : ∀ {K} {κ : K ⇾ proj-cone} → rep-cone (unrep-cone κ) ≜₁ Fl.floatʳ (g-η-cone₀ {κ = κ}) κ
    g-η-cone {κ = κ} = terminal.!-unique (Fl.floatʳ (g-η-cone₀ {κ = κ}) κ)

    .g-η : ∀ {X} {f : X ⇒ vertex} → rep (unrep f) ≡ f
    g-η {f = f} = terminal.!-unique (conify f)

    .η-cone : Cones F [ rep-cone proj-cone ≡ Category.id (Cones F) ]
    η-cone = terminal.⊤-id (rep-cone proj-cone)

    .η : rep proj-cone ≡ id
    η = η-cone

    .rep-cone-cong : ∀ {K₁ K₂} (K₁≜K₂ : K₁ ≜ K₂) → Cones F [ Fl.floatʳ K₁≜K₂ (rep-cone K₁) ≡ rep-cone K₂ ]
    rep-cone-cong {K₁} {K₂} K₁≜K₂ =
      Equiv.sym (terminal.!-unique (Fl.floatʳ K₁≜K₂ (rep-cone K₁)))

    .rep-cong′ : ∀ {N} {K₁ K₂ : ConeUnder N} → K₁ ≜′ K₂ → rep (untether K₁) ≡ rep (untether K₂)
    rep-cong′ {N} {K₁} {K₂} K₁≜′K₂ =
      Equiv.sym (terminal.!-unique (Fl.floatʳ (heterogenize K₁≜′K₂) (rep-cone (untether K₁))))

    rep-cong : ∀ {K₁ K₂} → K₁ ≜ K₂ → rep K₁ ∼ rep K₂
    rep-cong K₁≜K₂ =
      ≡⇒∼ʳ (≜.N-≣ K₁≜K₂) (rep-cone-cong K₁≜K₂)

    .rep-cone∘ : ∀ {K K′} {q : K′ ⇾ K} → Cones F [ Cones F [ rep-cone K ∘ q ] ≡ rep-cone K′ ]
    rep-cone∘ {K} {q = q} = Equiv.sym (terminal.!-unique (rep-cone K ▵ q))

    .rep∘ : ∀ {K K′} {q : K′ ⇾ K} → rep K ∘ ConeMorphism.f q ≡ rep K′
    rep∘ {K} {K′} {q} = rep-cone∘ {K} {K′} {q}

    .rep-cone-self-id : rep-cone proj-cone ≜₁ id▵
    rep-cone-self-id = terminal.!-unique id▵

    .rep-self-id : rep proj-cone ≡ id
    rep-self-id = terminal.!-unique id▵

  open Limit

  -- Properties
  --
  -- These are a little different from the raw ones for Terminal since they
  -- deal with isomorphisms in C instead of in Cones F.

  -- First, a lemma:

  open import Categories.Square

  -- do these lemmas belong in Cones?

  isos-lift-to-cones : ∀ (κ : Cone) {v : Obj} → Cone.N κ ≅ v → Σ[ κ′ ∈ Cone ] κ ⇿ κ′
  isos-lift-to-cones κ {v} κ≅v =
      record
      { N = v
      ; ψ = λ X → (Cone.ψ κ X) ∘ g
      ; commute = λ f' → pullˡ (Cone.commute κ f')
      }
    , record
      { f = record { f = f; commute = Equiv.sym (cancelRight isoˡ) }
      ; g = record { f = g; commute = Equiv.refl }
      ; iso = record { isoˡ = isoˡ; isoʳ = isoʳ }
      }
    where
    open Mor._≅_ κ≅v
    open GlueSquares C

  isos-lower-from-cones : ∀ {κ₁ κ₂ : Cone} → κ₁ ⇿ κ₂ → Cone.N κ₁ ≅ Cone.N κ₂
  isos-lower-from-cones κ₁⇿κ₂ = record
    { f = ConeMorphism.f f
    ; g = ConeMorphism.f g
    ; iso = record { isoˡ = isoˡ; isoʳ = isoʳ }
    }
    where
    open Mor._≅_ κ₁⇿κ₂

  ≜ⁱ⇒≡ⁱ : ∀ {κ₁ κ₂} {i₁ i₂ : κ₁ ⇿ κ₂} → i₁ ≜ⁱ i₂
        → isos-lower-from-cones i₁ ≡ⁱ isos-lower-from-cones i₂
  ≜ⁱ⇒≡ⁱ pf = record { f-≡ = f-≡; g-≡ = g-≡ }
    where open Mor._≡ⁱ_ pf

  up-to-iso-cone : (L₁ L₂ : Limit) → proj-cone L₁ ⇿ proj-cone L₂
  up-to-iso-cone L₁ L₂ = T.up-to-iso (Cones F) (terminal L₁) (terminal L₂)

  up-to-iso : (L₁ L₂ : Limit) → vertex L₁ ≅ vertex L₂
  up-to-iso L₁ L₂ = isos-lower-from-cones (up-to-iso-cone L₁ L₂)

  transport-by-iso-cone : (L : Limit) {κ : Cone} → proj-cone L ⇿ κ → Limit
  transport-by-iso-cone L L⇿κ = record
    { terminal = T.transport-by-iso (Cones F) (terminal L) L⇿κ
    }

  transport-by-iso : (L : Limit) {v : Obj} → vertex L ≅ v → Limit
  transport-by-iso L L≅v = transport-by-iso-cone L (proj₂ p)
    where p = isos-lift-to-cones (proj-cone L) L≅v

  .up-to-iso-cone-unique : ∀ L L′ → (i : proj-cone L ⇿ proj-cone L′) → up-to-iso-cone L L′ ≜ⁱ i
  up-to-iso-cone-unique L L′ i = T.up-to-iso-unique (Cones F) (terminal L) (terminal L′) i

  -- XXX probably not true -- what is?  only the above?
  -- .up-to-iso-unique : ∀ L L′ → (i : vertex L ≅ vertex L′) → up-to-iso L L′ ≡ⁱ i
  -- up-to-iso-unique L L′ i = ≜ⁱ⇒≡ⁱ {!up-to-iso-unique-cone L L′ !}

  .up-to-iso-cone-invˡ : ∀ {L κ} {i : proj-cone L ⇿ κ} → up-to-iso-cone L (transport-by-iso-cone L i) ≜ⁱ i
  up-to-iso-cone-invˡ {L} {i = i} = up-to-iso-cone-unique L (transport-by-iso-cone L i) i

  .up-to-iso-invˡ : ∀ {L X} {i : vertex L ≅ X} → up-to-iso L (transport-by-iso L i) ≡ⁱ i
  up-to-iso-invˡ {L₁} {i = i} = ≜ⁱ⇒≡ⁱ (up-to-iso-cone-invˡ {L₁} {i = proj₂ (isos-lift-to-cones (proj-cone L₁) i)})

  up-to-iso-cone-invʳ : ∀ {L L′} → proj-cone (transport-by-iso-cone L (up-to-iso-cone L L′)) ≜ proj-cone L′
  up-to-iso-cone-invʳ {L} {L′} = ≜-refl

  up-to-iso-invʳ : ∀ {L L′} → vertex (transport-by-iso L (up-to-iso L L′)) ≣ vertex L′
  up-to-iso-invʳ {t} {t′} = ≣-refl

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Data.Maybe
open import Data.Product hiding (Σ)

open import Axiom.Extensionality.Propositional
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

open import EffectAnnotations
open import Types

module AEff where

-- ARITY ASSIGNMENT TO SIGNATURES OF SIGNALS, INTERRUPTS, AND BASE CONSTANTS

postulate payload : Σₛ → GType     -- payload type assignment for signal and interrupt names

postulate Σ-base : Set             -- set of base constants
postulate ar-base : Σ-base → BType -- arity assignment to base constants

-- SNOC LISTS FOR MODELLING CONTEXTS

infixl 30 _∷_

data SnocList (A : Set) : Set where
  []  : SnocList A
  _∷_ : SnocList A → A → SnocList A

-- CONTEXTS AND VARIABLES IN THEM (I.E., DE BRUIJN INDICES)

Ctx = SnocList VType

data _∈_ (X : VType) : Ctx → Set where
  Hd : {Γ : Ctx} → X ∈ (Γ ∷ X)
  Tl : {Γ : Ctx} {Y : VType} → X ∈ Γ → X ∈ (Γ ∷ Y)

-- DERIVATIONS OF WELL-TYPED TERMS

mutual

  data _⊢V⦂_ (Γ : Ctx) : VType → Set where

    `_  : {X : VType} →
          X ∈ Γ →
          -------------
          Γ ⊢V⦂ X

    ``_  : (c : Σ-base) →
          --------------
          Γ ⊢V⦂ ``(ar-base c)

    ƛ   : {X : VType}
          {C : CType} →
          Γ ∷ X ⊢M⦂ C →
          -------------
          Γ ⊢V⦂ X ⇒ C

    ⟨_⟩ : {X : VType} →
          Γ ⊢V⦂ X →
          -------------
          Γ ⊢V⦂ ⟨ X ⟩

  infix 40 _·_

  data _⊢M⦂_ (Γ : Ctx) : CType → Set where

    return           : {X : VType}
                       {o : O}
                       {i : I} →
                       Γ ⊢V⦂ X →
                       -----------------
                       Γ ⊢M⦂ X ! (o , i)

    let=_`in_        : {X Y : VType}
                       {o : O}
                       {i : I} →
                       Γ ⊢M⦂ X ! (o , i) →
                       Γ ∷ X ⊢M⦂ Y ! (o , i) →
                       -----------------------
                       Γ ⊢M⦂ Y ! (o , i)

    letrec_`in_      : {X : VType}
                       {C D : CType} →
                       Γ ∷ (X ⇒ C) ∷ X ⊢M⦂ C →
                       Γ ∷ (X ⇒ C) ⊢M⦂ D →
                       -----------------------
                       Γ ⊢M⦂ D

    _·_              : {X : VType}
                       {C : CType} →
                       Γ ⊢V⦂ X ⇒ C →
                       Γ ⊢V⦂ X →
                       -------------
                       Γ ⊢M⦂ C

    ↑                : {X : VType}
                       {o : O}
                       {i : I} →
                       (op : Σₛ) →
                       op ∈ₒ o →
                       Γ ⊢V⦂ ``(payload op) →
                       Γ ⊢M⦂ X ! (o , i) →
                       ----------------------
                       Γ ⊢M⦂ X ! (o , i)

    ↓                : {X : VType}
                       {o : O}
                       {i : I}
                       (op : Σₛ) →
                       Γ ⊢V⦂ ``(payload op) →
                       Γ ⊢M⦂ X ! (o , i) →
                       ----------------------
                       Γ ⊢M⦂ X ! op ↓ₑ (o , i)

    promise_∣_↦_`in_ : {X Y : VType}
                       {o o' : O}
                       {i i' : I} →
                       (op : Σₛ) →
                       lkpᵢ op i ≡ just (o' , i') →
                       Γ ∷ ``(payload op) ⊢M⦂ ⟨ X ⟩ ! (o' , i') →
                       Γ ∷ ⟨ X ⟩ ⊢M⦂ Y ! (o , i) →
                       ------------------------------------------
                       Γ ⊢M⦂ Y ! (o , i)

    await_until_     : {X : VType}
                       {C : CType} →
                       Γ ⊢V⦂ ⟨ X ⟩ →
                       Γ ∷ X ⊢M⦂ C →
                       --------------
                       Γ ⊢M⦂ C

    coerce           : {X : VType}
                       {o o' : O}
                       {i i' : I} →
                       o ⊑ₒ o' →
                       i ⊑ᵢ i' →
                       Γ ⊢M⦂ X ! (o , i) →
                       -------------------
                       Γ ⊢M⦂ X ! (o' , i')

-- DERIVATIONS OF WELL-TYPED PROCESSES

infix 10 _⊢P⦂_

data _⊢P⦂_ (Γ : Ctx) : {o : O} → PType o → Set where

  run     : {X : VType}
            {o : O}
            {i : I} →
            Γ ⊢M⦂ X ! (o , i) →
            -------------------
            Γ ⊢P⦂ X ‼ o , i

  _∥_     : {o o' : O}
            {PP : PType o} →
            {QQ : PType o'} →
            Γ ⊢P⦂ PP →
            Γ ⊢P⦂ QQ →
            --------------
            Γ ⊢P⦂ (PP ∥ QQ)

  ↑       : {o : O} →
            {PP : PType o}
            (op : Σₛ) →
            op ∈ₒ o →
            Γ ⊢V⦂ ``(payload op) →
            Γ ⊢P⦂ PP →
            ----------------------
            Γ ⊢P⦂ PP

  ↓       : {o : O}
            {PP : PType o}
            (op : Σₛ) →
            Γ ⊢V⦂ ``(payload op) →
            Γ ⊢P⦂ PP →
            ----------------------
            Γ ⊢P⦂ op ↓ₚ PP

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


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

open import HoTT
open import homotopy.HSpace

module homotopy.EM1HSpace where

module EM₁HSpace {i} (G : AbGroup i) where

  private
    module G = AbGroup G

  mult-loop : (g : G.El) (x : EM₁ G.grp) → x == x
  mult-loop g = EM₁-elim
    {P = λ x → x == x}

    (emloop g)
    loop'
    (λ _ _ → set-↓-has-all-paths-↓)
    where
    abstract
      loop' : (g' : G.El) → emloop' G.grp g == emloop g [ (λ x → x == x) ↓ emloop g' ]
      loop' g' = ↓-idf=idf-in' $
        emloop g ∙ emloop g'     =⟨ ! (emloop-comp' G.grp g g') ⟩
        emloop (G.comp g g')     =⟨ ap (emloop' G.grp) (G.comm g g') ⟩
        emloop (G.comp g' g)     =⟨ emloop-comp' G.grp g' g ⟩
        emloop g' ∙ emloop g     =⟨ ∙=∙' (emloop g') (emloop g) ⟩
        emloop g' ∙' emloop g    ∎

  mult-hom : GroupHom G.grp
    (Ω^S-group 0 ⊙[ (EM₁ G.grp → EM₁ G.grp) , (λ x → x) ])
  mult-hom = record {f = f; pres-comp = pres-comp}
    where
    f = λ g → λ= (mult-loop g)

    pres-comp = λ g₁ g₂ →
      ap λ= (λ= (EM₁-elim
        {P = λ x → mult-loop (G.comp g₁ g₂) x
                == mult-loop g₁ x ∙ mult-loop g₂ x}
        (emloop-comp g₁ g₂)
        (λ _ → prop-has-all-paths-↓)
        (λ _ _ → set-↓-has-all-paths-↓)))
      ∙ ! (∙-λ= _ _)

  mult : EM₁ G.grp → EM₁ G.grp → EM₁ G.grp
  mult = EM₁-rec {C = EM₁ G.grp → EM₁ G.grp} (λ x → x) mult-hom

  H-⊙EM₁ : HSpaceStructure (⊙EM₁ G.grp)
  H-⊙EM₁ = from-alt-h-space $ record { μ = mult; unit-l = unit-l; unit-r = unit-r; coh = coh }
    where
    unit-l : (x : EM₁ G.grp) → mult embase x == x
    unit-l = EM₁-elim
      {P = λ x → mult embase x == x}
      idp
      (λ g → ↓-app=idf-in $ ∙'-unit-l (emloop g) ∙ (! (ap-idf (emloop g)))
                            ∙ ! (∙-unit-r (ap (mult embase) (emloop g))))
      (λ _ _ → set-↓-has-all-paths-↓)

    unit-r : (x : EM₁ G.grp) → mult x embase == x
    unit-r = EM₁-elim
      {P = λ x → mult x embase == x}
      idp
      (λ g → ↓-app=idf-in $
         idp ∙' emloop g
           =⟨ ∙'-unit-l (emloop g) ⟩
         emloop g
           =⟨ ! (app=-β (mult-loop g) embase) ⟩
         app= (λ= (mult-loop g)) embase
           =⟨ ! (EM₁Rec.emloop-β {C = EM₁ G.grp → EM₁ G.grp}
                   (λ x → x) mult-hom g)
              |in-ctx (λ w → app= w embase) ⟩
         app= (ap mult (emloop g)) embase
           =⟨ ∘-ap (λ f → f embase) mult (emloop g) ⟩
         ap (λ z → mult z embase) (emloop g)
           =⟨ ! (∙-unit-r (ap (λ z → mult z embase) (emloop g))) ⟩
         ap (λ z → mult z embase) (emloop g) ∙ idp ∎)
      (λ _ _ → set-↓-has-all-paths-↓)

    coh : unit-l embase == unit-r embase
    coh = idp

  open HSpaceStructure H-⊙EM₁

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Sigma.Renaming.Vec where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Fin as Fin using (Fin; zero; suc)

open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)

open import Data.Vec as V using (Vec; []; _∷_; map; _[_]≔_)
  renaming (head to headᵥ; tail to tailᵥ; lookup to lookupᵥ; insert to insertᵥ; remove to removeᵥ; updateAt to updateAtᵥ)
open import Data.HVec as HV using (HVec; []; _∷_)
  renaming (head to headₕ; tail to tailₕ; lookup to lookupₕ; insert to insertₕ; remove to removeₕ; updateAt to updateAtₕ)

open import Function as Fun using (_∘_)

open import Sigma.Renaming.Base as R using (Ren)
  renaming (id to idᵣ; ↑ to ↑ᵣ; _⇑ to _⇑ᵣ)

open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; refl; sym; trans; cong; cong₂; cong-app; subst)
open Eq.≡-Reasoning

-- ------------------------------------------------------------------------
-- Vectored Renaming Shape

-- A renaming ρ : 𝕀ᵐ → 𝕀ⁿ is defined by a *shape*, denoted m ↦ n.
--
-- Similarly, a vectored renaming ρs = [ρ₁ ; ...; ρₖ] : [𝕀ᵐ₁ → 𝕀ⁿ₁, ...; 𝕀ᵐₖ → 𝕀ⁿₖ]
-- is defined by a vector of renaming shapes, denoted [m₁ ↦ n₁; ...; mₖ ↦ nₖ]

module Shape where

  open import Data.Vec using (lookup; replicate; _[_]%=_; _[_]≔_)

  -- TODO: Implement shape for renaming?

  Shape : ℕ → Set
  Shape n = Vec (ℕ × ℕ) n

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

  pattern _↦_ m n = ⟨ m , n ⟩

  shape : ∀ { n } → Shape n → Fin n → ℕ × ℕ
  shape = lookup

  dom : ∀ { n } → Shape n → Fin n → ℕ
  dom s = proj₁ ∘ (shape s)

  rng : ∀ { n } → Shape n → Fin n → ℕ
  rng s = proj₂ ∘ (shape s)

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

  id : ∀ { m } → ℕ → Shape m
  id n = replicate (n ↦ n)

  ↑ : ∀ { m } → ℕ → Fin m → Shape m
  ↑ n i = id n [ i ]≔ n ↦ (1 + n)

  -- TODO: This may become a pain, used a hack to use := instead of
  -- %=
  infix 10 _⇑_
  _⇑_ : ∀ { n } → Shape n → Fin n → Shape n
  s ⇑ i = s [ i ]≔ ⇑ (lookup s i)
    where
      ⇑ : ℕ × ℕ → ℕ × ℕ
      ⇑ (m ↦ n) = (1 + m) ↦ (1 + n)

open Shape using (Shape; _↦_) renaming (id to idₛ; ↑ to ↑ₛ; _⇑_ to _⇑ₛ_)

-- TODO: Move this when implementing shapes on renamings?
-- IDEA: Call it an interpretation of a shape
-- use the nice brackets ;)

⦅_⦆ : ℕ × ℕ → Set
⦅ m ↦ n ⦆ = Ren m n

-- ------------------------------------------------------------------------
-- Vectored Renaming

-- A vectored renaming ρs = [ρ₁ ; ...; ρₖ] : [𝕀ᵐ₁ → 𝕀ⁿ₁, ...; 𝕀ᵐₖ → 𝕀ⁿₖ]
-- defined by it's shape: [m₁ ↦ n₁; ...; mₖ ↦ nₖ]
-- It is implemented as a hetrogenous vector.

VRen : ∀ n → Shape n → Set
VRen n shape = HVec n (map ⦅_⦆ shape)

length : ∀ { n S } → VRen n S → ℕ
length { n = n } _ = n

shape : ∀ { n S } → VRen n S → Shape n
shape { S = shape } _ = shape

-- ------------------------------------------------------------------------
-- Basic operations (ported from HVec)

-- Anonymous module containing properties about
-- Data.Vec's map composed w/ other operations
module _ { ℓ₁ ℓ₂ } { A : Set ℓ₁ } { B : Set ℓ₂ } where
  open import Data.Vec using (head; tail; insert; remove)

  private
    variable
      m n k : ℕ

  open import Data.Vec.Properties using (lookup-map; map-[]≔) public

  unfold-map : (f : A → B) (x : A) (xs : Vec A n)
    → map f (x ∷ xs) ≡ f x ∷ map f xs
  unfold-map f x [] = refl
  unfold-map f x (_ ∷ xs) = refl

  unfold-remove : (x : A) (xs : Vec A (1 + n)) (i : Fin (1 + n))
    → remove (x ∷ xs) (suc i) ≡ x ∷ remove xs i
  unfold-remove x (_ ∷ xs) zero = refl
  unfold-remove x (y ∷ xs) (suc i) = refl

  head-map : (f : A → B) (xs : Vec A (1 + n))
    → head (map f xs) ≡ f (head xs)
  head-map f (x ∷ xs) = refl

  tail-map : (f : A → B) (xs : Vec A (1 + n))
    → tail (map f xs) ≡ map f (tail xs)
  tail-map f (x ∷ xs) = refl

  insert-map : (f : A → B) (x : A) (xs : Vec A n) (i : Fin (1 + n))
    → insert (map f xs) i (f x) ≡ map f (insert xs i x)
  insert-map f x xs zero = refl
  insert-map f x (_ ∷ xs) (suc i) rewrite insert-map f x xs i = refl

  remove-map : (f : A → B) (xs : Vec A (1 + n)) (i : Fin (1 + n))
    → remove (map f xs) i ≡ map f (remove xs i)
  remove-map f (_ ∷ xs) zero = refl
  remove-map f (x ∷ y ∷ xs) (suc i) rewrite remove-map f (y ∷ xs) i = refl

module _ where

  private
    variable
      m n k : ℕ
      S : Shape m

  head : VRen (1 + m) S → ⦅ headᵥ S ⦆
  head ρs rewrite sym (head-map ⦅_⦆ (shape ρs)) = headₕ ρs

  tail : VRen (1 + m) S → VRen m (tailᵥ S)
  tail ρs rewrite sym (tail-map ⦅_⦆ (shape ρs)) = tailₕ ρs

  lookup : VRen m S → (i : Fin m) → ⦅ lookupᵥ S i ⦆
  lookup ρs i rewrite sym (lookup-map i ⦅_⦆ (shape ρs)) = lookupₕ ρs i

  insert : VRen m S → (i : Fin (1 + m)) → Ren n k → VRen (1 + m) (insertᵥ S i (n ↦ k))
  insert { n = n } { k = k } ρs i ρ rewrite sym (insert-map ⦅_⦆ (n ↦ k) (shape ρs) i) = insertₕ ρs i ρ

  remove : VRen (1 + m) S → (i : Fin (1 + m)) → VRen m (removeᵥ S i)
  remove ρs i rewrite sym (remove-map ⦅_⦆ (shape ρs) i) = removeₕ ρs i

  updateAt : (i : Fin m) → (⦅ lookupᵥ S i ⦆ → Ren n k) → VRen m S → VRen m (S [ i ]≔ n ↦ k)
  updateAt { n = n } { k = k } i f ρs rewrite map-[]≔ ⦅_⦆ (shape ρs) i { x = n ↦ k } = updateAtₕ i f' ρs
    where
      f' : lookupᵥ (map ⦅_⦆ (shape ρs)) i → Ren n k
      f' rewrite lookup-map i ⦅_⦆ (shape ρs) = f

  infixl 6 _[_]$=_

  _[_]$=_ : VRen m S → (i : Fin m) → (⦅ lookupᵥ S i ⦆ → Ren n k) → VRen m (S [ i ]≔ n ↦ k)
  ρs [ i ]$= f = updateAt i f ρs

  infixl 6 _[_]&=_

  _[_]&=_ : VRen m S → (i : Fin m) → Ren n k → VRen m (S [ i ]≔ n ↦ k)
  ρs [ i ]&= ρ = ρs [ i ]$= Fun.const ρ

-- ------------------------------------------------------------------------
-- Primitives

id : ∀ m { n } → VRen m (idₛ n)
id zero = []
id (suc m) = idᵣ ∷ id m

↑ : ∀ m { n } → (i : Fin m) → VRen m (↑ₛ n i)
↑ m i = (id m) [ i ]&= ↑ᵣ

_⇑_ : ∀ { n S } → VRen n S → (i : Fin n) → VRen n (S ⇑ₛ i)
ρs ⇑ i = ρs [ i ]$= (_⇑ᵣ)

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

max_stars_repo_name: johnyob/agda-sigma

max_issues_repo_name: johnyob/agda-sigma

max_forks_repo_name: johnyob/agda-sigma


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

module Issue3a where

module A where
  postulate
    D    : Set
    _≡_  : D → D → Set
    a b  : D

  postulate p : a ≡ b

open A
{-# ATP axiom p #-}

postulate foo : a ≡ b
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Magma.MorphismProperties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma
open import Cubical.Data.Prod using (isPropProd)

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Magma.Morphism

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Record

open import Cubical.Relation.Binary.Reasoning.Equality

open Iso

private
  variable
    ℓ ℓ′ ℓ′′ : Level
    L : Magma ℓ
    M : Magma ℓ′
    N : Magma ℓ′′

isPropIsMagmaHom : ∀ (M : Magma ℓ) (N : Magma ℓ′) f → isProp (IsMagmaHom M N f)
isPropIsMagmaHom M N f = isPropHomomorphic₂ (Magma.is-set N) f (Magma._•_ M) (Magma._•_ N)

isSetMagmaHom : isSet (M ⟶ᴴ N)
isSetMagmaHom {M = M} {N = N} = isOfHLevelRespectEquiv 2 equiv
                                (isSetΣ (isSetΠ λ _ → is-set N)
                                        (λ f → isProp→isSet (isPropIsMagmaHom M N f)))
  where
    open Magma
    equiv : (Σ[ g ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsMagmaHom M N g) ≃ MagmaHom M N
    equiv = isoToEquiv (iso (λ (g , m) → magmahom g m)
                            (λ (magmahom g m) → g , m)
                            (λ _ → refl) λ _ → refl)

isMagmaHomComp : {f : ⟨ L ⟩ → ⟨ M ⟩} {g : ⟨ M ⟩ → ⟨ N ⟩} →
                  IsMagmaHom L M f → IsMagmaHom M N g → IsMagmaHom L N (g ∘ f)
isMagmaHomComp {g = g} fHom gHom _ _ = cong g (fHom _ _) ∙ gHom _ _

private
  isMagmaHomComp′ : (f : L ⟶ᴴ M) (g : M ⟶ᴴ N) →
                    IsMagmaHom L N (MagmaHom.fun g ∘ MagmaHom.fun f)
  isMagmaHomComp′ (magmahom f fHom) (magmahom g gHom) _ _ = cong g (fHom _ _) ∙ gHom _ _

compMagmaHom : (L ⟶ᴴ M) → (M ⟶ᴴ N) → (L ⟶ᴴ N)
compMagmaHom f g = magmahom _ (isMagmaHomComp′ f g)

compMagmaEquiv : L ≃ᴴ M → M ≃ᴴ N → L ≃ᴴ N
compMagmaEquiv f g = magmaequiv (compEquiv f.eq g.eq) (isMagmaHomComp′ f.hom g.hom)
  where
    module f = MagmaEquiv f
    module g = MagmaEquiv g

isMagmaHomId : (M : Magma ℓ) → IsMagmaHom M M id
isMagmaHomId M _ _ = refl

idMagmaHom : (M : Magma ℓ) → (M ⟶ᴴ M)
idMagmaHom M = record
  { fun   = id
  ; isHom = isMagmaHomId M
  }

idMagmaEquiv : (M : Magma ℓ) → M ≃ᴴ M
idMagmaEquiv M = record
  { eq    = idEquiv ⟨ M ⟩
  ; isHom = isMagmaHomId M
  }

-- Isomorphism inversion
isMagmaHomInv : (eqv : M ≃ᴴ N) → IsMagmaHom N M (invEq (MagmaEquiv.eq eqv))
isMagmaHomInv {M = M} {N = N} (magmaequiv eq isHom) x y = isInj-f _ _ (
  f (f⁻¹ (x •ᴺ y))       ≡⟨ retEq eq _ ⟩
  x •ᴺ y                 ≡˘⟨ cong₂ _•ᴺ_ (retEq eq x) (retEq eq y) ⟩
  f (f⁻¹ x) •ᴺ f (f⁻¹ y) ≡˘⟨ isHom (f⁻¹ x) (f⁻¹ y) ⟩
  f (f⁻¹ x •ᴹ f⁻¹ y)     ∎)
  where
    _•ᴹ_ = Magma._•_ M
    _•ᴺ_ = Magma._•_ N
    f = equivFun eq
    f⁻¹ = invEq eq
    isInj-f : (x y : ⟨ M ⟩) → f x ≡ f y → x ≡ y
    isInj-f x y = invEq (_ , isEquiv→isEmbedding (eq .snd) x y)

invMagmaHom : M ≃ᴴ N → (N ⟶ᴴ M)
invMagmaHom eq = record { isHom = isMagmaHomInv eq }

invMagmaEquiv : (M ≃ᴴ N) → (N ≃ᴴ M)
invMagmaEquiv eq = record
  { eq    = invEquiv (MagmaEquiv.eq eq)
  ; isHom = isMagmaHomInv eq
  }

magmaHomEq : {f g : M ⟶ᴴ N} → (MagmaHom.fun f ≡ MagmaHom.fun g) → f ≡ g
magmaHomEq {M = M} {N = N} {magmahom f fm} {magmahom g gm} p i = magmahom (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsMagmaHom M N (p i)) fm gm
    p-hom = toPathP (isPropIsMagmaHom M N _ _ _)

magmaEquivEq : {f g : M ≃ᴴ N} → (MagmaEquiv.eq f ≡ MagmaEquiv.eq g) → f ≡ g
magmaEquivEq {M = M} {N = N} {magmaequiv f fm} {magmaequiv g gm} p i = magmaequiv (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsMagmaHom M N (p i .fst)) fm gm
    p-hom = toPathP (isPropIsMagmaHom M N _ _ _)

module MagmaΣTheory {ℓ} where

  RawMagmaStructure : Type ℓ → Type ℓ
  RawMagmaStructure A = A → A → A

  RawMagmaEquivStr = AutoEquivStr RawMagmaStructure

  rawMagmaUnivalentStr : UnivalentStr _ RawMagmaEquivStr
  rawMagmaUnivalentStr = autoUnivalentStr RawMagmaStructure

  MagmaAxioms : (A : Type ℓ) → RawMagmaStructure A → Type ℓ
  MagmaAxioms A _•_ = isSet A

  MagmaStructure : Type ℓ → Type ℓ
  MagmaStructure = AxiomsStructure RawMagmaStructure MagmaAxioms

  MagmaΣ : Type (ℓ-suc ℓ)
  MagmaΣ = TypeWithStr ℓ MagmaStructure

  isPropMagmaAxioms : (A : Type ℓ) (_•_ : RawMagmaStructure A)
                      → isProp (MagmaAxioms A _•_)
  isPropMagmaAxioms _ _ = isPropIsSet

  MagmaEquivStr : StrEquiv MagmaStructure ℓ
  MagmaEquivStr = AxiomsEquivStr RawMagmaEquivStr MagmaAxioms

  MagmaAxiomsIsoIsMagma : {A : Type ℓ} (_•_ : RawMagmaStructure A)
                              → Iso (MagmaAxioms A _•_) (IsMagma A _•_)
  fun (MagmaAxiomsIsoIsMagma s) x           = ismagma x
  inv (MagmaAxiomsIsoIsMagma s) (ismagma x) = x
  rightInv (MagmaAxiomsIsoIsMagma s) _      = refl
  leftInv (MagmaAxiomsIsoIsMagma s) _       = refl

  MagmaAxioms≡IsMagma : {A : Type ℓ} (_•_ : RawMagmaStructure A)
                              → MagmaAxioms A _•_ ≡ IsMagma A _•_
  MagmaAxioms≡IsMagma s = isoToPath (MagmaAxiomsIsoIsMagma s)

  Magma→MagmaΣ : Magma ℓ → MagmaΣ
  Magma→MagmaΣ (mkmagma A _•_ isMagma) =
    A , _•_ , MagmaAxiomsIsoIsMagma _ .inv isMagma

  MagmaΣ→Magma : MagmaΣ → Magma ℓ
  MagmaΣ→Magma (A , _•_ , isMagma•) =
    mkmagma A _•_ (MagmaAxiomsIsoIsMagma _ .fun isMagma•)

  MagmaIsoMagmaΣ : Iso (Magma ℓ) MagmaΣ
  MagmaIsoMagmaΣ =
    iso Magma→MagmaΣ MagmaΣ→Magma (λ _ → refl) (λ _ → refl)

  magmaUnivalentStr : UnivalentStr MagmaStructure MagmaEquivStr
  magmaUnivalentStr = axiomsUnivalentStr _ isPropMagmaAxioms rawMagmaUnivalentStr

  MagmaΣPath : (M N : MagmaΣ) → (M ≃[ MagmaEquivStr ] N) ≃ (M ≡ N)
  MagmaΣPath = SIP magmaUnivalentStr

  MagmaEquivΣ : (M N : Magma ℓ) → Type ℓ
  MagmaEquivΣ M N = Magma→MagmaΣ M ≃[ MagmaEquivStr ] Magma→MagmaΣ N

  MagmaIsoΣPath : {M N : Magma ℓ} → Iso (MagmaEquiv M N) (MagmaEquivΣ M N)
  fun MagmaIsoΣPath (magmaequiv e h)   = (e , h)
  inv MagmaIsoΣPath (e , h)            = magmaequiv e h
  rightInv MagmaIsoΣPath _             = refl
  leftInv MagmaIsoΣPath _              = refl

  MagmaPath : (M N : Magma ℓ) → (MagmaEquiv M N) ≃ (M ≡ N)
  MagmaPath M N =
    MagmaEquiv M N                    ≃⟨ isoToEquiv MagmaIsoΣPath ⟩
    MagmaEquivΣ M N                   ≃⟨ MagmaΣPath _ _ ⟩
    Magma→MagmaΣ M ≡ Magma→MagmaΣ N   ≃⟨ isoToEquiv (invIso (congIso MagmaIsoMagmaΣ)) ⟩
    M ≡ N                             ■

  RawMagmaΣ : Type (ℓ-suc ℓ)
  RawMagmaΣ = TypeWithStr ℓ RawMagmaStructure

  Magma→RawMagmaΣ : Magma ℓ → RawMagmaΣ
  Magma→RawMagmaΣ M = (⟨ M ⟩ , Magma._•_ M)

  InducedMagma : (M : Magma ℓ) (N : RawMagmaΣ) (e : ⟨ M ⟩ ≃ ⟨ N ⟩)
                 → RawMagmaEquivStr (Magma→RawMagmaΣ M) N e → Magma ℓ
  InducedMagma M N e r =
    MagmaΣ→Magma (inducedStructure rawMagmaUnivalentStr (Magma→MagmaΣ M) N (e , r))

  InducedMagmaPath : (M : Magma ℓ) (N : RawMagmaΣ) (e : ⟨ M ⟩ ≃ ⟨ N ⟩)
                      (E : RawMagmaEquivStr (Magma→RawMagmaΣ M) N e)
                    → M ≡ InducedMagma M N e E
  InducedMagmaPath M N e E =
    MagmaPath M (InducedMagma M N e E) .fst (magmaequiv e E)

open MagmaΣTheory public using (InducedMagma; InducedMagmaPath)

MagmaPath : (M ≃ᴴ N) ≃ (M ≡ N)
MagmaPath = MagmaΣTheory.MagmaPath _ _

open Magma

uaMagma : M ≃ᴴ N → M ≡ N
uaMagma = equivFun MagmaPath

carac-uaMagma : {M N : Magma ℓ} (f : M ≃ᴴ N) → cong Carrier (uaMagma f) ≡ ua (MagmaEquiv.eq f)
carac-uaMagma (magmaequiv f m) =
  (refl ∙∙ ua f ∙∙ refl)
    ≡˘⟨ rUnit (ua f) ⟩
  ua f ∎

Magma≡ : (M N : Magma ℓ) → (
  Σ[ p ∈ ⟨ M ⟩ ≡ ⟨ N ⟩ ]
  Σ[ q ∈ PathP (λ i → p i → p i → p i) (_•_ M) (_•_ N) ]
  PathP (λ i → IsMagma (p i) (q i)) (isMagma M) (isMagma N))
  ≃ (M ≡ N)
Magma≡ M N = isoToEquiv (iso
  (λ (p , q , r) i → mkmagma (p i) (q i) (r i))
  (λ p → cong Carrier p , cong _•_ p , cong isMagma p)
  (λ _ → refl) (λ _ → refl))

caracMagma≡ : (p q : M ≡ N) → cong Carrier p ≡ cong Carrier q → p ≡ q
caracMagma≡ {M = M} {N = N} p q t = cong (Magma≡ M N .fst) (Σ≡Prop (λ _ →
    isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set N) _ _) λ _ →
    isOfHLevelPathP 1 (λ { (ismagma x) (ismagma y) → cong ismagma (isPropIsSet x y) }) _ _)
  t)

uaMagmaId : (M : Magma ℓ) → uaMagma (idMagmaEquiv M) ≡ refl
uaMagmaId M = caracMagma≡ _ _ (carac-uaMagma (idMagmaEquiv M) ∙ uaIdEquiv)

uaCompMagmaEquiv : {L M N : Magma ℓ} (f : L ≃ᴴ M) (g : M ≃ᴴ N)
                    → uaMagma (compMagmaEquiv f g) ≡ uaMagma f ∙ uaMagma g
uaCompMagmaEquiv f g = caracMagma≡ _ _ (
  cong Carrier (uaMagma (compMagmaEquiv f g))
    ≡⟨ carac-uaMagma (compMagmaEquiv f g) ⟩
  ua (eq (compMagmaEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡⟨ cong (_∙ ua (eq g)) (sym (carac-uaMagma f)) ⟩
  cong Carrier (uaMagma f) ∙ ua (eq g)
    ≡⟨ cong (cong Carrier (uaMagma f) ∙_) (sym (carac-uaMagma g)) ⟩
  cong Carrier (uaMagma f) ∙ cong Carrier (uaMagma g)
    ≡⟨ sym (cong-∙ Carrier (uaMagma f) (uaMagma g)) ⟩
  cong Carrier (uaMagma f ∙ uaMagma g) ∎)
  where open MagmaEquiv


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

open import Base
open import Homotopy.TruncatedHIT
open import Sets.Quotient

module Sets.QuotientUP {i j} (A : Set i) ⦃ A-set : is-set A ⦄
  (R : A → A → Set j) ⦃ R-prop : (x y : A) → is-prop (R x y) ⦄ where

-- [X →→ Y ~ R] is the set of functions [X → Y] respecting the relation [R]
_→→_~_ : ∀ {i j k}
  (X : Set i) ⦃ X-set : is-set X ⦄
  (Y : Set j) ⦃ Y-set : is-set Y ⦄
  (R : X → X → Set k) ⦃ R-prop : (x x' : X) → is-prop (R x x')⦄
    → Set _
X →→ Y ~ R = Σ (X → Y) (λ f → (x x' : X) → (R x x' → f x ≡ f x'))

module UP {k} (B : Set k) (B-set : is-set B) where

  factor : ((A →→ B ~ R) → (A / R → B))
  factor (f , p) = /-rec-nondep A R B f p B-set

  extend : ((A / R → B) → (A →→ B ~ R))
  extend f = ((f ◯ proj A R) , (λ x x' p₁ → ap f (eq A R x x' p₁)))

  extend-factor : (f : A →→ B ~ R) → extend (factor f) ≡ f
  extend-factor (f , p) = ap (λ x → f , x)
                           (funext (λ x →
                            funext (λ x' →
                            funext (λ p₁ → π₁ (B-set _ _ _ _)))))

  factor-extend : (f : A / R → B) → factor (extend f) ≡ f
  factor-extend f =
    funext (/-rec A R (λ x → factor (extend f) x ≡ f x)
           (λ x → refl)
           (λ x y _ → π₁ (B-set _ _ _ _))
           (λ x → truncated-is-truncated-S _ (B-set _ _)))

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue1168 where

id : {A : Set} → A → A
id {A = A} a = a


text:
module Compilation.Encode.Core where

open import Context
open import Type.Core
open import Compilation.Data

open import Function
open import Data.List.Base as List

{- Note [Compilation]
We compile data descriptions to System Fωμ in two steps:

1. Lambda-bind
     a) a tag to distinguish between the data types from the family
     b) a variable for each of the data types from the family
   then apply the tag to all of the data types after Scott-encoding them in order to be able to
   choose one particular data type from the family later. This way we get a valid System Fωμ type,
   but it's not a legal pattern functor yet, as it binds one tag and `n` variables responsible for
   recursion and we need to have only one variable responsible for recursion and one tag in order
   to be able to feed a type function to `μ` and actually tie the knot. Thus the next step is
2. Instantiate all the variables responsible for recursion using a single variable applied to
   distinct tags. This way we transform `1` (tag) + `n` (recursion) variables into
   `1` (recursion) + `1` (tag) variables, i.e. just two variables of right kinds, thus the result
   can be passed to `μ`.

We can now look at the `ProdTree`/`Tree` example.

After the first step (which is performed by the `encodeDataN` function, which calls `scottEncode`
internally) we get the following type (I'll save you from the De Bruijn reverse Turing test and
use the Agda notation instead, but note that this is still a System Fωμ type):

> prodTreeTreeReprN =
>   λ (tag : (Set -> Set -> Set) -> (Set -> Set) -> Set)
>       (prodTree : Set -> Set -> Set) (tree : Set -> Set) ->
>         ∀ (R : Set) ->                                     -- Binding the result variable.
>           tag                                              -- Choosing between the two data types.
>             (λ A B                                         -- The two types that `ProdTree` binds.
>                -> (tree (∀ Q -> (A -> B -> Q) -> Q) -> R)  -- Case over the `Prod` constructor.
>                -> R)
>             (λ A                                           -- The type that `Tree` binds.
>                -> (A -> R)                                 -- Case over the `Leaf` constructor.
>                -> (prodTree A A -> R)                      -- Case over the `Fork` constructor.
>                -> R)

Here we lambda-bind `prodTree` and `tree` directly, Scott-encode the definition of the data types
and use `tag` in order to choose between the two data types.

At the next step we instantiate `prodTree` and `tree` (`instantiations` computes the instantiations)
using a single `rec` (`packEncodedDataN` does this):

> prodTreeTreeRepr1 =
>   λ (rec : ((Set -> Set -> Set) -> (Set -> Set) -> Set) -> Set)
>       (tag : (Set -> Set -> Set) -> (Set -> Set) -> Set) ->
>         prodTreeTreeReptN
>           tag
>           (λ A B -> rec λ prodTree tree -> prodTree A B)
>           (λ A   -> rec λ prodTree tree -> tree A)

It only remains to take the fixed point of this pattern functor:

> prodTreeTree = λ tag -> μ prodTreeTreeRepr1 tag

And that's it, `prodTreeTree` is a valid System Fωμ type that encodes the `ProdTree`/`Tree` family.
-}

{- Note [Data description denotations]
Once we compile a data description to a System Fωμ type, we could already take the denotation of
the latter, but then we'd just get an Agda type that encodes the whole family of mutually recursive
data types, while what we really want is getting all the separate data types, not the whole family
at once.

Hence rather than take the denotation directly, we first instantiate the resulting System Fωμ type
using the tags that the data types from the family correspond to. I.e. we call `instantiations` once
again, get an environment of System Fωμ types and take denotations of those. The result then is an
environment of Agda types, each of which represents a data type from the original family of data
types. We only need to extract them from the environment. Unfortunately, Agda lacks top-level
matches, so we do it like this:

>  ProdTreeTree′ = Encoded.⟦ prodTreeTree ⟧ᵈ
>
>  ProdTree′ : Set -> Set -> Set
>  ProdTree′ with ProdTreeTree′
>  ... | ∅ ▷ PT′ ▷ T′ = PT′
>
>  Tree′ : Set -> Set
>  Tree′ with ProdTreeTree′
>  ... | ∅ ▷ PT′ ▷ T′ = T′
-}

-- | Get the kind of tags from the context of a data description.
--
-- > dataConToTagKind (ε ▻ (σ¹₁ ▻ … ▻ σ¹ₙ₁) ▻ … ▻ (σ¹ₘ ▻ … ▻ σᵐₙₘ)) τ =
-- >   (σ¹₁ ⇒ᵏ … ⇒ᵏ σ¹ₙ₁ ⇒ᵏ ⋆) ⇒ᵏ … ⇒ᵏ (σ¹₁ ⇒ᵏ … ⇒ᵏ σᵐₙₘ ⇒ᵏ ⋆) ⇒ᵏ τ
dataConToTagKind : Con Conᵏ -> Kind -> Kind
dataConToTagKind = conToKindBy $ λ Θ -> conToKind Θ ⋆

-- | Scott-encode a single data type. The type variable (denoted as `ρ`) that represents
-- the result is assumed to be in scope, because we Scott-encode a bunch of data types
-- at the same time and hence the resulting type variable has to be bound outside of all of them,
-- which is why we keep it implicit while encoding a single data type.
--
-- > scottEncode (ε ▻ α₁ ▻ … ▻ αₙ) [(β¹₁ ⇒ᶜ … ⇒ᶜ β¹ₙ₁ ⇒ᶜ endᶜ) , … , (βᵐ₁ ⇒ᶜ … ⇒ᶜ βᵐₙₘ ⇒ᶜ endᶜ)] =
-- >     λ α₁ … αₙ → (β¹₁ ⇒ … ⇒ β¹ₙ₁ ⇒ ρ) ⇒ … ⇒ (βᵐ₁ ⇒ … ⇒ βᵐₙₘ ⇒ ρ) ⇒ ρ
scottEncode : ∀ {Ξ} Θ -> List (Cons (Ξ ▻▻ Θ)) -> Ξ ▻ ⋆ ⊢ᵗ conToKind Θ ⋆
scottEncode Θ = Lamⁿ' Θ ∘ foldr (λ ξ γ -> consToType (renᶜ (keepⁿ Θ topᵒ) ξ) ρ ⇒ γ) ρ where
  ρ = renᵗ (extʳ Θ) $ Var vz

-- | Encode a `Data` description as an n-ary type function.
--
-- > encodeDataN (PackData [data¹ , … , dataᵐ]) =
-- >    λ tag δ¹ … δᵐ → tag (scott data¹) … (scott dataᵐ)
--
-- (`δᵢ` is the name of `dataᵢ` that is potentially used internally in any `dataⱼ`,
-- because the data types are allowed to be mutually recursive).
encodeDataN : ∀ {Ξ Θs} -> Data Ξ Θs -> Ξ ⊢ᵗ dataConToTagKind Θs ⋆ ⇒ᵏ dataConToTagKind Θs ⋆
encodeDataN {Ξ} {Θs} (PackData datas) =
  Lam_ ∘′ Lamⁿ Θs ∘′ π ⋆ $′
    applyᵗⁿ Θs
      (Var ∘ vsⁿ $ mapᶜ _ Θs ▻ ⋆)
      (mapˢ (λ {Θ} -> renᵗ (keepⁿ (mapᶜ _ Θs ▻ ⋆) topᵒ) ∘ scottEncode Θ) datas)

-- | Compute all instantiations of a thing of kind `dataConToTagKind Θs ⋆ ⇒ᵏ ⋆`, which is either
-- the first variable that a packed pattern functor binds (i.e. the one responsible for recursion)
-- or the final data type representing a family of mutually recursive data types.
-- "Instantiations" then are particular data types from a family of mutually recursive data types
-- (or represent them if we're are inside a pattern functor).
-- For example, the instantiations of `treeForest` are `tree` and `forest`, i.e. precisely those
-- data types that form the family.
--
-- > instantiations ψ
-- >     = ∅
-- >     ▷ (λ α¹₁ … α¹ₙ₁ → ψ λ β¹ … βᵐ → β¹ α¹₁ … α¹ₙ₁)
-- >     ▷ …
-- >     ▷ (λ αᵐ₁ … αᵐₙₘ → ψ λ β¹ … βᵐ → βᵐ αᵐ₁ … αᵐₙₘ)
instantiations : ∀ {Θs Ξ} -> Ξ ⊢ᵗ dataConToTagKind Θs ⋆ ⇒ᵏ ⋆ -> Seq (λ Θ -> Ξ ⊢ᵗ conToKind Θ ⋆) Θs
instantiations {ε}      ψ = ø
instantiations {Θs ▻ Θ} ψ
  = instantiations {Θs} (Lam_ $ shiftᵗ ψ ∙
      Lamⁿ (Θs ▻ Θ) (applyᵗⁿ Θs (Var (vsⁿ (mapᶜ _ (Θs ▻ Θ)))) (mapˢ shiftᵗ subVars)))
  ▶ Lamⁿ' Θ (shiftᵗⁿ Θ ψ ∙
      Lamⁿ (Θs ▻ Θ) (applyᵗⁿ Θ (Var vz) (mapˢ (shiftᵗⁿ (mapᶜ _ $ Θs ▻ Θ)) subVars')))

-- | Pack an encoded family of mutually recursive data types as an 1-ary pattern functor.
-- The encoded family is of this form (see `encodeDataN`):
--
-- > φ : ((σ¹₁ ⇒ᵏ … ⇒ᵏ σ¹ₙ₁ ⇒ᵏ ⋆) ⇒ᵏ … ⇒ᵏ (σᵐ₁ ⇒ᵏ … ⇒ᵏ σᵐₙₘ ⇒ᵏ ⋆) ⇒ᵏ ⋆)
-- >   ⇒ᵏ (σ¹₁ ⇒ᵏ … ⇒ᵏ σ¹ₙ₁ ⇒ᵏ ⋆) ⇒ᵏ … ⇒ᵏ (σᵐ₁ ⇒ᵏ … ⇒ᵏ σᵐₙₘ ⇒ᵏ ⋆) ⇒ᵏ ⋆
-- > φ = λ tag δ¹ … δᵐ → <body>
--
-- Where `tag` is a tag and `δʲ` is a variable that stands for a data type from the family.
--
-- The definition of `packEncodedDataN` then is
--
-- > packEncodedDataN _ φ =
-- >     λ rec tag → φ tag
-- >         (λ α¹₁ … α¹ₙ₁ → rec λ ψ¹ … ψᵐ → ψ¹ α¹₁ … α¹ₙ₁)
-- >         …
-- >         (λ αᵐ₁ … αᵐₙₘ → rec λ ψ¹ … ψᵐ → ψᵐ αᵐ₁ … αᵐₙₘ)
--
-- where `αʲᵢ` is a parameter of a data type and `λ ψ¹ … ψᵐ → ψʲ αʲ₁ … αʲᵢ` is the tag of
-- the data type. That is, we put parameters of data types into their corresponding tags.
--
-- So we instantiate each data type argument of `φ` as `rec` applied to an appropriate tag. This
-- way we represent all of the data types using just a single `rec` applied to different tags.
packEncodedDataN
  : ∀ {Ξ} Θs
  -> Ξ ⊢ᵗ dataConToTagKind Θs ⋆ ⇒ᵏ dataConToTagKind Θs ⋆
  -> Ξ ⊢ᵗ (dataConToTagKind Θs ⋆ ⇒ᵏ ⋆) ⇒ᵏ dataConToTagKind Θs ⋆ ⇒ᵏ ⋆
packEncodedDataN Θs φ =
  Lam_ ∘′ Lam_ ∘′ applyᵗⁿ Θs (shiftᵗⁿ (ε ▻ _ ▻ _) φ ∙ Var vz) ∘′ instantiations $ Var (vs vz)

-- | Encode a `Data` as a 1-ary pattern functor.
encodeData1
  : ∀ {Ξ Θs} -> Data Ξ Θs -> Ξ ⊢ᵗ (dataConToTagKind Θs ⋆ ⇒ᵏ ⋆) ⇒ᵏ dataConToTagKind Θs ⋆ ⇒ᵏ ⋆
encodeData1 {Θs = Θs} = packEncodedDataN Θs ∘ encodeDataN

-- | Compile a `Data` to System Fωμ.
compileData : ∀ {Ξ Θs} -> Data Ξ Θs -> Ξ ⊢ᵗ dataConToTagKind Θs ⋆ ⇒ᵏ ⋆
compileData d = Lam μ (shiftᵗ $ encodeData1 d) (Var vz)

compileDatas : ∀ {Ξ Θs} -> Data Ξ Θs -> Seq (λ Θ -> Ξ ⊢ᵗ conToKind Θ ⋆) Θs
compileDatas = instantiations ∘ compileData

-- | Return the denotations of all the data types from a family of mutually recursive data types
-- encoded as a `Data`.
⟦_⟧ᵈ : ∀ {Θs} -> Data ε Θs -> Seq (λ Θ -> ⟦ conToKind Θ ⋆ ⟧ᵏ) Θs
⟦_⟧ᵈ = mapˢ ⟦_⟧ᵗ ∘ compileDatas

module Unused where
  constructorTypes : ∀ {Θs Ξ} -> Data Ξ Θs -> Con (Star (Ξ ▻▻ mapᶜ (λ Θᵢ -> conToKind Θᵢ ⋆) Θs))
  constructorTypes {Θs} {Ξ} (PackData constructors) =
    joinᶜ ∘′ eraseˢ $′ mapElˢ consesToCon constructors where
      consesToCon
        : ∀ {Θ}
        -> Θ ∈ Θs
        -> List (Cons (Ξ ▻▻ mapᶜ (λ Θᵢ -> conToKind Θᵢ ⋆) Θs ▻▻ Θ))
        -> Con (Star (Ξ ▻▻ mapᶜ (λ Θᵢ -> conToKind Θᵢ ⋆) Θs))
      consesToCon {Θ} v = listToCon ∘ List.map (λ ξ -> πⁿ' Θ $ consToType ξ ρ) where
        ρ = applyᵗⁿ Θ (Var ∘ renᵛ (skipⁿ Θ extˡ) $ mapᵛ v) subVars'

  constructorFullTypes : ∀ {Θs Ξ} -> Data Ξ Θs -> Con (Star Ξ)
  constructorFullTypes δ = mapᶜ (instᵗⁿ $ compileDatas δ) $ constructorTypes δ

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
module Issue1760e where

-- Skipping a single record definition in a private block.
private
  {-# NO_POSITIVITY_CHECK #-}
  record U : Set where
    field ap : U → U

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module STLC.Typing where

open import STLC.Syntax
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Product using (∃-syntax; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst)
open import Relation.Nullary using (Dec; yes; no; ¬_)

private
  variable
    m n : ℕ
    v : Fin n
    Γ : Ctx n
    A B : Type
    a b f x p : Term n

data _∋_⦂_ : Ctx n → Fin n → Type → Set where
  vzero : (Γ ,- A) ∋ fzero ⦂ A
  vsuc : (Γ ∋ v ⦂ A) → (Γ ,- B) ∋ fsuc v ⦂ A

lookup : (Γ : Ctx n) → (v : Fin n) → Γ ∋ v ⦂ find Γ v
lookup (Γ ,- A) fzero = vzero
lookup (Γ ,- B) (fsuc v) = vsuc (lookup Γ v)

data _⊢_⦂_ : Ctx n → Term n → Type → Set where
  ty-abs : (Γ ,- A) ⊢ b ⦂ B → Γ ⊢ abs A b ⦂ (A ⇒ B)
  ty-app : Γ ⊢ f ⦂ (A ⇒ B) → Γ ⊢ x ⦂ A → Γ ⊢ app f x ⦂ B
  ty-var : Γ ∋ v ⦂ A → Γ ⊢ var v ⦂ A
  ty-⋆ : Γ ⊢ ⋆ ⦂ unit
  ty-pair : Γ ⊢ a ⦂ A → Γ ⊢ b ⦂ B → Γ ⊢ pair a b ⦂ (A ×' B)
  ty-projₗ : Γ ⊢ p ⦂ (A ×' B) → Γ ⊢ projₗ p ⦂ A
  ty-projᵣ : Γ ⊢ p ⦂ (A ×' B) → Γ ⊢ projᵣ p ⦂ B

principal-var : (Γ ∋ v ⦂ A) → (Γ ∋ v ⦂ B) → A ≡ B
principal-var vzero vzero = refl
principal-var (vsuc u) (vsuc v) rewrite principal-var u v = refl

principal : Γ ⊢ x ⦂ A → Γ ⊢ x ⦂ B → A ≡ B
principal (ty-abs {A = A} body₁) (ty-abs {A = (.A)} body₂) =
  cong (λ B → A ⇒ B) (principal body₁ body₂)
principal (ty-app f x) (ty-app g y) with principal f g
... | refl = refl
principal (ty-var u) (ty-var v) rewrite principal-var u v = refl
principal ty-⋆ ty-⋆ = refl
principal (ty-pair a₁ b₁) (ty-pair a₂ b₂) rewrite principal a₁ a₂ | principal b₁ b₂ = refl
principal (ty-projₗ p₁) (ty-projₗ p₂) with principal p₁ p₂
... | refl = refl
principal (ty-projᵣ p₁) (ty-projᵣ p₂) with principal p₁ p₂
... | refl = refl

ill-typed-fun
  : (Γ ⊢ f ⦂ A)
  → ¬ (∃[ B ] ∃[ C ] (A ≡ B ⇒ C))
  → ¬ (∃[ T ] (Γ ⊢ app f x ⦂ T))
ill-typed-fun f-ill-typed ineq (_ , ty-app {A = A} {B = B} f-typing _)
  with principal f-ill-typed f-typing
... | eq = ineq (A , B , eq)

ill-typed-pairₗ
  : (Γ ⊢ p ⦂ A)
  → ¬ (∃[ B ] ∃[ C ] (A ≡ B ×' C))
  → ¬ (∃[ T ] (Γ ⊢ projₗ p ⦂ T))
ill-typed-pairₗ pair-ill-typed ineq (_ , ty-projₗ {A = A} {B = B} pair-typing)
  with principal pair-ill-typed pair-typing
... | eq = ineq (A , B , eq)

ill-typed-pairᵣ
  : (Γ ⊢ p ⦂ A)
  → ¬ (∃[ B ] ∃[ C ] (A ≡ B ×' C))
  → ¬ (∃[ T ] (Γ ⊢ projᵣ p ⦂ T))
ill-typed-pairᵣ pair-ill-typed ineq (_ , ty-projᵣ {A = A} {B = B} pair-typing)
  with principal pair-ill-typed pair-typing
... | eq = ineq (A , B , eq)

typecheck : (Γ : Ctx n) → (t : Term n) → Dec (∃[ T ] (Γ ⊢ t ⦂ T))
typecheck Γ (var v) = yes (find Γ v , ty-var (lookup Γ v))
typecheck Γ (abs A t) with typecheck (Γ ,- A) t
... | yes (B , well-typed) = yes (A ⇒ B , ty-abs well-typed)
... | no ill-typed = no λ { (ty , ty-abs {B = B} ty-body) → ill-typed ((B , ty-body)) }
typecheck Γ (app f x) with typecheck Γ f | typecheck Γ x
... | yes (_ ×' _ , f-wrong-typing) | _ = no (ill-typed-fun f-wrong-typing λ ())
... | yes (unit , f-wrong-typing) | _ = no (ill-typed-fun f-wrong-typing λ ())
... | yes (_ ⇒ _ , _) | no ill-typed =
        no λ { (_ , ty-app {A = A} _ x) → ill-typed (A , x)}
... | no ill-typed | _ =
        no λ { (_ , ty-app {A = A} {B = B} f _) → ill-typed (A ⇒ B , f)}
... | yes (A ⇒ B , f-typing) | yes (A' , x-typing) with A' =?= A
...     | yes eq = yes (B , ty-app f-typing (subst (λ A → Γ ⊢ x ⦂ A) eq x-typing))
...     | no neq = no (helper neq)
  where helper : ¬ A' ≡ A → ¬ (∃[ B ] (Γ ⊢ app f x ⦂ B))
        helper neq (B'' , ty-app {A = A''} f'' x'')
          with principal f-typing f'' | principal x-typing x''
        ... | refl | refl = neq refl
typecheck _ ⋆ = yes (unit , ty-⋆)
typecheck Γ (pair l r) with typecheck Γ l | typecheck Γ r
... | yes (A , l-typing) | yes (B , r-typing) = yes (A ×' B , ty-pair l-typing r-typing)
... | yes _ | no ill-typed = no λ { (A ×' B , ty-pair _ r) → ill-typed (B , r) }
... | no ill-typed | _ = no λ { (A ×' B , ty-pair l _) → ill-typed (A , l)}
typecheck Γ (projₗ p) with typecheck Γ p
... | yes (A ×' _ , typing) = yes (A , ty-projₗ typing)
... | yes (_ ⇒ _ , typing) = no (ill-typed-pairₗ typing λ ())
... | yes (unit , typing) = no (ill-typed-pairₗ typing λ ())
... | no ill-typed = no λ { (_ , ty-projₗ {A = A} {B = B} p) → ill-typed ((A ×' B) , p) }
typecheck Γ (projᵣ p) with typecheck Γ p
... | yes (_ ×' B , typing) = yes (B , ty-projᵣ typing)
... | yes (_ ⇒ _ , typing) = no (ill-typed-pairᵣ typing λ ())
... | yes (unit , typing) = no (ill-typed-pairᵣ typing λ ())
... | no ill-typed = no λ { (_ , ty-projᵣ {A = A} {B = B} p) → ill-typed ((A ×' B) , p) }

max_stars_repo_name: TypesLogicsCats/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


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

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude

open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.CommMonoid.Base

open CommMonoidStr
open IsCommMonoid hiding (rid ; lid)
open IsMonoid hiding (rid ; lid)
open IsSemigroup

private
  variable
    ℓ ℓ' : Level

CommMonoidProd : CommMonoid ℓ → CommMonoid ℓ' → CommMonoid (ℓ-max ℓ ℓ')
CommMonoidProd M N = makeCommMonoid ε× _·×_ is-set× assoc× rid× comm×
  where
  ε× : (fst M) × (fst N)
  ε× = (ε (snd M)) , (ε (snd N))

  _·×_ : (fst M) × (fst N) → (fst M) × (fst N) → (fst M) × (fst N)
  (x₁ , x₂) ·× (y₁ , y₂) = (_·_ (snd M) x₁ y₁) , (_·_ (snd N) x₂ y₂)

  is-set× : isSet ((fst M) × (fst N))
  is-set× = isSet× (is-set (snd M)) (is-set (snd N))

  assoc× : ∀ x y z → x ·× (y ·× z) ≡ (x ·× y) ·× z
  assoc× _ _ _ = cong₂ (_,_) (assoc (snd M) _ _ _) (assoc (snd N) _ _ _)

  rid× : ∀ x → x ·× ε× ≡ x
  rid× _ =  cong₂ (_,_) (rid (snd M) _) (rid (snd N) _)

  comm× : ∀ x y → x ·× y ≡ y ·× x
  comm× _ _ = cong₂ (_,_) (comm (snd M) _ _) (comm (snd N) _ _)

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
-- Andreas, 2014-10-05, code by Jesper Cockx

{-# OPTIONS --cubical-compatible --guardedness #-}

open import Common.Coinduction
open import Common.Equality

data False : Set where

data Pandora : Set where
  C : ∞ False → Pandora

postulate
  ext : (False → Pandora) → (Pandora → False) → False ≡ Pandora

f : False → Pandora
f ()

g : Pandora → False
g (C x) = ♭ x

foo : False ≡ Pandora
foo = ext f g

-- should be rejected
loop : (A : Set) → A ≡ Pandora → A
loop .Pandora refl = C (♯ (loop False foo))

absurd : False
absurd = loop False foo


text:
{-# OPTIONS --without-K #-}
module Truncation_Level_Criteria where

open import lib.Basics hiding (_⊔_)
open import lib.NType2

open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Unit
open import lib.types.Empty
open import lib.types.TLevel

open import Preliminaries
open import Pointed

-- Chapter 3: Truncation Level Criteria

-- Chapter 3.1: Hedberg's Theorem Revisited

-- Proposition 3.1.1 is below.

-- Definition 3.1.2
const : ∀{i j} {X : Type i} {Y : Type j} → (f : X → Y) → Type (i ⊔ j)
const {X = X} f = (x₁ x₂ : X) → (f x₁) == (f x₂)

coll : ∀{i} → Type i → Type i
coll X = Σ (X → X) const

pathColl : ∀ {i} → Type i → Type i
pathColl X = (x₁ x₂ : X) → coll (x₁ == x₂)

-- Lemma 3.1.3
discr→pathColl : ∀ {i} {X : Type i} → has-dec-eq X → pathColl X
discr→pathColl dec x₁ x₂ with (dec x₁ x₂)
discr→pathColl dec x₁ x₂ | inl p  = (λ _ → p) , (λ _ _ → idp)
discr→pathColl dec x₁ x₂ | inr np = idf _ , λ p → Empty-elim (np p)

-- Lemma 3.1.4
pathColl→isSet : ∀ {i} {X : Type i} → pathColl X → is-set X
pathColl→isSet {X = X} pc x₁ x₂ = all-paths-is-prop paths-equal where
  claim : (y₁ y₂ : X) → (p : y₁ == y₂) → p == ! (fst (pc _ _) idp) ∙ fst (pc _ _) p
  claim x₁ .x₁ idp = ! (!-inv-l (fst (pc x₁ x₁) idp))
  paths-equal : (p₁ p₂ : x₁ == x₂) → p₁ == p₂
  paths-equal p₁ p₂ =
    p₁                                      =⟨ claim _ _ p₁ ⟩
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₁  =⟨ ap (λ q → (! (fst (pc x₁ x₁) idp)) ∙ q) (snd (pc _ _) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₂  =⟨ ! (claim _ _ p₂) ⟩
    p₂                                      ∎

-- Proposition 3.1.1
hedberg : ∀ {i} {X : Type i} → has-dec-eq X → is-set X
hedberg = pathColl→isSet ∘ discr→pathColl

-- Definition 3.1.5
stable : ∀ {i} → Type i → Type i
stable X = ¬ (¬ X) → X

separated : ∀ {i} → Type i → Type i
separated X = (x₁ x₂ : X) → stable (x₁ == x₂)

-- Proposition 3.1.6
sep→set : ∀ {i} {X : Type i} → (separated X) → is-set X
sep→set {X = X} sep = pathColl→isSet isPc where
  isPc : pathColl X
  isPc x₁ x₂ = f , c where
    f : x₁ == x₂ → x₁ == x₂
    f = (sep x₁ x₂) ∘ (λ p np → np p)
    c : const f
    c p₁ p₂ =
      f p₁                        =⟨ idp ⟩
      (sep x₁ x₂) (λ np → np p₁)  =⟨ ap (sep x₁ x₂)
                                     (λ= λ np → Empty-elim {P = λ _ → np p₁ == np p₂} (np p₁)) ⟩
      (sep x₁ x₂) (λ np → np p₂)  =⟨ idp ⟩
      f p₂                        ∎

-- Lemma 3.1.7
-- first: definition of 'reflexive propositional relation that implies identity'
rel-ref-id : ∀ {i} → Type i → Type (lsucc i)
rel-ref-id {i} X = Σ (X → X → Type i)
                     λ R →
                           ((x : X) → R x x)
                         × ((x₁ x₂ : X) → (R x₁ x₂) → x₁ == x₂)
                         × ((x₁ x₂ : X) → is-prop (R x₁ x₂))

-- the actual Lemma 3.1.7
module lem317 {i : _} (X : Type i) (Rrip : rel-ref-id X) where

  R : X → X → Type i
  R = fst Rrip
  ref : (x : X) → R x x
  ref = fst (snd (Rrip)) -- fst (fst (snd Rrip))
  ii : (x₁ x₂ : X) → (R x₁ x₂) → x₁ == x₂
  ii = fst (snd (snd (Rrip))) -- snd (fst (snd Rrip))
  pr : (x₁ x₂ : X) → is-prop (R x₁ x₂)
  pr = snd (snd (snd Rrip))

  f : (x₁ x₂ : X) → x₁ == x₂ → R x₁ x₂
  f x₁ .x₁ idp = ref x₁

  id↔R : (x₁ x₂ : X) → (x₁ == x₂) ↔ R x₁ x₂
  id↔R x₁ x₂ = f _ _ , ii _ _

  pc : pathColl X
  pc x₁ x₂ = ii _ _ ∘ f _ _ , λ p₁ p₂ → ap (ii x₁ x₂) (prop-has-all-paths (pr x₁ x₂) _ _)

  isSet : is-set X
  isSet = pathColl→isSet pc

open wtrunc

-- Definition 3.1.9
splitSup : ∀ {i} → (X : Type i) → Type i
splitSup X = ∣∣ X ∣∣ → X

hSeparated : ∀ {i} → (X : Type i) → Type i
hSeparated X = (x₁ x₂ : X) → splitSup (x₁ == x₂)

-- Proposition 3.1.10
-- we show "2->1", "1->3", "3->2" as in the thesis.
-- for the last part, we show "1->4" and "4->3
set-characterisations : ∀ {i} → (X : Type i) →
      (pathColl X → is-set X)
    × (is-set X → rel-ref-id X)
    × (rel-ref-id X → pathColl X)
    × (is-set X → hSeparated X)
    × (hSeparated X → rel-ref-id X)
set-characterisations X =
  pathColl→isSet ,
  (λ ss → _==_ , (λ _ → idp) , (λ _ _ p → p) , ss) ,
  (lem317.pc X) ,
  (λ ss x₁ x₂ → tr-rec (ss x₁ x₂) (λ p → p)) ,
  (λ hsep → ((λ x₁ x₂ → ∣∣ x₁ == x₂ ∣∣) , (λ _ → ∣ idp ∣) , hsep , λ _ _ → tr-is-prop))

-- The rest of this section is only a replication of the arguments that we have given so far (for that reason, the proofs are not given in the article).
-- They do not directly follow from the propositions that we have proved before, but they directly imply them.
-- Of course, replication of arguments is not a good style for a formalization -
-- we chose this "disadvantageous" order purely as we believe it led to a better presentation in the article.

-- Lemma 3.1.11
pathColl→isSet-local : ∀ {i} {X : Type i} → {x₀ : X} → ((y : X) → coll (x₀ == y)) → (y : X) → is-prop (x₀ == y)
pathColl→isSet-local {X = X} {x₀} pc y = all-paths-is-prop paths-equal  where
  claim : (y : X) → (p : x₀ == y) → p == ! (fst (pc _) idp) ∙ fst (pc _) p
  claim .x₀ idp = ! (!-inv-l (fst (pc _) idp))
  paths-equal : (p₁ p₂ : x₀ == y) → p₁ == p₂
  paths-equal p₁ p₂ =
    p₁                                  =⟨ claim _ p₁ ⟩
    ! (fst (pc _) idp) ∙ fst (pc _) p₁  =⟨ ap (λ q → (! (fst (pc x₀) idp)) ∙ q) (snd (pc y) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _) idp) ∙ fst (pc _) p₂  =⟨ ! (claim _ p₂) ⟩
    p₂                                  ∎

-- Proposition 3.11.12
hedberg-local : ∀ {i} {X : Type i} → {x₀ : X} → ((y : X) → Coprod (x₀ == y) (¬(x₀ == y))) → (y : X) → is-prop (x₀ == y)
hedberg-local {X = X} {x₀ = x₀} dec = pathColl→isSet-local local-pathColl where
  local-pathColl : (y : X) → coll (x₀ == y)
  local-pathColl y with (dec y)
  local-pathColl y₁ | inl p  = (λ _ → p) , (λ _ _ → idp)
  local-pathColl y₁ | inr np = idf _ , (λ p → Empty-elim (np p))

-- Lemma 3.1.13. This needs function extensionality.
sep→set-local : ∀ {i} {X : Type i} {x₀ : X} → ((y : X) → stable (x₀ == y)) → (y : X) → is-prop (x₀ == y)
sep→set-local {X = X} {x₀ = x₀} sep = pathColl→isSet-local is-pathColl where
  is-pathColl : (y : X) → coll (x₀ == y)
  is-pathColl y = f , c where
    f : x₀ == y → x₀ == y
    f = (sep y) ∘ (λ p np → np p)
    c : const f
    c p₁ p₂ =
      f p₁                    =⟨ idp ⟩
      (sep _) (λ np → np p₁) =⟨ ap (sep y)
                                    (λ= (λ np → prop-has-all-paths Empty-is-prop _ _)) ⟩
      (sep _) (λ np → np p₂) =⟨ idp ⟩
      f p₂ ∎

-- Chapter 3.2: Generalisations to Higher Levels

-- first: some lemmata.

-- If A -> B -> A is the identity, then
-- a₁ == a₂ → s a₁ == s a₂ → r(s a₁) == r(s a₂)
-- is also the identity in an appropriate sense
retract-path-retract : ∀ {i j} {A : Type i} {B : Type j}
  → (s : A → B) → (r : B → A) → (s-r : (a : A) → r (s a) == a)
  → (a₁ a₂ : A)
  → (p : a₁ == a₂) → ! (s-r a₁) ∙ (ap r (ap s p)) ∙ (s-r a₂) == p
retract-path-retract s r s-r a₁ .a₁ idp = !-inv-l (s-r a₁)

-- retracts of n-types are n-truncated
retract-is-truncated : ∀ {n : ℕ₋₂} {i j} {A : Type i} {B : Type j}
  → (has-level n B) → (s : A → B) → (r : B → A) → ((a : A) → r (s a) == a) → has-level n A
retract-is-truncated {⟨-2⟩} h s r s-r = inhab-prop-is-contr (r (fst h)) (all-paths-is-prop (λ a₁ a₂ →
                       a₁       =⟨ ! (s-r a₁) ⟩
                       r(s(a₁)) =⟨ ap r (contr-has-all-paths h _ _) ⟩
                       r(s(a₂)) =⟨ s-r a₂ ⟩
                       a₂ ∎
                       ))
retract-is-truncated {S n} h s r s-r a₁ a₂ =
  retract-is-truncated {n} {A = a₁ == a₂} {B = s a₁ == s a₂}
                       (h (s a₁) (s a₂))
                       (ap s)
                       (λ p → ! (s-r a₁) ∙ (ap r p) ∙ (s-r a₂))
                       (retract-path-retract s r s-r a₁ a₂)

-- this is essentially one direction of a local version of the lemma which says that
-- a type is n-truncated iff its loop spaces are (n-1)-truncated
trunclevel-aux₁ : ∀ {i} {X : Type i} {x₀ : X} → (n : ℕ) → ((x : X) → has-level (n -2) (x₀ == x))
                   → is-contr (fst ((Ω ^ n) (X , x₀)))
trunclevel-aux₁ {x₀ = x₀} O h = x₀ , λ x → fst (h x)
trunclevel-aux₁ {X = X} {x₀ = x₀} (S n) h = trunclevel-aux₁ n (h x₀ idp)

-- the other direction...
trunclevel-aux₂ : ∀ {i} {X : Type i} {x₀ : X} → (n : ℕ) → is-contr (fst ((Ω ^ n) (X , x₀)))
                   → ((x : X) → has-level (n -2) (x₀ == x))
trunclevel-aux₂ {X = X} {x₀ = x₀} O h = λ x → inhab-prop-is-contr (contr-has-all-paths h x₀ x) (contr-is-prop (contr-is-prop h x₀ x))
trunclevel-aux₂ {X = X} {x₀ = x₀} (S n) h .x₀ idp = trunclevel-aux₂ n h

-- Theorem 3.2.1

-- in the thesis, we write "let n ≥ -1 be a number".
-- As we do not want to introduce a type of number that are at least -1,
-- we use ℕ.
-- To make up for this, we reduce n everywhere by 1.
module GLHA {i : ULevel} {X : Type i} {x₀ : X} {n : ℕ} where

  Ω-contr : Type i
--  loop-contr = is-contr (fst ((Ω ^ (n + 1)) (X , x₀)))
  Ω-contr = is-contr (fst ((Ω ^ n) (X , x₀)))

  locally-truncated : Type i
--  locally-truncated = (x : X) → has-level (n -1) (x₀ == x)
  locally-truncated = (x : X) → has-level (n -2) (x₀ == x)

  tr-rel-id : Type (lsucc i)
  tr-rel-id = Σ (X → Type i) λ Q →
--                ((x : X) → has-level (n -1) (Q x))
                ((x : X) → has-level (n -2) (Q x))
                × (Q x₀)
                × ((x : X) → Q x → x₀ == x)

  tr-rel-id→locally-truncated : tr-rel-id → locally-truncated
  tr-rel-id→locally-truncated (Q , h , q₀ , ii) = λ x → retract-is-truncated {n = n -2} {A = x₀ == x} {B = Q x} (h x) s r r-s where

    r : {x : X} → (Q x) → (x₀ == x)
    r {x} q = ! (ii x₀ q₀) ∙ (ii x q)

    s : {x : X} → (x₀ == x) → Q x
    s idp = q₀

    r-s : {x : X} → (p : x₀ == x) → r (s p) == p
    r-s idp = !-inv-l (ii x₀ q₀)

  locally-truncated→Ω-contr : locally-truncated → Ω-contr
  locally-truncated→Ω-contr loctr = trunclevel-aux₁ n loctr -- trunclevel-aux n loctr

  Ω-contr→tr-rel-id : Ω-contr → tr-rel-id
  Ω-contr→tr-rel-id h = (λ x → x₀ == x) , (trunclevel-aux₂ n h) , idp , (λ x p → p)

  module with-higher-truncs where
    -- for convenience, we import truncations from the library.
    open import lib.types.Truncation

    -- fourth item in Theorem 3.2.1
    id-stable : Type i
    id-stable = (x : X) → Trunc (n -2) (x₀ == x) → x₀ == x

    -- it is very easy to see that (4) and (2) are logically equivalent.
    -- 2 ⇒ 4
    tr-rel-id→id-stable : tr-rel-id → id-stable
    tr-rel-id→id-stable (Q , h , q₀ , ii) = λ x → (ii x) ∘ (Trunc-rec (h x) (λ p → transport _ p q₀))

    -- 4 ⇒ 2
    id-stable→tr-rel-id : id-stable → tr-rel-id
    id-stable→tr-rel-id idst = (λ x → Trunc (n -2) (x₀ == x)) , (λ _ → Trunc-level) , [ idp ] , idst

max_stars_repo_name: nicolaikraus/HoTT-Agda


text:
open import MJ.Types
import MJ.Classtable.Core as Core

module MJ.Syntax.Typed {c}(Ct : Core.Classtable c) where

open import Prelude
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.Vec as Vec
open import Data.Star as Star
open import Data.List hiding (null)
open import Data.List.Relation.Unary.All
open import Data.List.Membership.Propositional
open import Data.List.Properties.Extra as List+
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.String

open Core c
open Classtable Ct
open import MJ.Classtable.Membership Ct
open import MJ.LexicalScope c

NativeBinOp = ℕ → ℕ → ℕ

{-
Expressions are indexed by a lexical context and a type.

MJ has n-ary calls for which we use All to express that an expression (of the
right type) is expected for every formal argument of the method signature.

In this nameless representation AccMember type is used to identify accessible
fields and methods on a particular class.
Here we exploit that AccMember is defined via a decision procedure: Agda
will be able to infer the membership proofs if they exist.
-}
data Expr (Γ : Ctx) : Ty c → Set where
  -- irreducible expressions
  unit     : Expr Γ void
  null     : ∀ {C} → Expr Γ (ref C)
  num      : ℕ → Expr Γ int

  -- storeless expressions
  var      : ∀ {a} → Var Γ a → Expr Γ a
  iop      : NativeBinOp → (l r : Expr Γ int) → Expr Γ int
  upcast   : ∀ {c c'} → Σ ⊢ c <: c' → Expr Γ (ref c) → Expr Γ (ref c')

  -- storeful
  new      : ∀ C → All (Expr Γ) (Class.constr (Σ C)) → Expr Γ (ref C)
  call     : ∀ {cid} →
             Expr Γ (ref cid) → ∀ m {as}{b}{acc : AccMember cid METHOD m (as , b)} → All (Expr Γ) as →
             Expr Γ b
  get      : ∀ {cid} → Expr Γ (ref cid) → ∀ f {ty}{acc : AccMember cid FIELD f ty} → Expr Γ ty

mutual
  {-
  Like Java, MJ distinguishes expressions from statements.
  We index the well-typed statement type Stmt
  with both an input and output context to capture that the constructor
  for declaration of locals loc adds to the lexical environment.
  We can interpret the type Stmt as a binary relation on contexts of which we
  can take the reflexive, transitive closure (Star)
  to obtain a datatype for sequenced statements:

  The type r represent the (possibly early) return type of a block of statements.
  -}
  infixl 20 if_then_else_
  data Stmt (I : Ctx)(r : Ty c) : (O : Ctx) → Set where
    loc        : ∀ a → Stmt I r (I +local a)
    asgn       : ∀ {a} → Var I a → Expr I a → Stmt I r I
    set        : ∀ {C} → Expr I (ref C) → ∀ f {a}{acc : AccMember C FIELD f a} → Expr I a → Stmt I r I
    run        : ∀ {a} → Expr I a → Stmt I r I
    ret        : Expr I r → Stmt I r I
    raise      : Stmt I r I
    try_catch_ : ∀ {O O'} → Stmt I r O → Stmt I r O' → Stmt I r I
    while_run_ : ∀ {O} → Expr I int → Stmt I r O → Stmt I r I
    block      : ∀ {O} → Stmts I r O → Stmt I r I
    if_then_else_ : ∀ {a} → Expr I int → Stmt I r a → Stmt I r a → Stmt I r a

  Stmts : Ctx → Ty c → Ctx → Set
  Stmts I r O = Star (λ I' O' → Stmt I' r O') I O


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.FinData.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
open import Cubical.Data.Bool.Base
open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    A B : Type ℓ

data Fin : ℕ → Type₀ where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

toℕ : ∀ {n} → Fin n → ℕ
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

¬Fin0 : ¬ Fin 0
¬Fin0 ()

_==_ : ∀ {n} → Fin n → Fin n → Bool
zero == zero   = true
zero == suc _  = false
suc _ == zero  = false
suc m == suc n = m == n

foldrFin : ∀ {n} → (A → B → B) → B → (Fin n → A) → B
foldrFin {n = zero}  _ b _ = b
foldrFin {n = suc n} f b l = f (l zero) (foldrFin f b (l ∘ suc))


text:
------------------------------------------------------------------------------
-- Propositional logic theorems
------------------------------------------------------------------------------

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

module FOL.PropositionalLogic.TheoremsI where

-- The theorems below are valid on intuitionistic logic and with an
-- empty domain.
open import FOL.Base hiding ( D≢∅ ; pem )

------------------------------------------------------------------------------
-- Boolean laws

→-transposition : {P Q : Set} → (P → Q) → ¬ Q → ¬ P
→-transposition p→q ¬q p = ¬q (p→q p)

∧∨-dist : {P Q R : Set} → P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
∧∨-dist {P} {Q} {R} = l→r , r→l
  where
  l→r : P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
  l→r (p , inj₁ q) = inj₁ (p , q)
  l→r (p , inj₂ r) = inj₂ (p , r)

  r→l : P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
  r→l (inj₁ (p , q)) = p , inj₁ q
  r→l (inj₂ (p , r)) = p , inj₂ r

∧∨-dist' : {P Q R : Set} → P ∧ (Q ∨ R) ⇔ P ∧ Q ∨ P ∧ R
∧∨-dist' {P} {Q} {R} = l⇒r , r⇒l
  where
  l→r : P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
  l→r (p , inj₁ q) = inj₁ (p , q)
  l→r (p , inj₂ r) = inj₂ (p , r)

  l⇒r : P ∧ (Q ∨ R) ⇒ P ∧ Q ∨ P ∧ R
  l⇒r = fun l→r

  r→l : P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
  r→l (inj₁ (p , q)) = p , inj₁ q
  r→l (inj₂ (p , r)) = p , inj₂ r

  -- TODO (21 February 2015). In r⇒l we needed parenthesis in the
  -- antecedent, but they aren't needed in r→l. That is, the fixity of
  -- _⇒_ should be the same than the fixity of _→_.
  r⇒l : (P ∧ Q ∨ P ∧ R) ⇒ P ∧ (Q ∨ R)
  r⇒l = fun r→l

DM : {P Q : Set} → ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q
DM {P} {Q} = l→r , r→l
  where
  l→r : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q
  l→r h = (λ p → h (inj₁ p)) , (λ q → h (inj₂ q))

  r→l : ¬ P ∧ ¬ Q → ¬ (P ∨ Q)
  r→l (¬p , ¬q) p∨q = case ¬p ¬q p∨q

-- The principle of the excluded middle implies the double negation
-- elimination
pem→¬¬-elim : ∀ {P} → (P ∨ ¬ P) → ¬ ¬ P → P
pem→¬¬-elim (inj₁ p)  _ = p
pem→¬¬-elim (inj₂ ¬p) h = ⊥-elim (h ¬p)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc