text:
------------------------------------------------------------------------
-- Binary trees
------------------------------------------------------------------------

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

open import Equality

module Tree {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude hiding (id)

open import Bag-equivalence eq
open import Bijection eq using (_↔_)
open import Function-universe eq
open import List eq

------------------------------------------------------------------------
-- Binary trees

data Tree (A : Type) : Type where
  leaf : Tree A
  node : (l : Tree A) (x : A) (r : Tree A) → Tree A

-- Any.

AnyT : ∀ {A} → (A → Type) → (Tree A → Type)
AnyT P leaf         = ⊥
AnyT P (node l x r) = AnyT P l ⊎ P x ⊎ AnyT P r

-- Membership.

infix 4 _∈T_

_∈T_ : ∀ {A} → A → Tree A → Type
x ∈T t = AnyT (_≡_ x) t

-- Bag equivalence.

_≈-bagT_ : ∀ {A} → Tree A → Tree A → Type
t₁ ≈-bagT t₂ = ∀ x → x ∈T t₁ ↔ x ∈T t₂

------------------------------------------------------------------------
-- Singleton

-- Singleton trees.

singleton : {A : Type} → A → Tree A
singleton x = node leaf x leaf

-- Any lemma for singleton.

Any-singleton : ∀ {A : Type} (P : A → Type) {x} →
                AnyT P (singleton x) ↔ P x
Any-singleton P {x} =
  AnyT P (singleton x)  ↔⟨⟩
  ⊥ ⊎ P x ⊎ ⊥           ↔⟨ ⊎-left-identity ⟩
  P x ⊎ ⊥               ↔⟨ ⊎-right-identity ⟩
  P x                   □

------------------------------------------------------------------------
-- Flatten

-- Inorder flattening of a tree.

flatten : {A : Type} → Tree A → List A
flatten leaf         = []
flatten (node l x r) = flatten l ++ x ∷ flatten r

-- Flatten does not add or remove any elements.

flatten-lemma : {A : Type} (t : Tree A) → ∀ z → z ∈ flatten t ↔ z ∈T t
flatten-lemma leaf         = λ z → ⊥ □
flatten-lemma (node l x r) = λ z →
  z ∈ flatten l ++ x ∷ flatten r         ↔⟨ Any-++ (_≡_ z) _ _ ⟩
  z ∈ flatten l ⊎ z ≡ x ⊎ z ∈ flatten r  ↔⟨ flatten-lemma l z ⊎-cong (z ≡ x □) ⊎-cong flatten-lemma r z ⟩
  z ∈T l        ⊎ z ≡ x ⊎ z ∈T r         □

------------------------------------------------------------------------
-- Bags can (perhaps) be defined as binary trees quotiented by bag
-- equivalence

-- Agda doesn't support quotients, so the following type is used to
-- state that two quotients are isomorphic.
--
-- Note that this definition may not actually make sense if the
-- relations _≈A_ and _≈B_ are not /proof-irrelevant/ equivalence
-- relations.

record _/_↔_/_ (A : Type) (_≈A_ : A → A → Type)
               (B : Type) (_≈B_ : B → B → Type) : Type where
  field
    to        : A → B
    to-resp   : ∀ x y → x ≈A y → to x ≈B to y
    from      : B → A
    from-resp : ∀ x y → x ≈B y → from x ≈A from y
    to∘from   : ∀ x → to (from x) ≈B x
    from∘to   : ∀ x → from (to x) ≈A x

-- Lists quotiented by bag equivalence are isomorphic to binary trees
-- quotiented by bag equivalence (assuming that one can actually
-- quotient by bag equivalence, and that the definition of _/_↔_/_
-- makes sense in this case).

list-bags↔tree-bags : {A : Type} → List A / _≈-bag_ ↔ Tree A / _≈-bagT_
list-bags↔tree-bags {A} = record
  { to        = to-tree
  ; to-resp   = λ xs ys xs≈ys z →
                  z ∈T to-tree xs  ↔⟨ to-tree-lemma xs z ⟩
                  z ∈ xs           ↔⟨ xs≈ys z ⟩
                  z ∈ ys           ↔⟨ inverse $ to-tree-lemma ys z ⟩
                  z ∈T to-tree ys  □
  ; from      = flatten
  ; from-resp = λ t₁ t₂ t₁≈t₂ z →
                  z ∈ flatten t₁  ↔⟨ flatten-lemma t₁ z ⟩
                  z ∈T t₁         ↔⟨ t₁≈t₂ z ⟩
                  z ∈T t₂         ↔⟨ inverse $ flatten-lemma t₂ z ⟩
                  z ∈ flatten t₂  □
  ; to∘from   = to∘from
  ; from∘to   = from∘to
  }
  where
  to-tree : List A → Tree A
  to-tree = foldr (node leaf) leaf

  to-tree-lemma : ∀ xs z → z ∈T to-tree xs ↔ z ∈ xs
  to-tree-lemma []       = λ z → ⊥ □
  to-tree-lemma (x ∷ xs) = λ z →
    ⊥ ⊎ z ≡ x   ⊎ z ∈T to-tree xs  ↔⟨ id ⊎-cong id ⊎-cong to-tree-lemma xs z ⟩
    ⊥ ⊎ z ≡ x   ⊎ z ∈ xs           ↔⟨ ⊎-assoc ⟩
    (⊥ ⊎ z ≡ x) ⊎ z ∈ xs           ↔⟨ ⊎-left-identity ⊎-cong id ⟩
    z ≡ x       ⊎ z ∈ xs           □

  to-tree-++ : ∀ {P : A → Type} xs {ys} →
               AnyT P (to-tree (xs ++ ys)) ↔
               AnyT P (to-tree xs) ⊎ AnyT P (to-tree ys)
  to-tree-++ {P} [] {ys} =
    AnyT P (to-tree ys)      ↔⟨ inverse ⊎-left-identity ⟩
    ⊥ ⊎ AnyT P (to-tree ys)  □
  to-tree-++ {P} (x ∷ xs) {ys} =
    ⊥ ⊎ P x ⊎ AnyT P (to-tree (xs ++ ys))                  ↔⟨ id ⊎-cong id ⊎-cong to-tree-++ xs ⟩
    ⊥ ⊎ P x ⊎ AnyT P (to-tree xs) ⊎ AnyT P (to-tree ys)    ↔⟨ lemma _ _ _ _ ⟩
    (⊥ ⊎ P x ⊎ AnyT P (to-tree xs)) ⊎ AnyT P (to-tree ys)  □
    where
    lemma : (A B C D : Type) → A ⊎ B ⊎ C ⊎ D ↔ (A ⊎ B ⊎ C) ⊎ D
    lemma A B C D =
      A ⊎ B ⊎ C ⊎ D      ↔⟨ ⊎-assoc ⟩
      (A ⊎ B) ⊎ C ⊎ D    ↔⟨ ⊎-assoc ⟩
      ((A ⊎ B) ⊎ C) ⊎ D  ↔⟨ inverse ⊎-assoc ⊎-cong id ⟩
      (A ⊎ B ⊎ C) ⊎ D    □

  to∘from : ∀ t → to-tree (flatten t) ≈-bagT t
  to∘from leaf         = λ z → ⊥ □
  to∘from (node l x r) = λ z →
    z ∈T to-tree (flatten l ++ x ∷ flatten r)                        ↔⟨ to-tree-++ (flatten l) ⟩
    z ∈T to-tree (flatten l) ⊎ ⊥ ⊎ z ≡ x ⊎ z ∈T to-tree (flatten r)  ↔⟨ to∘from l z ⊎-cong id ⊎-cong id ⊎-cong to∘from r z ⟩
    z ∈T l                   ⊎ ⊥ ⊎ z ≡ x ⊎ z ∈T r                    ↔⟨ id ⊎-cong ⊎-left-identity ⟩
    z ∈T l                   ⊎     z ≡ x ⊎ z ∈T r                    □

  from∘to : ∀ xs → flatten (to-tree xs) ≈-bag xs
  from∘to []       = λ z → ⊥ □
  from∘to (x ∷ xs) = λ z →
    z ≡ x ⊎ z ∈ flatten (to-tree xs)  ↔⟨ id ⊎-cong from∘to xs z ⟩
    z ≡ x ⊎ z ∈ xs                    □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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 j} {A : Type i} (X : A → Ptd j) 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})

module _ {i j} {A : Type i} (dec : has-dec-eq A) {X : Ptd j} where

  {- The dependent version increases the complexity significantly
     and we do not need it. -}

  ⊙bwproj-in : A → A → X ⊙→ X
  ⊙bwproj-in a a' with dec a a'
  ... | inl _ = ⊙idf _
  ... | inr _ = ⊙cst

  module BigWedgeProj (a : A) = BigWedgeRec
    {X = λ _ → X}
    (pt X)
    (λ a' → fst (⊙bwproj-in a a'))
    (λ a' → ! (snd (⊙bwproj-in a a')))

  bwproj : A → BigWedge (λ _ → X) → de⊙ X
  bwproj = BigWedgeProj.f

  ⊙bwproj : A → ⊙BigWedge (λ _ → X) ⊙→ X
  ⊙bwproj a = bwproj a , idp

  abstract
    bwproj-bwin-diag : (a : A) → bwproj a ∘ bwin a ∼ idf (de⊙ X)
    bwproj-bwin-diag a x with dec a a
    ... | inl _ = idp
    ... | inr a≠a with a≠a idp
    ...           | ()

    bwproj-bwin-≠ : {a a' : A} → a ≠ a' → bwproj a ∘ bwin a' ∼ cst (pt X)
    bwproj-bwin-≠ {a} {a'} a≠a' x with dec a a'
    ... | inr _ = idp
    ... | inl a=a' with a≠a' a=a'
    ...            | ()

module _ {i j k} {A : Type i} (dec : has-dec-eq A) {X : Ptd j} (a : A) where

  abstract
    private
      bwproj-BigWedge-emap-r-lift-in : ∀ a'
        → bwproj dec {X = ⊙Lift {j = k} X} a ∘ bwin a' ∘ lift
        ∼ lift {j = k} ∘ bwproj dec {X = X} a ∘ bwin a'
      bwproj-BigWedge-emap-r-lift-in a' with dec a a'
      ... | inl _ = λ _ → idp
      ... | inr _ = λ _ → idp

      bwproj-BigWedge-emap-r-lift-glue' : ∀ (a' : A)
        → ap (lift {j = k}) (! (snd (⊙bwproj-in dec {X = X} a a')))
        == ! (snd (⊙bwproj-in dec {X = ⊙Lift {j = k} X} a a')) ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)
      bwproj-BigWedge-emap-r-lift-glue' a' with dec a a'
      ... | inl _ = idp
      ... | inr _ = idp

    bwproj-BigWedge-emap-r-lift-glue : ∀ (a' : A)
      →  idp == bwproj-BigWedge-emap-r-lift-in a' (pt X)
      [ (λ x → bwproj dec {X = ⊙Lift {j = k} X} a (–> (BigWedge-emap-r (λ _ → ⊙lift-equiv {j = k})) x)
            == lift {j = k} (bwproj dec {X = X} a x)) ↓ bwglue a' ]
    bwproj-BigWedge-emap-r-lift-glue a' = ↓-='-in' $
      ap (lift {j = k} ∘ bwproj dec a) (bwglue a')
        =⟨ ap-∘ (lift {j = k}) (bwproj dec a) (bwglue a') ⟩
      ap (lift {j = k}) (ap (bwproj dec a) (bwglue a'))
        =⟨ ap (ap (lift {j = k})) $ BigWedgeProj.glue-β dec a a' ⟩
      ap (lift {j = k}) (! (snd (⊙bwproj-in dec a a')))
        =⟨ bwproj-BigWedge-emap-r-lift-glue' a' ⟩
      ! (snd (⊙bwproj-in dec a a')) ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)
        =⟨ ap (_∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)) $
            ( ! $ BigWedgeProj.glue-β dec a a') ⟩
      ap (bwproj dec a) (bwglue a') ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)
        =⟨ ap (λ p → ap (bwproj dec a) p
                  ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)) $
            (! $ PushoutFmap.glue-β (fst (bigwedge-span-emap-r (λ _ → ⊙lift-equiv {j = k}))) a') ⟩
      ap (bwproj dec a) (ap (–> (BigWedge-emap-r (λ _ → ⊙lift-equiv {j = k}))) (bwglue a'))
      ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)
        =⟨ ap (_∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)) $
            (∘-ap (bwproj dec a) (–> (BigWedge-emap-r (λ _ → ⊙lift-equiv {j = k}))) (bwglue a')) ⟩
      ap (bwproj dec a ∘ –> (BigWedge-emap-r (λ _ → ⊙lift-equiv {j = k}))) (bwglue a')
      ∙' bwproj-BigWedge-emap-r-lift-in a' (pt X)
        =∎

    bwproj-BigWedge-emap-r-lift :
        bwproj dec {X = ⊙Lift {j = k} X} a ∘ –> (BigWedge-emap-r (λ _ → ⊙lift-equiv {j = k}))
      ∼ lift {j = k} ∘ bwproj dec a
    bwproj-BigWedge-emap-r-lift =
      BigWedge-elim {X = λ _ → X} idp
        bwproj-BigWedge-emap-r-lift-in
        bwproj-BigWedge-emap-r-lift-glue

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Categories.Category
open import Categories.Functor

Constant : ∀ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} (x : Category.Obj D) → ∀ {o ℓ e} {C : Category o ℓ e} → Functor C D
Constant {D = D} x = record
                     { F₀ = λ _ → x
                     ; F₁ = λ _ → D.id
                     ; identity = D.Equiv.refl
                     ; homomorphism = D.Equiv.sym D.identityˡ
                     ; F-resp-≡ = λ _ → D.Equiv.refl
                     }
                     where
                     module D = Category D

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --allow-unsolved-metas #-}
postulate
  A : Set
  a : A

record Q .(x : A) : Set where
  field q : A

record R : Set where
  field s : Q _

  t : A
  t = Q.q s

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module LinkedList.Properties where

open import LinkedList

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_; refl; cong; cong₂; trans; sym; inspect)
open PropEq.≡-Reasoning

incr-suc : ∀ {A x} → {xs : LinkedList A} → ⟦ incr x xs ⟧ ≡ suc ⟦ xs ⟧
incr-suc {_} {x} {xs} = refl

decr-pred : ∀ {A} → {xs : LinkedList A} → (p : False (null? xs)) → ⟦ decr xs p ⟧ ≡ pred ⟦ xs ⟧
decr-pred {xs = []    } ()
decr-pred {xs = x ∷ xs} p = refl

++-left-indentity : ∀ {A} → {xs : LinkedList A} → [] ++ xs ≡ xs
++-left-indentity {A} {xs} = refl

++-right-indentity : ∀ {A} → {xs : LinkedList A} → [] ++ xs ≡ xs
++-right-indentity {A} {xs} = refl

⟦xs++ys⟧≡⟦xs⟧+⟦ys⟧ : ∀ {A} → (xs : LinkedList A)
                         → (ys : LinkedList A)
                         → ⟦ xs ++ ys ⟧ ≡ ⟦ xs ⟧ + ⟦ ys ⟧
⟦xs++ys⟧≡⟦xs⟧+⟦ys⟧ []       ys = refl
⟦xs++ys⟧≡⟦xs⟧+⟦ys⟧ (x ∷ xs) ys = cong suc (⟦xs++ys⟧≡⟦xs⟧+⟦ys⟧ xs ys)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Nat.Order.Recursive where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Empty
open import Cubical.Data.Unit

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties

open import Cubical.Relation.Nullary

infix 4 _≤_ _<_

_≤_ : ℕ → ℕ → Type₀
zero ≤ _ = Unit
suc m ≤ zero = ⊥
suc m ≤ suc n = m ≤ n

_<_ : ℕ → ℕ → Type₀
m < n = suc m ≤ n

data Trichotomy (m n : ℕ) : Type₀ where
  lt : m < n → Trichotomy m n
  eq : m ≡ n → Trichotomy m n
  gt : n < m → Trichotomy m n

private
  variable
    k l m n : ℕ

m≤n-isProp : isProp (m ≤ n)
m≤n-isProp {zero} = isPropUnit
m≤n-isProp {suc m} {zero}  = isProp⊥
m≤n-isProp {suc m} {suc n} = m≤n-isProp {m} {n}

≤-k+ : m ≤ n → k + m ≤ k + n
≤-k+ {k = zero}  m≤n = m≤n
≤-k+ {k = suc k} m≤n = ≤-k+ {k = k} m≤n

≤-+k : m ≤ n → m + k ≤ n + k
≤-+k {m} {n} {k} m≤n
  = transport (λ i → +-comm k m i ≤ +-comm k n i) (≤-k+ {m} {n} {k} m≤n)

≤-refl : ∀ m → m ≤ m
≤-refl zero = _
≤-refl (suc m) = ≤-refl m

≤-trans : k ≤ m → m ≤ n → k ≤ n
≤-trans {zero} _ _ = _
≤-trans {suc k} {suc m} {suc n} = ≤-trans {k} {m} {n}

≤-antisym : m ≤ n → n ≤ m → m ≡ n
≤-antisym {zero} {zero} _ _ = refl
≤-antisym {suc m} {suc n} m≤n n≤m = cong suc (≤-antisym m≤n n≤m)

≤-k+-cancel : k + m ≤ k + n → m ≤ n
≤-k+-cancel {k =  zero} m≤n = m≤n
≤-k+-cancel {k = suc k} m≤n = ≤-k+-cancel {k} m≤n

≤-+k-cancel : m + k ≤ n + k → m ≤ n
≤-+k-cancel {m} {k} {n}
  = ≤-k+-cancel {k} {m} {n} ∘ transport λ i → +-comm m k i ≤ +-comm n k i

¬m<m : ¬ m < m
¬m<m {suc m} = ¬m<m {m}

≤0→≡0 : n ≤ 0 → n ≡ 0
≤0→≡0 {zero} _ = refl

¬m+n<m : ¬ m + n < m
¬m+n<m {suc m} = ¬m+n<m {m}

<-weaken : m < n → m ≤ n
<-weaken {zero} _ = _
<-weaken {suc m} {suc n} = <-weaken {m}

Trichotomy-suc : Trichotomy m n → Trichotomy (suc m) (suc n)
Trichotomy-suc (lt m<n) = lt m<n
Trichotomy-suc (eq m≡n) = eq (cong suc m≡n)
Trichotomy-suc (gt n<m) = gt n<m

_≟_ : ∀ m n → Trichotomy m n
zero  ≟ zero = eq refl
zero  ≟ suc n = lt _
suc m ≟ zero = gt _
suc m ≟ suc n = Trichotomy-suc (m ≟ n)

k≤k+n : ∀ k → k ≤ k + n
k≤k+n zero    = _
k≤k+n (suc k) = k≤k+n k

n≤k+n : ∀ n → n ≤ k + n
n≤k+n {k} n = transport (λ i → n ≤ +-comm n k i) (k≤k+n n)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --show-irrelevant #-}

module Control.Category.Product where

open import Level using (suc; _⊔_)
open import Relation.Binary hiding (_⇒_)

open import Control.Category
open Category using () renaming (Obj to obj; _⇒_ to _▹_⇒_)

-- Pre-Product

-- Given a category C and two objects A, B in C we can define a new category
-- whose objects are triples of an object A×B in C that has
-- morphisms fst, snd to A and B.
-- We call such a triple a pre-product of A and B.
-- Alternatively, it could be called a bislice.

record PreProductObj {o h e} (C : Category o h e) (A B : obj C) : Set (o ⊔ h ⊔ e) where
  open Category C -- public
  field
    A×B : Obj
    fst : A×B ⇒ A
    snd : A×B ⇒ B

-- In the following, we fix a category C and two objects A and B.

module PreProduct {o h e} {C : Category o h e} {A B : obj C} where

  -- We use _⇒_ for C's morphisms and _∘_ for their composition.
  open module C = Category C using (_⇒_; _⟫_; _∘_; _≈_; ≈-refl; ≈-sym; ≈-trans; ∘-cong)

  -- We consider only pre-products of A and B.
  Obj = PreProductObj C A B

  open PreProductObj using () renaming (A×B to A×B◃_)

  -- A morphism in the category of pre-products of A and B
  -- from pre-product (X, f, g) to (A×B, fst, snd)
  -- is a morphism ⟨f,g⟩ : X ⇒ A×B such that fst ∘ ⟨f,g⟩ ≡ f
  -- and snd ∘ ⟨f,g⟩ ≡ g.

  record IsPair (P : Obj) {X} (f : X ⇒ A) (g : X ⇒ B) (⟨f,g⟩ : X ⇒ (A×B◃ P))
      : Set (o ⊔ h ⊔ e)
    where
    constructor β-pair

    open PreProductObj P using (fst; snd)
    field
      β-fst : (fst ∘ ⟨f,g⟩) ≈ f
      β-snd : (snd ∘ ⟨f,g⟩) ≈ g

  record PreProductMorphism (O P : Obj) : Set (o ⊔ h ⊔ e)
    where
    constructor pair

    open PreProductObj O using () renaming (A×B to X; fst to f; snd to g)
    open PreProductObj P
    field
      ⟨f,g⟩   : X ⇒ A×B
      isPair : IsPair P f g ⟨f,g⟩
    open IsPair isPair public

  open PreProductMorphism using (isPair)

  -- We write O ⇉ P for a morphism from pre-product O to pre-product P.
  _⇉_ = PreProductMorphism

  -- The identity pre-product morphism is just the identity morphism.

  id : ∀ {P} → P ⇉ P
  id = record
    { ⟨f,g⟩ = C.id
    ; isPair = record
      { β-fst = C.id-first
      ; β-snd = C.id-first
      }
    }

  -- The composition of pre-product morphims is just the composition in C.

  comp : ∀ {N O P} → N ⇉ O → O ⇉ P → N ⇉ P
  comp (pair o (β-pair o-fst o-snd)) (pair p (β-pair p-fst p-snd)) = record
    { ⟨f,g⟩ = o ⟫ p
    ; isPair = record
      { β-fst = ≈-trans (C.∘-assoc o) (≈-trans (∘-cong ≈-refl p-fst) o-fst)
      ; β-snd = ≈-trans (C.∘-assoc o) (≈-trans (∘-cong ≈-refl p-snd) o-snd)
      }
    }

  -- Thus, we have a category of PreProducts, inheriting the laws from C.

  PreProductHom : (O P : Obj) → Setoid _ _
  PreProductHom O P = record
    { Carrier       = PreProductMorphism O P
    ; _≈_           = λ h i → PreProductMorphism.⟨f,g⟩ h ≈ PreProductMorphism.⟨f,g⟩ i
    ; isEquivalence = record
      { refl  = ≈-refl
      ; sym   = ≈-sym
      ; trans = ≈-trans
      }
    }

  preProductIsCategory : IsCategory PreProductHom
  preProductIsCategory = record
    { ops = record
      { id = id
      ; _⟫_ = comp
      }
    ; laws = record
      { id-first = C.id-first
      ; id-last  = C.id-last
      ; ∘-assoc  = λ f → C.∘-assoc _
      ; ∘-cong   = C.∘-cong
      }
    }

open PreProduct public

{-
record Pair {o h} {C : Category o h} {A B} (P : PreProductObj C A B)
    {X} (f : C ▹ X ⇒ A) (g : C ▹ X ⇒ B) : Set (h ⊔ o)
  where
  open PreProductObj P
  field
    ⟨f,g⟩  : C ▹ X ⇒ A×B
    isPair : IsPair P f g ⟨f,g⟩
    unique : ∀ {h} → IsPair P f g h → h ≈ ⟨f,g⟩

  open IsPair isPair public

-- The product of A and B is the terminal object in the PreProductCategory

record IsProduct {o h} {C : Category o h} {A B} (P : PreProductObj C A B) : Set (h ⊔ o) where
  open Category C
  open PreProductObj P
  field
    pairing : ∀ {X} (f : X ⇒ A) (g : X ⇒ B) → Pair P f g

record Product {o h} (C : Category o h) (A B : obj C) : Set (h ⊔ o) where
  field
    preProduct : PreProductObj C A B
    isProduct  : IsProduct preProduct

  open PreProductObj preProduct public
  open IsProduct isProduct public

{-
record IsProduct {o h} (C : Category o h) (A B A×B : Obj C) : Set (h ⊔ o) where
  open Category C
  field
    fst   : A×B ⇒ A
    snd   : A×B ⇒ B
    pair  : ∀ {X} (f : X ⇒ A) (g : X ⇒ B) → X ⇒ A×B
    β-fst : ∀ {X} {f : X ⇒ A} {g : X ⇒ B} → fst ∘ pair f g ≡ f
    β-snd : ∀ {X} {f : X ⇒ A} {g : X ⇒ B} → fst ∘ pair f g ≡ f

-}

-- Category with Products

HasProducts : ∀ {o h} (C : Category o h) → Set (o ⊔ h)
HasProducts C = ∀ (A B : obj C) → Product C A B

-}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
-- Andreas, 2012-05-04
module PruningNonMillerPatternFail where

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

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

-- bad variable y is not in head position under lambda, so do not prune
fail4 : let X : Nat -> Nat -> Nat
            X = _ -- λ x y → suc x
            Y : Nat → ((Nat → Nat) → Nat) -> Nat
            Y = _  -- More than one solution:
                   -- λ x f → x
                   -- λ x f → f (λ z → x)
        in  (C : Set) ->
            (({x y : Nat} -> X x x ≡ suc (Y x (λ k → k y))) ->
             ({x y : Nat} -> Y x (λ k → k x) ≡ x)           ->
             ({x y : Nat} -> X (Y x (λ k → k y)) y ≡ X x x) -> C) -> C
fail4 C k = k refl refl refl

-- this should not solve, since there are more than one solutions for Y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Data.Binary.Operations.Unary where

open import Data.Binary.Definitions
open import Function

inc⁺⁺ : 𝔹⁺ → 𝔹⁺
inc⁺⁺ 1ᵇ = O ∷ 1ᵇ
inc⁺⁺ (O ∷ xs) = I ∷ xs
inc⁺⁺ (I ∷ xs) = O ∷ inc⁺⁺ xs

inc⁺ : 𝔹 → 𝔹⁺
inc⁺ 0ᵇ = 1ᵇ
inc⁺ (0< x) = inc⁺⁺ x

inc : 𝔹 → 𝔹
inc x = 0< inc⁺ x

dec⁺⁺ : Bit → 𝔹⁺ → 𝔹⁺
dec⁺⁺ I xs = O ∷ xs
dec⁺⁺ O 1ᵇ = 1ᵇ
dec⁺⁺ O (x ∷ xs) = I ∷ dec⁺⁺ x xs

dec⁺ : 𝔹⁺ → 𝔹
dec⁺ 1ᵇ = 0ᵇ
dec⁺ (x ∷ xs) = 0< dec⁺⁺ x xs

dec : 𝔹 → 𝔹
dec 0ᵇ = 0ᵇ
dec (0< x) = dec⁺ x

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.S3 where

{-
This file contains a summary of what remains for π₄S³≅ℤ/2 to be proved.
See the module π₄S³ at the end of this file.
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function

open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.Int
  renaming (_·_ to _·ℤ_ ; _+_ to _+ℤ_)

open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.Whitehead
open import Cubical.Algebra.Group.Instances.IntMod
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.Sn
open import Cubical.HITs.SetTruncation

open import Cubical.Algebra.Group
  renaming (ℤ to ℤGroup ; Bool to BoolGroup ; Unit to UnitGroup)
open import Cubical.Algebra.Group.ZAction

[_]× : ∀ {ℓ} {X : Pointed ℓ} {n m : ℕ}
  → π' (suc n) X × π' (suc m) X → π' (suc (n + m)) X
[_]× (f , g) = [ f ∣ g ]π'

-- Some type abbreviations (unproved results)
π₃S²-gen : Type
π₃S²-gen = gen₁-by (π'Gr 2 (S₊∙ 2)) ∣ HopfMap ∣₂

π₄S³≅ℤ/something : GroupEquiv ℤGroup (π'Gr 2 (S₊∙ 2))
                 → Type
π₄S³≅ℤ/something eq =
  GroupIso (π'Gr 3 (S₊∙ 3))
           (ℤ/ abs (invEq (fst eq)
             [ ∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂ ]×))

miniLem₁ : Type
miniLem₁ = (g : ℤ) → gen₁-by ℤGroup g → (g ≡ 1) ⊎ (g ≡ -1)

miniLem₂ : Type
miniLem₂ = (ϕ : GroupEquiv ℤGroup ℤGroup) (g : ℤ)
      → (abs g ≡ abs (fst (fst ϕ) g))

-- some minor group lemmas
groupLem-help : miniLem₁ → (g : ℤ) →
      gen₁-by ℤGroup g →
      (ϕ : GroupHom ℤGroup ℤGroup) →
      (fst ϕ g ≡ pos 1) ⊎ (fst ϕ g ≡ negsuc 0)
    → isEquiv (fst ϕ)
groupLem-help grlem1 g gen ϕ = main (grlem1 g gen)
  where
  isEquiv- : isEquiv (-_)
  isEquiv- = isoToIsEquiv (iso -_ -_ -Involutive -Involutive)

  lem : fst ϕ (pos 1) ≡ pos 1 → fst ϕ ≡ idfun _
  lem p = funExt lem2
    where
    lem₁ : (x₁ : ℕ) → fst ϕ (pos x₁) ≡ idfun ℤ (pos x₁)
    lem₁ zero = IsGroupHom.pres1 (snd ϕ)
    lem₁ (suc zero) = p
    lem₁ (suc (suc n)) =
      IsGroupHom.pres· (snd ϕ) (pos (suc n)) 1
                             ∙ cong₂ _+ℤ_ (lem₁ (suc n)) p

    lem2 : (x₁ : ℤ) → fst ϕ x₁ ≡ idfun ℤ x₁
    lem2 (pos n) = lem₁ n
    lem2 (negsuc zero) =
      IsGroupHom.presinv (snd ϕ) 1 ∙ cong (λ x → pos 0 - x) p
    lem2 (negsuc (suc n)) =
        (cong (fst ϕ) (sym (+Comm (pos 0) (negsuc (suc n))))
      ∙ IsGroupHom.presinv (snd ϕ) (pos (suc (suc n))))
      ∙∙ +Comm (pos 0) _
      ∙∙ cong (-_) (lem₁ (suc (suc n)))

  lem₂ : fst ϕ (negsuc 0) ≡ pos 1 → fst ϕ ≡ -_
  lem₂ p = funExt lem2
    where
    s = IsGroupHom.presinv (snd ϕ) (negsuc 0)
     ∙∙ +Comm (pos 0) _
     ∙∙ cong -_ p

    lem2 : (n : ℤ) → fst ϕ n ≡ - n
    lem2 (pos zero) = IsGroupHom.pres1 (snd ϕ)
    lem2 (pos (suc zero)) = s
    lem2 (pos (suc (suc n))) =
         IsGroupHom.pres· (snd ϕ) (pos (suc n)) 1
       ∙ cong₂ _+ℤ_ (lem2 (pos (suc n))) s
    lem2 (negsuc zero) = p
    lem2 (negsuc (suc n)) =
         IsGroupHom.pres· (snd ϕ) (negsuc n) (negsuc 0)
       ∙ cong₂ _+ℤ_ (lem2 (negsuc n)) p

  main : (g ≡ pos 1) ⊎ (g ≡ negsuc 0)
      → (fst ϕ g ≡ pos 1) ⊎ (fst ϕ g ≡ negsuc 0)
      → isEquiv (fst ϕ)
  main (inl p) =
    J (λ g p → (fst ϕ g ≡ pos 1)
             ⊎ (fst ϕ g ≡ negsuc 0) → isEquiv (fst ϕ))
      (λ { (inl x) → subst isEquiv (sym (lem x)) (snd (idEquiv _))
         ; (inr x) → subst isEquiv
                            (sym (lem₂ (IsGroupHom.presinv (snd ϕ) (pos 1)
                          ∙ (cong (λ x → pos 0 - x) x))))
                            isEquiv- })
                 (sym p)
  main (inr p) =
    J (λ g p → (fst ϕ g ≡ pos 1)
             ⊎ (fst ϕ g ≡ negsuc 0) → isEquiv (fst ϕ))
      (λ { (inl x) → subst isEquiv (sym (lem₂ x)) isEquiv-
         ; (inr x) → subst isEquiv
                       (sym (lem (
                       IsGroupHom.presinv (snd ϕ) (negsuc 0)
                     ∙ cong (λ x → pos 0 - x) x)))
                    (snd (idEquiv _))})
      (sym p)

groupLem : {G : Group₀}
         → miniLem₁
         → GroupEquiv ℤGroup G
         → (g : fst G)
         → gen₁-by G g
         → (ϕ : GroupHom G ℤGroup)
         → (fst ϕ g ≡ 1) ⊎ (fst ϕ g ≡ -1)
         → isEquiv (fst ϕ)
groupLem {G = G} s =
  GroupEquivJ
    (λ G _ → (g : fst G)
         → gen₁-by G g
         → (ϕ : GroupHom G ℤGroup)
         → (fst ϕ g ≡ 1) ⊎ (fst ϕ g ≡ -1)
         → isEquiv (fst ϕ))
    (groupLem-help s)

-- summary
module π₄S³
  (mini-lem₁ : miniLem₁)
  (mini-lem₂ : miniLem₂)
  (ℤ≅π₃S² : GroupEquiv ℤGroup (π'Gr 2 (S₊∙ 2)))
  (gen-by-HopfMap : π₃S²-gen)
  (π₄S³≅ℤ/whitehead : π₄S³≅ℤ/something ℤ≅π₃S²)
  (hopfWhitehead :
       abs (HopfInvariant-π' 0
             ([ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×))
     ≡ 2)
  where
  π₄S³ = π'Gr 3 (S₊∙ 3)

  hopfInvariantEquiv : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤGroup
  fst (fst hopfInvariantEquiv) = HopfInvariant-π' 0
  snd (fst hopfInvariantEquiv) =
    groupLem mini-lem₁ ℤ≅π₃S² ∣ HopfMap ∣₂
             gen-by-HopfMap
             (GroupHom-HopfInvariant-π' 0)
             (abs→⊎ _ _ HopfInvariant-HopfMap)
  snd hopfInvariantEquiv = snd (GroupHom-HopfInvariant-π' 0)

  lem : ∀ {G : Group₀} (ϕ ψ : GroupEquiv ℤGroup G) (g : fst G)
      → abs (invEq (fst ϕ) g) ≡ abs (invEq (fst ψ) g)
  lem =
    GroupEquivJ
      (λ G ϕ → (ψ : GroupEquiv ℤGroup G) (g : fst G)
      → abs (invEq (fst ϕ) g) ≡ abs (invEq (fst ψ) g))
      λ ψ → mini-lem₂ (invGroupEquiv ψ)

  main : GroupIso π₄S³ (ℤ/ 2)
  main = subst (GroupIso π₄S³)
               (cong (ℤ/_) (lem ℤ≅π₃S² (invGroupEquiv (hopfInvariantEquiv)) _
                               ∙ hopfWhitehead))
               π₄S³≅ℤ/whitehead


text:
-- Andreas, 2021-05-06, issue #5365
-- Error message for incomplete binding in do-block.

postulate _>>=_ : Set

test = do
  x ←

-- Expected: proper error like
--
-- Incomplete binding x ←
-- <EOF><ERROR>
-- ...


text:
-- Andreas, 2017-10-19, issue #2808
-- The fix of #1077 was not general enough.

-- module _ where  -- If this is added, we get the error about duplicate module

postulate A : Set  -- Accepted if this is deleted

module Issue2808 where

record Issue2808 : Set where

-- Expected error: (at the postulate)
-- Illegal declaration(s) before top-level module

-- We now raise this error if the first module of the file
-- has the same name as the inferred top-level module.


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Standard evaluation for MTerm
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value

import Parametric.Syntax.MType as MType
import Parametric.Syntax.MTerm as MTerm
import Parametric.Denotation.MValue as MValue

module Parametric.Denotation.MEvaluation
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (ValConst : MTerm.ValConstStructure Const)
    (CompConst : MTerm.CompConstStructure Const)
    (cbnToCompConst : MTerm.CbnToCompConstStructure Const CompConst)
    (cbvToCompConst : MTerm.CbvToCompConstStructure Const CompConst)
  where

open Type.Structure Base

open MType.Structure Base
open MTerm.Structure Const ValConst CompConst cbnToCompConst cbvToCompConst
open MValue.Structure Base ⟦_⟧Base

open import Base.Data.DependentList
open import Base.Denotation.Notation

-- Extension Point: Evaluation of constants.
ValStructure : Set
ValStructure = ∀ {τ} → ValConst τ → ⟦ τ ⟧

CompStructure : Set
CompStructure = ∀ {τ} → CompConst τ → ⟦ τ ⟧

module Structure
       (⟦_⟧ValBase  : ValStructure)
       (⟦_⟧CompBase : CompStructure)
    where

  -- We provide: Evaluation of arbitrary value/computation terms.
  ⟦_⟧Comp : ∀ {τ Γ} → Comp Γ τ → ⟦ Γ ⟧ValContext → ⟦ τ ⟧CompType
  ⟦_⟧Val : ∀ {τ Γ} → Val Γ τ → ⟦ Γ ⟧ValContext → ⟦ τ ⟧ValType

  ⟦ vVar x     ⟧Val ρ  = ⟦ x ⟧ValVar ρ
  ⟦ vThunk x   ⟧Val ρ  = ⟦ x ⟧Comp ρ
  ⟦ vConst c   ⟧Val ρ  = ⟦ c ⟧ValBase

  ⟦ cConst c   ⟧Comp ρ = ⟦ c ⟧CompBase
  ⟦ cForce x   ⟧Comp ρ = ⟦ x ⟧Val ρ
  ⟦ cReturn v  ⟧Comp ρ = ⟦ v ⟧Val ρ
  ⟦ cAbs c     ⟧Comp ρ = λ x → ⟦ c ⟧Comp (x • ρ)
  ⟦ cApp s t   ⟧Comp ρ = ⟦ s ⟧Comp ρ (⟦ t ⟧Val ρ)
  ⟦ c₁ into c₂ ⟧Comp ρ = ⟦ c₂ ⟧Comp (⟦ c₁ ⟧Comp ρ • ρ)

  meaningOfVal : ∀ {Γ τ} → Meaning (Val Γ τ)
  meaningOfVal = meaning ⟦_⟧Val

  -- Evaluation.agda also proves weaken-sound.

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{- Denotational semantics of the types in the category of temporal types. -}
module Semantics.Types where

open import Syntax.Types
open import CategoryTheory.Instances.Reactive hiding (_+_)
open import TemporalOps.Box
open import TemporalOps.Diamond

-- Denotation of types
⟦_⟧ₜ : Type -> τ
⟦ Unit     ⟧ₜ = ⊤
⟦ A & B    ⟧ₜ = ⟦ A ⟧ₜ ⊗ ⟦ B ⟧ₜ
⟦ A + B    ⟧ₜ = ⟦ A ⟧ₜ ⊕ ⟦ B ⟧ₜ
⟦ A => B   ⟧ₜ = ⟦ A ⟧ₜ ⇒ ⟦ B ⟧ₜ
⟦ Event A  ⟧ₜ = ◇ ⟦ A ⟧ₜ
⟦ Signal A ⟧ₜ = □ ⟦ A ⟧ₜ

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.ListedFiniteSet.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Prod using (_×_; _,_)

open import Cubical.HITs.ListedFiniteSet.Base

private
  variable
    ℓ : Level
    A B : Type ℓ

assoc-++ : ∀ (xs : LFSet A) ys zs → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc-++ []       ys zs = refl
assoc-++ (x ∷ xs) ys zs = cong (x ∷_) (assoc-++ xs ys zs)
assoc-++ (dup x xs i) ys zs j = dup x (assoc-++ xs ys zs j) i
assoc-++ (comm x y xs i) ys zs j = comm x y (assoc-++ xs ys zs j) i
assoc-++ (trunc xs xs' p q i k) ys zs j =
  trunc
    (assoc-++ xs ys zs j) (assoc-++ xs' ys zs j)
    (cong (λ xs → assoc-++ xs ys zs j) p) (cong (λ xs → assoc-++ xs ys zs j) q)
    i k

comm-++-[] : ∀ (xs : LFSet A) → xs ++ [] ≡ [] ++ xs
comm-++-[] xs =
  PropElim.f
    refl
    (λ x {xs} ind →
      (x ∷ xs) ++ [] ≡⟨ refl ⟩
      x ∷ (xs ++ []) ≡⟨ cong (x ∷_) ind ⟩
      x ∷ xs ≡⟨ refl ⟩
      [] ++ (x ∷ xs) ∎
    )
    (λ _ → trunc _ _)
    xs

comm-++-∷
  : ∀ (z : A) xs ys
  → xs ++ (z ∷ ys) ≡ (z ∷ xs) ++ ys
comm-++-∷ z xs ys =
  PropElim.f
    refl
    (λ x {xs} ind →
      x ∷ (xs ++ (z ∷ ys)) ≡⟨ cong (x ∷_) ind ⟩
      x ∷ z ∷ (xs ++ ys) ≡⟨ comm x z (xs ++ ys) ⟩
      z ∷ x ∷ (xs ++ ys) ∎
    )
    (λ _ → trunc _ _)
    xs

comm-++ : (xs ys : LFSet A) → xs ++ ys ≡ ys ++ xs
comm-++ xs ys =
  PropElim.f
    (comm-++-[] xs)
    (λ y {ys} ind →
      xs ++ (y ∷ ys) ≡⟨ comm-++-∷ y xs ys ⟩
      y ∷ (xs ++ ys) ≡⟨ cong (y ∷_) ind ⟩
      y ∷ (ys ++ xs) ≡⟨ refl ⟩
      (y ∷ ys) ++ xs ∎
    )
    (λ _ → trunc _ _)
    ys

idem-++ : (xs : LFSet A) → xs ++ xs ≡ xs
idem-++ =
  PropElim.f
    refl
    (λ x {xs} ind →
      (x ∷ xs) ++ (x ∷ xs) ≡⟨ refl ⟩
      x ∷ (xs ++ (x ∷ xs)) ≡⟨ refl ⟩
      x ∷ (xs ++ ((x ∷ []) ++ xs)) ≡⟨ cong (x ∷_) (assoc-++ xs (x ∷ []) xs) ⟩
      x ∷ ((xs ++ (x ∷ [])) ++ xs)
        ≡⟨ cong (λ h → x ∷ (h ++ xs)) (comm-++ xs (x ∷ [])) ⟩
      x ∷ x ∷ (xs ++ xs) ≡⟨ cong (λ ys → x ∷ x ∷ ys) ind ⟩
      x ∷ x ∷ xs ≡⟨ dup x xs ⟩
      x ∷ xs ∎
    )
    (λ xs → trunc (xs ++ xs) xs)

cart-product : LFSet A → LFSet B → LFSet (A × B)
cart-product [] ys = []
cart-product (x ∷ xs) ys = map (x ,_) ys ++ cart-product xs ys
cart-product (dup x xs i) ys =
  ( map (x ,_) ys ++ (map (x ,_) ys ++ cart-product xs ys)
      ≡⟨ assoc-++ (map (x ,_) ys) (map (x ,_) ys) (cart-product xs ys) ⟩
    (map (x ,_) ys ++ map (x ,_) ys) ++ cart-product xs ys
      ≡⟨ cong (_++ cart-product xs ys) (idem-++ (map (x ,_) ys)) ⟩
    map (x ,_) ys ++ cart-product xs ys
      ∎
  ) i
cart-product (comm x y xs i) ys =
  ( map (x ,_) ys ++ (map (y ,_) ys ++ cart-product xs ys)
      ≡⟨ assoc-++ (map (x ,_) ys) (map (y ,_) ys) (cart-product xs ys) ⟩
    (map (x ,_) ys ++ map (y ,_) ys) ++ cart-product xs ys
      ≡⟨ cong (_++ cart-product xs ys) (comm-++ (map (x ,_) ys) (map (y ,_) ys)) ⟩
    (map (y ,_) ys ++ map (x ,_) ys) ++ cart-product xs ys
      ≡⟨ sym (assoc-++ (map (y ,_) ys) (map (x ,_) ys) (cart-product xs ys)) ⟩
    map (y ,_) ys ++ (map (x ,_) ys ++ cart-product xs ys)
      ∎
  ) i
cart-product (trunc xs xs′ p q i j) ys =
  trunc
    (cart-product xs ys) (cart-product xs′ ys)
    (λ k → cart-product (p k) ys) (λ k → cart-product (q k) ys)
    i j

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Sigma

open import Cubical.Foundations.SIP
open import Cubical.Foundations.Pointed
open import Cubical.Structures.Axioms
open import Cubical.Structures.Pointed

private
  variable
    ℓ ℓ' ℓ'' : Level

TypeEqvTo : (ℓ : Level) (X : Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
TypeEqvTo ℓ X = TypeWithStr ℓ (λ Y → ∥ Y ≃ X ∥)

PointedEqvTo : (ℓ : Level) (X : Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
PointedEqvTo ℓ X = TypeWithStr ℓ (λ Y → Y × ∥ Y ≃ X ∥)

module _ (X : Type ℓ') where

  PointedEqvToStructure : Type ℓ → Type (ℓ-max ℓ ℓ')
  PointedEqvToStructure = AxiomsStructure PointedStructure (λ Y _ → ∥ Y ≃ X ∥)

  PointedEqvToEquivStr : StrEquiv PointedEqvToStructure ℓ''
  PointedEqvToEquivStr = AxiomsEquivStr PointedEquivStr (λ Y _ → ∥ Y ≃ X ∥)

  pointedEqvToUnivalentStr : UnivalentStr {ℓ} PointedEqvToStructure PointedEqvToEquivStr
  pointedEqvToUnivalentStr = axiomsUnivalentStr PointedEquivStr {axioms = λ Y _ → ∥ Y ≃ X ∥}
                                          (λ _ _ → squash) pointedUnivalentStr

  PointedEqvToSIP : (A B : PointedEqvTo ℓ X) → A ≃[ PointedEqvToEquivStr ] B ≃ (A ≡ B)
  PointedEqvToSIP = SIP pointedEqvToUnivalentStr

  PointedEqvTo-sip : (A B : PointedEqvTo ℓ X) → A ≃[ PointedEqvToEquivStr ] B → (A ≡ B)
  PointedEqvTo-sip A B = equivFun (PointedEqvToSIP A B)


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

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Maybe

module Numbers.Naturals.Subtraction where

_-N'_ : (a b : ℕ) → Maybe ℕ
zero -N' zero = yes 0
zero -N' succ b = no
succ a -N' zero = yes (succ a)
succ a -N' succ b = a -N' b

subtractZero : (a : ℕ) → a -N' 0 ≡ yes a
subtractZero zero = refl
subtractZero (succ a) = refl


text:
open import Common.Equality
open import Common.Prelude

NaN : Float
NaN = primFloatDiv 0.0 0.0

NaN≢-NaN : primFloatEquality NaN (primFloatNegate NaN) ≡ false
NaN≢-NaN = refl


text:
module Prelude.Strings where

import Data.String.Literals
import Data.List.Literals
open import Data.Unit
open import Agda.Builtin.FromString public

instance
  isStringStringPublic = Data.String.Literals.isString
  isStringListPublic = Data.List.Literals.isString

  unitInstance = tt

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module B where

import C


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

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

open Category C

open import Level

open import Categories.Square

import Categories.Object.Product
open Categories.Object.Product C
  hiding (repack; repack≡id; repack∘; repack-cancel; up-to-iso; transport-by-iso)

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

import Categories.Morphisms as Morphisms

record Exponential (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    B^A : Obj
    product : Product B^A A

  module product = Product product

  B^A×A : Obj
  B^A×A = product.A×B

  field
    eval : B^A×A ⇒ B
    λg : {X : Obj} → (X×A : Product X A) → (Product.A×B X×A ⇒ B) → (X ⇒ B^A)

    .β
        : {X : Obj} → (X×A : Product X A)
        → {g : Product.A×B X×A ⇒ B}
        → (eval ∘ [ X×A ⇒ product ]first (λg X×A g) ≡ g)
    .λ-unique
        : {X : Obj} → (X×A : Product X A)
        → {g : Product.A×B X×A ⇒ B}
        → {h : X ⇒ B^A}
        → (eval ∘ [ X×A ⇒ product ]first h ≡ g)
        → (h ≡ λg X×A g)

  .η
      : ∀ {X : Obj} (X×A : Product X A)
      {f : X ⇒ B^A }
      → λg X×A (eval ∘ [ X×A ⇒ product ]first f) ≡ f
  η X×A {f} = sym (λ-unique X×A refl)
    where open Equiv

  .λ-cong
      : {X : Obj}(X×A : Product X A)
      → ∀{f g}
      → (f ≡ g)
      → (λg X×A f ≡ λg X×A g)
  λ-cong X×A {f}{g} f≡g = λ-unique X×A (trans (β X×A) f≡g)
    where
      open Equiv

  .subst : ∀ {C D}
    → (p₂ : Product C A)
    → (p₃ : Product D A)
    → {f : Product.A×B p₃ ⇒ B}{g : C ⇒ D}
    → λg p₃ f ∘ g
    ≡ λg p₂ (f ∘ [ p₂ ⇒ p₃ ]first g)
  subst {C}{D} p₂ p₃ {f}{g} = λ-unique p₂ subst-commutes
    where
    open HomReasoning
    open Equiv
    subst-commutes =
      let p₁ = product in
      begin
          eval ∘ [ p₂ ⇒ p₁ ]first (λg p₃ f ∘ g)
        ↑⟨ refl ⟩∘⟨ [ p₂ ⇒ p₃ ⇒ p₁ ]first∘first ⟩
          eval
            ∘ [ p₃ ⇒ p₁ ]first (λg p₃ f)
            ∘ [ p₂ ⇒ p₃ ]first g
        ↑⟨ assoc ⟩
          (eval ∘ [ p₃ ⇒ p₁ ]first (λg p₃ f))
                   ∘ [ p₂ ⇒ p₃ ]first g
        ↓⟨ β p₃ ⟩∘⟨ refl ⟩
          f ∘ [ p₂ ⇒ p₃ ]first g
      ∎

  .η-id : λg product eval ≡ id
  η-id =
    begin
      λg product eval
    ↑⟨ identityʳ ⟩
      λg product eval ∘ id
    ↓⟨ subst _ _ ⟩
      λg product (eval ∘ [ product ⇒ product ]first id)
    ↓⟨ η product ⟩
      id
    ∎
    where
    open Equiv
    open HomReasoning

open Morphisms C

-- some aliases to make proof signatures less ugly
[_]eval : ∀{A B}(e₁ : Exponential A B) → Exponential.B^A×A e₁ ⇒ B
[ e₁ ]eval = Exponential.eval e₁

[_]λ : ∀{A B}(e₁ : Exponential A B)
  → {X : Obj} → (X×A : Product X A) → (Product.A×B X×A ⇒ B) → (X ⇒ Exponential.B^A e₁)
[ e₁ ]λ = Exponential.λg e₁

.λ-distrib : ∀ {A B C D}
  → (e₁ : Exponential C B)
  → (e₂ : Exponential A B)
  → (p₃ : Product D C)
  → (p₄ : Product D A)
  → (p₅ : Product (Exponential.B^A e₂) C)
  → {f : C ⇒ A}{g : Product.A×B p₄ ⇒ B}
  → [ e₁ ]λ p₃ (g ∘ [ p₃ ⇒ p₄ ]second f)
    ≡ [ e₁ ]λ p₅ ([ e₂ ]eval ∘ [ p₅ ⇒ Exponential.product e₂ ]second f)
    ∘ [ e₂ ]λ p₄ g
λ-distrib {A}{B}{C}{D} e₁ e₂ p₃ p₄ p₅ {f}{g} =
  begin
    [ e₁ ]λ p₃ (g ∘ [ p₃ ⇒ p₄ ]second f)
  ↑⟨ e₁.λ-cong p₃ eval∘second∘first ⟩
    [ e₁ ]λ p₃ (([ e₂ ]eval ∘ [ p₅ ⇒ Exponential.product e₂ ]second f) ∘ [ p₃ ⇒ p₅ ]first ([ e₂ ]λ p₄ g))
  ↑⟨ e₁.subst p₃ p₅ ⟩
      [ e₁ ]λ p₅ ([ e₂ ]eval ∘ [ p₅ ⇒ Exponential.product e₂ ]second f)
    ∘ [ e₂ ]λ p₄ g
  ∎

  where
  open HomReasoning
  open Equiv
  module e₁ = Exponential e₁
  module e₂ = Exponential e₂

  eval∘second∘first =
    let p₁ = e₁.product in
    let p₂ = e₂.product in
    begin
      ([ e₂ ]eval ∘ [ p₅ ⇒ Exponential.product e₂ ]second f) ∘ [ p₃ ⇒ p₅ ]first ([ e₂ ]λ p₄ g)
    ↓⟨ assoc ⟩
      [ e₂ ]eval
          ∘ [ p₅ ⇒ p₂ ]second f
          ∘ [ p₃ ⇒ p₅ ]first ([ e₂ ]λ p₄ g)
    ↑⟨ refl ⟩∘⟨ [ p₄ ⇒ p₂ , p₃ ⇒ p₅ ]first↔second ⟩
      [ e₂ ]eval
          ∘ [ p₄ ⇒ p₂ ]first ([ e₂ ]λ p₄ g)
          ∘ [ p₃ ⇒ p₄ ]second f
    ↑⟨ assoc ⟩
      ([ e₂ ]eval ∘ [ p₄ ⇒ p₂ ]first ([ e₂ ]λ p₄ g))
                  ∘ [ p₃ ⇒ p₄ ]second f
    ↓⟨ e₂.β p₄ ⟩∘⟨ refl ⟩
      g ∘ [ p₃ ⇒ p₄ ]second f
    ∎

repack : ∀{A B} (e₁ e₂ : Exponential A B) → Exponential.B^A e₁ ⇒ Exponential.B^A e₂
repack e₁ e₂ = e₂.λg e₁.product e₁.eval
  where
    module e₁ = Exponential e₁
    module e₂ = Exponential e₂

.repack≡id : ∀{A B} (e : Exponential A B) → repack e e ≡ id
repack≡id e = Exponential.η-id e

.repack∘ : ∀{A B} (e₁ e₂ e₃ : Exponential A B) → repack e₂ e₃ ∘ repack e₁ e₂ ≡ repack e₁ e₃
repack∘ {A} {B} e₁ e₂ e₃ =
  let p₁ = product e₁ in
  let p₂ = product e₂ in
  begin
      [ e₃ ]λ p₂ [ e₂ ]eval
    ∘ [ e₂ ]λ p₁ [ e₁ ]eval
  ↓⟨ λ-cong e₃ p₂ (introʳ (second-id p₂)) ⟩∘⟨ refl ⟩
      [ e₃ ]λ p₂ ([ e₂ ]eval ∘ [ p₂ ⇒ p₂ ]second id)
    ∘ [ e₂ ]λ p₁ [ e₁ ]eval
  ↑⟨ λ-distrib e₃ e₂ p₁ p₁ p₂ ⟩
    [ e₃ ]λ p₁ ([ e₁ ]eval ∘ [ p₁ ⇒ p₁ ]second id)
  ↑⟨ λ-cong e₃ p₁ (introʳ (second-id p₁)) ⟩
    [ e₃ ]λ p₁ [ e₁ ]eval
  ∎
  where
    open Equiv
    open Exponential
    open HomReasoning
    open GlueSquares C

.repack-cancel : ∀{A B} (e₁ e₂ : Exponential A B) → repack e₁ e₂ ∘ repack e₂ e₁ ≡ id
repack-cancel e₁ e₂ = Equiv.trans (repack∘ e₂ e₁ e₂) (repack≡id e₂)

up-to-iso : ∀{A B} (e₁ e₂ : Exponential A B) → Exponential.B^A e₁ ≅ Exponential.B^A e₂
up-to-iso e₁ e₂ = record
  { f = repack e₁ e₂
  ; g = repack e₂ e₁
  ; iso = record
    { isoˡ = repack-cancel e₂ e₁
    ; isoʳ = repack-cancel e₁ e₂
    }
  }

transport-by-iso : ∀{A B} (e : Exponential A B) → ∀ {X} → Exponential.B^A e ≅ X → Exponential A B
transport-by-iso e {X} e≅X = record
  { B^A = X
  ; product = X×A
  ; eval = e.eval
  ; λg = λ Y×A y → f ∘ e.λg Y×A y
  ; β = λ Y×A → let open HomReasoning in let open GlueSquares C in let open Equiv in begin
      e.eval ∘ [ Y×A ⇒ X×A ]first (f ∘ e.λg Y×A _)
    ↓⟨ ∘-resp-≡ʳ (e.product.⟨⟩-cong₂ (pullˡ (cancelLeft isoˡ)) (pullˡ identityˡ)) ⟩
      e.eval ∘ [ Y×A ⇒ e.product ]first (e.λg Y×A _)
    ↓⟨ (e.β Y×A) ⟩
      _
    ∎
  ; λ-unique = λ Y×A y → let open GlueSquares C in
    switch-gfˡ e≅X
     (e.λ-unique Y×A
      (Equiv.trans
       (∘-resp-≡ʳ
        (e.product.⟨⟩-cong₂
         assoc
         (Equiv.sym (pullˡ identityˡ))))
      y)) -- look ma i can write lisp in agda  --xplat
  }
  where
  module e = Exponential e
  X×A = Mobile e.product e≅X idⁱ
  open _≅_ e≅X


text:
{-# OPTIONS --no-sized-types #-}

open import Common.Size renaming (↑_ to _^)

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {size ^}
  suc  : {size : Size} -> Nat {size} -> Nat {size ^}

weak : {i : Size} -> Nat {i} -> Nat {∞}
weak x = x

-- Should give error without sized types.

-- .i != ∞ of type Size
-- when checking that the expression x has type Nat


text:
module datatypes-safe where

open import bool public
open import integer public
open import list public
open import level public
open import maybe public
open import nat public
open import nat-division public
open import product public
open import sum public
open import tree public
open import trie public
open import unit public
open import vector public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --without-K #-}
module hott.topology.spaces.s1 where

open import hott.core

-- The universe where we work.
𝒰 = Type₀

module Definition where
  private data SInternal : 𝒰 where
               pointInternal : SInternal
  S₁ : 𝒰
  S₁ = SInternal

  point : S₁
  point = pointInternal

  postulate loop : point ≡ point

  -- the induction principle for s₁
  ind-S₁ : {ℓ : Level}{B : S₁ → Type ℓ}
         → (b : B point)
         → (b ≡ b)
         → (x : S₁) → B x
  ind-S₁ b x pointInternal = b

open Definition

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

open import LogicalFormulae
open import Setoids.Setoids
open import Setoids.Lists
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals
open import Sets.FinSet
open import Groups.GroupDefinition
open import Lists.Lists
open import Orders
open import Groups.Groups

module Groups.GeneratedGroup where
  data FreeCompletion {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
    ofLetter : A → FreeCompletion S
    ofInv : A → FreeCompletion S

  freeCompletionMap : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → FreeCompletion S → FreeCompletion T
  freeCompletionMap f (ofLetter x) = ofLetter (f x)
  freeCompletionMap f (ofInv x) = ofInv (f x)

  freeInverse : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (l : FreeCompletion S) → FreeCompletion S
  freeInverse (ofLetter x) = ofInv x
  freeInverse (ofInv x) = ofLetter x

  freeCompletionSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (FreeCompletion S)
  (freeCompletionSetoid S Setoid.∼ ofLetter w) (ofLetter x) = Setoid._∼_ S w x
  (freeCompletionSetoid S Setoid.∼ ofLetter w) (ofInv x) = False'
  (freeCompletionSetoid S Setoid.∼ ofInv w) (ofLetter x) = False'
  (freeCompletionSetoid S Setoid.∼ ofInv w) (ofInv x) = Setoid._∼_ S w x
  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter x} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv x} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofInv x} ()
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofLetter x} ()
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} {ofLetter y} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} {ofInv y} _ ()
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofInv x} {y} ()
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofLetter x} {y} ()
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} {ofLetter y} _ ()
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} {ofInv y} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))

  freeCompletionMapWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → ({x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)) → {x y : FreeCompletion S} → (Setoid._∼_ (freeCompletionSetoid S) x y) → (Setoid._∼_ (freeCompletionSetoid T) (freeCompletionMap f x) (freeCompletionMap f y))
  freeCompletionMapWellDefined f fWD {ofLetter x} {ofLetter x₁} w1=w2 = fWD w1=w2
  freeCompletionMapWellDefined f fWD {ofLetter x} {ofInv x₁} ()
  freeCompletionMapWellDefined f fWD {ofInv x} {ofLetter x₁} ()
  freeCompletionMapWellDefined f fWD {ofInv x} {ofInv x₁} w1=w2 = fWD w1=w2

  record Word {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
    field
      word : List (FreeCompletion S)

  wordSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (Word S)
  (wordSetoid S Setoid.∼ record { word = word1 }) record { word = word2 } = Setoid._∼_ (listSetoid (freeCompletionSetoid S)) word1 word2
  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (wordSetoid S))) {record { word = word }} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (listSetoid (freeCompletionSetoid S))))
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (wordSetoid S))) {record { word = word1 }} {record { word = word2 }} pr = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (listSetoid (freeCompletionSetoid S)))) pr
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (wordSetoid S))) {record { word = word1 }} {record { word = word2 }} {record { word = word3 }} pr1 pr2 = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (listSetoid (freeCompletionSetoid S)))) pr1 pr2

  evalWord : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) (w : Word S) → A
  evalWord G record { word = [] } = Group.identity G
  evalWord {_+_ = _+_} G record { word = (ofLetter x :: w) } = x + evalWord G record { word = w }
  evalWord {_+_ = _+_} G record { word = (ofInv x :: w) } = (Group.inverse G x) + evalWord G record { word = w }

  mapWord : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) (w : Word S) → Word T
  mapWord f record { word = word } = record { word = map (freeCompletionMap f) word }

  subgroupSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Setoid (Word T)
  Setoid._∼_ (subgroupSetoid {S = S} T G {f} fInj) w1 w2 = Setoid._∼_ S (evalWord G (mapWord f w1)) (evalWord G (mapWord f w2))
  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))

  evalWordWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) (w1 w2 : Word S) → Setoid._∼_ (wordSetoid S) w1 w2 → Setoid._∼_ S (evalWord G w1) (evalWord G w2)
  evalWordWellDefined {S = S} G record { word = [] } record { word = [] } w1=w2 = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  evalWordWellDefined G record { word = [] } record { word = (x :: word) } ()
  evalWordWellDefined {_+_ = _+_} G record { word = (x :: xs) } record { word = [] } ()
  evalWordWellDefined {_+_ = _+_} G record { word = (ofLetter x :: xs) } record { word = (ofLetter y :: ys) } (x=y ,, snd) = Group.wellDefined G x=y (evalWordWellDefined G record { word = xs } record { word = ys } snd)
  evalWordWellDefined {_+_ = _+_} G record { word = (ofLetter x :: xs) } record { word = (ofInv y :: ys) } (() ,, snd)
  evalWordWellDefined {_+_ = _+_} G record { word = (ofInv x :: xs) } record { word = (ofLetter y :: ys) } (() ,, snd)
  evalWordWellDefined {_+_ = _+_} G record { word = (ofInv x :: xs) } record { word = (ofInv y :: ys) } (x=y ,, snd) = Group.wellDefined G (inverseWellDefined G x=y) (evalWordWellDefined G record { word = xs } record { word = ys } snd)

  mapWordWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → ({x y : A} → (Setoid._∼_ S x y) → (Setoid._∼_ T (f x) (f y))) → {w1 : Word S} {w2 : Word S} → Setoid._∼_ (wordSetoid S) w1 w2 → Setoid._∼_ (wordSetoid T) (mapWord f w1) (mapWord f w2)
  mapWordWellDefined {S = S} {T = T} f fWD {w1} {w2} w1=w2 = p
    where
      p : listEquality (freeCompletionSetoid T) (map (freeCompletionMap {S = S} {T = T} f) (Word.word w1)) (map (freeCompletionMap f) (Word.word w2))
      p = listEqualityRespectsMap (freeCompletionSetoid S) (freeCompletionSetoid T) (freeCompletionMap {S = S} {T} f) (λ {x} {y} → freeCompletionMapWellDefined {S = S} {T = T} f fWD {x} {y}) {w1 = Word.word w1} {w2 = Word.word w2} w1=w2

  subgroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Word T → Word T → Word T
  subgroupOp T G fInj record { word = word1 } record { word = word2 } = record { word = word1 ++ word2 }

  generatedSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Group (subgroupSetoid T G fInj) (subgroupOp T G fInj)
  Group.wellDefined (generatedSubgroup {S = S} T G {f = f} fInj) {record { word = w }} {record { word = x }} {record { word = y }} {record { word = z }} w=y x=z = need
    where
      need : Setoid._∼_ (subgroupSetoid T G fInj) (subgroupOp T G fInj (record { word = w }) (record { word = x })) (subgroupOp T G fInj (record { word = y }) (record { word = z }))
      need = {!!}
  Group.identity (generatedSubgroup T G fInj) = record { word = [] }
  Group.inverse (generatedSubgroup T G fInj) record { word = word } = record { word = map freeInverse (rev word) }
  Group.multAssoc (generatedSubgroup T G fInj) = {!!}
  Group.multIdentRight (generatedSubgroup {S = S} T G {f = f} fInj) {a = record { word = word }} = need
    where
      open Setoid S
      open Group G
      need : evalWord G (mapWord f (record { word = word ++ [] })) ∼ evalWord G (mapWord f record { word = word })
      need = {!!}
  Group.multIdentLeft (generatedSubgroup {S = S} T G {f = f} fInj) = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  Group.invLeft (generatedSubgroup {S = S} T G {f} fInj) {record { word = [] }} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
  Group.invLeft (generatedSubgroup {S = S} T G {f} fInj) {record { word = x :: word }} = need
    where
      open Setoid S
      open Group G
      need : Setoid._∼_ (subgroupSetoid T G fInj) (record { word = (map freeInverse (rev (x :: word))) ++ (x :: word) }) (Group.identity (generatedSubgroup T G fInj))
      need = {!!}
  Group.invRight (generatedSubgroup T G fInj) = {!!}


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

data ⊥ : Set where

[_] : {A : Set} → A → List A
[ x ] = x ∷ []

vArg : {A : Set} → A → Arg A
vArg x = arg (arg-info visible relevant) x

macro
  getFunDef : Name → Term → TC ⊤
  getFunDef f hole = do
    function cls ← getDefinition f
      where _ → error
    niceCls ← quoteTC cls
    unify hole niceCls

    where postulate error : _

noooo : (A : Set) → ⊥ → A
noooo A ()

-- Quoting the term `noooo Nat x` used to produce an absurd lambda
-- applied to `x`, which should not happen. It should instead simply
-- keep the term `noooo Nat x` as-is.
fooooo : ⊥ → Nat
fooooo x = noooo Nat x

test : getFunDef fooooo ≡
         [
           clause [ "x" , vArg (def (quote ⊥) []) ] [ vArg (var 0) ]
                  (def (quote noooo) (vArg (def (quote Nat) []) ∷ vArg (var 0 []) ∷ []))
         ]
test = refl

max_forks_repo_name: shlevy/agda


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

open import Agda.Primitive

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
  idr : ∀ {i} {A : Set i} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

postulate
  _==_ : ∀ {i} {A : Set i} → A → A → Set i
  idp : ∀ {i} {A : Set i} {a : A} → a == a

postulate
  HetEq : ∀ {i} {A B : Set i} (e : A == B) (a : A) (b : B) → Set i
  HetEq↦ : ∀ {i} {A : Set i} (a b : A) → HetEq idp a b ↦ (a == b)
  {-# REWRITE HetEq↦ #-}

HetEq↦2 : ∀ {i j} {A : Set i} {B : Set j} (u v : A → B) → HetEq idp u v ↦ (u == v)
HetEq↦2 u v = idr

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module RedBlack where

open import Data.Nat

-- | The colour of a node.
data Color : Set where
  red   : Color
  black : Color

-- | The red black tree
data Tree  (A : Set) : ℕ       -- black height
                     → Color   -- color of the root
                     → Set
     where

  -- Empty node is always black
  empty :  Tree A 0 black

  -- Both the children of the red node are black.
  red   :  {d : ℕ}
        → Tree A d black  -- left child
        → A               -- element on the node
        → Tree A d black  -- right child
        → Tree A d red    -- The black height does not change

  -- The children can be of either color
  black : {d : ℕ} {cL cR : Color}
        → Tree A d       cL    -- left child
        → A                    -- element
        → Tree A d       cR    -- right child
        → Tree A (d + 1) black -- black height goes up by one.

-- Converts a tree with red root to a black tree. The type encodes the
-- fact that the height of the tree goes up by 1.
blacken : {A : Set} {d : ℕ}
        → Tree A d       red
        → Tree A (d + 1) black
blacken (red lt x rt) = black lt x rt

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Agda.Primitive

infixr 2 _×_

_×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
A × B = Σ A λ _ → B

∃-notation exists-notation :
  ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-notation      = Σ _
exists-notation = Σ _

Σ-notation : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-notation = Σ

infixr 2 ∃-notation exists-notation Σ-notation

syntax ∃-notation (λ x → B)      = ∃ x × B
syntax exists-notation (λ x → B) = exists x × B
syntax Σ-notation A (λ x → B)    = [ x ∶ A ] × B

_ : ∃ b × b ≡ true × Bool
_ = true , refl , false

_ : exists b × b ≡ true
_ = true , refl

_ : [ b ∶ Bool ] × b ≡ true
_ = true , refl

_ : [ b₁ ∶ Bool ] × [ b₂ ∶ Bool ] × b₁ ≡ b₂
_ = true , true , refl

_ : [ b₁ ∶ Bool ] × ∃ b₂ × b₁ ≡ b₂
_ = true , true , refl

_ : [ f ∶ (Bool → Bool) ] × f ≡ λ x → x
_ = (λ x → x) , refl

data List (A : Set) : Set where
  []   : List A
  cons : A → List A → List A

infixr 5 cons

syntax []        = [ ]
syntax cons x xs = x consed to xs

_ : List Bool
_ = true consed to false consed to [ ]

f : List Bool → Bool
f [ ]                               = true
f (true consed to [ ])              = false
f (false consed to x consed to [ ]) = x
f _                                 = true

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

funny : true ≡ false → true ≡ false
funny x = x

{-# REWRITE funny #-}


text:
module A.M where

import A.B.M


text:
{-# OPTIONS --type-in-type #-}
module dyn where
open import prelude
open import functors
open import poly0 public
open import prelude.Stream
open Stream
open import Data.List as L using (List)

record Dyn : Set where
  constructor dyn
  field
    {state} : Set
    {body}  : ∫
    pheno   : ∫[ (state , λ _ → state) , body ]
open Dyn public

run : (d : Dyn) → ∫[ body d , 𝒴 ] → state d → Stream (π₁ (body d))
hd (run d@(dyn l) e s₀) = s₀ ★ l
tl (run d@(dyn l) e s₀) = run d e (s₀ # l ← hd (run d e s₀) # e ← tt)

module _ (d₁ d₂ : Dyn) where
    _⊠⊠⊠_ : Dyn
    _⊠⊠⊠_ = dyn (pheno d₁ ⟦⊠⟧ pheno d₂)

_⟫_ : (d : Dyn) → ∫[ body d , A ] → Dyn
d ⟫ l = dyn (pheno d ▸ l)

fun→dyn : ∀ {a b} → (a → b) → Dyn
fun→dyn f = dyn (λ a⁺ → a⁺ , f)

delay : Set → Dyn
delay s = fun→dyn (id {A = s})

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text: module Categories.Coequalizer where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Mockingbird.Forest using (Forest)

module Mockingbird.Forest.Combination.Properties {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_×_; _,_)
open import Relation.Binary using (_Respects_)
open import Relation.Unary using (Pred; _∈_; _⊆_; ∅; _∩_)
open import Level using (Level; _⊔_)

open Forest forest

open import Mockingbird.Forest.Combination.Base forest

private
  variable
    x y z : Bird
    p : Level
    P Q : Pred Bird p

subst : P Respects _≈_ → x ≈ y → x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩
subst respects x≈y [ x∈P ] = [ respects x≈y x∈P ]
subst respects x≈y (x₁∈⟨P⟩ ⟨∙⟩ x₂∈⟨P⟩ ∣ x₁x₂≈x) = x₁∈⟨P⟩ ⟨∙⟩ x₂∈⟨P⟩ ∣ trans x₁x₂≈x x≈y

subst′ : P Respects _≈_ → y ≈ x → x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩
subst′ respects y≈x = subst respects (sym y≈x)

-- TODO: maybe lift ∅ to an arbitrary level p
⟨∅⟩ : ⟨ ∅ ⟩ ⊆ ∅
⟨∅⟩ (X ⟨∙⟩ Y ∣ xy≈z) = ⟨∅⟩ X

⟨_⟩⊆⟨_⟩ : ∀ {p} (P Q : Pred Bird p) → P ⊆ Q → ⟨ P ⟩ ⊆ ⟨ Q ⟩
⟨ P ⟩⊆⟨ Q ⟩ P⊆Q [ x∈P ] = [ P⊆Q x∈P ]
⟨ P ⟩⊆⟨ Q ⟩ P⊆Q (x∈⟨P⟩ ⟨∙⟩ y∈⟨P⟩ ∣ xy≈z) = ⟨ P ⟩⊆⟨ Q ⟩ P⊆Q x∈⟨P⟩ ⟨∙⟩ ⟨ P ⟩⊆⟨ Q ⟩ P⊆Q y∈⟨P⟩ ∣ xy≈z

weaken : ∀ {p} {P Q : Pred Bird p} → P ⊆ Q → ⟨ P ⟩ ⊆ ⟨ Q ⟩
weaken {P = P} {Q} = ⟨ P ⟩⊆⟨ Q ⟩

⟨_∩_⟩ : ∀ {p} (P Q : Pred Bird p) → ⟨ (P ∩ Q) ⟩ ⊆ ⟨ P ⟩ ∩ ⟨ Q ⟩
⟨ P ∩ Q ⟩ [ (x∈P , x∈Q) ] = ([ x∈P ] , [ x∈Q ])
⟨ P ∩ Q ⟩ (_⟨∙⟩_∣_ {x} {y} {z} x∈⟨P∩Q⟩ y∈⟨P∩Q⟩ xy≈z) =
  let (x∈⟨P⟩ , x∈⟨Q⟩) = ⟨_∩_⟩ P Q x∈⟨P∩Q⟩
      (y∈⟨P⟩ , y∈⟨Q⟩) = ⟨_∩_⟩ P Q y∈⟨P∩Q⟩
  in (x∈⟨P⟩ ⟨∙⟩ y∈⟨P⟩ ∣ xy≈z , x∈⟨Q⟩ ⟨∙⟩ y∈⟨Q⟩ ∣ xy≈z)

-- NOTE: the inclusion ⟨P⟩ ∩ ⟨Q⟩ ⊆ ⟨P ∩ Q⟩ does not hold for all P and Q; let
-- for example P = {S, K}, Q = {I}, then SKK = I ∈ ⟨P⟩ ∩ ⟨Q⟩, but P ∩ Q = ∅, and
-- hence SKK = I ∉ ⟨P ∩ Q⟩.
-- TODO: formalise

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


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

open import HoTT
open import homotopy.RibbonCover
import homotopy.CoverClassification

module experimental.CoverClassificationCat {i} (A∙ : Ptd i)
  (A-conn : is-connected 0 (fst A∙)) where

  open Cover
  open Gset
  open homotopy.CoverClassification A∙ A-conn

  private
    A : Type i
    A = fst A∙
    a₁ : A
    a₁ = snd A∙
    π1A = fundamental-group A∙

  -- A covering space constructed from a G-set.
  cover-hom-to-gset-hom : ∀ {j}
    → {cov₁ cov₂ : Cover A j}
    → CoverHom cov₁ cov₂
    → GsetHom (cover-to-gset cov₁) (cover-to-gset cov₂)
  cover-hom-to-gset-hom {cov₁ = cov₁}{cov₂} f = record
    { f = f a₁
    ; pres-act = λ l x → lemma₂ x l
    }
    where
      lemma₁ : ∀ x {a₂} (p : a₁ == a₂)
        → f a₂ (transport (Fiber cov₁) p x)
        == transport (Fiber cov₂) p (f a₁ x)
      lemma₁ _ idp = idp

      lemma₂ : ∀ x {a₂} (p : a₁ =₀ a₂)
        → f a₂ (transport₀ (Fiber cov₁) (Fiber-level cov₁ a₂) p x)
        == transport₀ (Fiber cov₂) (Fiber-level cov₂ a₂) p (f a₁ x)
      lemma₂ x {a₂} = Trunc-elim
        (λ p → =-preserves-level 0 (Fiber-level cov₂ a₂))
        (lemma₁ x {a₂})

  gset-hom-to-cover-hom : ∀ {j}
    → {gset₁ gset₂ : Gset π1A j}
    → GsetHom gset₁ gset₂
    → CoverHom (gset-to-cover gset₁) (gset-to-cover gset₂)
  gset-hom-to-cover-hom {gset₁ = gset₁}{gset₂} (gset-hom f pres-act) a₂ =
    Ribbon-rec
      {P = Ribbon A∙ gset₂ a₂}
      Ribbon-level
      (λ el p → trace (f el) p)
      (λ el loop p →
        trace (f (act gset₁ el loop)) p
          =⟨ pres-act loop el |in-ctx (λ x → trace x p) ⟩
        trace (act gset₂ (f el) loop) p
          =⟨ paste (f el) loop p ⟩
        trace (f el) (loop ∙₀ p)
          ∎)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Nat
open import Prelude
open import contexts
open import dynamics-core
open import type-assignment-unicity

module canonical-indeterminate-forms where

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at num type
  data cif-num : (Δ : hctx) (d : ihexp) → Set where
    CIFNPlus1 : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
        ((d == d1 ·+ d2) ×
         (Δ , ∅ ⊢ d1 :: num) ×
         (Δ , ∅ ⊢ d2 :: num) ×
         (d1 indet) ×
         (d2 final)
        )
        → cif-num Δ d
    CIFNPlus2 : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
        ((d == d1 ·+ d2) ×
         (Δ , ∅ ⊢ d1 :: num) ×
         (Δ , ∅ ⊢ d2 :: num) ×
         (d1 final) ×
         (d2 indet)
        )
        → cif-num Δ d
    CIFNAp : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2 ==> num) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-num Δ d
    CIFNCase : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ x ∈ Nat ] Σ[ d2 ∈ ihexp ] Σ[ y ∈ Nat ] Σ[ d3 ∈ ihexp ]
      Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == case d1 x d2 y d3) ×
         (Δ , ∅ ⊢ d1 :: τ1 ⊕ τ2) ×
         (Δ , ■ (x , τ1) ⊢ d2 :: num) ×
         (Δ , ■ (y , τ2) ⊢ d3 :: num) ×
         (d1 indet) ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inl τ d') ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inr τ d') ×
         ((τ3 τ4 τ3' τ4' : htyp) (d' : ihexp) →
           d1 ≠ (d' ⟨(τ3 ⊕ τ4) ⇒ (τ3' ⊕ τ4')⟩))
        )
        → cif-num Δ d
    CIFNFst : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: num ⊠ τ') ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-num Δ d
    CIFNSnd : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊠ num) ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-num Δ d
    CIFNEHole : ∀{Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: num [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-num Δ d
    CIFNNEHole : ∀{Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: num [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-num Δ d
    CIFNCast : ∀{Δ d} →
      Σ[ d' ∈ ihexp ]
        ((d == d' ⟨ ⦇-⦈ ⇒ num ⟩) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-num Δ d
    CIFNFailedCast : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == d' ⟨ τ' ⇒⦇-⦈⇏ num ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ num)
        )
        → cif-num Δ d

  canonical-indeterminate-forms-num : ∀{Δ d} →
                                      Δ , ∅ ⊢ d :: num →
                                      d indet →
                                      cif-num Δ d
  canonical-indeterminate-forms-num TANum ()
  canonical-indeterminate-forms-num (TAPlus wt wt₁) (IPlus1 x x₁) = CIFNPlus1 (_ , _ , refl , wt , wt₁ , x , x₁)
  canonical-indeterminate-forms-num (TAPlus wt wt₁) (IPlus2 x x₁) = CIFNPlus2 (_ , _  , refl , wt , wt₁ , x , x₁)
  canonical-indeterminate-forms-num (TAVar x₁) ()
  canonical-indeterminate-forms-num (TAAp wt wt₁) (IAp x ind x₁) = CIFNAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-num {Δ = Δ} (TACase {τ1 = τ1} {τ2 = τ2} {x = x} {d1 = d1} {y = y} {d2 = d2} wt _ wt₁ _ wt₂) (ICase ninl ninr ncast ind) = CIFNCase (_ , _ , _ , _ , _ , _ , _ , refl , wt , tr (λ Γ' → Δ , Γ' ⊢ d1 :: num) (extend-empty x τ1) wt₁ , tr (λ Γ' → Δ , Γ' ⊢ d2 :: num) (extend-empty y τ2) wt₂ , ind , ninl , ninr , ncast)
  canonical-indeterminate-forms-num (TAFst wt) (IFst x x₁ ind) = CIFNFst (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-num (TASnd wt) (ISnd x x₁ ind) = CIFNSnd (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-num (TAEHole x x₁) IEHole = CIFNEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-num (TANEHole x wt x₁) (INEHole x₂) = CIFNNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-num (TACast wt x) (ICastHoleGround x₁ ind x₂) = CIFNCast (_ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-num (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = CIFNFailedCast (_ , _ , refl , x , x₅ , x₇)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at arrow type
  data cif-arr : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CIFAEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-arr Δ d τ1 τ2
    CIFANEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-arr Δ d τ1 τ2
    CIFAAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ==> τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFACase : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ x ∈ Nat ] Σ[ d2 ∈ ihexp ] Σ[ y ∈ Nat ] Σ[ d3 ∈ ihexp ]
      Σ[ τ3 ∈ htyp ] Σ[ τ4 ∈ htyp ]
        ((d == case d1 x d2 y d3) ×
         (Δ , ∅ ⊢ d1 :: τ3 ⊕ τ4) ×
         (Δ , ■ (x , τ3) ⊢ d2 :: τ1 ==> τ2) ×
         (Δ , ■ (y , τ4) ⊢ d3 :: τ1 ==> τ2) ×
         (d1 indet) ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inl τ d') ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inr τ d') ×
         ((τ5 τ6 τ5' τ6' : htyp) (d' : ihexp) →
           d1 ≠ (d' ⟨(τ5 ⊕ τ6) ⇒ (τ5' ⊕ τ6')⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFAFst : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: (τ1 ==> τ2) ⊠ τ') ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFASnd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊠ (τ1 ==> τ2)) ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFACast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == d' ⟨ (τ1' ==> τ2') ⇒ (τ1 ==> τ2) ⟩) ×
         (Δ , ∅ ⊢ d' :: τ1' ==> τ2') ×
         (d' indet) ×
         ((τ1' ==> τ2') ≠ (τ1 ==> τ2))
        )
       → cif-arr Δ d τ1 τ2
    CIFACastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (d' ⟨ ⦇-⦈ ⇒ ⦇-⦈ ==> ⦇-⦈ ⟩)) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFAFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == (d' ⟨ τ' ⇒⦇-⦈⇏ ⦇-⦈ ==> ⦇-⦈ ⟩) ) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ (⦇-⦈ ==> ⦇-⦈))
        )
        → cif-arr Δ d τ1 τ2

  canonical-indeterminate-forms-arr : ∀{Δ d τ1 τ2 } →
                                      Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                                      d indet →
                                      cif-arr Δ d τ1 τ2
  canonical-indeterminate-forms-arr (TAVar x₁) ()
  canonical-indeterminate-forms-arr (TALam _ wt) ()
  canonical-indeterminate-forms-arr (TAAp wt wt₁) (IAp x ind x₁) = CIFAAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-arr {Δ = Δ} (TACase {τ1 = τ1} {τ2 = τ2} {τ = τ3 ==> τ4} {x = x} {d1 = d1} {y = y} {d2 = d2} wt _ wt₁ _ wt₂) (ICase ninl ninr ncast ind) = CIFACase (_ , _ , _ , _ , _ , _ , _ , refl , wt , tr (λ Γ' → Δ , Γ' ⊢ d1 :: τ3 ==> τ4) (extend-empty x τ1) wt₁ , tr (λ Γ' → Δ , Γ' ⊢ d2 :: τ3 ==> τ4) (extend-empty y τ2) wt₂ , ind , ninl , ninr , ncast)
  canonical-indeterminate-forms-arr (TAFst wt) (IFst x x₁ ind) = CIFAFst (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-arr (TASnd wt) (ISnd x x₁ ind) = CIFASnd (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-arr (TAEHole x x₁) IEHole = CIFAEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-arr (TANEHole x wt x₁) (INEHole x₂) = CIFANEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-arr (TACast wt x) (ICastArr x₁ ind) = CIFACast (_ , _ , _ , _ , _ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TACast wt TCHole2) (ICastHoleGround x₁ ind GArrHole) = CIFACastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TAFailedCast x x₁ GArrHole x₃) (IFailedCast x₄ x₅ GArrHole x₇) = CIFAFailedCast (_ , _ , refl , refl , refl , x , x₅ , x₇)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at sum type
  data cif-sum : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CIFSEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ⊕ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-sum Δ d τ1 τ2
    CIFSNEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ⊕ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-sum Δ d τ1 τ2
    CIFSAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ⊕ τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-sum Δ d τ1 τ2
    CIFSInl : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == inl τ2 d') ×
         (Δ , ∅ ⊢ d' :: τ1) ×
         (d' indet)
        )
        → cif-sum Δ d τ1 τ2
    CIFSInr : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == inr τ1 d') ×
         (Δ , ∅ ⊢ d' :: τ2) ×
         (d' indet)
        )
        → cif-sum Δ d τ1 τ2
    CIFSCase : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ x ∈ Nat ] Σ[ d2 ∈ ihexp ] Σ[ y ∈ Nat ] Σ[ d3 ∈ ihexp ]
      Σ[ τ3 ∈ htyp ] Σ[ τ4 ∈ htyp ]
        ((d == case d1 x d2 y d3) ×
         (Δ , ∅ ⊢ d1 :: τ3 ⊕ τ4) ×
         (Δ , ■ (x , τ3) ⊢ d2 :: τ1 ⊕ τ2) ×
         (Δ , ■ (y , τ4) ⊢ d3 :: τ1 ⊕ τ2) ×
         (d1 indet) ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inl τ d') ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inr τ d') ×
         ((τ5 τ6 τ5' τ6' : htyp) (d' : ihexp) →
           d1 ≠ (d' ⟨(τ5 ⊕ τ6) ⇒ (τ5' ⊕ τ6')⟩))
        )
        → cif-sum Δ d τ1 τ2
    CIFSFst : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: (τ1 ⊕ τ2) ⊠ τ') ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-sum Δ d τ1 τ2
    CIFSSnd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊠ (τ1 ⊕ τ2)) ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-sum Δ d τ1 τ2
    CIFSCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == d' ⟨ (τ1' ⊕ τ2') ⇒ (τ1 ⊕ τ2) ⟩) ×
         (Δ , ∅ ⊢ d' :: τ1' ⊕ τ2') ×
         (d' indet) ×
         ((τ1' ⊕ τ2') ≠ (τ1 ⊕ τ2))
        )
       → cif-sum Δ d τ1 τ2
    CIFSCastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (d' ⟨ ⦇-⦈ ⇒ ⦇-⦈ ⊕ ⦇-⦈ ⟩)) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-sum Δ d τ1 τ2
    CIFSFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == (d' ⟨ τ' ⇒⦇-⦈⇏ ⦇-⦈ ⊕ ⦇-⦈ ⟩) ) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ (⦇-⦈ ⊕ ⦇-⦈))
        )
        → cif-sum Δ d τ1 τ2

  canonical-indeterminate-forms-sum : ∀{Δ d τ1 τ2 } →
                                      Δ , ∅ ⊢ d :: (τ1 ⊕ τ2) →
                                      d indet →
                                      cif-sum Δ d τ1 τ2
  canonical-indeterminate-forms-sum (TAAp wt wt₁) (IAp x ind x₁) = CIFSAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-sum (TAInl wt) (IInl ind) = CIFSInl (_ , refl , wt , ind)
  canonical-indeterminate-forms-sum (TAInr wt) (IInr ind) = CIFSInr (_ , refl , wt , ind)
  canonical-indeterminate-forms-sum {Δ = Δ} (TACase {τ1 = τ1} {τ2 = τ2} {τ = τ3 ⊕ τ4} {x = x} {d1 = d1} {y = y} {d2 = d2} wt _ wt₁ _ wt₂) (ICase ninl ninr ncast ind) = CIFSCase (_ , _ , _ , _ , _ , _ , _ , refl , wt , tr (λ Γ' → Δ , Γ' ⊢ d1 :: (τ3 ⊕ τ4)) (extend-empty x τ1) wt₁ , tr (λ Γ' → Δ , Γ' ⊢ d2 :: (τ3 ⊕ τ4)) (extend-empty y τ2) wt₂ , ind , ninl , ninr , ncast)
  canonical-indeterminate-forms-sum (TAFst wt) (IFst x x₁ ind) = CIFSFst (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-sum (TASnd wt) (ISnd x x₁ ind) = CIFSSnd (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-sum (TAEHole x x₁) IEHole = CIFSEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-sum (TANEHole x wt x₁) (INEHole x₂) = CIFSNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-sum (TACast wt x) (ICastSum x₁ ind) = CIFSCast (_ , _ , _ , _ , _ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-sum (TACast wt x) (ICastHoleGround x₁ ind GSumHole) = CIFSCastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-sum (TAFailedCast wt x x₁ x₂) (IFailedCast x₃ x₄ GSumHole x₆) = CIFSFailedCast (_ , _ , refl , refl , refl , wt , x₄ , x₆)
  canonical-indeterminate-forms-sum (TAVar x) ()

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at product type
  data cif-prod : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CIFPEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ⊠ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-prod Δ d τ1 τ2
    CIFPNEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ⊠ τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-prod Δ d τ1 τ2
    CIFPAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ⊠ τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPCase : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ x ∈ Nat ] Σ[ d2 ∈ ihexp ] Σ[ y ∈ Nat ] Σ[ d3 ∈ ihexp ]
      Σ[ τ3 ∈ htyp ] Σ[ τ4 ∈ htyp ]
        ((d == case d1 x d2 y d3) ×
         (Δ , ∅ ⊢ d1 :: τ3 ⊕ τ4) ×
         (Δ , ■ (x , τ3) ⊢ d2 :: τ1 ⊠ τ2) ×
         (Δ , ■ (y , τ4) ⊢ d3 :: τ1 ⊠ τ2) ×
         (d1 indet) ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inl τ d') ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inr τ d') ×
         ((τ5 τ6 τ5' τ6' : htyp) (d' : ihexp) →
           d1 ≠ (d' ⟨(τ5 ⊕ τ6) ⇒ (τ5' ⊕ τ6')⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPPair1 : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
        ((d == ⟨ d1 , d2 ⟩) ×
         (Δ , ∅ ⊢ d1 :: τ1) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         d1 indet ×
         d2 final
        )
        → cif-prod Δ d τ1 τ2
    CIFPPair2 : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
        ((d == ⟨ d1 , d2 ⟩) ×
         (Δ , ∅ ⊢ d1 :: τ1) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         d1 final ×
         d2 indet
        )
        → cif-prod Δ d τ1 τ2
    CIFPFst : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: (τ1 ⊠ τ2) ⊠ τ') ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPSnd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊠ (τ1 ⊠ τ2)) ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == d' ⟨ (τ1' ⊠ τ2') ⇒ (τ1 ⊠ τ2) ⟩) ×
         (Δ , ∅ ⊢ d' :: τ1' ⊠ τ2') ×
         (d' indet) ×
         ((τ1' ⊠ τ2') ≠ (τ1 ⊠ τ2))
        )
       → cif-prod Δ d τ1 τ2
    CIFPCastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (d' ⟨ ⦇-⦈ ⇒ ⦇-⦈ ⊠ ⦇-⦈ ⟩)) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-prod Δ d τ1 τ2
    CIFPFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == (d' ⟨ τ' ⇒⦇-⦈⇏ ⦇-⦈ ⊠ ⦇-⦈ ⟩) ) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ (⦇-⦈ ⊠ ⦇-⦈))
        )
        → cif-prod Δ d τ1 τ2

  canonical-indeterminate-forms-prod : ∀{Δ d τ1 τ2} →
                                       Δ , ∅ ⊢ d :: (τ1 ⊠ τ2) →
                                       d indet →
                                       cif-prod Δ d τ1 τ2
  canonical-indeterminate-forms-prod (TAVar x) ()
  canonical-indeterminate-forms-prod (TAAp wt wt₁) (IAp x ind x₁) = CIFPAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-prod {Δ = Δ} (TACase {τ1 = τ1} {τ2 = τ2} {τ = τ3 ⊠ τ4} {x = x} {d1 = d1} {y = y} {d2 = d2} wt _ wt₁ _ wt₂) (ICase ninl ninr ncast ind) = CIFPCase (_ , _ , _ , _ , _ , _ , _ , refl , wt , tr (λ Γ' → Δ , Γ' ⊢ d1 :: (τ3 ⊠ τ4)) (extend-empty x τ1) wt₁ , tr (λ Γ' → Δ , Γ' ⊢ d2 :: (τ3 ⊠ τ4)) (extend-empty y τ2) wt₂ , ind , ninl , ninr , ncast)
  canonical-indeterminate-forms-prod (TAPair wt wt₁) (IPair1 ind x) = CIFPPair1 (_ , _ , refl , wt , wt₁ , ind , x)
  canonical-indeterminate-forms-prod (TAPair wt wt₁) (IPair2 x ind) = CIFPPair2 (_ , _ , refl , wt , wt₁ , x , ind)
  canonical-indeterminate-forms-prod (TAFst wt) (IFst x x₁ ind) = CIFPFst (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-prod (TASnd wt) (ISnd x x₁ ind) = CIFPSnd (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-prod (TAEHole x x₁) IEHole = CIFPEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-prod (TANEHole x wt x₁) (INEHole x₂) = CIFPNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-prod (TACast wt x) (ICastProd x₁ ind) = CIFPCast (_ , _ , _ , _ , _ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-prod (TACast wt x) (ICastHoleGround x₁ ind GProdHole) = CIFPCastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-prod (TAFailedCast wt x GProdHole x₂) (IFailedCast x₃ x₄ GProdHole x₆) = CIFPFailedCast (_ , _ , refl , refl , refl , wt , x₄ , x₆)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at hole type
  data cif-hole : (Δ : hctx) (d : ihexp) → Set where
    CIFHEHole : ∀{Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: ⦇-⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHNEHole : ∀{Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: ⦇-⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHAp : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: (τ2 ==> ⦇-⦈)) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
      → cif-hole Δ d
    CIFHCase : ∀{Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ x ∈ Nat ] Σ[ d2 ∈ ihexp ] Σ[ y ∈ Nat ] Σ[ d3 ∈ ihexp ]
      Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == case d1 x d2 y d3) ×
         (Δ , ∅ ⊢ d1 :: τ1 ⊕ τ2) ×
         (Δ , ■ (x , τ1) ⊢ d2 :: ⦇-⦈) ×
         (Δ , ■ (y , τ2) ⊢ d3 :: ⦇-⦈) ×
         (d1 indet) ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inl τ d') ×
         ((τ : htyp) (d' : ihexp) → d1 ≠ inr τ d') ×
         ((τ3 τ4 τ3' τ4' : htyp) (d' : ihexp) →
           d1 ≠ (d' ⟨(τ3 ⊕ τ4) ⇒ (τ3' ⊕ τ4')⟩))
        )
        → cif-hole Δ d
    CIFHFst : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == fst d') ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈ ⊠ τ') ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-hole Δ d
    CIFHSnd : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == snd d') ×
         (Δ , ∅ ⊢ d' :: τ' ⊠ ⦇-⦈) ×
         (d' indet) ×
         ((d1 d2 : ihexp) → d' ≠ ⟨ d1 , d2 ⟩) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d'' : ihexp) →
           d' ≠ (d'' ⟨(τ3 ⊠ τ4) ⇒ (τ3' ⊠ τ4')⟩))
        )
        → cif-hole Δ d
    CIFHCast : ∀{Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == d' ⟨ τ' ⇒ ⦇-⦈ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (d' indet)
        )
      → cif-hole Δ d

  canonical-indeterminate-forms-hole : ∀{Δ d} →
                                       Δ , ∅ ⊢ d :: ⦇-⦈ →
                                       d indet →
                                       cif-hole Δ d
  canonical-indeterminate-forms-hole (TAVar x₁) ()
  canonical-indeterminate-forms-hole (TAAp wt wt₁) (IAp x ind x₁) = CIFHAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-hole {Δ = Δ} (TACase {τ1 = τ1} {τ2 = τ2} {x = x} {d1 = d1} {y = y} {d2 = d2} wt _ wt₁ _ wt₂) (ICase ninl ninr ncast ind) = CIFHCase (_ , _ , _ , _ , _ , _ , _ , refl , wt , tr (λ Γ' → Δ , Γ' ⊢ d1 :: ⦇-⦈) (extend-empty x τ1) wt₁ , tr (λ Γ' → Δ , Γ' ⊢ d2 :: ⦇-⦈) (extend-empty y τ2) wt₂ , ind , ninl , ninr , ncast)
  canonical-indeterminate-forms-hole (TAFst wt) (IFst x x₁ ind) = CIFHFst (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-hole (TASnd wt) (ISnd x x₁ ind) = CIFHSnd (_ , _ , refl , wt , ind , x , x₁)
  canonical-indeterminate-forms-hole (TAEHole x x₁) IEHole = CIFHEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-hole (TANEHole x wt x₁) (INEHole x₂) = CIFHNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastGroundHole x₁ ind) = CIFHCast (_ , _ , refl , wt , x₁ , ind)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastHoleGround x₁ ind ())
  canonical-indeterminate-forms-hole (TAFailedCast x x₁ () x₃) (IFailedCast x₄ x₅ x₆ x₇)

  canonical-indeterminate-forms-coverage : ∀{Δ d τ} →
                                           Δ , ∅ ⊢ d :: τ →
                                           d indet →
                                           τ ≠ num →
                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊕ τ2)) →
                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊠ τ2)) →
                                           τ ≠ ⦇-⦈ →
                                           ⊥
  canonical-indeterminate-forms-coverage {τ = num} wt ind nn na ns np nh = nn refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} wt ind nn na ns np nh = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} wt ind nn na ns np nh = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊕ τ₁} wt ind nn na ns np nh = ns τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = τ ⊠ τ₁} wt ind nn na ns np nh = np τ τ₁ refl

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
------------------------------------------------------------------------------
-- Testing the FOL schemata
------------------------------------------------------------------------------

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

module FOT.FOL.SchemataATP where

open import FOL.Base

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

postulate id₁ : {A₁ : D → Set} → ∀ {x} → A₁ x → A₁ x
{-# ATP prove id₁ #-}

id₂ : {A₁ : D → Set} → ∀ {x} → A₁ x → A₁ x
id₂ {A} {x} = prf
  where
    postulate prf : A x → A x
    {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Unit where

record Unit : Set where
  constructor unit

{-# COMPILE GHC Unit = data () (()) #-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui