text:
module Generic.Function.Elim where

open import Generic.Core

AllAny : ∀ {ι α β γ δ} {I : Set ι} {A : Set α} {C : I -> Set γ}
       -> (B : I -> A -> Set β)
       -> (∀ x -> (∀ {j} -> B j x -> C j) -> Set δ)
       -> (xs : List A)
       -> (∀ {j} -> Any (B j) xs -> C j)
       -> Set δ
AllAny B D  []          k = ⊤
AllAny B D (x ∷ [])     k = D x k
AllAny B D (x ∷ y ∷ xs) k = D x (k ∘ inj₁) × AllAny B D (y ∷ xs) (k ∘ inj₂)

data VarView {ι β} {I : Set ι} : Desc I β -> Set where
  yes-var : ∀ {i} -> VarView (var i)
  no-var  : ∀ {D} -> VarView  D

varView : ∀ {ι β} {I : Set ι} -> (D : Desc I β) -> VarView D
varView (var i) = yes-var
varView  D      = no-var

mutual
  Hyp : ∀ {ι β γ} {I : Set ι} {B}
      -> (∀ {i} -> B i -> Set γ) -> (D : Desc I β) -> ⟦ D ⟧ B -> Set (β ⊔ γ)
  Hyp {β = β} C (var i)    y      = Lift β (C y)
  Hyp         C (π i q D)  f      = Hypᵇ i C D f
  Hyp         C (D ⊛ E)   (x , y) = Hyp C D x × Hyp C E y

  Hypᵇ : ∀ {ι α β γ δ q q′} {I : Set ι} {B} i
       -> (∀ {i} -> B i -> Set γ) -> (D : Binder α β δ i q′ I) -> ⟦ i / D ⟧ᵇ q B -> Set (β ⊔ γ)
  Hypᵇ {γ = γ} {q = q} i C (coerce (A , D)) f =
    Coerce′ (cong (γ ⊔_) q) $ Pi i A λ x -> Hyp C (D x) (appPi i (uncoerce′ q f) x)

mutual
  Elim : ∀ {ι β γ} {I : Set ι} {B}
       -> (∀ {i} -> B i -> Set γ)
       -> (D : Desc I β)
       -> (∀ {j} -> Extend D B j -> B j)
       -> Set (β ⊔ γ)
  Elim {β = β} C (var i)   k = Lift β (C (k lrefl))
  Elim         C (π i q D) k = Elimᵇ i C D k
  Elim         C (D ⊛ E)   k with varView D
  ... | yes-var = ∀ {x} -> C x -> Elim C E (k ∘ _,_ x)
  ... | no-var  = ∀ {x} -> Hyp C D x -> Elim C E (k ∘ _,_ x)

  Elimᵇ : ∀ {ι α β γ δ q q′} {I : Set ι} {B} i
        -> (∀ {i} -> B i -> Set γ)
        -> (D : Binder α β δ i q′ I)
        -> (∀ {j} -> Extendᵇ i D q B j -> B j)
        -> Set (β ⊔ γ)
  Elimᵇ {γ = γ} {q = q} i C (coerce (A , D)) k =
    Coerce′ (cong (γ ⊔_) q) $ Pi i A λ x -> Elim C (D x) (k ∘ coerce′ q ∘ _,_ x)

module _ {ι β γ} {I : Set ι} {D₀ : Data (Desc I β)} (C : ∀ {j} -> μ D₀ j -> Set γ) where
  K : Name -> Type -> Type -> (Ds : List (Desc I β)) -> All (const Name) Ds -> Set (ι ⊔ β)
  K d a b Ds ns = ∀ {j} -> Node D₀ (packData d a b Ds ns) j -> μ D₀ j

  Elims : ∀ d a b (Ds : List (Desc I β)) ns -> K d a b Ds ns -> Set (β ⊔ γ)
  Elims d a b Ds ns = AllAny (λ j D -> Extend D (μ D₀) j) (Elim C) Ds

  module _ (hs : Elims (dataName  D₀)
                       (parsTele  D₀)
                       (indsTele  D₀)
                       (consTypes D₀)
                       (consNames D₀)
                        node) where
    {-# TERMINATING #-}
    mutual
      elimHyp : (D : Desc I β) -> (d : ⟦ D ⟧ (μ D₀)) -> Hyp C D d
      elimHyp (var i)    d      = lift (elim d)
      elimHyp (π i q D)  f      = elimHypᵇ i D f
      elimHyp (D ⊛ E)   (x , y) = elimHyp D x , elimHyp E y

      elimHypᵇ : ∀ {α δ q q′} i
               -> (D : Binder α β δ i q′ I)
               -> (f : ⟦ i / D ⟧ᵇ q (μ D₀))
               -> Hypᵇ i C D f
      elimHypᵇ {q = q} i (coerce (A , D)) f =
        coerce′ (cong (_⊔_ γ) q) (lamPi i λ x -> elimHyp (D x) (appPi i (uncoerce′ q f) x))

      elimExtend : ∀ {j}
                 -> (D : Desc I β) {k : ∀ {j} -> Extend D (μ D₀) j -> μ D₀ j}
                 -> Elim C D k
                 -> (e : Extend D (μ D₀) j)
                 -> C (k e)
      elimExtend (var i)   z  lrefl  = lower z
      elimExtend (π i q D) h  p      = elimExtendᵇ i D h p
      elimExtend (D ⊛ E)   h (d , e) with varView D
      ... | yes-var = elimExtend E (h (elim d))  e
      ... | no-var  = elimExtend E (h (elimHyp D d)) e

      elimExtendᵇ : ∀ {α δ q q′ j} i
                  -> (D : Binder α β δ i q′ I) {k : ∀ {j} -> Extendᵇ i D q (μ D₀) j -> μ D₀ j}
                  -> Elimᵇ i C D k
                  -> (p : Extendᵇ i D q (μ D₀) j)
                  -> C (k p)
      elimExtendᵇ {q = q} i (coerce (A , D)) h p with p | inspectUncoerce′ q p
      ... | _ | (x , e) , refl = elimExtend (D x) (appPi i (uncoerce′ (cong (γ ⊔_) q) h) x) e

      elimAny : ∀ {j} (Ds : List (Desc I β)) d a b ns {k : K d a b Ds ns}
              -> Elims d a b Ds ns k -> (a : Node D₀ (packData d a b Ds ns) j) -> C (k a)
      elimAny  []          d a b  tt       tt       ()
      elimAny (D ∷ [])     d a b (n , ns)  h        e       = elimExtend D h e
      elimAny (D ∷ E ∷ Ds) d a b (n , ns) (h , hs) (inj₁ e) = elimExtend D h e
      elimAny (D ∷ E ∷ Ds) d a b (n , ns) (h , hs) (inj₂ r) = elimAny (E ∷ Ds) d a b ns hs r

      elim : ∀ {j} -> (d : μ D₀ j) -> C d
      elim (node e) = elimAny (consTypes D₀)
                              (dataName  D₀)
                              (parsTele  D₀)
                              (indsTele  D₀)
                              (consNames D₀)
                               hs
                               e

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

open import lib.Base
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.NType

module lib.Equivalences where

{-
We use the half-adjoint definition of equivalences (but this fact should be
invisible to the user of the library). The constructor of the type of
equivalences is [equiv], it takes two maps and the two proofs that the composites
are equal: [equiv to from to-from from-to]

The type of equivalences between two types [A] and [B] can be written either
[A ≃ B] or [Equiv A B].

Given an equivalence [e] : [A ≃ B], you can extract the two maps as follows:
[–> e] : [A → B] and [<– e] : [B → A] (the dash is an en dash)
The proofs that the composites are the identities are [<–-inv-l] and [<–-inv-r].

The identity equivalence on [A] is [ide A], the composition of two equivalences
is [_∘e_] (function composition order) and the inverse of an equivalence is [_⁻¹]
-}

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

  record is-equiv (f : A → B) : Type (lmax i j)
    where
    field
      g : B → A
      f-g : (b : B) → f (g b) == b
      g-f : (a : A) → g (f a) == a
      adj : (a : A) → ap f (g-f a) == f-g (f a)

    abstract
      adj' : (b : B) → ap g (f-g b) == g-f (g b)
      adj' b = anti-whisker-left (ap g (f-g (f (g b)))) $ ! $
        ap g (f-g (f (g b))) ∙ g-f (g b)
          =⟨ ! $ htpy-natural-app=idf f-g b |in-ctx (λ p → ap g p ∙ g-f (g b)) ⟩
        ap g (ap (f ∘ g) (f-g b)) ∙ g-f (g b)
          =⟨ ! $ ap-∘ g (f ∘ g) (f-g b) |in-ctx (λ p → p ∙ g-f (g b)) ⟩
        ap (g ∘ f ∘ g) (f-g b) ∙ g-f (g b)
          =⟨ htpy-natural (g-f ∘ g) (f-g b) ⟩
        g-f (g (f (g b))) ∙ ap g (f-g b)
          =⟨ ! $ htpy-natural-app=idf g-f (g b) |in-ctx (λ p → p ∙ ap g (f-g b)) ⟩
        ap (g ∘ f) (g-f (g b)) ∙ ap g (f-g b)
          =⟨ ap-∘ g f (g-f (g b)) |in-ctx (λ p → p ∙ ap g (f-g b)) ⟩
        ap g (ap f (g-f (g b))) ∙ ap g (f-g b)
          =⟨ adj (g b) |in-ctx (λ p → ap g p ∙ ap g (f-g b)) ⟩
        ap g (f-g (f (g b))) ∙ ap g (f-g b)
          ∎

  {-
  In order to prove that something is an equivalence, you have to give an inverse
  and a proof that it’s an inverse (you don’t need the adj part).
  [is-eq] is a very, very bad name.
  -}
  is-eq : (f : A → B)
    (g : B → A) (f-g : (b : B) → f (g b) == b)
    (g-f : (a : A) → g (f a) == a) → is-equiv f
  is-eq f g f-g g-f =
   record {g = g; f-g = f-g'; g-f = g-f; adj = adj} where
    f-g' : (b : B) → f (g b) == b
    f-g' b = ! (ap (f ∘ g) (f-g b)) ∙ ap f (g-f (g b)) ∙ f-g b

    adj : (a : A) → ap f (g-f a) == f-g' (f a)
    adj a =
      ap f (g-f a)
        =⟨ ! (!-inv-l (ap (f ∘ g) (f-g (f a)))) |in-ctx (λ q → q ∙ ap f (g-f a)) ⟩
      (! (ap (f ∘ g) (f-g (f a))) ∙ ap (f ∘ g) (f-g (f a))) ∙ ap f (g-f a)
        =⟨ ∙-assoc (! (ap (f ∘ g) (f-g (f a)))) (ap (f ∘ g) (f-g (f a))) _ ⟩
      ! (ap (f ∘ g) (f-g (f a))) ∙ ap (f ∘ g) (f-g (f a)) ∙ ap f (g-f a)
        =⟨ lemma |in-ctx (λ q → ! (ap (f ∘ g) (f-g (f a))) ∙ q) ⟩
      ! (ap (f ∘ g) (f-g (f a))) ∙ ap f (g-f (g (f a))) ∙ f-g (f a) ∎
      where
      lemma : ap (f ∘ g) (f-g (f a)) ∙ ap f (g-f a)
           == ap f (g-f (g (f a))) ∙ f-g (f a)
      lemma =
        ap (f ∘ g) (f-g (f a)) ∙ ap f (g-f a)
          =⟨ htpy-natural-app=idf f-g (f a) |in-ctx (λ q → q ∙ ap f (g-f a)) ⟩
        f-g (f (g (f a))) ∙ ap f (g-f a)
          =⟨ ! (ap-idf (ap f (g-f a))) |in-ctx (λ q → f-g (f (g (f a))) ∙ q) ⟩
        f-g (f (g (f a))) ∙ ap (idf B) (ap f (g-f a))
          =⟨ ! (htpy-natural f-g (ap f (g-f a))) ⟩
        ap (f ∘ g) (ap f (g-f a)) ∙ f-g (f a)
          =⟨ ap-∘ f g (ap f (g-f a)) |in-ctx (λ q → q ∙ f-g (f a)) ⟩
        ap f (ap g (ap f (g-f a))) ∙ f-g (f a)
          =⟨ ∘-ap g f (g-f a) ∙ htpy-natural-app=idf g-f a
             |in-ctx (λ q → ap f q ∙ f-g (f a)) ⟩
        ap f (g-f (g (f a))) ∙ f-g (f a) ∎

infix 30 _≃_

_≃_ : ∀ {i j} (A : Type i) (B : Type j) → Type (lmax i j)
A ≃ B = Σ (A → B) is-equiv

Equiv = _≃_

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

  equiv : (f : A → B) (g : B → A) (f-g : (b : B) → f (g b) == b)
          (g-f : (a : A) → g (f a) == a) → A ≃ B
  equiv f g f-g g-f = (f , is-eq f g f-g g-f)

  –> : (e : A ≃ B) → (A → B)
  –> e = fst e

  <– : (e : A ≃ B) → (B → A)
  <– e = is-equiv.g (snd e)

  <–-inv-l : (e : A ≃ B) (a : A)
    → (<– e (–> e a) == a)
  <–-inv-l e a = is-equiv.g-f (snd e) a

  <–-inv-r : (e : A ≃ B) (b : B)
    → (–> e (<– e b) == b)
  <–-inv-r e b = is-equiv.f-g (snd e) b

  <–-inv-adj : (e : A ≃ B) (a : A)
    → ap (–> e) (<–-inv-l e a) == <–-inv-r e (–> e a)
  <–-inv-adj e a = is-equiv.adj (snd e) a

  <–-inv-adj' : (e : A ≃ B) (b : B)
    → ap (<– e) (<–-inv-r e b) == <–-inv-l e (<– e b)
  <–-inv-adj' e b = is-equiv.adj' (snd e) b

  -- Equivalences are "injective"
  equiv-inj : (e : A ≃ B) {x y : A}
    → (–> e x == –> e y → x == y)
  equiv-inj e {x} {y} p = ! (<–-inv-l e x) ∙ ap (<– e) p ∙ <–-inv-l e y

idf-is-equiv : ∀ {i} (A : Type i) → is-equiv (idf A)
idf-is-equiv A = is-eq _ (idf A) (λ _ → idp) (λ _ → idp)

ide : ∀ {i} (A : Type i) → A ≃ A
ide A = equiv (idf A) (idf A) (λ _ → idp) (λ _ → idp)

infixr 80 _∘e_
infixr 80 _∘ise_

_∘e_ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  → B ≃ C → A ≃ B → A ≃ C
e1 ∘e e2 = ((–> e1 ∘ –> e2) , record {g = (<– e2 ∘ <– e1);
  f-g = (λ c → ap (–> e1) (<–-inv-r e2 (<– e1 c)) ∙ <–-inv-r e1 c);
  g-f = (λ a → ap (<– e2) (<–-inv-l e1 (–> e2 a)) ∙ <–-inv-l e2 a);
  adj = λ a →
      ap (–> e1 ∘ –> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a)) ∙ <–-inv-l e2 a)
          =⟨ ap-∘ (–> e1) (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a)) ∙ <–-inv-l e2 a) ⟩
      ap (–> e1) (ap (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a)) ∙ <–-inv-l e2 a))
          =⟨ ap-∙ (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))) (<–-inv-l e2 a)  |in-ctx ap (–> e1) ⟩
      ap (–> e1) (ap (–> e2) (ap (<– e2) (<–-inv-l e1 (–> e2 a))) ∙ ap (–> e2) (<–-inv-l e2 a))
          =⟨ ! (ap-∘ (–> e2) (<– e2) (<–-inv-l e1 (–> e2 a))) ∙2 <–-inv-adj e2 a |in-ctx ap (–> e1) ⟩
      ap (–> e1) (ap (–> e2 ∘ <– e2) (<–-inv-l e1 (–> e2 a)) ∙ <–-inv-r e2 (–> e2 a))
          =⟨ htpy-natural (<–-inv-r e2) (<–-inv-l e1 (–> e2 a))    |in-ctx ap (–> e1) ⟩
      ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a)) ∙ ap (λ z → z) (<–-inv-l e1 (–> e2 a)))
          =⟨ <–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a)) ∙ₗ ap-idf (<–-inv-l e1 (–> e2 a)) |in-ctx ap (–> e1) ⟩
      ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a)) ∙ <–-inv-l e1 (–> e2 a))
          =⟨ ap-∙ (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a))) (<–-inv-l e1 (–> e2 a)) ⟩
      ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a))) ∙ ap (–> e1) (<–-inv-l e1 (–> e2 a))
          =⟨  ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a))) ∙ₗ (<–-inv-adj e1 (–> e2 a)) ⟩
      ap (–> e1) (<–-inv-r e2 (<– e1 ((–> e1 ∘ –> e2) a))) ∙ <–-inv-r e1 ((–> e1 ∘ –> e2) a)
      ∎})

_∘ise_ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {f : A → B} {g : B → C}
  → is-equiv g → is-equiv f → is-equiv (g ∘ f)
i1 ∘ise i2 = snd ((_ , i1) ∘e (_ , i2))

infix 120 _⁻¹
_⁻¹ : ∀ {i j} {A : Type i} {B : Type j} → (A ≃ B) → (B ≃ A)
e ⁻¹ = equiv (<– e) (–> e) (<–-inv-l e) (<–-inv-r e)

{- Equational reasoning for equivalences -}
infix 15 _≃∎
infixr 10 _≃⟨_⟩_

_≃⟨_⟩_ : ∀ {i j k} (A : Type i) {B : Type j} {C : Type k} → A ≃ B → B ≃ C → A ≃ C
A ≃⟨ u ⟩ v = v ∘e u

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

{- lifting is an equivalence -}
lower-equiv : ∀ {i j} {A : Type i} → Lift {j = j} A ≃ A
lower-equiv = equiv lower lift (λ _ → idp) (λ _ → idp)

{- Any contractible type is equivalent to (all liftings of) the unit type -}
module _ {i} {A : Type i} (h : is-contr A) where
  contr-equiv-Unit : A ≃ Unit
  contr-equiv-Unit = equiv (λ _ → unit) (λ _ → fst h) (λ _ → idp) (snd h)

  contr-equiv-LiftUnit : ∀ {j} → A ≃ Lift {j = j} Unit
  contr-equiv-LiftUnit = lower-equiv ⁻¹ ∘e contr-equiv-Unit

{- An equivalence induces an equivalence on the path spaces -}
module _ {i j} {A : Type i} {B : Type j} (e : A ≃ B) where

  private
    abstract
      left-inverse : {x y : A} (p : x == y) → equiv-inj e (ap (–> e) p) == p
      left-inverse idp = !-inv-l (<–-inv-l e _)

      right-inverse : {x y : A} (p : –> e x == –> e y)
        → ap (–> e) (equiv-inj e p) == p
      right-inverse {x} {y} p =
        ap f (! (g-f x) ∙ ap g p ∙ (g-f y))
          =⟨ ap-∙ f (! (g-f x)) (ap g p ∙ (g-f y)) ⟩
        ap f (! (g-f x)) ∙ ap f (ap g p ∙ (g-f y))
          =⟨ ap-∙ f (ap g p) (g-f y) |in-ctx (λ q →  ap f (! (g-f x)) ∙ q) ⟩
        ap f (! (g-f x)) ∙ ap f (ap g p) ∙ ap f (g-f y)
          =⟨ ∘-ap f g p |in-ctx (λ q → ap f (! (g-f x)) ∙ q ∙ ap f (g-f y)) ⟩
        ap f (! (g-f x)) ∙ ap (f ∘ g) p ∙ ap f (g-f y)
          =⟨ adj y |in-ctx (λ q →  ap f (! (g-f x)) ∙ ap (f ∘ g) p ∙ q) ⟩
        ap f (! (g-f x)) ∙ ap (f ∘ g) p ∙ (f-g (f y))
          =⟨ ap-! f (g-f x) |in-ctx (λ q → q ∙ ap (f ∘ g) p ∙ (f-g (f y))) ⟩
        ! (ap f (g-f x)) ∙ ap (f ∘ g) p ∙ (f-g (f y))
          =⟨ adj x |in-ctx (λ q →  ! q ∙ ap (f ∘ g) p ∙ (f-g (f y))) ⟩
        ! (f-g (f x)) ∙ ap (f ∘ g) p ∙ (f-g (f y))
          =⟨ htpy-natural f-g p |in-ctx (λ q →  ! (f-g (f x)) ∙ q) ⟩
        ! (f-g (f x)) ∙ (f-g (f x)) ∙ ap (idf B) p
          =⟨ ! (∙-assoc (! (f-g (f x))) (f-g (f x)) (ap (idf B) p))
             ∙ ap (λ q → q ∙ ap (idf B) p) (!-inv-l (f-g (f x))) ∙ ap-idf p ⟩
        p ∎
        where f : A → B
              f = fst e

              open is-equiv (snd e)

  equiv-ap : (x y : A) → (x == y) ≃ (–> e x == –> e y)
  equiv-ap x y = equiv (ap (–> e)) (equiv-inj e) right-inverse left-inverse

{- Equivalent types have the same truncation level -}
equiv-preserves-level : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
  → (has-level n A → has-level n B)
equiv-preserves-level {n = ⟨-2⟩} e (x , p) =
  (–> e x , (λ y → ap (–> e) (p _) ∙ <–-inv-r e y))
equiv-preserves-level {n = S n} e c = λ x y →
   equiv-preserves-level (equiv-ap (e ⁻¹) x y ⁻¹) (c (<– e x) (<– e y))

{- This is a collection of type equivalences involving basic type formers.
   We exclude Empty since Π₁-Empty requires λ=.
-}
module _ {j} {B : Unit → Type j} where
  Σ₁-Unit : Σ Unit B ≃ B unit
  Σ₁-Unit = equiv (λ {(unit , b) → b}) (λ b → (unit , b)) (λ _ → idp) (λ _ → idp)

  Π₁-Unit : Π Unit B ≃ B unit
  Π₁-Unit = equiv (λ f → f unit) (λ b _ → b) (λ _ → idp) (λ _ → idp)

module _ {i} {A : Type i} where
  Σ₂-Unit : Σ A (λ _ → Unit) ≃ A
  Σ₂-Unit = equiv fst (λ a → (a , unit)) (λ _ → idp) (λ _ → idp)

  Π₂-Unit : Π A (λ _ → Unit) ≃ Unit
  Π₂-Unit = equiv (λ _ → unit) (λ _ _ → unit) (λ _ → idp) (λ _ → idp)

module _ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k} where
  Σ-assoc : Σ (Σ A B) (uncurry C) ≃ Σ A (λ a → Σ (B a) (C a))
  Σ-assoc = equiv (λ {((a , b) , c) → (a , (b , c))})
                  (λ {(a , (b , c)) → ((a , b) , c)}) (λ _ → idp) (λ _ → idp)

  curry-equiv : Π (Σ A B) (uncurry C) ≃ Π A (λ a → Π (B a) (C a))
  curry-equiv = equiv curry uncurry (λ _ → idp) (λ _ → idp)

  {- The type-theoretic axiom of choice -}
  choice : Π A (λ a → Σ (B a) (λ b → C a b)) ≃ Σ (Π A B) (λ g → Π A (λ a → C a (g a)))
  choice = equiv f g (λ _ → idp) (λ _ → idp)
    where f = λ c → ((λ a → fst (c a)) , (λ a → snd (c a)))
          g = λ d → (λ a → (fst d a , snd d a))

{- Homotopy fibers -}
hfiber : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) (y : B) → Type (lmax i j)
hfiber {A = A} f y = Σ A (λ x → f x == y)

ext: agda

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Andreas, fixed #1349 on 2016-06-08

-- {-# OPTIONS -v tc.term.exlam:50 -v scope.extendedLambda:10 #-}

module Issue1349 where

open import Common.Prelude

module Logic {s} (F : Set s) (arF : F → Nat) where

  data Term : Nat → Set s where
    var : ∀ n → Term (suc n)

d : Unit → Nat
d = \ {unit → zero}  -- fails
-- d unit = zero     -- works

module M = Logic Unit d -- (λ{unit -> zero})

test : Logic.Term Unit {!!} (suc zero)
test = M.var zero

-- WAS:
-- Agda2> Ambiguous name: Issue1349._..extendedlambda0
-- (agda2-info-action "*Error*" "An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Reduce/Monad.hs:172" nil)

-- Gives proper error now.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Data.Bool using ( Bool ; true ; false ; _∨_ )
open import Data.List.Primitive using ( #List ; [] ; _∷_ )
open import Data.Maybe using ( Maybe ; just ; nothing )
open import Data.Maybe.Primitive using ( #Maybe ; just ; nothing )
open import Data.String using ( String )
open import Web.URI.Primitive using ( #URI ; #toString ; #fromString ; #abs ; #rel )
open import Web.URI.Scheme using ( Scheme? ; http: )
open import Web.URI.Port using ( Port? ; ε )

module Web.URI where

infixl 5 _/_ _#_ _//_∶_ _//_

-- No authority or query component for now, and no parent path segments.
-- URIRef? isAbs isRef tracks whether a URI is absolute or relative,
-- and whether it is a URI reference (allows a #fragment) or not.

data URIRef? : Bool → Bool → Set where
  root : {isRef : Bool} → (URIRef? false isRef)
  _//_∶_ : {isRef : Bool} → Scheme? → String → Port? → (URIRef? true isRef)
  _/_ : {isAbs isRef : Bool} → (URIRef? isAbs false) → String → (URIRef? isAbs isRef)
  _#_ : {isAbs : Bool} → (URIRef? isAbs false) → String → (URIRef? isAbs true)

RURI     = URIRef? false false
RURIRef  = URIRef? false true
RURIRef? = URIRef? false
AURI     = URIRef? true false
AURIRef  = URIRef? true true
AURIRef? = URIRef? true

URIRef : Bool → Set
URIRef isAbs = URIRef? isAbs true

URI : Bool → Set
URI isAbs = URIRef? isAbs false

_//_ : {isRef : Bool} → Scheme? → String → (URIRef? true isRef)
s // h = s // h ∶ ε

http://_ : {isRef : Bool} → String → (URIRef? true isRef)
http:// h = http: // h

xsd: : String → AURIRef
xsd:(local) = http://"www.w3.org"/"2001"/"XMLSchema"#(local)

rdf: : String → AURIRef
rdf:(local) = http://"www.w3.org"/"1999"/"02"/"22-rdf-syntax-ns"#(local)

rdfs: : String → AURIRef
rdfs:(local) = http://"www.w3.org"/"2000"/"01"/"rdf-schema"#(local)

owl: : String → AURIRef
owl:(local) = http://"www.w3.org"/"2002"/"07"/"owl"#(local)

-- Parsing --

fromURI : {isAbs isRef : Bool} → (URIRef? isAbs false) → (URIRef? isAbs isRef)
fromURI {isAbs} {false} u = u
fromURI root              = root
fromURI (s // h ∶ n)      = s // h ∶ n
fromURI (u / a)           = u / a

from#Path : {isAbs : Bool} → (URIRef? isAbs false) → (#List String) → (URIRef? isAbs false)
from#Path u []       = u
from#Path u (a ∷ as) = from#Path (u / a) as

from#Fragment : {isAbs isRef : Bool} → (URIRef? isAbs false) → (#Maybe String) → (Maybe (URIRef? isAbs isRef))
from#Fragment {isAbs} {true}  u (just f) = just (u # f)
from#Fragment {isAbs} {false} u (just f) = nothing
from#Fragment {isAbs} {isRef} u nothing  = just (fromURI u)

from#URI : {isAbs isRef : Bool} → (#Maybe #URI) → (Maybe (URIRef? isAbs isRef))
from#URI {true}  (just (#abs s h n p f)) = from#Fragment (from#Path (s // h ∶ n) p) f
from#URI {false} (just (#rel       p f)) = from#Fragment (from#Path root p) f
from#URI         _                       = nothing

fromString : {isAbs isRef : Bool} → String → (Maybe (URIRef? isAbs isRef))
fromString s = from#URI (#fromString s)

-- Serializing to#URI'

to#URI : {isAbs isRef : Bool} → (URIRef? isAbs isRef) → (#List String) → (#Maybe String) → #URI
to#URI root         as f? = #rel as f?
to#URI (s // h ∶ n) as f? = #abs s h n as f?
to#URI (u / a)      as f? = to#URI u (a ∷ as) f?
to#URI (u # f)      as f? = to#URI u as (just f)

toString :  {isAbs isRef : Bool} → (URIRef? isAbs isRef) → String
toString u = #toString (to#URI u [] nothing)

-- Composing --

_&_ : {isAbs₁ isAbs₂ isRef : Bool} → (URIRef? isAbs₁ false) → (URIRef? isAbs₂ isRef) → (URIRef? (isAbs₂ ∨ isAbs₁) isRef)
u & root         = fromURI u
u & (s // h ∶ n) = s // h ∶ n
u & (v / a)      = (u & v) / a
u & (v # a)      = (u & v) # a

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri


text:
open import Oscar.Prelude
open import Oscar.Data.Constraint

module Oscar.Class where

record InnerClass {ℓ} {𝔢} {CONSTRAINTS : Ø 𝔢} (constraints : CONSTRAINTS) (_ : Constraint constraints) (SET-METHOD : Ø ℓ) : Ø ℓ where
  constructor ∁
  field
    ⋆ : SET-METHOD

open InnerClass public

module ℭLASS
  {ℓ}
  {𝔢}
  {CONSTRAINTS : Ø 𝔢}
  (constraints : CONSTRAINTS)
  (c : Ø ℓ)
  where
  class = InnerClass constraints ∅ c
  type = c
  method : ⦃ _ : class ⦄ → type
  method ⦃ ⌶ ⦄ = InnerClass.⋆ ⌶

record Rℭlass
  {ℓ 𝔯}
  {𝔢}
  {CONSTRAINTS : Ø 𝔢}
  (constraints : CONSTRAINTS)
  : Ø ↑̂ (ℓ ∙̂ 𝔯)
  where
  constructor ∁
  field
    SET-METHOD : Ø ℓ
    SET-R : SET-METHOD → Ø 𝔯
  record SET-CLASS
    ⦃ _ : Constraint constraints ⦄
    : Ø ℓ ∙̂ 𝔯
    where
    constructor ∁
    field ⋆ : SET-METHOD
          ⦃ ⋆⋆ ⦄ : SET-R ⋆
  open SET-CLASS public
  GET-CLASS : Ø _
  GET-CLASS = SET-CLASS
  GET-METHOD : ⦃ _ : GET-CLASS ⦄ → SET-METHOD
  GET-METHOD ⦃ ⌶ ⦄ = SET-CLASS.⋆ ⌶

open Rℭlass using (⋆; ∁) public


text:
{-# OPTIONS --without-K  #-}
module algebra.group.morphism where

open import level
open import algebra.group.core
open import algebra.monoid.morphism

module _ {i}{j}
         {X : Set i}⦃ sX : IsGroup X ⦄
         {Y : Set j}⦃ sY : IsGroup Y ⦄ where
  open IsGroup ⦃ ... ⦄

  IsGroupMorphism : (X → Y) → Set (i ⊔ j)
  IsGroupMorphism f = IsMonoidMorphism f

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2016-07-21 adapted from MagicWith.agda
-- Testing correct printing of postfix projections.

{-# OPTIONS --postfix-projections #-}

-- {-# OPTIONS -v tc.cc:60 #-}
-- {-# OPTIONS -v tc.conv.elim:50 #-}

open import Common.Product
open import Common.Nat

record True  : Set where
data   False : Set where

IsZero : Nat → Set
IsZero zero    = True
IsZero (suc _) = False

Uncurry : {A : Set}{B : A → Set} → ((x : A) → B x → Set) → Σ A B → Set
Uncurry F p = F (p .proj₁) (p .proj₂)

F : (n : Nat) → IsZero n → Set
F zero _ = True
F (suc _) ()

-- Trying to match only on p .proj₁ doesn't work since we can't abstract
-- p .proj₁ without also abstracting p .proj₂.
f : (p : Σ Nat IsZero) → Uncurry F p
f p with p .proj₁
f p | zero  = _
f p | suc _ = ?


text:
{-# OPTIONS --allow-unsolved-metas --no-termination-check #-}

module TT where

module Prelude where

-- Props ------------------------------------------------------------------

  data True : Set where
    tt : True

  data False : Set where

  postulate
    falseE : (A : Set) -> False -> A

  infix 3 _/\_

  data _/\_ (P Q : Set) : Set where
    andI : P -> Q -> P /\ Q

  -- Zero and One -----------------------------------------------------------

  data Zero : Set where

  data One : Set where
    unit : One

  -- Natural numbers --------------------------------------------------------

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

  _+_ : Nat -> Nat -> Nat
  zero  + m = m
  suc n + m = suc (n + m)

  module NatEq where

    infix 5 _==_

    _==_ : Nat -> Nat -> Set
    zero  == zero = True
    suc n == suc m = n == m
    _     == _     = False

    rewriteEq : (C : Nat -> Set){m n : Nat} -> m == n -> C n -> C m
    rewriteEq C {zero}  {zero}  _  x = x
    rewriteEq C {suc _} {suc _} eq x = rewriteEq (\z -> C (suc z)) eq x
    rewriteEq C {zero}  {suc _} () _
    rewriteEq C {suc _} {zero}  () _

module Chain {A : Set}(_==_ : A -> A -> Set)
             (_trans_ : {x y z : A} -> x == y -> y == z -> x == z)
    where

  infixl 4 _=-=_
  infixl 4 _===_
  infixr 8 _since_

  _=-=_ : (x : A){y : A} -> x == y -> x == y
  x =-= xy = xy

  _===_ : {x y z : A} -> x == y -> y == z -> x == z
  xy === yz = xy trans yz

  _since_ : {x : A}(y : A) -> x == y -> x == y
  y since xy = xy

module Fin where

  open Prelude

  -- Finite sets ------------------------------------------------------------

  data Suc (A : Set) : Set where
    fzero' : Suc A
    fsuc'  : A -> Suc A

  mutual
    data Fin (n : Nat) : Set where
      finI : Fin' n -> Fin n

    Fin' : Nat -> Set
    Fin'  zero   = Zero
    Fin' (suc n) = Suc (Fin n)

  fzero : {n : Nat} -> Fin (suc n)
  fzero = finI fzero'

  fsuc : {n : Nat} -> Fin n -> Fin (suc n)
  fsuc i = finI (fsuc' i)

  finE : {n : Nat} -> Fin n -> Fin' n
  finE (finI i) = i

  module FinEq where

    infix 5 _==_

    _==_ : {n : Nat} -> Fin n -> Fin n -> Set
    _==_ {suc _} (finI  fzero'  ) (finI  fzero'  ) = True
    _==_ {suc _} (finI (fsuc' i)) (finI (fsuc' j)) = i == j
    _==_          _                _               = False

    rewriteEq : {n : Nat}(C : Fin n -> Set){i j : Fin n} -> i == j -> C j -> C i
    rewriteEq {suc _} C {finI  fzero'  } {finI  fzero'  } eq x = x
    rewriteEq {suc _} C {finI (fsuc' i)} {finI (fsuc' j)} eq x = rewriteEq (\z -> C (fsuc z)) eq x
    rewriteEq {suc _} C {finI (fsuc' _)} {finI fzero'   } () _
    rewriteEq {suc _} C {finI fzero'   } {finI (fsuc' _)} () _
    rewriteEq {zero}  C {finI ()}        {_}              _  _

module Vec where

  open Prelude
  open Fin

  infixr 15 _::_

  -- Vectors ----------------------------------------------------------------

  data Nil : Set where
    nil' : Nil

  data Cons (A As : Set) : Set where
    cons' : A -> As -> Cons A As

  mutual
    data Vec (A : Set)(n : Nat) : Set where
      vecI : Vec' A n -> Vec A n

    Vec' : Set -> Nat -> Set
    Vec' A  zero   = Nil
    Vec' A (suc n) = Cons A (Vec A n)

  nil : {A : Set} -> Vec A zero
  nil = vecI nil'

  _::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
  x :: xs = vecI (cons' x xs)

  vecE : {A : Set}{n : Nat} -> Vec A n -> Vec' A n
  vecE (vecI xs) = xs

  vec : {A : Set}(n : Nat) -> A -> Vec A n
  vec  zero   _ = nil
  vec (suc n) x = x :: vec n x

  map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n
  map {zero}  f (vecI nil')         = nil
  map {suc n} f (vecI (cons' x xs)) = f x :: map f xs

  _!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A
  _!_ {zero } _                   (finI ())
  _!_ {suc n} (vecI (cons' x _ )) (finI fzero')    = x
  _!_ {suc n} (vecI (cons' _ xs)) (finI (fsuc' i)) = xs ! i

  tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
  tabulate {zero}  f = nil
  tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x))

module Untyped where

  open Prelude
  open Fin
  open Vec

  Name = Nat

  data Expr (n : Nat) : Set where
    eVar : Fin n -> Expr n
    eApp : Expr n -> Expr n -> Expr n
    eLam : Expr (suc n) -> Expr n
    eSet : Expr n
    eEl  : Expr n
    ePi  : Expr n
    eCon : Name -> Expr n

  module ExprEq where

    infix 5 _==_

    _==_ : {n : Nat} -> Expr n -> Expr n -> Set
    eVar i              == eVar j                = FinEq._==_ i j
    eApp e1 e2          == eApp e3 e4            = e1 == e3 /\ e2 == e4
    eLam e1             == eLam e2               = e1 == e2
    eSet                == eSet                  = True
    eEl                 == eEl                   = True
    ePi                 == ePi                   = True
    eCon f              == eCon g                = NatEq._==_ f g
    _                   == _                     = False

    rewriteEq : {n : Nat}(C : Expr n -> Set){r s : Expr n} -> r == s -> C s -> C r
    rewriteEq C {eVar i    } {eVar j    } eq x = FinEq.rewriteEq (\z -> C (eVar z)) eq x
    rewriteEq C {eLam e1   } {eLam e2   } eq x = rewriteEq (\z -> C (eLam z)) eq x
    rewriteEq C {eSet      } {eSet      } eq x = x
    rewriteEq C {eEl       } {eEl       } eq x = x
    rewriteEq C {ePi       } {ePi       } eq x = x
    rewriteEq C {eCon f    } {eCon g    } eq x = NatEq.rewriteEq (\z -> C (eCon z)) eq x
    rewriteEq C {eApp e1 e2} {eApp e3 e4} (andI eq13 eq24) x =
      rewriteEq (\z -> C (eApp z e2)) eq13 (
        rewriteEq (\z -> C (eApp e3 z)) eq24 x
      )
    rewriteEq C {eVar _} {eLam _  } () _
    rewriteEq C {eVar _} {eSet    } () _
    rewriteEq C {eVar _} {eEl     } () _
    rewriteEq C {eVar _} {eCon _  } () _
    rewriteEq C {eVar _} {ePi     } () _
    rewriteEq C {eVar _} {eApp _ _} () _

    rewriteEq C {eLam _} {eVar _  } () _
    rewriteEq C {eLam _} {eSet    } () _
    rewriteEq C {eLam _} {eEl     } () _
    rewriteEq C {eLam _} {eCon _  } () _
    rewriteEq C {eLam _} {ePi     } () _
    rewriteEq C {eLam _} {eApp _ _} () _

    rewriteEq C {eSet  } {eLam _  } () _
    rewriteEq C {eSet  } {eVar _  } () _
    rewriteEq C {eSet  } {eEl     } () _
    rewriteEq C {eSet  } {eCon _  } () _
    rewriteEq C {eSet  } {ePi     } () _
    rewriteEq C {eSet  } {eApp _ _} () _

    rewriteEq C {eEl   } {eLam _  } () _
    rewriteEq C {eEl   } {eSet    } () _
    rewriteEq C {eEl   } {eVar _  } () _
    rewriteEq C {eEl   } {eCon _  } () _
    rewriteEq C {eEl   } {ePi     } () _
    rewriteEq C {eEl   } {eApp _ _} () _

    rewriteEq C {eCon _} {eLam _  } () _
    rewriteEq C {eCon _} {eSet    } () _
    rewriteEq C {eCon _} {eEl     } () _
    rewriteEq C {eCon _} {eVar _  } () _
    rewriteEq C {eCon _} {ePi     } () _
    rewriteEq C {eCon _} {eApp _ _} () _

    rewriteEq C {ePi   } {eLam _  } () _
    rewriteEq C {ePi   } {eSet    } () _
    rewriteEq C {ePi   } {eEl     } () _
    rewriteEq C {ePi   } {eCon _  } () _
    rewriteEq C {ePi   } {eVar _  } () _
    rewriteEq C {ePi   } {eApp _ _} () _

    rewriteEq C {eApp _ _} {eLam _  } () _
    rewriteEq C {eApp _ _} {eSet    } () _
    rewriteEq C {eApp _ _} {eEl     } () _
    rewriteEq C {eApp _ _} {eCon _  } () _
    rewriteEq C {eApp _ _} {ePi     } () _
    rewriteEq C {eApp _ _} {eVar _  } () _

module Typed where

  open Prelude
  open Fin
  open Vec

  infixl 15 _&_
  infix  13 _!!_
  infix  5  _==_

  -- Contexts ---------------------------------------------------------------
  data CSuc (n : Nat) : Set

  Context' : Nat -> Set
  Context' zero    = Nil
  Context' (suc n) = CSuc n

  data Context (n : Nat) : Set
  data Type {n : Nat}(Γ : Context n) : Set

  data CSuc n where
    ext : (Γ : Context n) -> Type Γ -> Context' (suc n)

  data Context n where
    ctxI : Context' n -> Context n

  -- Types ------------------------------------------------------------------
  _&_ : {n : Nat}(Γ : Context n) -> Type Γ -> Context (suc n)
  data Term {n : Nat}(Γ : Context n)(A : Type Γ) : Set

  data Type {n} Γ where
    SET : Type Γ
    Pi  : (A : Type Γ) -> Type (Γ & A) -> Type Γ
    El  : Term Γ SET -> Type Γ

  Γ & A = ctxI (ext Γ A)

  -- Variables --------------------------------------------------------------
  data VarSuc {n : Nat}(Γ : Context n)(B : Type Γ)(A : Type (Γ & B)) : Set

  Var' : {n : Nat}(Γ : Context n) -> Type Γ -> Set
  Var' {zero}   Γ              A = Zero
  Var' {suc n} (ctxI (ext Γ B)) A = VarSuc Γ B A

  _==_ : {n : Nat}{Γ : Context n} -> Type Γ -> Type Γ -> Set
  data Ren {n m : Nat}(Γ : Context n)(Δ : Context m) : Set

  rename : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ
  upR : {n : Nat}{Γ : Context n}{A : Type Γ} -> Ren Γ (Γ & A)
  data Var {n : Nat}(Γ : Context n)(A : Type Γ) : Set

  data VarSuc {n} Γ B A where
    vzero_ : A == rename upR B -> Var' (Γ & B) A
    vsuc_  : (C : Type Γ) -> A == rename upR C -> Var Γ C -> Var' (Γ & B) A

  data Var {n} Γ A where
    varI : Var' Γ A -> Var Γ A

  -- Terms ------------------------------------------------------------------
  data Sub {n m : Nat}(Γ : Context n)(Δ : Context m) : Set
  subst : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ
  down : {n : Nat}{Γ : Context n}{A : Type Γ} -> Term Γ A -> Sub (Γ & A) Γ

  data Term {n} Γ A where
    var : (x : Var Γ A) -> Term Γ A
    app : {B : Type Γ}{C : Type (Γ & B)} -> Term Γ (Pi B C) -> (t : Term Γ B) ->
          A == subst (down t) C -> Term Γ A
    lam : {B : Type Γ}{C : Type (Γ & B)} -> Term (Γ & B) C -> A == Pi B C -> Term Γ A

  -- Context manipulation ---------------------------------------------------

  ∅ : Context zero
  ∅ = ctxI nil'

  _!!_ : {n : Nat}(Γ : Context n) -> Fin n -> Type Γ
  _!!_ {zero}  _                (finI ())
  _!!_ {suc _} (ctxI (ext Γ A)) (finI fzero')           = rename upR A
  _!!_ {suc _} (ctxI (ext Γ A)) (finI (fsuc' i)) = rename upR (Γ !! i)

  -- Renamings --------------------------------------------------------------
  data ConsRen {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set

  Ren' : {n m : Nat} -> Context n -> Context m -> Set
  Ren' {zero}  {m} (ctxI nil')      Δ = Nil
  Ren' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsRen Γ A Δ

  data ConsRen {n m} Γ A Δ where
    extRen' : (ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren' (Γ & A) Δ

  data Ren {n m} Γ Δ where
    renI : Ren' Γ Δ -> Ren Γ Δ

  -- Performing renamings ---------------------------------------------------
  rename' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Ren Γ Δ -> Type Γ -> Type Δ

  rename ρ SET = SET
  rename ρ A  = rename' ρ A

  liftR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} ->
          (ρ : Ren Γ Δ) -> Ren (Γ & A) (Δ & rename ρ A)
  renameTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ}
               (ρ : Ren Γ Δ) -> Term Γ A -> Term Δ (rename ρ A)

  rename' ρ SET      = SET
  rename' ρ (Pi A B) = Pi (rename ρ A) (rename (liftR ρ) B)
  rename' ρ (El t)   = El (renameTerm ρ t)

  lookupR : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
            (ρ : Ren Γ Δ)(x : Var Γ A) -> Var Δ (rename ρ A)
  cong : {n m : Nat}{Γ : Context n}{Δ : Context m}(f : Type Γ -> Type Δ)
         {A B : Type Γ} -> A == B -> f A == f B
  _trans_ : {n : Nat}{Γ : Context n}{A B C : Type Γ} -> A == B -> B == C -> A == C
  renameSubstCommute :
    {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ}{B : Type (Γ & A)}
    {ρ : Ren Γ Δ}{t : Term Γ A} ->
    rename ρ (subst (down t) B) == subst (down (renameTerm ρ t)) (rename (liftR ρ) B)

  renameTerm ρ (var x)      = var (lookupR ρ x)
  renameTerm {_}{_}{_}{_}{A} ρ (app{_}{C} s t eq) =
      app (renameTerm ρ s) (renameTerm ρ t)
          (cong (rename ρ) eq  trans  renameSubstCommute)
  renameTerm ρ (lam t eq)   = lam (renameTerm (liftR ρ) t) (cong (rename ρ) eq)

  lookupR {zero} _ (varI ())
  lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ}
          (renI (extRen' ρ z)) (varI (vzero_ eq)) = {!!}
  lookupR {suc n} {_} {ctxI (ext Γ B)} {A} {Δ}
          (renI (extRen' ρ z)) (varI (vsuc_ C eq x)) = {!!}

  -- Building renamings -----------------------------------------------------

  extRen : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
           (ρ : Ren Γ Δ) -> Var Δ (rename ρ A) -> Ren (Γ & A) Δ
  extRen ρ x = renI (extRen' ρ x)

  _coR_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Ren Δ Θ -> Ren Γ Δ -> Ren Γ Θ

  liftR {_}{_}{_}{A} ρ = extRen (upR coR ρ) (varI {!!})

  idR : {n : Nat} {Γ : Context n} -> Ren Γ Γ
  idR = {!!}

  _coR_ = {!!}

  upR = {!!}

  -- Substitutions ----------------------------------------------------------
  data ConsSub {n m : Nat}(Γ : Context n)(A : Type Γ)(Δ : Context m) : Set

  Sub' : {n m : Nat} -> Context n -> Context m -> Set
  Sub' {zero}  {m} (ctxI nil')      Δ = Nil
  Sub' {suc n} {m} (ctxI (ext Γ A)) Δ = ConsSub Γ A Δ

  data ConsSub {n m} Γ A Δ  where
    extSub' : (σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub' (Γ & A) Δ

  data Sub {n m} Γ Δ where
    subI : Sub' Γ Δ -> Sub Γ Δ

  -- Performing substitution ------------------------------------------------
  subst' : {n m : Nat}{Γ : Context n}{Δ : Context m} -> Sub Γ Δ -> Type Γ -> Type Δ

  subst σ SET              = SET
  subst σ A        = subst' σ A

  liftS : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m} ->
          (σ : Sub Γ Δ) -> Sub (Γ & A) (Δ & subst σ A)

  substTerm : {n m : Nat}{Γ : Context n}{Δ : Context m}{A : Type Γ} ->
              (σ : Sub Γ Δ) -> Term Γ A -> Term Δ (subst σ A)

  subst' σ (Pi A B) = Pi (subst σ A) (subst (liftS σ) B)
  subst' σ (El t)   = El (substTerm σ t)
  subst' σ SET      = SET

  substTerm σ (var x)             = {!!}
  substTerm σ (app s t eq) = {!!}
  substTerm σ (lam t eq)   = {!!}

  -- Building substitutions -------------------------------------------------

  liftS {_}{_}{_}{A} σ = {!!} -- extSub (upS ∘ σ) (var fzero (substCompose upS σ A))
    -- Works with hidden args to substCompose when inlined in subst
    -- but not here. Weird.

  topS : {n : Nat}{Γ : Context n} -> Sub ∅ Γ
  topS = subI nil'

  extSub : {n m : Nat}{Γ : Context n}{A : Type Γ}{Δ : Context m}
           (σ : Sub Γ Δ) -> Term Δ (subst σ A) -> Sub (Γ & A) Δ
  extSub σ t = subI (extSub' σ t)

  idS : {n : Nat}{Γ : Context n} -> Sub Γ Γ
  idS {zero}  {ctxI nil'}      = topS
  idS {suc _} {ctxI (ext Γ A)} = {!!} -- extSub upS (var fzero refl)

  convert : {n : Nat}{Γ : Context n}{A B : Type Γ} -> A == B -> Term Γ B -> Term Γ A

  _∘_ : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p} -> Sub Δ Θ -> Sub Γ Δ -> Sub Γ Θ

  substCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p}
                 (σ : Sub Δ Θ)(δ : Sub Γ Δ)(A : Type Γ) ->
                 subst (σ ∘ δ) A == subst σ (subst δ A)

  _∘_ {zero} {_}{_} {ctxI nil'}      _  _                 = topS
  _∘_ {suc _}{_}{_} {ctxI (ext Γ A)} σ (subI (extSub' δ t)) =
    extSub (σ ∘ δ) (convert (substCompose σ δ A) (substTerm σ t))

  upS : {n : Nat}{Γ : Context n}{A : Type Γ} -> Sub Γ (Γ & A)
  upS = {!!}

  substId : {n : Nat}{Γ : Context n}{A : Type Γ} -> subst idS A == A

  down t = extSub idS (convert substId t)

  -- Convertibility ---------------------------------------------------------

  A == B = {!!}

  refl : {n : Nat}{Γ : Context n}{A : Type Γ} -> A == A
  refl = {!!}

  cong f eq = {!!}

  ab trans bc = {!!}

  convert eq t = {!!}

  -- Properties -------------------------------------------------------------

  renameId : {n : Nat}{Γ : Context n}{A : Type Γ} -> rename idR A == A
  renameId = {!!}

  renameCompose : {n m p : Nat}{Γ : Context n}{Δ : Context m}{Θ : Context p}
                  (σ : Ren Δ Θ)(δ : Ren Γ Δ)(A : Type Γ) ->
                  rename (σ coR δ) A == rename σ (rename δ A)
  renameCompose σ δ A = {!!}

  substId = {!!}

  substCompose σ δ A = {!!}

  renameSubstCommute = {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.BinaryTree where

import      Lvl
open import Type

private variable ℓ ℓᵢ ℓₗ ℓₙ ℓₒ : Lvl.Level
private variable N N₁ N₂ L T A B : Type{ℓ}

data BinaryTree (L : Type{ℓₗ}) (N : Type{ℓₙ}) : Type{ℓₗ Lvl.⊔ ℓₙ} where
  Leaf : L → BinaryTree L N
  Node : N → BinaryTree L N → BinaryTree L N → BinaryTree L N

elim : (P : BinaryTree L N → Type{ℓ}) → ((l : L) → P(Leaf l)) → (∀{tl tr} → (n : N) → (pl : P(tl)) → (pr : P(tr)) → P(Node n tl tr)) → ((t : BinaryTree L N) → P(t))
elim P pl pn (Leaf l)     = pl l
elim P pl pn (Node n l r) = pn n (elim P pl pn l) (elim P pl pn r)

open import Data using (Unit ; <>)
open import Data.Boolean
open import Data.Option
open import Data.Tuple using (_⨯_ ; _,_)
open import Functional as Fn using (_$_)
open import Numeral.Natural
open import Numeral.Natural.Function
open import Numeral.Natural.Oper hiding (_^_)

emptyTree : BinaryTree{ℓₗ} Unit N
emptyTree = Leaf <>

singleton : N → BinaryTree{ℓₗ} Unit N
singleton a = Node a emptyTree emptyTree

isLeaf : BinaryTree L N → Bool
isLeaf (Leaf _)     = 𝑇
isLeaf (Node _ _ _) = 𝐹

isNode : BinaryTree L N → Bool
isNode (Leaf _)     = 𝐹
isNode (Node _ _ _) = 𝑇

root : BinaryTree L N → Option(N)
root (Leaf _)     = None
root (Node a _ _) = Some a

flip : BinaryTree L N → BinaryTree L N
flip (Leaf l)     = Leaf l
flip (Node n l r) = Node n (flip r) (flip l)

foldPreOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  a ▫ₙ_                                         $
  Fn.swap(foldPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  Fn.swap(foldPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  id

foldInOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldInOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldInOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  Fn.swap(foldInOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  a ▫ₙ_                                        $
  Fn.swap(foldInOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  id

foldPostOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  Fn.swap(foldPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  Fn.swap(foldPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  a ▫ₙ_                                          $
  id

foldReversedPreOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldReversedPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldReversedPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  a ▫ₙ_                                                 $
  Fn.swap(foldReversedPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  Fn.swap(foldReversedPreOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  id

foldReversedInOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldReversedInOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldReversedInOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  Fn.swap(foldReversedInOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  a ▫ₙ_                                                $
  Fn.swap(foldReversedInOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  id

foldReversedPostOrderDepthFirst : (L → T → T) → (N → T → T) → T → BinaryTree L N → T
foldReversedPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Leaf a)     = a ▫ₗ id
foldReversedPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_) id (Node a l r) =
  Fn.swap(foldReversedPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) r $
  Fn.swap(foldReversedPostOrderDepthFirst(_▫ₗ_)(_▫ₙ_)) l $
  a ▫ₙ_                                                  $
  id

-- The size is the number of nodes in the tree.
size : BinaryTree L N → ℕ
size (Leaf _)     = 𝟎
size (Node _ l r) = 𝐒(size(l) + size(r))

-- The number of leaves in the tree.
numberOfLeaves : BinaryTree L N → ℕ
numberOfLeaves (Leaf _)     = 1
numberOfLeaves (Node _ l r) = numberOfLeaves(l) + numberOfLeaves(r)

-- The height is the length of the longest path from the root.
height : BinaryTree L N → ℕ
height (Leaf _)     = 𝟎
height (Node _ l r) = 𝐒(max (height l) (height r))

open import Data.Boolean.Operators
open        Data.Boolean.Operators.Programming

isFull : BinaryTree L N → Bool
isFull (Leaf _)                               = 𝑇
isFull (Node _ (Leaf _)        (Leaf _))      = 𝑇
isFull (Node _ (Node _ _ _)    (Leaf _))      = 𝐹
isFull (Node _ (Leaf _)        (Node _ _ _))  = 𝐹
isFull (Node _ l@(Node _ _ _) r@(Node _ _ _)) = isFull l && isFull r

open import Data.List
import      Data.List.Functions as List

treesOfDepth : ℕ → BinaryTree L N → List(BinaryTree L N)
treesOfDepth 𝟎      tree         = tree ⊰ ∅
treesOfDepth (𝐒(_)) (Leaf _)     = ∅
treesOfDepth (𝐒(n)) (Node _ l r) = (treesOfDepth n l) List.++ (treesOfDepth n r)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

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

open import Cubical.Data.Nat
open import Cubical.Data.Vec.Base

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

nAryLevel : Level → Level → ℕ → Level
nAryLevel ℓ₁ ℓ₂ zero    = ℓ₂
nAryLevel ℓ₁ ℓ₂ (suc n) = ℓ-max ℓ₁ (nAryLevel ℓ₁ ℓ₂ n)

nAryOp : (n : ℕ) → Type ℓ → Type ℓ' → Type (nAryLevel ℓ ℓ' n)
nAryOp zero A B    = B
nAryOp (suc n) A B = A → nAryOp n A B

_$ⁿ_ : ∀ {n} → nAryOp n A B → (Vec A n → B)
f $ⁿ []       = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs

curryⁿ : ∀ {n} → (Vec A n → B) → nAryOp n A B
curryⁿ {n = zero}  f   = f []
curryⁿ {n = suc n} f x = curryⁿ (λ xs → f (x ∷ xs))

$ⁿ-curryⁿ : ∀ {n} (f : Vec A n → B) → _$ⁿ_ (curryⁿ f) ≡ f
$ⁿ-curryⁿ {n = zero} f  = funExt λ { [] → refl }
$ⁿ-curryⁿ {n = suc n} f = funExt λ { (x ∷ xs) i → $ⁿ-curryⁿ {n = n} (λ ys → f (x ∷ ys)) i xs}

curryⁿ-$ⁿ : ∀ {n} (f : nAryOp {ℓ = ℓ} {ℓ' = ℓ'} n A B) → curryⁿ {A = A} {B = B} (_$ⁿ_ f) ≡ f
curryⁿ-$ⁿ {n = zero} f  = refl
curryⁿ-$ⁿ {n = suc n} f = funExt λ x → curryⁿ-$ⁿ {n = n} (f x)

nAryOp≃VecFun : ∀ {n} → nAryOp n A B ≃ (Vec A n → B)
nAryOp≃VecFun {n = n} = isoToEquiv f
  where
  f : Iso (nAryOp n A B) (Vec A n → B)
  Iso.fun f      = _$ⁿ_
  Iso.inv f      = curryⁿ
  Iso.rightInv f = $ⁿ-curryⁿ
  Iso.leftInv f  = curryⁿ-$ⁿ {n = n}

-- In order to apply ua to nAryOp≃VecFun we probably need to change
-- the base-case of nAryLevel to "ℓ-max ℓ₁ ℓ₂". This will make it
-- necessary to add lots of Lifts in zero cases so it's not done yet,
-- but if the Path is ever needed then it might be worth to do.

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Dagger.Construction.Discrete where

open import Relation.Binary.PropositionalEquality

open import Categories.Category.Dagger
open import Categories.Category.Discrete

Discrete-HasDagger : ∀ {a} (A : Set a) → HasDagger (Discrete A)
Discrete-HasDagger A = record
  { _† = sym
  ; †-identity = refl
  ; †-homomorphism = λ { {f = refl} {g = refl} → refl }
  ; †-resp-≈ = cong sym
  ; †-involutive = λ { refl → refl}
  }

Discrete-DaggerCategory : ∀ {a} (A : Set a) → DaggerCategory a a a
Discrete-DaggerCategory A = record { hasDagger = Discrete-HasDagger A }

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: andrejbauer/agda-categories

max_forks_repo_name: andrejbauer/agda-categories


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

module Categories.Diagram.Colimit.Lan where

open import Level
open import Categories.Category
open import Categories.Category.Cocomplete
open import Categories.Diagram.Duality
open import Categories.Diagram.Limit.Ran
open import Categories.Functor
open import Categories.Kan
open import Categories.Kan.Duality

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

module _ {o ℓ e o′ ℓ′ e′} {C : Category o′ ℓ′ e′} {D : Category o ℓ e}
         (F : Functor C D) (X : Functor C E) (Com : Cocomplete (o′ ⊔ ℓ) (ℓ′ ⊔ e) e′ E) where
  private
    module F = Functor F
    module X = Functor X

  colimit-is-lan : Lan F X
  colimit-is-lan = coRan⇒Lan (limit-is-ran F.op X.op λ G → Colimit⇒coLimit E (Com (Functor.op G)))

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Possible improvements:
-- * Most of the code below is not reachable from main.
-- * The following primitives are not used at all: primPOr, primComp,
--   primHComp, prim^glueU and prim^unglueU.

{-# OPTIONS --erased-cubical #-}

-- The code from Agda.Builtin.Cubical.Glue should not be compiled.

open import Agda.Builtin.Cubical.Glue

open import Agda.Builtin.Cubical.HCompU
open import Agda.Builtin.Cubical.Id
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Builtin.IO
open import Agda.Builtin.Nat
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Primitive.Cubical

open import Erased-cubical-Cubical

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

i₁ : I
i₁ = primIMax (primIMax (primINeg i0) i1) (primIMin i1 i0)

i₁-1 : IsOne i₁
i₁-1 = IsOne1 (primIMax (primINeg i0) i1) (primIMin i1 i0)
         (IsOne2 (primINeg i0) i1 itIsOne)

p₁ : Partial i1 Nat
p₁ = λ _ → 12

p₂ : PartialP i1 (λ _ → Nat)
p₂ = λ _ → 12

p₃ : PartialP i0 (λ _ → Nat)
p₃ = isOneEmpty

subst :
  ∀ {a p} {A : Set a}
  (P : A → Set p) (f : I → A) → P (f i0) → P (f i1)
subst P eq p = primTransp (λ i → P (eq i)) i0 p

p₄ : 12 ≡ 12
p₄ = λ _ → 12

n₁ : Nat
n₁ = p₄ i0

s : Sub Nat i1 (λ _ → 13)
s = inc 13

n₂ : Nat
n₂ = primSubOut s

i₂ : I
i₂ = primFaceForall (λ _ → i1)

i₃ : Id 12 12
i₃ = conid i0 p₄

i₄ : I
i₄ = primDepIMin i1 (λ _ → i0)

i₅ : I
i₅ = primIdFace i₃

p₅ : 12 ≡ 12
p₅ = primIdPath i₃

n₃ : Nat
n₃ = primIdJ (λ _ _ → Nat) 14 i₃

n₄ : Nat
n₄ = primIdElim (λ _ _ → Nat) (λ _ _ _ → 14) i₃

Is-proposition : Set → Set
Is-proposition A = (x y : A) → x ≡ y

data ∥_∥ (A : Set) : Set where
  ∣_∣        : A → ∥ A ∥
  @0 trivial : Is-proposition ∥ A ∥

rec : {A B : Set} → @0 Is-proposition B → (A → B) → ∥ A ∥ → B
rec p f ∣ x ∣           = f x
rec p f (trivial x y i) = p (rec p f x) (rec p f y) i

main : IO ⊤
main =
  putStr (rec easy
            (λ where
               true  → "Success\n"
               false → "Failure\n")
            ∣ true ∣)

-- It should be possible to mention things that are not compiled in
-- type signatures.

u₁ : Not-compiled → ⊤
u₁ _ = tt

@0 A : Set₁
A = Set

u₂ : A → ⊤
u₂ _ = tt


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Unit | U

type
  𝟙 : 0-ary

term
  unit : 𝟙

theory
  (𝟙η) u : 𝟙 |> u = unit
-}

module Unit.Signature where

open import SOAS.Context

-- Type declaration
data UT : Set where
  𝟙 : UT

open import SOAS.Syntax.Signature UT public
open import SOAS.Syntax.Build UT public

-- Operator symbols
data Uₒ : Set where
  unitₒ : Uₒ

-- Term signature
U:Sig : Signature Uₒ
U:Sig = sig λ
  {  unitₒ  → ⟼₀ 𝟙
  }

open Signature U:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Numeric.Nat.Sqrt where

open import Prelude hiding (_<?_)
open import Numeric.Nat.Properties
open import Tactic.Nat
open import Numeric.Nat.BinarySearch

data Sqrt (n : Nat) : Set where
  root : ∀ r → r ^ 2 ≤ n → n < suc r ^ 2 → Sqrt n

getSqrt : ∀ {n} → Sqrt n → Nat
getSqrt (root r _ _) = r

private
  infix 4 _<?_
  _<?_ : (a b : Nat) → Dec (a < b)
  a <?  b with compare a b
  a <?  b | less    a<b = yes a<b
  a <? .a | equal  refl = no (λ a<a → refute a<a)
  a <?  b | greater a>b = no (λ a<b → less-antisym {A = Nat} a>b a<b)

sqrt : (n : Nat) → Sqrt n
sqrt 0 = root 0 (diff! 0) (diff! 0)  -- just to avoid unfolding neutral application
sqrt n with binarySearch 0 n (λ r → n <? r ^ 2)
sqrt n | here k !n< n< _ _ = root k (less-raa (λ lt → !n< (by lt))) n<
sqrt 0 | none _ = root 0 (diff! 0) (diff! 0)
sqrt 1 | none _ = root 1 (diff! 0) (diff! 2)
sqrt (suc (suc n)) | none !n<n² = ⊥-elim (!n<n² auto)
sqrt n | below (diff _ ())
sqrt n | bad-range (diff _ ())

sqrt! : Nat → Nat
sqrt! n = getSqrt (sqrt n)

sqrt-below : ∀ n → sqrt! n ^ 2 ≤ n
sqrt-below n with sqrt n
... | root _ lo _ = lo

sqrt-above : ∀ n → suc (sqrt! n) ^ 2 > n
sqrt-above n with sqrt n
... | root _ _ hi = hi

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Issue561.Core where

postulate Char : Set

{-# BUILTIN CHAR Char #-}

open import Agda.Builtin.IO public

postulate
  return  : ∀ {a} {A : Set a} → A → IO A

{-# COMPILE GHC return = \_ _ -> return #-}
{-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE JS return =
    function(u0) { return function(u1) { return function(x) { return function(cb) { cb(x); }; }; }; } #-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


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

module Data.Bits where

import Prelude
import Logic.Base
import Data.List as List
import Data.Nat  as Nat
import Data.Bool as Bool

open Prelude
open Nat
open Bool
open List

Bit = Bool

shiftL : Nat -> Nat -> Nat
shiftL n i = n * 2 ^ i

sucBits : List Bit -> List Bit
sucBits []            = true :: []
sucBits (false :: xs) = true :: xs
sucBits (true  :: xs) = false :: sucBits xs

-- Least significant bit first. Last bit (when present) is always one.
toBits : Nat -> List Bit
toBits zero    = []
toBits (suc n) = sucBits (odd n :: toBits (div n 2))

fromBits : List Bit -> Nat
fromBits xs = foldr (\b n -> bitValue b + 2 * n) 0 xs
  where
    bitValue : Bit -> Nat
    bitValue b = if b then 1 else 0

nofBits : Nat -> Nat
nofBits = length ∘ toBits

module Proofs where

  open Logic.Base

--   fromBits∘toBits=id : (n : Nat) -> fromBits (toBits n) ≡ n
--   fromBits∘toBits=id  zero   = tt
--   fromBits∘toBits=id (suc n) = ?


text:
data A : Set where
  a : A

data T : A → Set where
  t : T a

postulate
  f : ∀ x → T x → Set

stuff : Set
stuff = f {!!} t

-- There should not be a (Checked) status for this module!

max_stars_repo_name: masondesu/agda


text:
module Data.Tuple where

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

fst : {A B : Set} -> A × B -> A
fst < x , y > = x

snd : {A B : Set} -> A × B -> B
snd < x , y > = y

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Hilbert-style formalisation of syntax with context pairs.
-- Nested terms.

module BasicIS4.Syntax.DyadicHilbert where

open import BasicIS4.Syntax.Common public

-- Derivations.

infix 3 _⊢_
data _⊢_ : Cx² Ty Ty → Ty → Set where
  var   : ∀ {A Γ Δ}     → A ∈ Γ → Γ ⁏ Δ ⊢ A
  app   : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
  ci    : ∀ {A Γ Δ}     → Γ ⁏ Δ ⊢ A ▻ A
  ck    : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ▻ B ▻ A
  cs    : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  mvar  : ∀ {A Γ Δ}     → A ∈ Δ → Γ ⁏ Δ ⊢ A
  box   : ∀ {A Γ Δ}     → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ □ A
  cdist : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ □ (A ▻ B) ▻ □ A ▻ □ B
  cup   : ∀ {A Γ Δ}     → Γ ⁏ Δ ⊢ □ A ▻ □ □ A
  cdown : ∀ {A Γ Δ}     → Γ ⁏ Δ ⊢ □ A ▻ A
  cpair : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ▻ B ▻ A ∧ B
  cfst  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ∧ B ▻ A
  csnd  : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ A ∧ B ▻ B
  unit  : ∀ {Γ Δ}       → Γ ⁏ Δ ⊢ ⊤

infix 3 _⊢⋆_
_⊢⋆_ : Cx² Ty Ty → Cx Ty → Set
Γ ⁏ Δ ⊢⋆ ∅     = 𝟙
Γ ⁏ Δ ⊢⋆ Ξ , A = Γ ⁏ Δ ⊢⋆ Ξ × Γ ⁏ Δ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ ⊢ A
mono⊢ η (var i)   = var (mono∈ η i)
mono⊢ η (app t u) = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η ci        = ci
mono⊢ η ck        = ck
mono⊢ η cs        = cs
mono⊢ η (mvar i)  = mvar i
mono⊢ η (box t)   = box t
mono⊢ η cdist     = cdist
mono⊢ η cup       = cup
mono⊢ η cdown     = cdown
mono⊢ η cpair     = cpair
mono⊢ η cfst      = cfst
mono⊢ η csnd      = csnd
mono⊢ η unit      = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ ⊢⋆ Ξ
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Monotonicity with respect to modal context inclusion.

mmono⊢ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ′ ⊢ A
mmono⊢ θ (var i)   = var i
mmono⊢ θ (app t u) = app (mmono⊢ θ t) (mmono⊢ θ u)
mmono⊢ θ ci        = ci
mmono⊢ θ ck        = ck
mmono⊢ θ cs        = cs
mmono⊢ θ (mvar i)  = mvar (mono∈ θ i)
mmono⊢ θ (box t)   = box (mmono⊢ θ t)
mmono⊢ θ cdist     = cdist
mmono⊢ θ cup       = cup
mmono⊢ θ cdown     = cdown
mmono⊢ θ cpair     = cpair
mmono⊢ θ cfst      = cfst
mmono⊢ θ csnd      = csnd
mmono⊢ θ unit      = unit

mmono⊢⋆ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ′ ⊢⋆ Ξ
mmono⊢⋆ {∅}     θ ∙        = ∙
mmono⊢⋆ {Ξ , A} θ (ts , t) = mmono⊢⋆ θ ts , mmono⊢ θ t

-- Monotonicity using context pairs.

mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A
mono²⊢ (η , θ) = mono⊢ η ∘ mmono⊢ θ

-- Shorthand for variables.

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

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

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

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

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

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

-- Reflexivity.

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

mrefl⊢⋆ : ∀ {Δ Γ} → Γ ⁏ Δ ⊢⋆ □⋆ Δ
mrefl⊢⋆ {∅}     = ∙
mrefl⊢⋆ {Δ , A} = mmono⊢⋆ weak⊆ mrefl⊢⋆ , box mv₀

-- Deduction theorem.

lam : ∀ {A B Γ Δ} → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ▻ B
lam (var top)     = ci
lam (var (pop i)) = app ck (var i)
lam (app t u)     = app (app cs (lam t)) (lam u)
lam ci            = app ck ci
lam ck            = app ck ck
lam cs            = app ck cs
lam (mvar i)      = app ck (mvar i)
lam (box t)       = app ck (box t)
lam cdist         = app ck cdist
lam cup           = app ck cup
lam cdown         = app ck cdown
lam cpair         = app ck cpair
lam cfst          = app ck cfst
lam csnd          = app ck csnd
lam unit          = app ck unit

lam⋆ : ∀ {Ξ A Γ Δ} → Γ ⧺ Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Combined axioms of distribution and transitivity.

cdistup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (□ A ▻ B) ▻ □ A ▻ □ B
cdistup = app (app cs (app (app cs (app ck cs))
                           (app (app cs (app (app cs (app ck cs))
                                             (lam (lam cdist))))
                                (app (app cs (app ck ck)) ci))))
              (app (app cs (app (app cs (app ck cs))
                                (lam (lam cup))))
                   (app ck ci))

-- Modal deduction theorem.

mlam : ∀ {A B Γ Δ} → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ ⊢ □ A ▻ B
mlam (var i)        = app ck (var i)
mlam (app t u)      = app (app cs (mlam t)) (mlam u)
mlam ci             = app ck ci
mlam ck             = app ck ck
mlam cs             = app ck cs
mlam (mvar top)     = cdown
mlam (mvar (pop i)) = app ck (mvar i)
mlam (box t)        = app cdistup (box (mlam t))
mlam cdist          = app ck cdist
mlam cup            = app ck cup
mlam cdown          = app ck cdown
mlam cpair          = app ck cpair
mlam cfst           = app ck cfst
mlam csnd           = app ck csnd
mlam unit           = app ck unit

mlam⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⧺ Ξ ⊢ A → Γ ⁏ Δ ⊢ □⋆ Ξ ▻⋯▻ A
mlam⋆ {∅}     = I
mlam⋆ {Ξ , B} = mlam⋆ {Ξ} ∘ mlam

mlam⋆₀ : ∀ {Δ A Γ} → Γ ⁏ Δ ⊢ A → Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A
mlam⋆₀ {∅}     = I
mlam⋆₀ {Δ , B} = mlam⋆₀ ∘ mlam

-- Detachment theorems.

det : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ , A ⁏ Δ ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⁏ Δ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A Δ} → ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A → Γ ⁏ Δ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

mdet : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A ▻ B → Γ ⁏ Δ , A ⊢ B
mdet t = app (mmono⊢ weak⊆ t) (box mv₀)

mdet⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢ □⋆ Ξ ▻⋯▻ A → Γ ⁏ Δ ⧺ Ξ ⊢ A
mdet⋆ {∅}     = I
mdet⋆ {Ξ , B} = mdet ∘ mdet⋆ {Ξ}

mdet⋆₀ : ∀ {Δ A Γ} → Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A → Γ ⁏ Δ ⊢ A
mdet⋆₀ {∅}     = I
mdet⋆₀ {Δ , B} = mdet ∘ mdet⋆₀

-- Context manipulation.

merge : ∀ {Δ A Γ} → Γ ⁏ Δ ⊢ A → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A
merge {Δ} = det⋆ {□⋆ Δ} ∘ mlam⋆₀

mmerge : ∀ {Γ A Δ} → □⋆ Γ ⁏ Δ ⊢ A → ∅ ⁏ Δ ⧺ Γ ⊢ A
mmerge {Γ} = mdet⋆ {Γ} ∘ lam⋆₀

split : ∀ {Δ A Γ} → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A → Γ ⁏ Δ ⊢ A
split {Δ} = mdet⋆₀ ∘ lam⋆ {□⋆ Δ}

msplit : ∀ {Γ A Δ} → ∅ ⁏ Δ ⧺ Γ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
msplit {Γ} = det⋆₀ ∘ mlam⋆ {Γ}

merge⋆ : ∀ {Ξ Δ Γ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢⋆ Ξ
merge⋆ {∅}     ∙        = ∙
merge⋆ {Ξ , A} (ts , t) = merge⋆ ts , merge t

split⋆ : ∀ {Ξ Δ Γ} → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
split⋆ {∅}     ∙        = ∙
split⋆ {Ξ , A} (ts , t) = split⋆ ts , split t

-- Cut and multicut.

cut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ B
cut t u = app (lam u) t

mcut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ ⊢ B
mcut t u = app (mlam u) t

multicut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

mmulticut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Ξ ⊢ A → Γ ⁏ Δ ⊢ A
mmulticut {∅}     ∙        u = mmono⊢ bot⊆ u
mmulticut {Ξ , B} (ts , t) u = app (mmulticut ts (mlam u)) t

-- Transitivity.

trans⊢⋆₀ : ∀ {Γ″ Γ′ Γ} → Γ ⁏ ∅ ⊢⋆ Γ′ → Γ′ ⁏ ∅ ⊢⋆ Γ″ → Γ ⁏ ∅ ⊢⋆ Γ″
trans⊢⋆₀ {∅}      ts ∙        = ∙
trans⊢⋆₀ {Γ″ , A} ts (us , u) = trans⊢⋆₀ ts us , multicut ts u

trans⊢⋆ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⁏ Δ ⊢⋆ Γ′ ⧺ (□⋆ Δ′) → Γ′ ⁏ Δ′ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
trans⊢⋆ ts us = split⋆ (trans⊢⋆₀ (merge⋆ ts) (merge⋆ us))

-- Contraction.

ccont : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ Δ} → Γ , A , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ B
cont t = det (app ccont (lam (lam t)))

mcont : ∀ {A B Γ Δ} → Γ ⁏ Δ , A , A ⊢ B → Γ ⁏ Δ , A ⊢ B
mcont t = mdet (app ccont (mlam (mlam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ Δ} → Γ , A , B ⁏ Δ ⊢ C → Γ , B , A ⁏ Δ ⊢ C
exch t = det (det (app cexch (lam (lam t))))

mexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ , A , B ⊢ C → Γ ⁏ Δ , B , A ⊢ C
mexch t = mdet (mdet (app cexch (mlam (mlam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ Δ} → Γ , B ⁏ Δ ⊢ C → Γ , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

mcomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ , B ⊢ □ C → Γ ⁏ Δ , A ⊢ □ B → Γ ⁏ Δ , A ⊢ □ C
mcomp t u = mdet (app (app ccomp (mlam t)) (mlam u))

-- Useful theorems in functional form.

dist : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ▻ B) → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B
dist t u = app (app cdist t) u

up : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ □ A
up t = app cup t

down : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ A
down t = app cdown t

distup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (□ A ▻ B) → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B
distup t u = dist t (up u)

unbox : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ C → Γ ⁏ Δ ⊢ C
unbox t u = app (mlam u) t

pair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ∧ B
pair t u = app (app cpair t) u

fst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ A
fst t = app cfst t

snd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ B
snd t = app csnd t

-- Internalisation, or lifting, and additional theorems.

lift : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ □ A
lift {∅}     t = box t
lift {Γ , B} t = det (app cdist (lift (lam t)))

hypup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ □ A ▻ B
hypup t = lam (app (mono⊢ weak⊆ t) (down v₀))

hypdown : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ □ A ▻ B → Γ ⁏ Δ ⊢ □ A ▻ B
hypdown t = lam (app (mono⊢ weak⊆ t) (up v₀))

cxup : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
cxup {∅}     t = t
cxup {Γ , B} t = det (hypup (cxup (lam t)))

cxdown : ∀ {Γ A Δ} → □⋆ □⋆ Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
cxdown {∅}     t = t
cxdown {Γ , B} t = det (hypdown (cxdown (lam t)))

box⋆ : ∀ {Ξ Γ Δ} → ∅ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ □⋆ Ξ
box⋆ {∅}     ∙        = ∙
box⋆ {Ξ , A} (ts , t) = box⋆ ts , box t

lift⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → □⋆ Γ ⁏ Δ ⊢⋆ □⋆ Ξ
lift⋆ {∅}     ∙        = ∙
lift⋆ {Ξ , A} (ts , t) = lift⋆ ts , lift t

up⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Δ ⊢⋆ □⋆ □⋆ Ξ
up⋆ {∅}     ∙        = ∙
up⋆ {Ξ , A} (ts , t) = up⋆ ts , up t

down⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
down⋆ {∅}     ∙        = ∙
down⋆ {Ξ , A} (ts , t) = down⋆ ts , down t

multibox : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → □⋆ Ξ ⁏ ∅ ⊢ A → Γ ⁏ Δ ⊢ □ A
multibox ts u = multicut (up⋆ ts) (mmono⊢ bot⊆ (lift u))

dist′ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ▻ B) → Γ ⁏ Δ ⊢ □ A ▻ □ B
dist′ t = lam (dist (mono⊢ weak⊆ t) v₀)

mpair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B → Γ ⁏ Δ ⊢ □ (A ∧ B)
mpair t u = dist (dist (box cpair) t) u

mfst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ∧ B) → Γ ⁏ Δ ⊢ □ A
mfst t = dist (box cfst) t

msnd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ∧ B) → Γ ⁏ Δ ⊢ □ B
msnd t = dist (box csnd) t

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ {Δ} → Γ , A ⁏ Δ ⊢ B → Γ′ ⁏ Δ ⊢ A → Γ ⧺ Γ′ ⁏ Δ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

mconcat : ∀ {A B Γ Δ} Δ′ → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ′ ⊢ □ A → Γ ⁏ Δ ⧺ Δ′ ⊢ B
mconcat Δ′ t u = app (mmono⊢ (weak⊆⧺₁ Δ′) (mlam t)) (mmono⊢ weak⊆⧺₂ u)

-- Convertibility.

data _⋙_ {Γ Δ : Cx Ty} : ∀ {A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A → Set where
  refl⋙     : ∀ {A} → {t : Γ ⁏ Δ ⊢ A}
                     → t ⋙ t

  trans⋙    : ∀ {A} → {t t′ t″ : Γ ⁏ Δ ⊢ A}
                     → t ⋙ t′ → t′ ⋙ t″
                     → t ⋙ t″

  sym⋙      : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ A}
                     → t ⋙ t′
                     → t′ ⋙ t

  congapp⋙  : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ▻ B} → {u u′ : Γ ⁏ Δ ⊢ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app t u ⋙ app t′ u′

  congi⋙    : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ A}
                     → t ⋙ t′
                     → app ci t ⋙ app ci t′

  congk⋙    : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A} → {u u′ : Γ ⁏ Δ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app ck t) u ⋙ app (app ck t′) u′

  congs⋙    : ∀ {A B C} → {t t′ : Γ ⁏ Δ ⊢ A ▻ B ▻ C} → {u u′ : Γ ⁏ Δ ⊢ A ▻ B} → {v v′ : Γ ⁏ Δ ⊢ A}
                         → t ⋙ t′ → u ⋙ u′ → v ⋙ v′

  -- NOTE: Rejected by Pfenning and Davies.
  -- congbox⋙  : ∀ {A} → {t t′ : ∅ ⁏ Δ ⊢ A}
  --                    → t ⋙ t′
  --                    → box {Γ} t ⋙ box {Γ} t′

  congdist⋙ : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ □ (A ▻ B)} → {u u′ : Γ ⁏ Δ ⊢ □ A}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cdist t) u ⋙ app (app cdist t′) u′

  congup⋙   : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ □ A}
                     → t ⋙ t′
                     → app cup t ⋙ app cup t′

  congdown⋙ : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ □ A}
                     → t ⋙ t′
                     → app cdown t ⋙ app cdown t′

  congpair⋙ : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A} → {u u′ : Γ ⁏ Δ ⊢ B}
                       → t ⋙ t′ → u ⋙ u′
                       → app (app cpair t) u ⋙ app (app cpair t′) u′

  congfst⋙  : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app cfst t ⋙ app cfst t′

  congsnd⋙  : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                       → t ⋙ t′
                       → app csnd t ⋙ app csnd t′

  -- TODO: Verify this.
  beta▻ₖ⋙   : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                       → app (app ck t) u ⋙ t

  -- TODO: Verify this.
  beta▻ₛ⋙   : ∀ {A B C} → {t : Γ ⁏ Δ ⊢ A ▻ B ▻ C} → {u : Γ ⁏ Δ ⊢ A ▻ B} → {v : Γ ⁏ Δ ⊢ A}
                         → app (app (app cs t) u) v ⋙ app (app t v) (app u v)

  -- TODO: What about eta for ▻? What about beta, eta, and commuting conversions for □?

  beta∧₁⋙   : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                       → app cfst (app (app cpair t) u) ⋙ t

  beta∧₂⋙   : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                       → app csnd (app (app cpair t) u) ⋙ u

  eta∧⋙     : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A ∧ B}
                       → t ⋙ app (app cpair (app cfst t)) (app csnd t)

  eta⊤⋙    : ∀ {t : Γ ⁏ Δ ⊢ ⊤} → t ⋙ unit

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --safe --without-K #-}
open import Relation.Binary

module Data.List.Membership.Setoid.Disjoint {a p} (S : Setoid a p) where
open Setoid S renaming (Carrier to A)
open import Data.List using (List ; [])
open import Data.List.Membership.Setoid (S)
open import Data.List.Membership.Setoid.Trans (S)
open import Data.Empty

open import Function

Disjoint : Rel (List A) _
Disjoint xs ys = ∀ {x} → x ∈ xs → x ∈ ys → ⊥

disjoint-sym : Symmetric Disjoint
disjoint-sym dis = flip dis

disjoint-[]ˡ : ∀ {xs} → Disjoint xs []
disjoint-[]ˡ _ ()

disjoint-[]ʳ :  ∀ {xs} → Disjoint [] xs
disjoint-[]ʳ ()

disjointness : ∀ {xs ys} → Disjoint xs ys → ∀ {x} → x ∈ xs → ∀ {y} → y ∈ ys → x ≈ y → ⊥
disjointness xs⋈ys x∈xs y∈ys x≈y = xs⋈ys x∈xs (≈-trans-∈ x≈y y∈ys)

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
module Monads.Except where

open import Class.Monad
open import Class.Monad.Except
open import Monads.ExceptT
open import Monads.Identity
open import Level

private
  variable
    a : Level
    A : Set a

Except : Set a -> Set a -> Set a
Except = ExceptT Id

instance
  Except-Monad : Monad (Except A)
  Except-Monad = ExceptT-Monad

  Except-MonadExcept : MonadExcept (Except A) A
  Except-MonadExcept = ExceptT-MonadExcept

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import HoTT
open import groups.SumOfSubIndicator
open import cohomology.Theory

{- It should be possible to prove lemmas for arbitrary universe levels,
   but this file is only used for [FinSkeleton], which is in the zeroth
   universe. -}

module cohomology.SubFinWedge (CT : CohomologyTheory lzero) (n : ℤ) where

open CohomologyTheory CT

{-
  [B-ac] and [B-dec] can actually be proved from [subfin],
  but maybe the user wants to supply a different [B-ac].

  Another good question is why the focus is on [B], not [A].
  Well, check the definition of [MinusPoint] and you will see why.
-}

module _ {I} {A B : Type₀} (p : Fin I → Coprod A B) (X : Ptd₀) where

  C-subfinite-additive : C n (⊙BigWedge (λ (_ : B) → X)) →ᴳ Πᴳ B (λ _ → C n X)
  C-subfinite-additive = C-additive n (λ (_ : B) → X)

  CEl-subfinite-additive : CEl n (⊙BigWedge (λ (_ : B) → X)) → Π B (λ _ → CEl n X)
  CEl-subfinite-additive = GroupHom.f C-subfinite-additive

  C-subfinite-additive-is-equiv : has-choice 0 B lzero → is-equiv CEl-subfinite-additive
  C-subfinite-additive-is-equiv = C-additive-is-equiv n (λ _ → X)

  C-subfinite-additive-iso : has-choice 0 B lzero
    → C n (⊙BigWedge (λ (_ : B) → X)) ≃ᴳ Πᴳ B (λ _ → C n X)
  C-subfinite-additive-iso = C-additive-iso n (λ (_ : B) → X)

  {- an explicit inverse function -}
  explicit-inverse-C-subfinite-additive : has-dec-eq B
    → Π B (λ _ → CEl n X) → CEl n (⊙BigWedge (λ (_ : B) → X))
  explicit-inverse-C-subfinite-additive B-dec f =
    Group.subsum-r (C n (⊙BigWedge (λ _ → X))) p (λ b → CEl-fmap n (⊙bwproj B-dec b) (f b))

module _ where

  {- this part is to prove the explicit inverse function is correct -}
  abstract
    private
      C-bwproj-bwin-≠ : {B : Type₀} (B-dec : has-dec-eq B) {X : Ptd₀}
        {b b' : B} (neq : b ≠ b') (g : CEl n X)
        → CEl-fmap n (⊙bwproj B-dec b ⊙∘ ⊙bwin {X = λ _ → X} b') g == Cident n X
      C-bwproj-bwin-≠ B-dec neq g =
        CEl-fmap-base-indep n (bwproj-bwin-≠ B-dec neq) g ∙ C-fmap-cst n g

      C-bwproj-bwin-diag : {B : Type₀} (B-dec : has-dec-eq B) {X : Ptd₀} (b : B) (g : CEl n X)
        → CEl-fmap n (⊙bwproj B-dec b ⊙∘ ⊙bwin {X = λ _ → X} b) g == g
      C-bwproj-bwin-diag B-dec b g =
        CEl-fmap-base-indep n (bwproj-bwin-diag B-dec b) g ∙ C-fmap-idf n g

      inverse-C-subfinite-additive-β' : ∀ {A B : Type₀} (B-dec : has-dec-eq B) {I}
        (p : Fin I ≃ Coprod A B) {X : Ptd₀}
        → ∀ f → GroupHom.f (C-subfinite-additive (–> p) X) (explicit-inverse-C-subfinite-additive (–> p) X B-dec f) ∼ f
      inverse-C-subfinite-additive-β' B-dec p {X} f b* =
        CEl-fmap n (⊙bwin b*) (Group.subsum-r (C n (⊙BigWedge (λ _ → X))) (–> p) (λ b → CEl-fmap n (⊙bwproj B-dec b) (f b)))
          =⟨ GroupHom.pres-subsum-r (C-fmap n (⊙bwin b*)) (–> p) (λ b → CEl-fmap n (⊙bwproj B-dec b) (f b)) ⟩
        Group.subsum-r (C n X) (–> p) (λ b → CEl-fmap n (⊙bwin b*) (CEl-fmap n (⊙bwproj B-dec b) (f b)))
          =⟨ ap (Group.subsum-r (C n X) (–> p)) (λ= λ b → ∘-CEl-fmap n (⊙bwin b*) (⊙bwproj B-dec b) (f b)) ⟩
        Group.subsum-r (C n X) (–> p) (λ b → CEl-fmap n (⊙bwproj B-dec b ⊙∘ ⊙bwin b*) (f b))
          =⟨ subsum-r-subindicator (C n X) p (λ b → CEl-fmap n (⊙bwproj B-dec b ⊙∘ ⊙bwin b*) (f b))
              b* (λ b≠b* → C-bwproj-bwin-≠ B-dec b≠b* _) ⟩
        CEl-fmap n (⊙bwproj B-dec b* ⊙∘ ⊙bwin b*) (f b*)
          =⟨ C-bwproj-bwin-diag B-dec b* (f b*) ⟩
        f b*
          =∎

    inverse-C-subfinite-additive-β : ∀ {A B : Type₀}
      (B-ac : has-choice 0 B lzero) (B-dec : has-dec-eq B) {I}
      (p : Fin I ≃ Coprod A B) {X : Ptd₀}
      → is-equiv.g (C-subfinite-additive-is-equiv (–> p) X B-ac)
      ∼ explicit-inverse-C-subfinite-additive (–> p) X B-dec
    inverse-C-subfinite-additive-β B-ac B-dec p {X} f =
      ! $ equiv-adj (GroupIso.f-equiv (C-subfinite-additive-iso (–> p) X B-ac)) $
        λ= $ inverse-C-subfinite-additive-β' B-dec p f

module _ (I : ℕ) (X : Ptd₀) where

  C-finite-additive : C n (⊙BigWedge (λ (_ : Fin I) → X)) →ᴳ Πᴳ (Fin I) (λ _ → C n X)
  C-finite-additive = C-subfinite-additive {A = Empty} inr X

  CEl-finite-additive : CEl n (⊙BigWedge (λ (_ : Fin I) → X)) → Π (Fin I) (λ _ → CEl n X)
  CEl-finite-additive = GroupHom.f C-finite-additive

  C-finite-additive-is-equiv : is-equiv CEl-finite-additive
  C-finite-additive-is-equiv = C-subfinite-additive-is-equiv {A = Empty} inr X (Fin-has-choice 0 lzero)

  C-finite-additive-iso : C n (⊙BigWedge (λ (_ : Fin I) → X)) ≃ᴳ Πᴳ (Fin I) (λ _ → C n X)
  C-finite-additive-iso = C-subfinite-additive-iso {A = Empty} inr X (Fin-has-choice 0 lzero)

  {- an explicit inverse function -}
  explicit-inverse-C-finite-additive : Π (Fin I) (λ _ → CEl n X) → CEl n (⊙BigWedge (λ (_ : Fin I) → X))
  explicit-inverse-C-finite-additive = explicit-inverse-C-subfinite-additive {A = Empty} inr X Fin-has-dec-eq

module _ where
  abstract
    inverse-C-finite-additive-β : ∀ {I : ℕ} {X : Ptd₀}
      → is-equiv.g (C-finite-additive-is-equiv I X)
      ∼ explicit-inverse-C-finite-additive I X
    inverse-C-finite-additive-β {I} {X} =
      inverse-C-subfinite-additive-β {A = Empty} {B = Fin I}
        (Fin-has-choice 0 lzero) Fin-has-dec-eq (⊔₁-Empty (Fin I) ⁻¹) {X}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module hierarchy where

data Bool : Set where
  true  : Bool
  false : Bool

_and_ : Bool → Bool → Bool
true and true = true
true and false = false
false and true = false
false and false = false

_or_ : Bool → Bool → Bool
true or true = true
true or false = true
false or true = true
false or false = false

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_==_ : ℕ → ℕ → Bool
zero == zero   = true
suc n == suc m = n == m
_ == _         = false

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

_∈_ : ℕ → List ℕ → Bool
x ∈ []      = false
x ∈ (y :: ys) with x == y
...              | true  = true
...              | false = x ∈ ys

_⊂_ : List ℕ → List ℕ → Bool
[] ⊂ ys      = true
(x :: xs) ⊂ ys with x ∈ ys
...               | true  = xs ⊂ ys
...               | false = false

_++_ : {A : Set} → List A → List A → List A
[] ++ ys        = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

map : {A : Set} → (A → A) → List A → List A
map f []        = []
map f (x :: xs) = (f x) :: (map f xs)

any : {A : Set} → (A → Bool) → List A → Bool
any _ []        = false
any f (x :: xs) = (f x) or (any f xs)

all : {A : Set} → (A → Bool) → List A → Bool
all _ []        = true
all f (x :: xs) = (f x) and (all f xs)

data Arrow : Set where
  _⇒_ : List ℕ → ℕ → Arrow

_⇔_ : Arrow → Arrow → Bool
(at ⇒ ah) ⇔ (bt ⇒ bh) = ((at ⊂ bt) and (bt ⊂ at)) and (ah == bh)

_∈∈_ : Arrow → List Arrow → Bool
x ∈∈ []      = false
x ∈∈ (y :: ys) with x ⇔ y
...               | true  = true
...               | false = x ∈∈ ys

_⊂⊂_ : List Arrow → List Arrow → Bool
[] ⊂⊂ ys      = true
(x :: xs) ⊂⊂ ys with x ∈∈ ys
...                | true  = xs ⊂⊂ ys
...                | false = false

ArrowSearch : List Arrow → List Arrow → ℕ → Bool
ArrowSearch [] ds g = false
ArrowSearch (([] ⇒ h) :: cs) ds g with (h == g)
...         | true  = true
...         | false = ArrowSearch cs (([] ⇒ h) :: ds) g
ArrowSearch ((ts ⇒ h) :: cs) ds g with (h == g)
...         | true  = (all (ArrowSearch (cs ++ ds) []) ts)
                  or (ArrowSearch cs ((ts ⇒ h) :: ds) g)
...         | false = ArrowSearch cs ((ts ⇒ h) :: ds) g

_⊢_ : List Arrow → Arrow → Bool
cs ⊢ ((t :: ts) ⇒ h) = (([] ⇒ t) :: cs) ⊢ (ts ⇒ h)
cs ⊢ ([] ⇒ h)        = ArrowSearch cs [] h

max_stars_repo_name: louisswarren/hieretikz

max_issues_repo_name: louisswarren/hieretikz

max_forks_repo_name: louisswarren/hieretikz


text:
module Lang.Inspect where

open import Type
open import Structure.Setoid
open import Structure.Relator.Properties

{-
module _ {ℓ₁ ℓ₂} {A : Type{ℓ₁}} {B : A → Type{ℓ₂}} ⦃ eqB : ∀{x} → Equiv(B(x)) ⦄ (f : ∀(x) → B(x)) (x : A) where
  data Inspect (y : B(x)) : Type{ℓ₂} where
    intro : (f(x) ≡ y) → Inspect(y)

  inspect : Inspect(f(x))
  inspect = intro(reflexivity(_≡_ ⦃ eqB ⦄))
  {-# INLINE inspect #-}
-}

module _ {ℓ₁ ℓ₂ ℓₑ₂} {A : Type{ℓ₁}} {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ (f : A → B) (x : A) where
  data Inspect (y : B) : Type{ℓₑ₂} where
    intro : (f(x) ≡ y) → Inspect(y)

  inspect : Inspect(f(x))
  inspect = intro(reflexivity(_≡_))
  {-# INLINE inspect #-}


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

open import HoTT hiding (left; right)

module homotopy.BlakersMassey {i j k}
  {A : Type i} {B : Type j} (Q : A → B → Type k)
  m (f-conn : ∀ a → is-connected (S m) (Σ B (λ b → Q a b)))
  n (g-conn : ∀ b → is-connected (S n) (Σ A (λ a → Q a b)))
  where

open import homotopy.blakersmassey.Pushout Q
import homotopy.blakersmassey.CoherenceData Q m f-conn n g-conn as Coh

-- These extra parameters will be discharged in the end
module _ {a₀} {b₀} (q₀₀ : Q a₀ b₀) where

  -- Step 1:
  -- Generalizing the theorem to [bmleft x == p] for arbitrary p.
  -- This requires a pushout-rec

  -- "extended" version
  code-bmleft-template : ∀ a₁ {p} (r' : bmleft a₁ == p) → bmleft a₀ == p → Type (lmax i (lmax j k))
  code-bmleft-template a₁ r' r = Trunc (m +2+ n) (hfiber (λ q₁₀ → bmglue q₀₀ ∙' ! (bmglue q₁₀) ∙' r') r)

  code-bmleft : ∀ a₁ → bmleft a₀ == bmleft a₁ → Type (lmax i (lmax j k))
  code-bmleft a₁ = code-bmleft-template a₁ idp

  code-bmright : ∀ b₁ → bmleft a₀ == bmright b₁ → Type (lmax i (lmax j k))
  code-bmright b₁ r = Trunc (m +2+ n) (hfiber bmglue r)

  -- The template from [Coh.eqv] to the input for [apd code glue]
  -- for using the identification elimination.
  code-bmglue-template : ∀ {a₁ p}
    → (code : (r : bmleft a₀ == p) → Type (lmax i (lmax j k)))
    → (r : bmleft a₁ == p)
    → (∀ r' → code-bmleft-template a₁ r r' ≃ code r')
    → code-bmleft-template a₁ idp == code [ (λ p → bmleft a₀ == p → Type (lmax i (lmax j k))) ↓ r ]
  code-bmglue-template _ idp lemma = λ= (ua ∘ lemma)

  -- The real glue, that is, the template with actual equivalence.
  code-bmglue : ∀ {a₁ b₁} (q₁₁ : Q a₁ b₁)
    → code-bmleft a₁ == code-bmright b₁
      [ (λ p → bmleft a₀ == p → Type (lmax i (lmax j k))) ↓ bmglue q₁₁ ]
  code-bmglue {a₁} {b₁} q₁₁ =
    code-bmglue-template (code-bmright b₁) (bmglue q₁₁) (Coh.eqv q₀₀ q₁₁)

  -- Here's the data structure for the generalized theorem.
  module Code = BMPushoutElim code-bmleft code-bmright code-bmglue

  code : ∀ p → bmleft a₀ == p → Type (lmax i (lmax j k))
  code = Code.f

  -- Step 2:
  -- [code] is contractible!

  -- The center for [idp].  We will use transport to find the center
  -- in other fibers.
  code-center-idp : code (bmleft a₀) idp
  code-center-idp = [ q₀₀ , !-inv'-r (bmglue q₀₀) ]

  -- The following is the breakdown of the path for coercing:
  --   [ap2 code r (↓-cst=idf-in' r)]
  -- We will need the broken-down version anyway,
  -- so why not breaking them down from the very beginning?

  -- The template here, again, is to keep the possibility
  -- of plugging in [idp] for [r].
  coerce-path-template : ∀ {p} r
    → code-bmleft a₀ == code p [ (λ p → bmleft a₀ == p → Type (lmax i (lmax j k))) ↓ r ]
    → code-bmleft a₀ idp == code p r
  coerce-path-template idp lemma = app= lemma idp

  -- The real path.
  coerce-path : ∀ {p} r → code (bmleft a₀) idp == code p r
  coerce-path r = coerce-path-template r (apd code r)

  -- Find the center in other fibers.
  code-center : ∀ {p} r → code p r
  code-center r = coe (coerce-path r) code-center-idp

  -- Part of the decomposed [coe (coerce-path r)]
  code-bmleft-template-diag : ∀ {p} (r : bmleft a₀ == p)
    → code-bmleft a₀ idp → code-bmleft-template a₀ r r
  code-bmleft-template-diag r = Trunc-rec Trunc-level
    λ {(q₀₀' , shift) →
      [ q₀₀' , ! (∙'-assoc (bmglue q₀₀) (! (bmglue q₀₀')) r) ∙ ap (_∙' r) shift ∙' ∙'-unit-l r ]}

  abstract
    code-bmleft-template-diag-idp : ∀ x → code-bmleft-template-diag idp x == x
    code-bmleft-template-diag-idp =
      Trunc-elim (λ _ → =-preserves-level Trunc-level)
        λ{(q₁₀ , shift) → ap (λ p → [ q₁₀ , p ]) (ap-idf shift)}

  -- Here shows the use of two templates.  It will be super painful
  -- if we cannot throw in [idp].  Now we only have to deal with
  -- simple computations.
  abstract
    coe-coerce-path-code-bmglue-template : ∀ {p} (r : bmleft a₀ == p)
      (lemma : ∀ r' → code-bmleft-template a₀ r r' ≃ code p r')
      (x : code-bmleft a₀ idp)
      → coe (coerce-path-template r (code-bmglue-template (code p) r lemma)) x
      == –> (lemma r) (code-bmleft-template-diag r x)
    coe-coerce-path-code-bmglue-template idp lemma x =
      coe (app= (λ= (ua ∘ lemma)) idp) x
        =⟨ ap (λ p → coe p x) (app=-β (ua ∘ lemma) idp) ⟩
      coe (ua (lemma idp)) x
        =⟨ coe-β (lemma idp) x ⟩
      –> (lemma idp) x
        =⟨ ! (ap (–> (lemma idp)) (code-bmleft-template-diag-idp x)) ⟩
      –> (lemma idp) (code-bmleft-template-diag idp x)
        =∎

  -- Here is the actually lemma we want!
  -- A succinct breakdown of [coerce-path code (glue q)].
  abstract
    coe-coerce-path-code-bmglue : ∀ {b₁} (q₀₁ : Q a₀ b₁) x
      → coe (coerce-path (bmglue q₀₁)) x
      == Coh.to q₀₀ q₀₁ (bmglue q₀₁) (code-bmleft-template-diag (bmglue q₀₁) x)
    coe-coerce-path-code-bmglue q₀₁ x =
      coe (coerce-path-template (bmglue q₀₁) (apd code (bmglue q₀₁))) x
        =⟨ ap (λ p → coe (coerce-path-template (bmglue q₀₁) p) x) (Code.glue-β q₀₁) ⟩
      coe (coerce-path-template (bmglue q₀₁) (code-bmglue q₀₁)) x
        =⟨ coe-coerce-path-code-bmglue-template (bmglue q₀₁) (Coh.eqv q₀₀ q₀₁) x ⟩
      Coh.to q₀₀ q₀₁ (bmglue q₀₁) (code-bmleft-template-diag (bmglue q₀₁) x)
        =∎

  -- This is the only case you care for contractibiltiy.
  abstract
    code-coh-lemma : ∀ {b₁} (q₀₁ : Q a₀ b₁) → code-center (bmglue q₀₁) == [ q₀₁ , idp ]
    code-coh-lemma q₀₁ =
      coe (coerce-path (bmglue q₀₁)) code-center-idp
        =⟨ coe-coerce-path-code-bmglue q₀₁ code-center-idp ⟩
      Coh.to' q₀₀ q₀₁ (bmglue q₀₁) (q₀₀ , α₁α₁⁻¹α₂=α₂ (bmglue q₀₀) (bmglue q₀₁))
        =⟨ ap (Coh.To.ext q₀₀ (_ , q₀₀) (_ , q₀₁) (bmglue q₀₁)) (path-lemma (bmglue q₀₀) (bmglue q₀₁)) ⟩
      Coh.To.ext q₀₀ (_ , q₀₀) (_ , q₀₁) (bmglue q₀₁) (! path)
        =⟨ Coh.To.β-r q₀₀ (_ , q₀₁) (bmglue q₀₁) (! path) ⟩
      [ q₀₁ , path ∙' ! path ]
        =⟨ ap (λ p → [ q₀₁ , p ]) (!-inv'-r path) ⟩
      [ q₀₁ , idp ]
        =∎
      where
        path = Coh.βPair.path (Coh.βpair-bmright q₀₀ q₀₁ (bmglue q₀₁))

        -- this is defined to be the path generated by [code-bmleft-template-diag]
        α₁α₁⁻¹α₂=α₂ : ∀ {p₁ p₂ p₃ : BMPushout} (α₁ : p₁ == p₂) (α₂ : p₁ == p₃)
          → α₁ ∙' ! α₁ ∙' α₂ == α₂
        α₁α₁⁻¹α₂=α₂ α₁ α₂ = ! (∙'-assoc α₁ (! α₁) α₂) ∙ ap (_∙' α₂) (!-inv'-r α₁) ∙' ∙'-unit-l α₂

        -- the relation of this path and the one from CoherenceData
        path-lemma : ∀ {p₁ p₂ p₃ : BMPushout} (α₁ : p₁ == p₂) (α₂ : p₁ == p₃)
          → α₁α₁⁻¹α₂=α₂ α₁ α₂ == ! (Coh.α₁=α₂α₂⁻¹α₁ α₂ α₁)
        path-lemma idp idp = idp

  -- Make [r] free to apply identification elimination.
  code-coh : ∀ {b₁} (r : bmleft a₀ == bmright b₁) (s : hfiber bmglue r) → code-center r == [ s ]
  code-coh ._ (q₀₁ , idp) = code-coh-lemma q₀₁

  -- Finish the lemma.
  code-contr : ∀ {b₁} (r : bmleft a₀ == bmright b₁) → is-contr (Trunc (m +2+ n) (hfiber bmglue r))
  code-contr r = code-center r , Trunc-elim
    (λ _ → =-preserves-level Trunc-level) (code-coh r)

-- The final theorem.
-- It is sufficient to find some [q₀₀].
blakers-massey : ∀ {a₀ b₀} → has-conn-fibers (m +2+ n) (bmglue {a₀} {b₀})
blakers-massey {a₀} r = Trunc-rec
  (prop-has-level-S is-connected-is-prop)
  (λ{(_ , q₀₀) → code-contr q₀₀ r})
  (fst (f-conn a₀))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- An ATP conjecture must be used with postulates.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadConjecture1 where

data Bool : Set where
  false true : Bool

{-# ATP prove false #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

module function.surjective where

open import sum
open import equality
open import function.isomorphism.core
open import hott.level.core
open import hott.equivalence.core
open import hott.truncation

surjective : ∀ {i j}{A : Set i}{B : Set j} → (A → B) → Set _
surjective f = ∀ b → ∥ f ⁻¹ b ∥

retr⇒surj : ∀ {i j}{A : Set i}{B : Set j}
          → (f : A → B)
          → retraction f
          → surjective f
retr⇒surj f retr b = η (retr b)

inj+surj⇒eq : ∀ {i j}{A : Set i}{B : Set j}
            → h 2 A → h 2 B
            → (f : A → B)
            → injective f
            → surjective f
            → weak-equiv f
inj+surj⇒eq {A = A}{B = B} hA hB f inj surj b = retr-f b , propFib b (retr-f b)
  where
    propFib : (b : B) → prop (f ⁻¹ b)
    propFib b (a , p) (a' , p') = unapΣ (inj (p · sym p') , h1⇒prop (hB (f a') b) _ _)

    retr-f : retraction f
    retr-f b = Trunc-elim (prop⇒h1 (propFib b)) (λ x → x) (surj b)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------------
-- The Booleans properties
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Bool.Properties where

open import LTC-PCF.Base
open import LTC-PCF.Data.Bool
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Type

------------------------------------------------------------------------------
-- Congruence properties

notCong : ∀ {a b} → a ≡ b → not a ≡ not b
notCong refl = refl

------------------------------------------------------------------------------
-- Basic properties

t&&x≡x : ∀ b → true && b ≡ b
t&&x≡x b = if-true b

f&&x≡f : ∀ b → false && b ≡ false
f&&x≡f b = if-false false

not-t : not true ≡ false
not-t = if-true false

not-f : not false ≡ true
not-f = if-false true

&&-Bool : ∀ {a b} → Bool a → Bool b → Bool (a && b)
&&-Bool {b = b} btrue  Bb = subst Bool (sym (t&&x≡x b)) Bb
&&-Bool {b = b} bfalse Bb = subst Bool (sym (f&&x≡f b)) bfalse

not-Bool : ∀ {b} → Bool b → Bool (not b)
not-Bool btrue  = subst Bool (sym not-t) bfalse
not-Bool bfalse = subst Bool (sym not-f) btrue

&&-comm : ∀ {a b} → Bool a → Bool b → a && b ≡ b && a
&&-comm btrue  btrue  = refl
&&-comm btrue  bfalse = trans (t&&x≡x false) (sym (f&&x≡f true))
&&-comm bfalse btrue  = trans (f&&x≡f true) (sym (t&&x≡x false))
&&-comm bfalse bfalse = refl

x≢not-x : ∀ {b} → Bool b → b ≢ not b
x≢not-x btrue  h = t≢f (trans h not-t)
x≢not-x bfalse h = t≢f (sym (trans h not-f))

not-x≢x : ∀ {b} → Bool b → not b ≢ b
not-x≢x Bb h = x≢not-x Bb (sym h)

not-involutive : ∀ {b} → Bool b → not (not b) ≡ b
not-involutive btrue  = trans (notCong not-t) not-f
not-involutive bfalse = trans (notCong not-f) not-t

------------------------------------------------------------------------------
-- Properties with inequalities

lt-Bool : ∀ {m n} → N m → N n → Bool (lt m n)
lt-Bool nzero          nzero          = subst Bool (sym lt-00) bfalse
lt-Bool nzero          (nsucc {n} Nn) = subst Bool (sym (lt-0S n)) btrue
lt-Bool (nsucc {m} Nm) nzero          = subst Bool (sym (lt-S0 m)) bfalse
lt-Bool (nsucc {m} Nm) (nsucc {n} Nn) = subst Bool (sym (lt-SS m n)) (lt-Bool Nm Nn)

le-Bool : ∀ {m n} → N m → N n → Bool (le m n)
le-Bool {n = n} nzero         Nn             = subst Bool (sym (lt-0S n)) btrue
le-Bool        (nsucc Nm)     nzero          = subst Bool (sym (Sx≰0 Nm)) bfalse
le-Bool        (nsucc {m} Nm) (nsucc {n} Nn) =
  subst Bool (sym (lt-SS m (succ₁ n))) (le-Bool Nm Nn)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Sum | S

type
  _⊕_ : 2-ary | l30

term
  inl  : α  ->  α ⊕ β
  inr  : β  ->  α ⊕ β
  case : α ⊕ β  α.γ  β.γ  ->  γ

theory
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
-}

module Sum.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Sum.Signature

private
  variable
    Γ Δ Π : Ctx
    α β γ : ST
    𝔛 : Familyₛ

-- Inductive term declaration
module S:Terms (𝔛 : Familyₛ) where

  data S : Familyₛ where
    var  : ℐ ⇾̣ S
    mvar : 𝔛 α Π → Sub S Π Γ → S α Γ

    inl  : S α Γ → S (α ⊕ β) Γ
    inr  : S β Γ → S (α ⊕ β) Γ
    case : S (α ⊕ β) Γ → S γ (α ∙ Γ) → S γ (β ∙ Γ) → S γ Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Sᵃ : MetaAlg S
  Sᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (inlₒ  ⋮ a)         → inl  a
      (inrₒ  ⋮ a)         → inr  a
      (caseₒ ⋮ a , b , c) → case a b c
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Sᵃ = MetaAlg Sᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : S ⇾̣ 𝒜
    𝕊 : Sub S Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (inl  a)     = 𝑎𝑙𝑔 (inlₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (inr  a)     = 𝑎𝑙𝑔 (inrₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (case a b c) = 𝑎𝑙𝑔 (caseₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b , 𝕤𝕖𝕞 c)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Sᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ S α Γ) → 𝕤𝕖𝕞 (Sᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (inlₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (inrₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (caseₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ S ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : S ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Sᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : S α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub S Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (inl a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (inr a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (case a b c) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b | 𝕤𝕖𝕞! c = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
S:Syn : Syntax
S:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = S:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open S:Terms 𝔛 in record
    { ⊥ = S ⋉ Sᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax S:Syn public
open S:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Sᵃ public
open import SOAS.Metatheory S:Syn public


text:
module LibB where
import LibC

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Experiments.IsoInt where

open import Cubical.Experiments.IsoInt.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

module lib.cubical.Cubical where

open import lib.cubical.Square public
open import lib.cubical.Cube public

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Sum

module Examples.Colists.Auxiliary.MaxOf where

  max : ℕ → ℕ → ℕ
  max zero zero = zero
  max zero (suc y) = suc y
  max (suc x) zero = suc x
  max (suc x) (suc y) = suc (max x y)

  max-refl : (x y : ℕ) → (x ≡ max x y) ⊎ (y ≡ max x y)
  max-refl zero zero = inj₂ refl
  max-refl zero (suc y) = inj₂ refl
  max-refl (suc x) zero = inj₁ refl
  max-refl (suc x) (suc y) with max-refl x y
  max-refl (suc x) (suc y) | inj₁ eq = inj₁ (cong (λ x₁ → suc x₁) eq)
  max-refl (suc x) (suc y) | inj₂ eq = inj₂ (cong (λ x₁ → suc x₁) eq)

  max-refl-eq : ∀{x y z} → z ≡ max x y → z ≡ x ⊎ z ≡ y
  max-refl-eq {x} {y} {z} refl with max-refl x y
  max-refl-eq {x} {y} {.(max x y)} refl | inj₁ x₁ = inj₁ (sym x₁)
  max-refl-eq {x} {y} {.(max x y)} refl | inj₂ y₁ = inj₂ (sym y₁)

  max-self : ∀ {n} → n ≡ max n n
  max-self {zero} = refl
  max-self {suc n} = cong (λ x → suc x) max-self

  max-trans : ∀{x y z} → y ≡ max y z → x ≡ max x y → x ≡ max x z
  max-trans {zero} {zero} {zero} _ _ = refl
  max-trans {suc x} {zero} {zero} refl refl = refl
  max-trans {suc x} {suc y} {zero} refl _ = refl
  max-trans {suc x} {suc y} {suc z} eq eq1 =
    let eq-pred = cong pred eq in
    let eq1-pred = cong pred eq1 in
    cong suc (max-trans eq-pred eq1-pred)

  max-comm : ∀{x y z} → x ≡ max y z → x ≡ max z y
  max-comm {x} {zero} {zero} eq = eq
  max-comm {x} {suc y} {zero} eq = eq
  max-comm {x} {zero} {suc z} eq = eq
  max-comm {suc x} {suc y} {suc z} eq = cong suc (max-comm (cong pred eq))

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
data Unit : Set where
  unit : Unit

mutual

  data D : Unit → Set where
    c : (x : Unit) → F x x → D x

  F : Unit → Unit → Set
  F unit x = D x

Works : (x : Unit) → D x → Set₁
Works .x (c x p) with x
Works .x (c x p) | _  = Set

Fails : (x : Unit) → D x → Set₁
Fails y = Fails′ y
  where
  Fails′ : (x : Unit) → D x → Set₁
  Fails′ .x (c x p) with x
  Fails′ .x (c x p) | _  = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda