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

module Ch2-4 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2
open import Ch2-3

-- Definition 2.4.1 (homotopy)
infixl 8 _~_
_~_ : ∀ {a b} {A : Set a} {P : A → Set b}
  → (f g : (z : A) → P z)
  → Set (a ⊔ b)
_~_ {a} {b} {A} {P} f g = ∀ (x : A) → f x ≡ g x

-- Lemma 2.4.2

open import Relation.Binary

~-isEquivalence : ∀ {a b} {A : Set a} {P : A → Set b} → IsEquivalence (_~_ {A = A} {P})
~-isEquivalence = record
  { refl = ~-refl
  ; sym = ~-sym
  ; trans = ~-trans
  }
  where
    ~-refl : Reflexive _~_
    ~-refl f = refl
    ~-sym : Symmetric _~_
    ~-sym i~j x = ¬ (i~j x)
    ~-trans : Transitive _~_
    ~-trans i~j j~k x = i~j x ∙ j~k x

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

open import Function using (id; _∘_)

∘-cong-right : ∀ {a} {b} {c} {A : Set a} {B : Set b} {C : Set c} {g h : A → B}
  → (f : B → C)
  → g ~ h
  → f ∘ g ~ f ∘ h
∘-cong-right f g~h x = ap f (g~h x)

∘-cong-left : ∀ {a} {b} {c} {A : Set a} {B : Set b} {C : Set c} {g h : B → C}
  → (f : A → B)
  → g ~ h
  → g ∘ f ~ h ∘ f
∘-cong-left f g~h x = g~h (f x)

-- Lemma 2.4.3
Lemma-2-4-3 : ∀ {a b} {A : Set a} {B : Set b} {x y : A}
  → (f g : A → B)
  → (H : f ~ g)
  → (p : x ≡ y)
  → H x ∙ ap g p ≡ ap f p ∙ H y
Lemma-2-4-3 {a} {b} {A} {B} {x} {y} f g H p = J A D d x y p f g H
  where
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (f g : A → B) (H : f ~ g) → H x ∙ ap g p ≡ ap f p ∙ H y

    --              f(p)
    --      f(x) ========== f(y)
    --       ||              ||
    --  H(x) ||              ||  H(y)
    --       ||              ||
    --      g(x) ========== g(y)
    --              g(p)
    --
    d : (x : A) → D x x refl
    d x f g H =
      begin
        H x ∙ ap g refl
      ≈⟨ ap (λ w → H x ∙ w) (ap-refl g) ⟩
        H x ∙ refl
      ≈⟨ ¬ ∙-identityʳ (H x) ⟩
        H x
      ≈⟨ refl ⟩
        H x
      ≈⟨ ∙-identityˡ (H x) ⟩
        refl ∙ H x
      ≈⟨ ap (λ w → w ∙ H x) (¬ ap-refl f) ⟩
        ap f refl ∙ H x
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid (f x ≡ g x))

--              f(H(x))
--      f(x) ========== f(y)
--       ||              ||
--  H(x) ||              ||  H(y)
--       ||              ||
--      g(x) ========== g(y)
--              g(p)
--
-- Corollary 2.4.4
Corollary-2-4-4 : ∀ {a} {A : Set a}
  → (f : A → A)
  → (H : f ~ id)
  → (x : A)
  → H (f x) ≡ ap f (H x)
Corollary-2-4-4 {a} {A} f H x =
  begin
    H (f x)
  ≈⟨ ∙-identityʳ (H (f x)) ⟩
    H (f x) ∙ refl
  ≈⟨ ap [ H (f x) ]∙ (¬ ¬-identityˡ (H x)) ⟩
    H (f x) ∙ (H x ∙ ¬ H x)
  ≈⟨ ∙-assoc (H (f x)) (H x) (¬ H x) ⟩
    (H (f x) ∙ H x) ∙ ¬ H x
  ≈⟨ ap (λ w → (H (f x) ∙ w) ∙ ¬ H x) (¬ ap-id (H x)) ⟩
    (H (f x) ∙ ap id (H x)) ∙ ¬ H x
  ≈⟨ ap ∙[ ¬ H x ] (Lemma-2-4-3 f id H (H x)) ⟩
    (ap f (H x) ∙ H x) ∙ ¬ H x
  ≈⟨ ¬ ∙-assoc (ap f (H x)) (H x) (¬ H x) ⟩
    ap f (H x) ∙ (H x ∙ ¬ H x)
  ≈⟨ ap [ ap f (H x) ]∙ (¬-identityˡ (H x)) ⟩
    ap f (H x) ∙ refl
  ≈⟨ ¬ ∙-identityʳ (ap f (H x)) ⟩
    ap f (H x)
  ∎
  where
    open import Relation.Binary.Reasoning.Setoid (setoid _)

open import Data.Product

-- Definition 2.4.6
qinv : ∀ {a b} {A : Set a} {B : Set b}
  → (f : A → B)
  → Set (a ⊔ b)
qinv {a} {b} {A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g ~ id × g ∘ f ~ id)

-- Example 2.4.7
example-2-4-7 : ∀ {a} {A : Set a} → qinv (id {a} {A})
example-2-4-7 = id , ((λ x → refl) , λ x → refl)

-- Example 2.4.8
example-2-4-8-i : ∀ {a} {A : Set a} {x y z : A}
  → (p : x ≡ y)
  → qinv (λ (q : y ≡ z) → p ∙ q)
example-2-4-8-i {a} {A} {x} {y} {z} p = (λ q → ¬ p ∙ q) , (α , β)
  where
    α : (q : x ≡ z) → p ∙ (¬ p ∙ q) ≡ q
    α q =
      begin
        p ∙ (¬ p ∙ q)
      ≈⟨ ∙-assoc p (¬ p) q ⟩
        p ∙ ¬ p ∙ q
      ≈⟨ ap (λ w → w ∙ q) (¬-identityˡ p) ⟩
        refl ∙ q
      ≈⟨ ¬ ∙-identityˡ q ⟩
        q
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)
    β : (q : y ≡ z) → ¬ p ∙ (p ∙ q) ≡ q
    β q =
      begin
        ¬ p ∙ (p ∙ q)
      ≈⟨ ∙-assoc (¬ p) p q ⟩
        ¬ p ∙ p ∙ q
      ≈⟨ ap (λ w → w ∙ q) (¬-identityʳ p) ⟩
        refl ∙ q
      ≈⟨ ¬ ∙-identityˡ q ⟩
        q
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)

example-2-4-8-ii : ∀ {a} {A : Set a} {x y z : A}
  → (p : x ≡ y)
  → qinv (λ (q : z ≡ x) → q ∙ p)
example-2-4-8-ii {a} {A} {x} {y} {z} p = (λ q → q ∙ ¬ p) , α , β
  where
    α : (q : z ≡ y) → q ∙ ¬ p ∙ p ≡ q
    α q =
      begin
        q ∙ ¬ p ∙ p
      ≈⟨ ¬ ∙-assoc q (¬ p) p ⟩
        q ∙ (¬ p ∙ p)
      ≈⟨ ap (λ w → q ∙ w) (¬-identityʳ p) ⟩
        q ∙ refl
      ≈⟨ ¬ (∙-identityʳ q) ⟩
        q
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)
    β : (q : z ≡ x) → q ∙ p ∙ ¬ p ≡ q
    β q =
      begin
        q ∙ p ∙ ¬ p
      ≈⟨ ¬ ∙-assoc q p (¬ p) ⟩
        q ∙ (p ∙ ¬ p)
      ≈⟨ ap (λ w → q ∙ w) (¬-identityˡ p) ⟩
        q ∙ refl
      ≈⟨ ¬ (∙-identityʳ q) ⟩
        q
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)

example-2-4-9 : ∀ {a b} {A : Set a} {x y : A}
  → (P : A → Set b)
  → (p : x ≡ y)
  → qinv (transport P p)
example-2-4-9 {a} {b} {A} {x} {y} P p = (transport P (¬ p)) , α , β
  where
    α : (w : P y) → transport P p (transport P (¬ p) w) ≡ w
    α w =
      begin
        transport P p (transport P (¬ p) w)
      ≈⟨ lemma-2-3-9 P (¬ p) p w ⟩
        transport P (¬ p ∙ p) w
      ≈⟨ ap (λ q → transport P q w) (¬-identityʳ p) ⟩
        transport P refl w
      ≈⟨ refl ⟩
        w
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)

    β : (w : P x) → transport P (¬ p) (transport P p w) ≡ w
    β w =
      begin
        transport P (¬ p) (transport P p w)
      ≈⟨ lemma-2-3-9 P p (¬ p) w ⟩
        transport P (p ∙ ¬ p) w
      ≈⟨ ap (λ q → transport P q w) (¬-identityˡ p) ⟩
        transport P refl w
      ≈⟨ refl ⟩
        w
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (setoid _)

-- Definition 2.4.10
isequiv : ∀ {a b} {A : Set a} {B : Set b}
  → (f : A → B)
  → Set (a ⊔ b)
isequiv {a} {b} {A} {B} f =
  (Σ[ g ∈ (B → A) ] f ∘ g ~ id) × (Σ[ h ∈ (B → A) ] h ∘ f ~ id)

-- Property 2.4.10-i
Property-2-4-10-i : ∀ {a b} {A : Set a} {B : Set b}
  → (f : A → B)
  → qinv f
  → isequiv f
Property-2-4-10-i f (g , α , β) = (g , α) , (g , β)

-- Property 2.4.10-ii
Property-2-4-10-ii : ∀ {a b} {A : Set a} {B : Set b}
  → (f : A → B)
  → isequiv f
  → qinv f
Property-2-4-10-ii {a} {b} {A} {B} f ((g , α) , (h , β)) = g , (α , β')
  where
    --
    --      β           α
    --    g ~ h ∘ f ∘ g ~ h
    --
    γ : g ~ h
    γ x = ¬ (β (g x)) ∙ ap h (α x)

    β' : g ∘ f ~ id
    β' x = γ (f x) ∙ β x

-- Property 2.4.10-iii
-- Property-2-4-10-iii : ∀ {a b} {A : Set a} {B : Set b}
--   → (f : A → B)
--   → (e₁ e₂ : isequiv f)
--   → e₁ ≡ e₂
-- Property-2-4-10-iii {a} {b} {A} {B} f e₁ e₂ = {!   !}

-- Definition 2.4.11
_≅_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A ≅ B = Σ[ f ∈ (A → B) ] isequiv f

≅→ : ∀ {a b} {A : Set a} {B : Set b} → A ≅ B → A → B
≅→ (f , _) = f

-- Lemma 2.4.12-i
Lemma-2-4-12-i : ∀ {a} (A : Set a) → A ≅ A
Lemma-2-4-12-i A = id , Property-2-4-10-i id example-2-4-7

-- Lemma 2.4.12-ii
Lemma-2-4-12-ii : ∀ {a} {b} {A : Set a} {B : Set b}
  → A ≅ B
  → B ≅ A
Lemma-2-4-12-ii {a} {b} {A} {B} (f , f-isequiv) = f⁻¹ , f⁻¹-isequiv
  where
    f-qinv : qinv f
    f-qinv = Property-2-4-10-ii f f-isequiv

    f⁻¹ : B → A
    f⁻¹ = proj₁ f-qinv

    f⁻¹-qinv : qinv f⁻¹
    f⁻¹-qinv = f , (swap (proj₂ f-qinv))

    f⁻¹-isequiv : isequiv f⁻¹
    f⁻¹-isequiv = Property-2-4-10-i f⁻¹ f⁻¹-qinv

←≅ : ∀ {a b} {A : Set a} {B : Set b} → A ≅ B → B → A
←≅ = ≅→ ∘ Lemma-2-4-12-ii

-- Lemma 2.4.12-iii
Lemma-2-4-12-iii : ∀ {a} {b} {c} {A : Set a} {B : Set b} {C : Set c}
  → A ≅ B → B ≅ C → A ≅ C
Lemma-2-4-12-iii {a} {b} {c} {A} {B} {C} (g , g-isequiv) (f , f-isequiv)
  = (f ∘ g) , f∘g-isequiv
  where
    f-qinv : qinv f
    f-qinv = Property-2-4-10-ii f f-isequiv

    g-qinv : qinv g
    g-qinv = Property-2-4-10-ii g g-isequiv

    f⁻¹ : C → B
    f⁻¹ = proj₁ f-qinv

    f∘f⁻¹~id : f ∘ f⁻¹ ~ id
    f∘f⁻¹~id = proj₁ (proj₂ f-qinv)

    f⁻¹∘f~id : f⁻¹ ∘ f ~ id
    f⁻¹∘f~id = proj₂ (proj₂ f-qinv)

    g⁻¹ : B → A
    g⁻¹ = proj₁ g-qinv

    g∘g⁻¹~id : g ∘ g⁻¹ ~ id
    g∘g⁻¹~id = proj₁ (proj₂ g-qinv)

    g⁻¹∘g~id : g⁻¹ ∘ g ~ id
    g⁻¹∘g~id = proj₂ (proj₂ g-qinv)

    α : (f ∘ g) ∘ (g⁻¹ ∘ f⁻¹) ~ id
    α = begin
        (f ∘ g) ∘ (g⁻¹ ∘ f⁻¹)
      ≈⟨ (λ x → refl) ⟩
        f ∘ (g ∘ g⁻¹) ∘ f⁻¹
      ≈⟨ ∘-cong-right f (∘-cong-left f⁻¹ g∘g⁻¹~id) ⟩
        f ∘ id ∘ f⁻¹
      ≈⟨ (λ x → refl) ⟩
        f ∘ f⁻¹
      ≈⟨ f∘f⁻¹~id ⟩
        id
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (~-setoid _ _)

    β : (g⁻¹ ∘ f⁻¹) ∘ (f ∘ g) ~ id
    β = begin
        (g⁻¹ ∘ f⁻¹) ∘ (f ∘ g)
      ≈⟨ (λ x → refl) ⟩
        g⁻¹ ∘ (f⁻¹ ∘ f) ∘ g
      ≈⟨ ∘-cong-right g⁻¹ (∘-cong-left g f⁻¹∘f~id) ⟩
        g⁻¹ ∘ id ∘ g
      ≈⟨ (λ x → refl) ⟩
        g⁻¹ ∘ g
      ≈⟨ g⁻¹∘g~id ⟩
        id
      ∎
      where
        open import Relation.Binary.Reasoning.Setoid (~-setoid _ _)

    f∘g-qinv : qinv (f ∘ g)
    f∘g-qinv = (g⁻¹ ∘ f⁻¹) , α , β

    f∘g-isequiv : isequiv (f ∘ g)
    f∘g-isequiv = Property-2-4-10-i (f ∘ g) f∘g-qinv

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
-- Andreas, 2016-07-08 testing the access to definitions in where blocks

-- Anonymous where modules do export

pub0 = priv0
  module _ where
    priv0 = Set

works = priv0 -- Should succeed

-- Unnamed where modules don't export

pub = priv
  where
    priv = Set

fail = priv -- Should fail

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
open import cw.CW
open import homotopy.DisjointlyPointedSet
open import cohomology.Theory
open import cohomology.ChainComplex

module cw.cohomology.ReconstructedCochainsIsoCellularCochains {i : ULevel}
  (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  open import cw.cohomology.CellularChainComplex as CCC
  open import cw.cohomology.ReconstructedCochainComplex OT as RCC
  open import cw.cohomology.TipAndAugment OT
  open import cw.cohomology.WedgeOfCells OT

  private
    rcc-iso-ccc-nth : ∀ {n} (⊙skel : ⊙Skeleton n) {m} (m≤n : m ≤ n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      →  AbGroup.grp (RCC.cochain-template ⊙skel (inl m≤n))
      ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (inl m≤n))) (C2-abgroup 0)
    rcc-iso-ccc-nth ⊙skel {m = O}   (inl idp) ac
      =   FreeAbGroup-extend-iso (C2-abgroup 0)
      ∘eᴳ Πᴳ-emap-l (λ _ → C2 0) (separable-unite-equiv (⊙Skeleton.pt-dec ⊙skel))
      ∘eᴳ Πᴳ₁-⊔-iso-×ᴳ {A = Unit} {B = MinusPoint (⊙cw-head ⊙skel)} (λ _ → C2 0) ⁻¹ᴳ
      ∘eᴳ ×ᴳ-emap (Πᴳ₁-Unit ⁻¹ᴳ) (CX₀-β ⊙skel 0 ac)
    rcc-iso-ccc-nth ⊙skel {m = S m} (inl idp) ac
      =   FreeAbGroup-extend-iso (C2-abgroup 0)
      ∘eᴳ CXₙ/Xₙ₋₁-β-diag ⊙skel ac
    rcc-iso-ccc-nth ⊙skel {m = O} (inr ltS) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inl idp) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = S m} (inr ltS) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inl idp) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = O} (inr (ltSR lt)) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inr lt) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = S m} (inr (ltSR lt)) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inr lt) (⊙init-has-cells-with-choice ⊙skel ac)

    rcc-iso-ccc-above : ∀ {n} (⊙skel : ⊙Skeleton n) {m} (m≰n : ¬ (m ≤ n))
      →  AbGroup.grp (RCC.cochain-template ⊙skel (inr m≰n))
      ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (inr m≰n))) (C2-abgroup 0)
    rcc-iso-ccc-above ⊙skel _
      =   pre∘ᴳ-iso (C2-abgroup 0) lower-iso
      ∘eᴳ trivial-iso-Unit (hom₁-Unit-is-trivial (C2-abgroup 0)) ⁻¹ᴳ
      ∘eᴳ lower-iso

  rcc-iso-ccc : ∀ {n} (⊙skel : ⊙Skeleton n) (m : ℕ)
    → ⊙has-cells-with-choice 0 ⊙skel i
    →  AbGroup.grp (RCC.cochain-template ⊙skel (≤-dec m n))
    ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (≤-dec m n))) (C2-abgroup 0)
  rcc-iso-ccc {n} ⊙skel m ac with ≤-dec m n
  rcc-iso-ccc ⊙skel m ac | inl m≤n = rcc-iso-ccc-nth ⊙skel m≤n ac
  rcc-iso-ccc ⊙skel m ac | inr m≰n = rcc-iso-ccc-above ⊙skel m≰n

  rhead-iso-chead : C2 0 ≃ᴳ hom-group ℤ-group (C2-abgroup 0)
  rhead-iso-chead
    =   pre∘ᴳ-iso (C2-abgroup 0) ℤ-iso-FreeAbGroup-Unit
    ∘eᴳ FreeAbGroup-extend-iso (C2-abgroup 0)
    ∘eᴳ Πᴳ₁-Unit ⁻¹ᴳ

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module Examples.BooleanCircuits where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; subst)

open import Singleton
open import PiFrac
open import Reasoning

------------------------------------------------------------------------------
𝔹 𝔹² 𝔹³ 𝔹⁴ : 𝕌
𝔹   = 𝟙 +ᵤ 𝟙
𝔹²  = 𝔹 ×ᵤ 𝔹
𝔹³  = 𝔹 ×ᵤ 𝔹²
𝔹⁴  = 𝔹 ×ᵤ 𝔹³

CONTROLLED : {A : 𝕌} → (A ⟷ A) → 𝔹 ×ᵤ A ⟷ 𝔹 ×ᵤ A
CONTROLLED c = dist ⊚ (id⟷ ⊕ (id⟷ ⊗ c)) ⊚ factor

NOT : 𝔹 ⟷ 𝔹
NOT = swap₊

CNOT : 𝔹² ⟷ 𝔹²
CNOT = CONTROLLED NOT

TOFFOLI : 𝔹³ ⟷ 𝔹³
TOFFOLI = CONTROLLED (CONTROLLED NOT)

CTOFFOLI : 𝔹⁴ ⟷ 𝔹⁴
CTOFFOLI = CONTROLLED (CONTROLLED (CONTROLLED NOT))

-- Ancilla examples from literature

-- Fig. 2 in Ricercar

fig2a : 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ⟷
        𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹
fig2a = CONTROLLED (CONTROLLED (CONTROLLED NOT))

-- first write the circuit with the additional ancilla

fig2b' : ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) ⟷ ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹)
fig2b' =
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- first ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back
  ⊚
  (assocl⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ swap⋆) ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- second ccnot
  ⊚
  (id⟷ ⊗ swap⋆) ⊚
  assocl⋆ ⊚
  (assocr⋆ ⊗ id⟷)                      -- move it back
  ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocr⋆ ⊚
  (id⟷ ⊗ CONTROLLED (CONTROLLED NOT))  -- third ccnot
  ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷) ⊚
  assocl⋆ ⊚
  (swap⋆ ⊗ id⟷)                        -- move it back

------------------------------------------------------------------------------
-- Examples

PERES : (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹 ⟷ (𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹
PERES = (id⟷ ⊗ NOT) ⊚ assocr⋆ ⊚ (id⟷ ⊗ swap⋆) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ swap⋆) ⊚ (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚
        TOFFOLI ⊚
        (id⟷ ⊗ (NOT ⊗ id⟷)) ⊚ assocl⋆

SWAP12 SWAP23 SWAP13 ROTL ROTR : 𝟙 +ᵤ 𝟙 +ᵤ 𝟙 ⟷ 𝟙 +ᵤ 𝟙 +ᵤ 𝟙
SWAP12 = assocl₊ ⊚ (swap₊ ⊕ id⟷) ⊚ assocr₊
SWAP23 = id⟷ ⊕ swap₊
SWAP13 = SWAP23 ⊚ SWAP12 ⊚ SWAP23
ROTR   = SWAP12 ⊚ SWAP23
ROTL   = SWAP13 ⊚ SWAP23

pattern ?𝔽 = inj₁ tt
pattern ?𝕋 = inj₂ tt

-- this version might look more contrived that the fully expanded
-- one via pattern matching, but it generalizes better.
-- controlled f (b , a) = (b , [ (λ _ → a) , (λ _ → f a) ]′ b)

𝔽 𝕋 : ⟦ 𝔹 ⟧
𝔽 = inj₁ tt
𝕋 = inj₂ tt

not : ⟦ 𝔹 ⟧ → ⟦ 𝔹 ⟧
not ?𝔽 = 𝕋
not ?𝕋 = 𝔽

controlled : ∀ {A} → (⟦ A ⟧ → ⟦ A ⟧) → ⟦ 𝔹 ⟧ × ⟦ A ⟧ → ⟦ 𝔹 ⟧ × ⟦ A ⟧
controlled f (?𝔽 , a) = (𝔽 , a  )
controlled f (?𝕋 , a) = (𝕋 , f a)

t3 : ∀ {b₁ b₂} →
     ● (𝔹 ×ᵤ 𝔹²) [ 𝔽 , (b₁ , b₂) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ 𝔽 , (b₁ , b₂) ]
t3 = lift TOFFOLI

{--
The following do not typecheck. Good

t4 : ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝔽 , 𝔽) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝔽 , 𝕋) ]
t4 = lift TOFFOLI

t5 : ∀ {b₁ b₂} →
     ● (𝔹 ×ᵤ 𝔹²) [ b₁ , (𝔽 , b₂) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ b₁ , (𝔽 , b₂) ]
t5 = lift TOFFOLI
--}

t6 : ∀ {b} →
     ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝕋 , b) ] ⟷
     ● (𝔹 ×ᵤ 𝔹²) [ 𝕋 , (𝕋 , eval NOT b) ]
t6 = lift TOFFOLI

NEG1 NEG2 NEG3 NEG4 NEG5 : 𝔹 ⟷ 𝔹
NEG1 = swap₊
NEG2 = id⟷ ⊚ NOT
NEG3 = NOT ⊚ NOT ⊚ NOT
NEG4 = NOT ⊚ id⟷
NEG5 = uniti⋆l ⊚ swap⋆ ⊚ (NOT ⊗ id⟷) ⊚ swap⋆ ⊚ unite⋆l
NEG6 = uniti⋆r ⊚ (NOT ⊗ id⟷) ⊚ unite⋆r -- same as above, but shorter

zigzag : ∀ b → ● 𝔹 [ b ] ⟷ ● 𝔹 [ b ]
zigzag b =
  uniti⋆l ⊚                -- ONE * POINTED TWO
  (η b ⊗ id⟷) ⊚          -- (POINTED TWO * RECIP TWO) * POINTED TWO
  assocr⋆ ⊚                -- POINTED TWO * (RECIP TWO * POINTED TWO)
  (id⟷ ⊗ swap⋆) ⊚         -- POINTED TWO * (POINTED TWO * RECIP TWO)
  (id⟷ ⊗ ε b) ⊚           -- POINTED TWO * ONE
  unite⋆r

test1 = eval (zigzag 𝔽) (𝔽 , refl)      -- (⇑ #f refl)
-- test2 = eval (zigzag 𝔽) (𝕋 , refl)   -- typechecks if given proof #f=#t
-- test3 = eval (zigzag 𝕋) (𝔽 , refl)   -- typechecks if given proof #f=#t
test4 = eval (zigzag 𝕋) (𝕋 , refl)      -- (⇑ #t refl)

zigzagU : ⟦ 𝔹 ⟧ → ⟦ 𝔹 ⟧
zigzagU b = unfocus (eval (zigzag b) (focus b))

-- then prove a theorem that specifies its semantics

fig2b'≡ : (a b c d : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , 𝔽)) ≡ 𝔽
fig2b'≡ a         (inj₁ tt) c d = refl
fig2b'≡ (inj₁ tt) (inj₂ tt) c d = refl
fig2b'≡ (inj₂ tt) (inj₂ tt) c d = refl

-- generalize above?  Method:
-- for 'dist' to evaluate, need to split on b first
--   in first case, split on e (same reason)
--   in second case, split on a (same reason)
--     split on e
--     split on e
foo : (a b c d e : ⟦ 𝔹 ⟧) →
          proj₂ (eval fig2b' ((a , b , c , d) , e)) ≡ e
foo a         (inj₁ x) c d (inj₁ x₁) = refl
foo a         (inj₁ x) c d (inj₂ y)  = refl
foo (inj₁ x)  (inj₂ y) c d (inj₁ x₁) = refl
foo (inj₁ x)  (inj₂ y) c d (inj₂ y₁) = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₁ x)  = refl
foo (inj₂ y₁) (inj₂ y) c d (inj₂ y₂) = refl

postulate
  -- boring...
  tensor4 : ∀ {a b c d e} →
          (● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ])  ×ᵤ ● 𝔹 [ e ] ⟷
          ● ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) [ (a , b , c , d) , e ]
  itensor4 : ∀ {a b c d e} →
          ● ((𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹 ×ᵤ 𝔹) ×ᵤ 𝔹) [ (a , b , c , d) , e ] ⟷
          (● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ])  ×ᵤ ● 𝔹 [ e ]

-- now lift it

fig2b : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ] ⟷
           ● 𝔹 [ x ] ×ᵤ ● 𝔹 [ y ] ×ᵤ ● 𝔹 [ z ] ×ᵤ ● 𝔹 [ w ]
fig2b {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (((== id⟷ (cong (λ H → ((x , y , z , w)) , H) (foo a b c d e))) ⊗ id⟷)) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ ε e) ⊚
        unite⋆r

-- This is mostly to show that == is really 'subst' in hiding.
fig2b₂ : ∀ {a b c d e} →
        let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
        in
           ● 𝔹 [ a ] ×ᵤ ● 𝔹 [ b ] ×ᵤ ● 𝔹 [ c ] ×ᵤ ● 𝔹 [ d ] ⟷
           ● 𝔹 [ x ] ×ᵤ ● 𝔹 [ y ] ×ᵤ ● 𝔹 [ z ] ×ᵤ ● 𝔹 [ w ]
fig2b₂ {a} {b} {c} {d} {e} =
  let ((x , y , z , w) , u) = eval fig2b' ((a , b , c , d) , e)
  in    uniti⋆r ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝟙[e]
        (id⟷ ⊗ η e) ⊚
        -- (●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × (●𝔹[e] x ●1/𝔹[e])
        assocl⋆ ⊚
        -- ((●𝔹[a] × ●𝔹[b] × ●𝔹[c] × ●𝔹[d]) × ●𝔹[e) x ●1/𝔹[e]
        (tensor4 ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (a,b,c,d),e ] x ●1/𝔹[e]
        (lift fig2b' ⊗ id⟷) ⊚
         -- ● ((𝔹 × 𝔹 × 𝔹 × 𝔹) × 𝔹) [ (x,y,z,w),e ] x ●1/𝔹[e]
        (itensor4 ⊗ id⟷) ⊚
         -- ((●𝔹[x] × ●𝔹[y] × ●𝔹[z] × ●𝔹[w]) × ●𝔹[e]) x ●1/𝔹[e]
        assocr⋆ ⊚
        (id⟷ ⊗ (subst (λ ee → ● 𝔹 [ ee ] ×ᵤ 𝟙/● 𝔹 [ e ] ⟷ 𝟙) (sym (foo a b c d e)) (ε e))) ⊚
        unite⋆r

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Agda.Primitive
open import Prelude
import GSeTT.Typed-Syntax
import Globular-TT.Syntax

{- Type theory for globular sets -}
module Globular-TT.Eqdec-syntax {l}
  (index : Set l) (eqdec-index : eqdec index) where

  open import Globular-TT.Syntax index

  eqdec-Ty : eqdec Pre-Ty
  eqdec-Tm : eqdec Pre-Tm
  eqdec-Sub : eqdec Pre-Sub

  eqdec-Ty ∗ ∗ = inl idp
  eqdec-Ty ∗ (⇒ _ _ _) = inr λ{()}
  eqdec-Ty (⇒ _ _ _ ) ∗ = inr λ{()}
  eqdec-Ty (⇒ A t u) (⇒ B t' u') with eqdec-Ty A B | eqdec-Tm t t' | eqdec-Tm u u'
  ...                            | inl idp | inl idp | inl idp = inl idp
  ...                            | inr A≠B | _ | _ = inr λ{idp → A≠B idp}
  ...                            | inl idp | inr t≠t' | _ = inr λ eq → t≠t' (snd (fst (=⇒ eq)))
  ...                            | inl idp | inl idp | inr u≠u' = inr λ eq → u≠u' (snd (=⇒ eq))
  eqdec-Tm (Var x) (Var y) with eqdecℕ x y
  ...                      | inl idp = inl idp
  ...                      | inr x≠y = inr λ {idp → x≠y idp}
  eqdec-Tm (Var _) (Tm-constructor _ _) = inr λ{()}
  eqdec-Tm (Tm-constructor _ _) (Var _) = inr λ{()}
  eqdec-Tm (Tm-constructor i γ) (Tm-constructor i' γ') with eqdec-index i i' | eqdec-Sub γ γ'
  ...                                                   | inl idp | inl idp = inl idp
  ...                                                   | inr i≠i' | _ = inr λ{idp → i≠i' idp}
  ...                                                   | inl idp | inr γ≠γ' = inr λ eq → γ≠γ' (snd (=Tm-constructor eq))
  eqdec-Sub <> <> = inl idp
  eqdec-Sub < _ , _ ↦ _ > <> = inr λ{()}
  eqdec-Sub <> < _ , _ ↦ _ > = inr λ{()}
  eqdec-Sub < γ , x ↦ t > < γ' , y ↦ t' > with eqdec-Sub γ γ' | eqdecℕ x y | eqdec-Tm t t'
  ...                                      | inl idp | inl idp | inl idp = inl idp
  ...                                      | inr γ≠γ' | _ | _ = inr λ{idp → γ≠γ' idp}
  ...                                      | inl idp | inr x≠y | _ = inr λ eq → x≠y (snd (fst (=<,> eq)))
  ...                                      | inl idp | inl idp | inr t≠t' = inr λ eq → t≠t' (snd (=<,> eq))

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

open import HoTT

-- an attempt to speed up [QuotGroup (quot-of-sub (ker-prop ...) (im-nprop ...))]
-- which removes most intermediate constructions

module groups.KernelImage {i j k}
  {G : Group i} {H : Group j} {K : Group k}
  (ψ : H →ᴳ K) (φ : G →ᴳ H) (H-ab : is-abelian H) where

  --  G ---φ--→ᴳ H ---ψ--→ᴳ K

  private
    module G = Group G
    module H = AbGroup (H , H-ab)
    module K = Group K
    module ψ = GroupHom ψ
    module φ = GroupHom φ

    ker-El : Type (lmax j k)
    ker-El = Σ H.El (λ h → ψ.f h == K.ident)

    ker-subtype : SubtypeProp H.El k
    ker-subtype = (λ h → ψ.f h == K.ident) , level
      where abstract level : ∀ h → is-prop (ψ.f h == K.ident)
                     level h = K.El-is-set _ _

  ker-El=-out = Subtype=-out ker-subtype

  ker/im-rel' : Rel H.El (lmax i j)
  ker/im-rel' h₁ h₂ = Trunc -1 (hfiber φ.f (H.diff h₁ h₂))

  ker/im-rel : Rel ker-El (lmax i j)
  ker/im-rel (h₁ , _) (h₂ , _) = Trunc -1 (hfiber φ.f (H.diff h₁ h₂))

  private
    ker/im-El : Type (lmax (lmax i j) k)
    ker/im-El = SetQuot ker/im-rel

  ker/im-struct : GroupStructure ker/im-El
  ker/im-struct = record {M} where
    module M where
      ident : ker/im-El
      ident = q[ H.ident , lemma ]
        where abstract lemma = ψ.pres-ident

      inv : ker/im-El → ker/im-El
      inv = SetQuot-rec SetQuot-level inv' inv-rel
        where
          inv' : ker-El → ker/im-El
          inv' (h , ψh=0) = q[ H.inv h , lemma ]
            where abstract lemma = ψ.pres-inv h ∙ ap K.inv ψh=0 ∙ K.inv-ident

          abstract
            inv-rel : ∀ {ker₁ ker₂} → ker/im-rel ker₁ ker₂ → inv' ker₁ == inv' ker₂
            inv-rel {h₁ , _} {h₂ , _} = Trunc-rec (SetQuot-level _ _)
              λ{(g , φg=h₁h₂⁻¹) → quot-rel
                [ G.inv g , φ.pres-inv g ∙ ap H.inv φg=h₁h₂⁻¹
                          ∙ H.inv-diff h₁ h₂ ∙ H.comm h₂ (H.inv h₁)
                          ∙ ap (H.comp (H.inv h₁)) (! (H.inv-inv h₂)) ]}

      comp : ker/im-El → ker/im-El → ker/im-El
      comp = SetQuot-rec level comp' comp-rel where
        abstract
          level : is-set (ker/im-El → ker/im-El)
          level = →-is-set SetQuot-level

        comp' : ker-El → ker/im-El → ker/im-El
        comp' (h₁ , ψh₁=0) = SetQuot-rec SetQuot-level comp'' comp'-rel where

          comp'' : ker-El → ker/im-El
          comp'' (h₂ , ψh₂=0) = q[ H.comp h₁ h₂ , lemma ]
            where abstract lemma = ψ.pres-comp h₁ h₂ ∙ ap2 K.comp ψh₁=0 ψh₂=0
                                 ∙ K.unit-l K.ident

          abstract
            comp'-rel : ∀ {ker₂ ker₂'} → ker/im-rel ker₂ ker₂' → comp'' ker₂ == comp'' ker₂'
            comp'-rel {h₂ , _} {h₂' , _} = Trunc-rec (SetQuot-level _ _)
              λ{(g , φg=h₂h₂'⁻¹) → quot-rel
                [ g , ! ( ap (H.comp (H.comp h₁ h₂)) (H.inv-comp h₁ h₂')
                        ∙ H.assoc h₁ h₂ (H.comp (H.inv h₂') (H.inv h₁))
                        ∙ ap (H.comp h₁) (! $ H.assoc h₂ (H.inv h₂') (H.inv h₁))
                        ∙ H.comm h₁ (H.comp (H.comp h₂ (H.inv h₂')) (H.inv h₁))
                        ∙ H.assoc (H.comp h₂ (H.inv h₂')) (H.inv h₁) h₁
                        ∙ ap2 H.comp (! φg=h₂h₂'⁻¹) (H.inv-l h₁)
                        ∙ H.unit-r (φ.f g) )]}

        abstract
          comp-rel : ∀ {ker₁ ker₁'} → ker/im-rel ker₁ ker₁' → comp' ker₁ == comp' ker₁'
          comp-rel {h₁ , _} {h₁' , _} = Trunc-rec (level _ _)
            λ{(g , φg=h₁h₁'⁻¹) → λ= $ SetQuot-elim (λ _ → =-preserves-set SetQuot-level)
              (λ{(h₂ , _) → quot-rel
                  [ g , ! ( ap (H.comp (H.comp h₁ h₂)) (H.inv-comp h₁' h₂)
                          ∙ H.assoc h₁ h₂ (H.comp (H.inv h₂) (H.inv h₁'))
                          ∙ ap (H.comp h₁) ( ! (H.assoc h₂ (H.inv h₂) (H.inv h₁'))
                                          ∙ ap (λ h → H.comp h (H.inv h₁')) (H.inv-r h₂)
                                          ∙ H.unit-l (H.inv h₁'))
                          ∙ ! φg=h₁h₁'⁻¹ )]})
              (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))}

      abstract
        unit-l : ∀ k/i → comp ident k/i == k/i
        unit-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ{(h , _) → ap q[_] $ ker-El=-out (H.unit-l h)})
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

        assoc : ∀ k/i₁ k/i₂ k/i₃ → comp (comp k/i₁ k/i₂) k/i₃ == comp k/i₁ (comp k/i₂ k/i₃)
        assoc = SetQuot-elim
          (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
          (λ{(h₁ , _) → SetQuot-elim
            (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
            (λ{(h₂ , _) → SetQuot-elim
              (λ _ → =-preserves-set SetQuot-level)
              (λ{(h₃ , _) → ap q[_] $ ker-El=-out (H.assoc h₁ h₂ h₃)})
              (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))})
            (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _))})
          (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → SetQuot-level _ _))

        inv-l : ∀ k/i → comp (inv k/i) k/i == ident
        inv-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ{(h , _) → ap q[_] $ ker-El=-out (H.inv-l h)})
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

  Ker/Im : Group (lmax i (lmax j k))
  Ker/Im = group _ SetQuot-level ker/im-struct

  module Ker/Im = Group Ker/Im

  {- correctness -}

  Ker/Im-β : Ker/Im ≃ᴳ QuotGroup (quot-of-sub (ker-propᴳ ψ) (im-npropᴳ φ H-ab))
  Ker/Im-β = ≃-to-≃ᴳ (ide _) to-pres-comp where
    abstract
      to-pres-comp : preserves-comp Ker/Im.comp
        (QuotGroup.comp (quot-of-sub (ker-propᴳ ψ) (im-npropᴳ φ H-ab))) (idf _)
      to-pres-comp = SetQuot-elim
        (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
        (λ _ → SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (λ _ → ap q[_] $ ker-El=-out idp)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _)))
        (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _))


text:
open import Data.Graph

module Data.Graph.Path.Search {ℓᵥ ℓₑ} (g : FiniteGraph ℓᵥ ℓₑ) where

open import Data.Graph.Path.Cut g
open import Data.Graph.Path.Finite g
open import Data.Product as Σ
open import Data.Sum as ⊎
open import Data.Vec as Vec
open import Finite
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary hiding (module Dec)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation as ¬

open FiniteGraph g
open IsFinite

pathSearchFrom : ∀ {ℓ} {P : Vertex → Set ℓ} →
  (∀ b → Dec (P b)) → ∀ a → Dec (∃ λ b → P b × ∃ (Path a b))
pathSearchFrom P? a =
  case ∃? (Path≤-finite (size vertexFinite) a) (P? ∘ proj₁) of λ where
    (yes ((_ , _ , _ , p) , pb)) → yes (-, pb , (-, p))
    (no ¬p) → no λ where (_ , pb , _ , p) → ¬p ((-, shortEnoughPath p) , pb)

pathSearchAcyclicFrom : ∀ {ℓ} {P : Vertex → Set ℓ} →
  (∀ b → Dec (P b)) → ∀ a →
  Dec (∃ λ b → P b × ∃₂ λ n (p : Path a b n) → Acyclic p)
pathSearchAcyclicFrom P? a =
  case ∃? (Path≤-finite (size vertexFinite) a) (P? ∘ proj₁) of λ where
    (yes ((_ , _ , _ , p) , pb)) →
      let (x , x≤n , p′) , ¬r′ = acyclicPath p in
        yes (-, pb , (-, (p′ , ¬r′)))
    (no ¬p) → no λ where (_ , pb , _ , p , r) → ¬p ((-, shortEnoughPath p) , pb)

pathSearchBetween : ∀ a b → Dec (∃ (Path a b))
pathSearchBetween a b =
  case pathSearchFrom (decEqVertex b) a of λ where
    (yes (_ , refl , p)) → yes p
    (no ¬p) → no λ where (n , p) → ¬p (-, refl , -, p)

searchFrom : ∀ {ℓ} {P : Vertex → Set ℓ} →
  (∀ b → Dec (P b)) →
  ∀ a → Dec (∃ λ b → P b × Star Edge a b)
searchFrom P? a =
  Dec.map′
    (Σ.map₂ (Σ.map₂ (toStar ∘ proj₂)))
    (Σ.map₂ (Σ.map₂ (-,_ ∘ fromStar)))
    (pathSearchFrom P? a)

searchBetween : ∀ a b → Dec (Star Edge a b)
searchBetween a b = Dec.map′ (toStar ∘ proj₂) (-,_ ∘ fromStar) (pathSearchBetween a b)

module _
  {ℓ ℓ≈ ℓ<}
  {P : Vertex → Set ℓ} (P? : ∀ a → Dec (P a))
  {_≈_ : ∀ {a} → Rel (∃ (Star Edge a)) ℓ≈}
  {_<_ : ∀ {a} → Rel (∃ (Star Edge a)) ℓ<}
  (<-po : ∀ {a} → IsDecStrictPartialOrder (_≈_ {a}) _<_)
  where

  record MaximalPath a : Set (ℓ ⊔ ℓᵥ ⊔ ℓₑ ⊔ ℓ<) where
    field
      destination : Vertex
      predicate : P destination
      path : Star Edge a destination
      acyclic : Acyclic (fromStar path)
      isMax : ∀
        {b} (p : Star Edge a b) (pb : P b) → Acyclic (fromStar p) →
        ¬ ((-, path) < (-, p))

  searchMaximalFrom : ∀ a → Dec (MaximalPath a)
  searchMaximalFrom a =
    case max of λ where
      (inj₁ ¬p) →
        no λ mp →
          let open MaximalPath mp in
            ¬p ((-, path , fromWitness acyclic) , fromWitness predicate)

      (inj₂ (((b , p , acp) , pb) , isMax)) →
        yes record
          { destination = b
          ; predicate = toWitness pb
          ; path = p
          ; acyclic = toWitness acp
          ; isMax = λ q pb acq → isMax ((-, q , fromWitness acq) , fromWitness pb)
          }
    where
      module DPO = IsDecStrictPartialOrder <-po

      _≈′_ = _≈_ on λ where ((b , p , acp) , pb) → b , p
      _<′_ = _<_ on λ where ((b , p , acp) , pb) → b , p

      <′-IsDecStrictPartialOrder : IsDecStrictPartialOrder _≈′_ _<′_
      <′-IsDecStrictPartialOrder = record
        { isStrictPartialOrder = record
          { isEquivalence = record
            { refl = IsEquivalence.refl DPO.isEquivalence
            ; sym = IsEquivalence.sym DPO.isEquivalence
            ; trans = IsEquivalence.trans DPO.isEquivalence
            }
          ; irrefl = DPO.irrefl
          ; trans = DPO.trans
          ; <-resp-≈ = proj₁ DPO.<-resp-≈ , proj₂ DPO.<-resp-≈
          }
        ; _≟_ = λ _ _ → _ DPO.≟ _
        ; _<?_ = λ _ _ → _ DPO.<? _
        }

      acyclicPaths = filter (AcyclicStar-finite a) (P? ∘ proj₁)

      open Ordered acyclicPaths <′-IsDecStrictPartialOrder


text:
open import Agda.Builtin.Bool

impor Agda.Builtin.Nat

import Agda.Builtin.Sigma

module issue4888 where

max_stars_repo_name: jappeace/agda

max_issues_repo_name: jappeace/agda

max_forks_repo_name: jappeace/agda


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

module Data.Binary.Tests.Addition where

import Data.Binary.Operations.Addition as 𝔹
open import Data.Binary.Tests.Helpers
open import Relation.Binary.PropositionalEquality
import Data.Nat as ℕ

_ : 𝔹._+_ ≡⌈ 60 ⌉₂≡ ℕ._+_
_ = refl

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how the Record module can be used
------------------------------------------------------------------------

-- Taken from Randy Pollack's paper "Dependently Typed Records in Type
-- Theory".

module README.Record where

open import Data.Product
open import Data.String
open import Function using (flip)
open import Level
import Record
open import Relation.Binary

-- Let us use strings as labels.

open Record String _≟_

-- Partial equivalence relations.

PER : Signature _
PER = ∅ , "S"     ∶ (λ _ → Set)
        , "R"     ∶ (λ r → r · "S" → r · "S" → Set)
        , "sym"   ∶ (λ r → Lift (Symmetric (r · "R")))
        , "trans" ∶ (λ r → Lift (Transitive (r · "R")))

-- Given a PER the converse relation is also a PER.

converse : (P : Record PER) →
           Record (PER With "S" ≔ (λ _ → P · "S")
                       With "R" ≔ (λ _ → flip (P · "R")))
converse P =
  Rec′⇒Rec
    (PER With "S" ≔ (λ _ → P · "S")
         With "R" ≔ (λ _ → flip (P · "R")))
    ((((_ ,) ,) , lift λ {_} → lower (P · "sym")) ,
     (lift λ {_} yRx zRy → lower (P · "trans") zRy yRx))


text:
module Golden.FstSnd where

open import Agda.Builtin.Nat

data Tuple a b : Set where
  Tup : a -> b -> Tuple a b

fst : {a b : Set} -> Tuple a b -> a
fst (Tup x x₁) = x
snd : {a b : Set} -> Tuple a b -> b
snd (Tup x b) = b

tup1 : Tuple Nat Nat
tup1 = Tup 0 1

a = fst tup1
b = snd tup1

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


text:
{-# OPTIONS --cubical #-}
module _ where

open import Agda.Builtin.Equality

-- Option --cubical implies --without-K
uip : {A : Set} {x : A} (p : x ≡ x) → p ≡ refl
uip refl = refl


text:
-- Check that checking of left-hand sides are postponed properly
-- when the type of an argument that is matched on is a meta.

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data X : Set where
  zero : X

easy : _ → Nat
easy (suc n) = n
easy zero    = zero

-- TODO: uncomment below once LHS postponing is actually implemented

-- hard : _ → Nat
-- hard zero    = zero
-- hard (suc n) = hard n

-- _$_ : {A B : Set} → (A → B) → A → B
-- f $ x = f x

-- plam : Nat
-- plam = (λ { zero → zero; (suc n) → n }) $ suc zero


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
module FLComm (n : ℕ) where

open import Level renaming ( suc to Suc ; zero to Zero ) hiding (lift)
open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
open import Data.Fin.Permutation
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality hiding ( [_] ) renaming ( sym to ≡-sym )
open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
open import Data.Product hiding (_,_ )
open import Relation.Nullary
open import Data.Unit hiding (_≤_)
open import Data.Empty
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions hiding (Symmetric )
open import logic
open import nat

open import FLutil
open import Putil
import Solvable
open import Symmetric

-- infixr  100 _::_

open import Relation.Nary using (⌊_⌋)
open import Data.List.Fresh hiding ([_])
open import Data.List.Fresh.Relation.Unary.Any

open import Algebra
open Group (Symmetric n) hiding (refl)
open Solvable (Symmetric n)
open _∧_
-- open import Relation.Nary using (⌊_⌋)
open import Relation.Nullary.Decidable hiding (⌊_⌋)

open import fin

-- all cobmbination in P and Q (could be more general)
record AnyComm {n m l : ℕ}  (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where
   field
     commList : FList l
     commAny : (p : FL n) (q : FL m)
         → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q
         → Any (fpq p q ≡_) commList

-------------
--    (p,q)   (p,qn) ....           (p,q0)
--    pn,q
--     :        AnyComm FL0 FL0 P  Q
--    p0,q

open AnyComm
anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l)  → AnyComm P Q fpq
anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () }
anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () }
anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () }
anyComm {n} {m} {l} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where
  commListP : (P1 : FList n) → FList l
  commListP [] = commList (anyComm P Q fpq)
  commListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (commListP P1)
  commListQ : (Q1 : FList m) → FList l
  commListQ [] = commListP P
  commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1)
  anyc0n : (p₁ : FL n) (q₁ : FL m) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr)
    → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q))
  anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q )
  anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where
     anyc01 : (Q1 : FList m) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
     anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _
     anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any)
  anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where
     anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1  → Any (_≡_ (fpq p₁ q₁)) (commListP P1)
     anyc03 (cons a P1 x) (here refl) = x∈FLins _ _
     anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any)
     anyc02 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
     anyc02 [] = anyc03 P anyp
     anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1)
  anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where
     anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1)
     anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq
     anyc05 (cons a P1 x) = insAny _ (anyc05 P1)
     anyc04 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1)
     anyc04 [] = anyc05 P
     anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)

-------------
--    # 0 :: # 0 :: # 0 : # 0 :: f0
--    # 0 :: # 0 :: # 1 : # 0 :: f0
--    # 0 :: # 1 :: # 0 : # 0 :: f0
--    # 0 :: # 1 :: # 1 : # 0 :: f0
--    # 0 :: # 2 :: # 0 : # 0 :: f0
--       ...
--    # 3 :: # 2 :: # 0 : # 0 :: f0
--    # 3 :: # 2 :: # 1 : # 0 :: f0

-- all FL
record AnyFL (n : ℕ) : Set where
   field
     allFL : FList n
     anyP : (x : FL n) → Any (x ≡_ ) allFL

open AnyFL

--   all FL as all combination
--      anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n)

anyFL01 :  (n : ℕ) → AnyFL (suc n)
anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl }  where
     anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y
     anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl
anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
     anyFL05 : {n i : ℕ} → (i < suc n) → FList (suc n)
     anyFL05 {_} {0} (s≤s z≤n) = zero :: FL0 ∷# []
     anyFL05 {n} {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {n} {i} (<-trans i<n a<sa))
     anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n}  → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n))
     anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin
                toℕ x                               ≡⟨ eq ⟩
                suc i                               ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _ )) ⟩
                suc (toℕ (fromℕ< (≤-pred i<n)) )
          ∎ ) where open ≡-Reasoning
     anyFL06 : {n i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n)
     anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl
     anyFL06 {n} {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i)
     ... | tri< a ¬b ¬c = insAny _ (anyFL06 (<-trans (s≤s i<n) a<sa) x a)
     ... | tri≈ ¬a b ¬c = subst (λ k →  Any (_≡_ (x :: FL0)) (FLinsert (k :: FL0) (anyFL05 {n} {i} (<-trans (s≤s i<n) a<sa))))
                  (anyFL08 {n} {i} {x} {s≤s (s≤s i<n)} b) (x∈FLins (x :: FL0)  (anyFL05 {n} {i} (<-trans (s≤s i<n) a<sa)))
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) )
     anyC = anyComm (anyFL05 a<sa) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
     anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
     anyFL02 (x :: y) = commAny anyC (x :: FL0) y
                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyFL06 a<sa (fromℕ< x≤n) fin<n) ) (anyP (anyFL01 n) y) where
         x≤n : suc (toℕ x)  ≤ suc (suc n)
         x≤n = toℕ<n x

anyFL :  (n : ℕ) → AnyFL n
anyFL zero = record { allFL = f0 ∷# [] ; anyP = anyFL4 } where
    anyFL4 : (x : FL zero) → Any (_≡_ x) ( f0 ∷# [] )
    anyFL4 f0 = here refl
anyFL (suc n) = anyFL01 n

at1 = proj₁ (toList (allFL (anyFL 1)))
at2 = proj₁ (toList (allFL (anyFL 2)))
at3 = proj₁ (toList (allFL (anyFL 3)))
at4 = proj₁ (toList (allFL (anyFL 4)))

CommFListN  : ℕ →  FList n
CommFListN  zero = allFL (anyFL n)
CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))

CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
CommStage→ zero x (Level.lift tt) = anyP (anyFL n) (perm→FL x)
CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 where
  G = perm→FL g
  H = perm→FL h
  comm3 :  perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
  comm3 = begin
              perm→FL [ FL→perm G , FL→perm H ]
           ≡⟨ pcong-pF (comm-resp (FL←iso _) (FL←iso _)) ⟩
              perm→FL [ g , h ]
          ∎  where open ≡-Reasoning
  comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i))
  comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3
     ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) )
CommStage→ (suc i) x (ccong {f} {x} eq p) =
      subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))))
          (comm4 eq) (CommStage→ (suc i) f p ) where
   comm4 : f =p= x →  perm→FL f ≡ perm→FL x
   comm4 = pcong-pF

CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
module _ where

open import Common.Prelude renaming (_∸_ to _-_) -- work-around for #1855

data Acc {a} {A : Set a} (_<_ : A → A → Set) (x : A) : Set a where
  acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x

data _<_ : Nat → Nat → Set where
  zero : ∀ {n} → zero < suc n
  suc  : ∀ {n m} → n < m → suc n < suc m

_≤_ : Nat → Nat → Set
n ≤ m = n < suc m

data LeqView (n : Nat) : Nat → Set where
  less : ∀ {m} → n < m → LeqView n m
  equal : LeqView n n

leqView : ∀ {n m} → n ≤ m → LeqView n m
leqView {m = zero} zero = equal
leqView {m = suc m} zero = less zero
leqView {m = zero} (suc ())
leqView {m = suc m} (suc leq) with leqView leq
leqView {._} {suc m} (suc leq) | less lt = less (suc lt)
leqView {.(suc m)} {suc m} (suc lt) | equal = equal

case_of_ : ∀ {A B : Set} → A → (A → B) → B
case x of f = f x

wfAux : ∀ {n y} → (∀ z → z < n → Acc _<_ z) → y ≤ n → Acc _<_ y
wfAux f leq with leqView leq
wfAux f leq | less lt = f _ lt
wfAux f leq | equal = acc f

wfNat : ∀ n → Acc _<_ n
wfNat zero = acc λ _ ()
wfNat (suc n) with wfNat n
... | acc f = acc (λ y lt → wfAux f lt)

≤-refl : ∀ n → n ≤ n
≤-refl zero = zero
≤-refl (suc n) = suc (≤-refl n)

wk< : ∀ {n m} → n < m → n < suc m
wk< zero = zero
wk< (suc lt) = suc (wk< lt)

less-minus : ∀ n m → (suc n - suc m) ≤ n
less-minus n zero    = ≤-refl n
less-minus zero (suc m) = zero
less-minus (suc n) (suc m) = wk< (less-minus n m)

NonZero : Nat → Set
NonZero zero = ⊥
NonZero (suc _) = ⊤

divsuc : ∀ n → Nat → Acc _<_ n → Nat
divsuc 0 _ _ = 0
divsuc (suc n) m (acc f) =
  suc (divsuc (n - m) m (f _ (less-minus n m)))

div : Nat → (m : Nat) → {_ : NonZero m} → Nat
div n zero {}
div n (suc m) = divsuc n m (wfNat n)

main : IO Unit
main = printNat (div 1000000 1000)


text:
module Data.Star.Indexed where

open import Relation.Binary
open import Function
open import Level

infixr 10 _◅_
data Star {i a t}(I : Set i){A : I → Set a}
     (T : ∀ n m → REL (A n) (A m) t) : ∀ {n m : I} → REL (A n) (A m) (i ⊔ a ⊔ t) where
  ε   : ∀ {i}{x : A i} → Star I T x x
  _◅_ : ∀ {n m k : I}{x : A n}{y : A m}{z : A k} → T n m x y → Star I T y z → Star I T x z


text:
open import Nat
open import Prelude
open import core

open import lemmas-gcomplete

module lemmas-complete where
  -- no term is both complete and indeterminate
  lem-ind-comp : ∀{d} → d dcomplete → d indet → ⊥
  lem-ind-comp DCVar ()
  lem-ind-comp DCConst ()
  lem-ind-comp (DCLam comp x₁) ()
  lem-ind-comp (DCAp comp comp₁) (IAp x ind x₁) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastArr x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastGroundHole x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastHoleGround x₂ ind x₃) = lem-ind-comp comp ind

  -- complete types that are consistent are equal
  complete-consistency : ∀{τ1 τ2} → τ1 ~ τ2 → τ1 tcomplete → τ2 tcomplete → τ1 == τ2
  complete-consistency TCRefl TCBase comp2 = refl
  complete-consistency TCRefl (TCArr comp1 comp2) comp3 = refl
  complete-consistency TCHole1 comp1 ()
  complete-consistency TCHole2 () comp2
  complete-consistency (TCArr consis consis₁) (TCArr comp1 comp2) (TCArr comp3 comp4)
   with complete-consistency consis comp1 comp3 | complete-consistency consis₁ comp2 comp4
  ... | refl | refl = refl

  -- a well typed complete term is assigned a complete type
  complete-ta : ∀{Γ Δ d τ} → (Γ gcomplete) →
                             (Δ , Γ ⊢ d :: τ) →
                             d dcomplete →
                             τ tcomplete
  complete-ta gc TAConst comp = TCBase
  complete-ta gc (TAVar x₁) DCVar = gc _ _ x₁
  complete-ta gc (TALam a wt) (DCLam comp x₁) = TCArr x₁ (complete-ta (gcomp-extend gc x₁ a ) wt comp)
  complete-ta gc (TAAp wt wt₁) (DCAp comp comp₁) with complete-ta gc wt comp
  complete-ta gc (TAAp wt wt₁) (DCAp comp comp₁) | TCArr qq qq₁ = qq₁
  complete-ta gc (TAEHole x x₁) ()
  complete-ta gc (TANEHole x wt x₁) ()
  complete-ta gc (TACast wt x) (DCCast comp x₁ x₂) = x₂
  complete-ta gc (TAFailedCast wt x x₁ x₂) ()

  -- a well typed term synthesizes a complete type
  comp-synth : ∀{Γ e τ} →
                   Γ gcomplete →
                   e ecomplete →
                   Γ ⊢ e => τ →
                   τ tcomplete
  comp-synth gc ec SConst = TCBase
  comp-synth gc (ECAsc x ec) (SAsc x₁) = x
  comp-synth gc ec (SVar x) = gc _ _ x
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAHole x₁) with comp-synth gc ec wt
  ... | ()
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAArr x₁) with comp-synth gc ec wt
  comp-synth gc (ECAp ec ec₁) (SAp _ wt MAArr x₁) | TCArr qq qq₁ = qq₁
  comp-synth gc () SEHole
  comp-synth gc () (SNEHole _ wt)
  comp-synth gc (ECLam2 ec x₁) (SLam x₂ wt) = TCArr x₁ (comp-synth (gcomp-extend gc x₁ x₂) ec wt)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
-- Andreas, 2020-03-27, issue #4534
-- Better error message for quote.

open import Agda.Builtin.Reflection

quote₀ : Set → Name
quote₀ X = quote X

-- Cannot quote a variable X
-- when checking that the expression quote X has type Name


text:
{-# OPTIONS --without-K #-}
module well-typed-syntax-context-helpers where
open import common
open import well-typed-syntax
open import well-typed-syntax-helpers

□_ : Typ ε → Set
□_ T = Term {Γ = ε} T

max_stars_repo_name: JasonGross/lob

max_issues_repo_name: JasonGross/lob

max_forks_repo_name: JasonGross/lob


text:
open import Everything

module Test.Surjidentity where

module _
  {𝔬₁ 𝔯₁ 𝔬₂ 𝔯₂ ℓ₂}
  {𝔒₁ : Ø 𝔬₁}
  (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {𝔒₂ : Ø 𝔬₂}
  (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼₂'_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  (_∼̇₂'_ : ∀ {x y} → x ∼₂' y → x ∼₂' y → Ø ℓ₂)
  (ε₁ : Reflexivity.type _∼₁_)
  (ε₂ : Reflexivity.type _∼₂_)
  (_↦₁_ : Transitivity.type _∼₁_)
  (_↦₂_ : Transitivity.type _∼₂_)
  {ℓ₁} (_∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁)
  {ℓ₁'} (_∼̇₁'_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁')
  (μ₁₂ : Surjection.type _ _)
  (μ₂₂ : Surjection.type _ _)
  {smap₁₂ : Smap.type _∼₁_ _∼₂_ μ₁₂ μ₁₂}
  {smap₂₂ : Smap.type _∼₂_ _∼₂_ μ₂₂ μ₂₂}
  ⦃ I1 : IsFunctor _∼₁_ _∼̇₁_ ε₁ _↦₁_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ smap₁₂ ⦄ -- FIXME using top-level instances does not work b/c then there is not instance found for reflexivity.
  ⦃ I2 : IsFunctor _∼₂_ _∼̇₂_ ε₂ _↦₂_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ smap₂₂ ⦄
  ⦃ I3 : IsFunctor _∼₁_ _∼̇₁'_ ε₁ _↦₁_ _∼₂_ _∼̇₂_ ε₂ _↦₂_ smap₁₂ ⦄
  where
  {- FIXME would like to try this instead of instance arguments
  postulate
    instance
      I1 : IsFunctor _∼₁_ _∼̇₁_ _↦₁_ _∼₂_ _∼̇₂_ _↦₂_ smap₁₂
      I2 : IsFunctor _∼₂_ _∼̇₂_ _↦₂_ _∼₂_ _∼̇₂_ _↦₂_ smap₂₂
      I3 : IsFunctor _∼₁_ _∼̇₁'_ _↦₁_ _∼₂_ _∼̇₂_ _↦₂_ smap₁₂
  -}

  test-surjidentity-from-IsFunctor : Surjidentity.type _∼₁_ _∼₂_ _∼̇₂_ smap₁₂ ε₁ ε₂
  test-surjidentity-from-IsFunctor = surjidentity -- FIXME this works only b/c of overlap (the Surjidentity instance found is I1, not I3)

module _
  {𝔬₁ 𝔯₁ 𝔬₂ 𝔯₂ ℓ₂}
  {𝔒₁ : Ø 𝔬₁}
  (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {𝔒₂ : Ø 𝔬₂}
  (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼₂'_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  (_∼̇₂'_ : ∀ {x y} → x ∼₂' y → x ∼₂' y → Ø ℓ₂)
  ⦃ `𝓢urjection : Surjection.class 𝔒₁ 𝔒₂ ⦄
  ⦃ `𝓢urjectivity : Smap!.class _∼₁_ _∼₂_ ⦄
  ⦃ `𝓢urjectextensivity : Smap!.class _∼₁_ _∼₂'_ ⦄
  ⦃ `𝓡eflexivity₁ : Reflexivity.class _∼₁_ ⦄
  ⦃ `𝓡eflexivity₂ : Reflexivity.class _∼₂_ ⦄
  ⦃ `𝓡eflexivity₂' : Reflexivity.class _∼₂'_ ⦄
  where

  instance

    `𝒮urjidentity : Surjidentity!.class _∼₁_ _∼₂_ _∼̇₂_
    `𝒮urjidentity .⋆ = magic

  test-surjidentity : Surjidentity!.type _∼₁_ _∼₂_ _∼̇₂_
  test-surjidentity = surjidentity


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for reasoning with a partial setoid
------------------------------------------------------------------------

{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.PartialEquivalence
  {c ℓ} {A : Type c} (E : PartialEquivalence A ℓ) where

open PartialEquivalence E
import Cubical.Relation.Binary.Reasoning.Base.Partial _≈_ transitive as Base

------------------------------------------------------------------------
-- Re-export the contents of the base module

open Base public
  renaming (_∼⟨_⟩_ to _≈⟨_⟩_)

------------------------------------------------------------------------
-- Additional reasoning combinators

infixr 1 _≈˘⟨_⟩_

_≈˘⟨_⟩_ : ∀ x {y z} → y ≈ x → y IsRelatedTo z → x IsRelatedTo z
x ≈˘⟨ y≈x ⟩ y∼z = x ≈⟨ symmetric y≈x ⟩ y∼z


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Float

NaN : Float
NaN = primFloatDiv 0.0 0.0

defNaN : NaN ≡ NaN
defNaN = refl

primEqNaN : primFloatEquality NaN NaN ≡ true
primEqNaN = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Lemmachine where
open import Lemmachine.Request public
open import Lemmachine.Response public
open import Lemmachine.Resource public
open import Lemmachine.Resource.Configure public
open import Lemmachine.Resolve
open import Lemmachine.Utils public
open import Lemmachine.Runner public

open import Data.Bool public hiding (_≟_)
open import Data.List public

toApp : Hooks → Application
toApp hs = resolve (toResource hs)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Prelude

module Implicits.Semantics.Preservation where

open import Implicits.Syntax
open import Implicits.WellTyped
open import Implicits.Semantics.Type
open import Implicits.Semantics.Context
open import Implicits.Semantics.Lemmas
open import Implicits.Semantics.RewriteContext
open import Implicits.Semantics.Term
open import SystemF.Everything as F using ()

module Preservation
  (_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set)
  (⟦_,_⟧r : ∀ {ν n} {K : Ktx ν n} {a} → (proj₂ K) ⊢ᵣ a → K# K →
            ∃ λ t → ⟦ proj₁ K ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→) where

  open TypingRules _⊢ᵣ_
  open TermSemantics _⊢ᵣ_ ⟦_,_⟧r

  -- interpretation of well-typed terms in System F preserves type
  ⟦⟧-preserves-tp : ∀ {ν n} {K : Ktx ν n} {t a} → (wt-t : K ⊢ t ∈ a) → (m : K# K) →
                    ⟦ proj₁ K ⟧ctx→ F.⊢ ⟦ wt-t , m ⟧ ∈ ⟦ a ⟧tp→
  ⟦⟧-preserves-tp {K = K} (var x) m = subst-wt-var (sym $ lookup-⟦⟧ctx→ (proj₁ K) x) (F.var x)
    where
      subst-wt-var = subst (λ a → ⟦ proj₁ K ⟧ctx→ F.⊢ (F.var x) ∈ a)
  ⟦⟧-preserves-tp {K = K} {a = ∀' a} (Λ wt-e) m with ⟦⟧-preserves-tp wt-e (#tvar m)
  ... | ih = F.Λ (subst-wt-ctx (⟦weaken⟧ctx→ (proj₁ K)) ih)
    where
      subst-wt-ctx = subst (λ c → c F.⊢ ⟦ wt-e , #tvar m ⟧ ∈ ⟦ a ⟧tp→)
  ⟦⟧-preserves-tp (λ' a wt-e) m with ⟦⟧-preserves-tp wt-e (#var a m)
  ⟦⟧-preserves-tp (λ' a wt-e) m | ih = F.λ' ⟦ a ⟧tp→ ih
  ⟦⟧-preserves-tp {K = K} (_[_] {a = a} wt-tc b) m with ⟦⟧-preserves-tp wt-tc m
  ... | ih = subst-tp (sym $ ⟦a/sub⟧tp→ a b) (ih F.[ ⟦ b ⟧tp→ ])
    where
      subst-tp = subst (λ c → ⟦ proj₁ K ⟧ctx→ F.⊢ ⟦ wt-tc [ b ] , m ⟧ ∈ c)
  ⟦⟧-preserves-tp (wt-f · wt-e) m with ⟦⟧-preserves-tp wt-f m | ⟦⟧-preserves-tp wt-e m
  ⟦⟧-preserves-tp (wt-f · wt-e) m | ih | y = ih F.· y
  ⟦⟧-preserves-tp (ρ {a = a} unamb-a wt-e) m with ⟦⟧-preserves-tp wt-e (#ivar a m)
  ⟦⟧-preserves-tp (ρ {a = a} unamb-a wt-e) m | ih = F.λ' ⟦ a ⟧tp→ ih
  ⟦⟧-preserves-tp (wt-r ⟨ e ⟩) m with ⟦⟧-preserves-tp wt-r m
  ⟦⟧-preserves-tp (wt-r ⟨ e ⟩) m | f-wt-r = f-wt-r F.· (proj₂ ⟦ e , m ⟧r)
  ⟦⟧-preserves-tp (wt-r with' wt-e ) m with ⟦⟧-preserves-tp wt-r m | ⟦⟧-preserves-tp wt-e m
  ⟦⟧-preserves-tp (wt-r with' wt-e ) m | f-wt-r | f-wt-e = f-wt-r F.· f-wt-e


text:
-- Andreas, 2012-03-09, example by Ulf
{-# OPTIONS -v tc.conv.irr:50 -v tc.decl.ax:10 -v tc.decl.mutual:20 #-}
module Issue351-5 where

open import Common.Prelude
open import Common.Equality
open import Common.Irrelevance

postulate
  foo : (x : Squash Nat) → ((r : Squash Nat) → r ≡ squash (suc (unsquash x))) → Set
  bar : foo (squash _) (λ r → refl)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module Path where

open import Basics hiding (_==_)
open import Proc
import Graph

private open module G = Graph Nat

data Node : Set where
  node : Nat -> Node
  stop : Node

_==_ : Node -> Node -> Bool
stop         == stop         = true
node zero    == node zero    = true
node (suc n) == node (suc m) = node n == node m
_            == _            = false

data U : Set where
  int : U
  ext : U

data Name : Set where
  fwd-edge : Nat -> Nat  -> Name
  bwd-edge : Nat -> Node -> Name
  start    : Nat -> Name
  finish   : Nat -> Name

N : U -> Set
N int = Name
N ext = False

data Msg : Set where
  forward  : Node -> Node -> Msg
  backward : Node -> Msg

T : U -> Set
T int = Msg
T ext = Node

private
 module Impl where
  private module P = ProcDef U T N
  open P hiding (_!_)

  P = Proc int

  infixr 40 _!_
  _!_ : Msg -> P -> P
  m ! p = P._!_ (lift m) p

  fwd : Nat -> Nat -> Msg
  fwd from to = forward (node from) (node to)

  fwd-runner : Nat -> Nat -> P
  fwd-runner from to = > react
    where
      react : Msg -> P
      react (forward from' to') =
        if   to' == node from
        then fwd from to ! def (bwd-edge from from')
        else def (fwd-edge from to)
      react (backward _) = o

  bwd-runner : Nat -> Node -> P
  bwd-runner from w = > react
    where
      react : Msg -> P
      react (backward n) =
        if   n == w then o
        else if n == node from
        then backward w ! o
        else def (bwd-edge from w)
      react (forward _ _) = def (bwd-edge from w)

  pitcher : Nat -> P
  pitcher n = forward stop (node n) ! o

  batter : Nat -> P
  batter n = > react
    where
      react : Msg -> P
      react (forward from to) =
        if   to == node n
        then backward from ! o
        else def (start n)
      react _ = def (start n)

  env : Env
  env int (fwd-edge from to) = fwd-runner from to
  env int (bwd-edge from w)  = bwd-runner from w
  env int (start n)          = batter n
  env int (finish n)         = pitcher n
  env ext ()

  edges : Graph -> P
  edges [] = o
  edges (edge x y :: G) = def (fwd-edge x y) || edges G

  φ : Tran ext int
  φ = record { upV = up; downV = down }
    where
      down : Node -> Lift Msg
      down x = lift (backward x)

      up : Msg -> Lift Node
      up (forward _ _) = bot
      up (backward x)  = lift x

  main : Graph -> Nat -> Nat -> Proc ext
  main G x y = φ /| def (finish y) || def (start x) || edges G

open Impl public

param : Param
param = record
        { U    = U
        ; T    = T
        ; Name = N
        ; env  = env
        }

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Setoids.Setoids
open import Groups.Definition
open import Sets.EquivalenceRelations

module Groups.Lemmas {a b : _} {A : Set a} {_·_ : A → A → A} {S : Setoid {a} {b} A} (G : Group S _·_) where

open Setoid S
open Group G
open Equivalence eq

groupsHaveLeftCancellation : (x y z : A) → (x · y) ∼ (x · z) → y ∼ z
groupsHaveLeftCancellation x y z pr = o
  where
  _^-1 = inverse
  j : ((x ^-1) · x) · y ∼ (x ^-1) · (x · z)
  j = transitive (symmetric (+Associative {x ^-1} {x} {y})) (+WellDefined ~refl pr)
  k : ((x ^-1) · x) · y ∼ ((x ^-1) · x) · z
  k = transitive j +Associative
  l : 0G · y ∼ ((x ^-1) · x) · z
  l = transitive (+WellDefined (symmetric invLeft) ~refl) k
  m : 0G · y ∼ 0G · z
  m = transitive l (+WellDefined invLeft ~refl)
  n : y ∼ 0G · z
  n = transitive (symmetric identLeft) m
  o : y ∼ z
  o = transitive n identLeft

groupsHaveRightCancellation : (x y z : A) → (y · x) ∼ (z · x) → y ∼ z
groupsHaveRightCancellation x y z pr = transitive m identRight
  where
  _^-1 = inverse
  i : (y · x) · (x ^-1) ∼ (z · x) · (x ^-1)
  i = +WellDefined pr ~refl
  j : y · (x · (x ^-1)) ∼ (z · x) · (x ^-1)
  j = transitive +Associative i
  j' : y · 0G ∼ (z · x) · (x ^-1)
  j' = transitive (+WellDefined ~refl (symmetric invRight)) j
  k : y ∼ (z · x) · (x ^-1)
  k = transitive (symmetric identRight) j'
  l : y ∼ z · (x · (x ^-1))
  l = transitive k (symmetric +Associative)
  m : y ∼ z · 0G
  m = transitive l (+WellDefined ~refl invRight)

rightInversesAreUnique : {x : A} → {y : A} → (y · x) ∼ 0G → y ∼ (inverse x)
rightInversesAreUnique {x} {y} f = transitive i (transitive j (transitive k (transitive l m)))
  where
  _^-1 = inverse
  i : y ∼ y · 0G
  j : y · 0G ∼ y · (x · (x ^-1))
  k : y · (x · (x ^-1)) ∼ (y · x) · (x ^-1)
  l : (y · x) · (x ^-1) ∼ 0G · (x ^-1)
  m : 0G · (x ^-1) ∼ x ^-1
  i = symmetric identRight
  j = +WellDefined ~refl (symmetric invRight)
  k = +Associative
  l = +WellDefined f ~refl
  m = identLeft

leftInversesAreUnique : {x : A} → {y : A} → (x · y) ∼ 0G → y ∼ (inverse x)
leftInversesAreUnique {x} {y} f = rightInversesAreUnique {x} {y} l
  where
    _^-1 = inverse
    i : y · (x · y) ∼ y · 0G
    i' : y · (x · y) ∼ y
    j : (y · x) · y ∼ y
    k : (y · x) · y ∼ 0G · y
    l : y · x ∼ 0G
    i = +WellDefined ~refl f
    i' = transitive i identRight
    j = transitive (symmetric +Associative) i'
    k = transitive j (symmetric identLeft)
    l = groupsHaveRightCancellation y (y · x) 0G k

invTwice : (x : A) → (inverse (inverse x)) ∼ x
invTwice x = symmetric (rightInversesAreUnique {x ^-1} {x} invRight)
  where
  _^-1 = inverse

replaceGroupOp : {a b c d w x y z : A} → (Setoid._∼_ S a c) → (Setoid._∼_ S b d) → (Setoid._∼_ S w y) → (Setoid._∼_ S x z) → Setoid._∼_ S (a · b) (w · x) → Setoid._∼_ S (c · d) (y · z)
replaceGroupOp a~c b~d w~y x~z pr = transitive (symmetric (+WellDefined a~c b~d)) (transitive pr (+WellDefined w~y x~z))

replaceGroupOpRight : {a b c x : A} → (Setoid._∼_ S a (b · c)) → (Setoid._∼_ S c x) → (Setoid._∼_ S a (b · x))
replaceGroupOpRight a~bc c~x = transitive a~bc (+WellDefined reflexive c~x)

inverseWellDefined : {x y : A} → (x ∼ y) → (inverse x) ∼ (inverse y)
inverseWellDefined {x} {y} x~y = groupsHaveRightCancellation x (inverse x) (inverse y) q
  where
    p : inverse x · x ∼ inverse y · y
    p = transitive invLeft (symmetric invLeft)
    q : inverse x · x ∼ inverse y · x
    q = replaceGroupOpRight {_·_ (inverse x) x} {inverse y} {y} {x} p (symmetric x~y)

transferToRight : {a b : A} → (a · (inverse b)) ∼ 0G → a ∼ b
transferToRight {a} {b} ab-1 = transitive (symmetric (invTwice a)) (transitive u (invTwice b))
  where
    t : inverse a ∼ inverse b
    t = symmetric (leftInversesAreUnique ab-1)
    u : inverse (inverse a) ∼ inverse (inverse b)
    u = inverseWellDefined t

transferToRight' : {a b : A} → (a · b) ∼ 0G → a ∼ (inverse b)
transferToRight' {a} {b} ab-1 = transferToRight lemma
  where
    lemma : a · (inverse (inverse b)) ∼ 0G
    lemma = transitive (+WellDefined reflexive (invTwice b)) ab-1

transferToRight'' : {a b : A} → Setoid._∼_ S a b → (a · (inverse b)) ∼ 0G
transferToRight'' {a} {b} a~b = transitive (+WellDefined a~b reflexive) invRight

invInv : {x : A} → (inverse (inverse x)) ∼ x
invInv {x} = symmetric (transferToRight' invRight)

invIdent : (inverse 0G) ∼ 0G
invIdent = symmetric (transferToRight' identLeft)

swapInv : {x y : A} → (inverse x) ∼ y → x ∼ (inverse y)
swapInv {x} {y} -x=y = transitive (symmetric invInv) (inverseWellDefined -x=y)

identityIsUnique : (e : A) → ((b : A) → ((b · e) ∼ b)) → (e ∼ 0G)
identityIsUnique thing fb = transitive (symmetric identLeft) (fb 0G)

invContravariant : {x y : A} → (Setoid._∼_ S (Group.inverse G (x · y)) ((Group.inverse G y) · (Group.inverse G x)))
invContravariant {x} {y} = ans
  where
    _^-1 = inverse
    otherInv = (y ^-1) · (x ^-1)
    many+Associatives : x · ((y · (y ^-1)) · (x ^-1)) ∼ (x · y) · ((y ^-1) · (x ^-1))
    oneMult : (x · y) · otherInv ∼ x · (x ^-1)
    many+Associatives = transitive +Associative (transitive (+WellDefined +Associative reflexive) (symmetric +Associative))
    oneMult = symmetric (transitive (+WellDefined reflexive (transitive (symmetric identLeft) (+WellDefined (symmetric invRight) reflexive))) many+Associatives)
    otherInvIsInverse : (x · y) · otherInv ∼ 0G
    otherInvIsInverse = transitive oneMult invRight
    ans : (x · y) ^-1 ∼ (y ^-1) · (x ^-1)
    ans = symmetric (leftInversesAreUnique otherInvIsInverse)

equalsDoubleImpliesZero : {x : A} → (x · x) ∼ x → x ∼ 0G
equalsDoubleImpliesZero 2x=x = transitive (symmetric identLeft) (transitive (+WellDefined (symmetric invLeft) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive 2x=x) invLeft)))

invZeroImpliesZero : {x : A} → (inverse x) ∼ 0G → x ∼ 0G
invZeroImpliesZero {x} pr = transitive (symmetric (invTwice x)) (transitive (inverseWellDefined pr) invIdent)


text:
open import MLib.Algebra.PropertyCode

module MLib.Algebra.PropertyCode.Dependent {k c ℓ} {code : Code k} (struct : Struct code c ℓ) where

open import MLib.Prelude
open import MLib.Algebra.PropertyCode.Core

open import Function.Equivalence using (Equivalence)

open Struct struct

private
  module FuncBased {c′ ℓ′} (depRawStruct : RawStruct K c′ ℓ′) (props : ∀ π → Maybe (∃ λ deps → ⦃ _ : Hasₚ deps ⦄ → ⟦ π ⟧P depRawStruct)) where
    Π′ : Properties code
    Π′ = properties λ π →
      case props π of λ
      { (just (deps , _)) → implies deps Π
      ; nothing → false
      }

    Π′-prop : ∀ {π} → π ∈ₚ Π′ → ∃ λ x → props π ≡ just x
    Π′-prop {π} π∈Π′ with props π | ≡.inspect props π
    Π′-prop {π} π∈Π′ | just x | _ = x , ≡.refl
    Π′-prop {π} (fromTruth truth) | nothing | ≡.[ eq ] rewrite eq = ⊥-elim truth

    reify′ : ∀ {π} → π ∈ₚ Π′ → ⟦ π ⟧P depRawStruct
    reify′ {π} π∈Π′ with Π′-prop π∈Π′ | hasProperty Π′ π | ≡.inspect (hasProperty Π′) π
    reify′ {_} (fromTruth truth) | (deps , f) , eq | false | ≡.[ eq₁ ] rewrite eq | eq₁ = ⊥-elim truth
    reify′ {_} (fromTruth truth) | (deps , f) , eq | true | ≡.[ eq₁ ] rewrite eq = f ⦃ fromTruth truth  ⦄

    dependentStruct :
      Struct code c′ ℓ′
    dependentStruct = record
      { rawStruct = depRawStruct
      ; Π = Π′
      ; reify = reify′
      }

  module ListBased {c′ ℓ′} (depRawStruct : RawStruct K c′ ℓ′) (props : List (∃₂ λ π deps → ⦃ _ : Hasₚ deps ⦄ → ⟦ π ⟧P depRawStruct)) where
    Func = ∀ π → Maybe (∃ (λ deps → ⦃ _ : Hasₚ deps ⦄ → ⟦ π ⟧P depRawStruct))

    singleFunc : (∃₂ λ π deps → ⦃ _ : Hasₚ deps ⦄ → ⟦ π ⟧P depRawStruct) → Func
    singleFunc (π , deps , f) π′ with π Property.≟ π′
    singleFunc (π , deps , f) π′ | yes p rewrite Property.≈⇒≡ p = just (deps , f)
    singleFunc (π , deps , f) π′ | no _ = nothing

    combineFuncs : Func → Func → Func
    combineFuncs f g π =
      case f π of λ
      { (just r) → just r
      ; nothing → case g π of λ
        { (just r) → just r
        ; nothing → nothing
        }
      }

    propsF : ∀ π → Maybe (∃ (λ deps → ⦃ _ : Hasₚ deps ⦄ → ⟦ π ⟧P depRawStruct))
    propsF = List.foldr combineFuncs (λ _ → nothing) (List.map singleFunc props)

    dependentStruct : Struct code c′ ℓ′
    dependentStruct = FuncBased.dependentStruct depRawStruct propsF

open ListBased using (dependentStruct) public


text:
module Nat where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero   + b = b
succ a + b = succ (a + b)

_×_ : ℕ → ℕ → ℕ
zero   × b = zero
succ a × b = (a × b) + b

open import Relation.Binary.PropositionalEquality

0-is-right-identity-of-+ : ∀ (n : ℕ) → n + zero ≡ n
0-is-right-identity-of-+ zero     = refl
0-is-right-identity-of-+ (succ n) = cong succ (0-is-right-identity-of-+ n)

+-is-associative : ∀ (a b c : ℕ) → a + (b + c) ≡ (a + b) + c
+-is-associative zero     b c = refl
+-is-associative (succ a) b c = cong succ (+-is-associative a b c)

lemma : ∀ (a b : ℕ) → a + succ b ≡ succ (a + b)
lemma zero     b = refl
lemma (succ a) b = cong succ (lemma a b)

import Relation.Binary.EqReasoning as EqR
open module EqNat = EqR (setoid ℕ)

+-is-commutative : ∀ (a b : ℕ) → a + b ≡ b + a
+-is-commutative a zero     = 0-is-right-identity-of-+ a
+-is-commutative a (succ b) =
  begin
    a + succ b
      ≈⟨ lemma a b ⟩
    succ (a + b)
      ≈⟨ cong succ (+-is-commutative a b) ⟩
    succ (b + a)
      ≈⟨ refl ⟩
    succ b + a
  ∎

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)

-- category of cones "over a Functor F"

module Categories.Category.Construction.Cones
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

open import Data.Product
import Categories.Diagram.Cone as Co
import Categories.Morphism as Mor
import Categories.Morphism.IsoEquiv as IsoEquiv
import Categories.Morphism.Reasoning as Reas

open Category C
open HomReasoning
open Mor C using (_≅_)
open IsoEquiv C using (_≃_; ⌞_⌟)
open Reas C

open Co F public
open Apex
open Cone
open Cone⇒

Cones : Category _ _ _
Cones = record
  { Obj       = Cone
  ; _⇒_       = Cone⇒
  ; _≈_       = λ f g → arr f ≈ arr g
  ; id        = record
    { arr     = id
    ; commute = identityʳ
    }
  ; _∘_       = λ {A B C} f g → record
    { arr     = arr f ∘ arr g
    ; commute = λ {X} → begin
      ψ C X ∘ arr f ∘ arr g ≈⟨ pullˡ (commute f) ⟩
      ψ B X ∘ arr g         ≈⟨ commute g ⟩
      ψ A X                 ∎
    }
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }

module Cones = Category Cones

private
  variable
    K K′ : Cone
    X : Obj
  module CM = Mor Cones
  module CI = IsoEquiv Cones

open CM using () renaming (_≅_ to _⇔_)
open CI using () renaming (_≃_ to _↮_)

cone-resp-iso : ∀ (κ : Cone) → Cone.N κ ≅ X → Σ[ κ′ ∈ Cone ] κ ⇔ κ′
cone-resp-iso {X = X} κ κ≅X = record
  { apex = record
    { ψ       = λ Y → Cone.ψ κ Y ∘ to
    ; commute = λ f → pullˡ (Cone.commute κ f)
    }
  } , record
  { from = record
    { arr     = from
    ; commute = cancelʳ isoˡ
    }
  ; to   = record
    { arr     = to
    ; commute = refl
    }
  ; iso  = record
    { isoˡ    = isoˡ
    ; isoʳ    = isoʳ
    }
  }
  where open _≅_ κ≅X
        open Cone
        open Apex

iso-cone⇒iso-apex : K ⇔ K′ → N K ≅ N K′
iso-cone⇒iso-apex K⇔K′ = record
  { from = arr from
  ; to   = arr to
  ; iso  = record
    { isoˡ = isoˡ
    ; isoʳ = isoʳ
    }
  }
  where open _⇔_ K⇔K′

↮⇒-≃ : ∀ {i₁ i₂ : K ⇔ K′} → i₁ ↮ i₂ → iso-cone⇒iso-apex i₁ ≃ iso-cone⇒iso-apex i₂
↮⇒-≃ i₁↮i₂ = ⌞ from-≈ ⌟
  where open _↮_ i₁↮i₂

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

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

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

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

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

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

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import lib.Basics
open import lib.types.Pointed

module lib.types.Lift where

⊙Lift : ∀ {i j} → Ptd i → Ptd (lmax i j)
⊙Lift {j = j} (A , a) =  ⊙[ Lift {j = j} A , lift a ]

⊙lift : ∀ {i j} {X : Ptd i} → fst (X ⊙→ ⊙Lift {j = j} X)
⊙lift = (lift , idp)

⊙lower : ∀ {i j} {X : Ptd i} → fst (⊙Lift {j = j} X ⊙→ X)
⊙lower = (lower , idp)

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

-- [lower-equiv] is in Equivalences.agda

Lift-level : ∀ {i j} {A : Type i} {n : ℕ₋₂} →
  has-level n A → has-level n (Lift {j = j} A)
Lift-level = equiv-preserves-level lift-equiv

⊙lift-equiv : ∀ {i j} {X : Ptd i} → X ⊙≃ ⊙Lift {j = j} X
⊙lift-equiv = (⊙lift , snd lift-equiv)

⊙lower-equiv : ∀ {i j} {X : Ptd i} → ⊙Lift {j = j} X ⊙≃ X
⊙lower-equiv = (⊙lower , snd lower-equiv)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Data.Num.Binary where

-- open import Data.Product using (_×_; Σ; _,_)
open import Data.List
open import Data.Unit
open import Data.Empty
-- open import Data.Nat renaming (_+_ to _⊹_)
--
-- data Bin : Set where
--     [] : Bin
--     0- : Bin → Bin
--     1- : Bin → Bin
--
-- carry : Bin → Bin
-- carry [] = 1- []
-- carry (0- xs) = 1- xs
-- carry (1- xs) = 0- (carry xs)
--
-- _+_ : Bin → Bin → Bin
-- [] + ys = ys
-- xs + [] = xs
-- 0- xs + 0- ys = 0- (xs + ys)
-- 0- xs + 1- ys = 1- (xs + ys)
-- 1- xs + 0- ys = 1- (xs + ys)
-- 1- xs + 1- ys = 0- (carry (xs + ys))
--

-- data Desc : Set₁ where
--     arg : (A : Set)             -- a bag of tags to choose constructors with
--         → (A → Desc)            -- given a tag, return the description of the constructor it corresponds to
--         → Desc
--     rec : Desc → Desc           -- recursive subnode
--     ret : Desc                  -- stop
--
-- -- the "decoder", "interpreter"
-- -- ⟦_⟧ : Desc → Set → Set
-- -- ⟦ arg A D ⟧ R = Σ A (λ a → ⟦ D a ⟧ R)
-- -- ⟦ rec D   ⟧ R = R × ⟦ D ⟧ R
-- -- ⟦ ret     ⟧ R = ⊤

-- data BinF : Set where
--     arg : (ℕ → BinF) → BinF
--     rec : BinF → BinF
--     ret : BinF
--
-- ⟦_⟧ : BinF → Set → Set
-- ⟦_⟧ (arg F) X = Σ ℕ (λ n → ⟦ F n ⟧ X)
-- ⟦_⟧ (rec F) X = X × ⟦ F ⟧ X
-- ⟦_⟧ ret X = ⊤
--
-- data μ (F : BinF) : Set where
--     ⟨_⟩ : ⟦ F ⟧ (μ F) → μ F
--
-- Bin : Set
-- Bin = μ (arg {! λ   !})

--
-- data Digit : Set where
--     [0] : Digit
--     [1] : Digit
--
-- Binary : Set
-- Binary = List Digit
--
-- _⊕_ : Digit → Digit → Digit
-- [0] ⊕ [0] = [0]
-- [0] ⊕ [1] = [1]
-- [1] ⊕ [0] = [1]
-- [1] ⊕ [1] = [0]
--
-- _⊚_ : Digit → Digit → Digit
-- [1] ⊚ [1] = [1]
-- _   ⊚ _   = [0]
--
-- carry : Digit → Binary → Binary
-- carry [0] ys = ys
-- carry [1] [] = [1] ∷ []
-- carry [1] ([0] ∷ ys) = [1] ∷ ys
-- carry [1] ([1] ∷ ys) = [0] ∷ carry [1] ys
--
-- _+_ : Binary → Binary → Binary
-- [] + ys = ys
-- xs + [] = xs
-- (x ∷ xs) + (y ∷ ys) = x ⊕ y ∷ carry (x ⊚ y) (xs + ys)
--
-- _≈_ : Binary → Binary → Set
-- [] ≈ [] = ⊤
-- [] ≈ (y ∷ ys) = ⊥
-- (x ∷ xs) ≈ [] = ⊥
-- ([0] ∷ xs) ≈ ([0] ∷ ys) = xs ≈ ys
-- ([0] ∷ xs) ≈ ([1] ∷ ys) = ⊥
-- ([1] ∷ xs) ≈ ([0] ∷ ys) = ⊥
-- ([1] ∷ xs) ≈ ([1] ∷ ys) = xs ≈ ys

data Bin : Set where
    ∙ : Bin
    [0]_ : Bin → Bin
    [1]_ : Bin → Bin

two : Bin
two = [1] [0] ∙

1+ : Bin → Bin
1+ ∙ = [1] ∙
1+ ([0] x) = [1] x
1+ ([1] x) = [0] 1+ x

_+_ : Bin → Bin → Bin
∙ + ys = ys
xs + ∙ = xs
([0] xs) + ([0] ys) = [0] (xs + ys)
([0] xs) + ([1] ys) = [1] (xs + ys)
([1] xs) + ([0] ys) = [1] (xs + ys)
([1] xs) + ([1] ys) = [0] (1+ (xs + ys))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

module Fragment.Examples.CSemigroup.Arith.Reasoning where

open import Fragment.Examples.CSemigroup.Arith.Base

+-direct : ∀ {m n} → (m + 2) + (3 + n) ≡ m + (n + 5)
+-direct {m} {n} = begin
    (m + 2) + (3 + n)
  ≡⟨ fragment CSemigroupFrex +-csemigroup ⟩
    m + (n + 5)
  ∎

open import Data.Nat.Properties using (*-distribˡ-+)

+-inner : ∀ {m n k} → k * (m + 2) + k * (3 + n) ≡ (m + n + 5) * k
+-inner {m} {n} {k} = begin
    k * (m + 2) + k * (3 + n)
  ≡⟨ sym (*-distribˡ-+ k (m + 2) (3 + n)) ⟩
    k * ((m + 2) + (3 + n))
  ≡⟨ cong (k *_) (fragment CSemigroupFrex +-csemigroup) ⟩
    k * (m + n + 5)
  ≡⟨ fragment CSemigroupFrex *-csemigroup ⟩
    (m + n + 5) * k
  ∎

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
import      Lvl

module Structure.Semicategory {ℓₒ ℓₘ ℓₑ : Lvl.Level} where

open import Functional using (swap)
open import Logic
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Operator
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

-- Obj is the collection of objects.
-- _⟶_ is the collection of morphisms.
module _
  {Obj : Type{ℓₒ}}
  (_⟶_ : Obj → Obj → Type{ℓₘ})
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(x ⟶ y) ⦄
  where

  -- A semicategory is a structure on a relation called a morphism.
  --
  -- It is similar to a category (a generalisation of it), but without the identity morphism/reflexivity.
  -- See `Structure.Category`.
  --
  -- It can also be seen as a generalized algebraic structure, or more specifically a generalization of semigroups (structure with an associative binary operator).
  -- The similarity between a semicategory and a category is like the similarity between a semigroup and a monoid.
  --
  -- An alternative interpretation of the definition:
  -- A type (Obj) and a binary relation (Morphism) on this type is a semicategory when:
  -- • The relator is transitive.
  -- • Chains of the transitivity proofs can be applied in any order and the resulting proof will be the same.
  record Semicategory : Stmt{ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
    field
      _∘_ : Names.SwappedTransitivity(_⟶_)

    field
      ⦃ binaryOperator ⦄ : ∀{x y z} → BinaryOperator(_∘_ {x}{y}{z})
      ⦃ associativity ⦄ : Morphism.Associativity(\{x} → _∘_ {x})

    -- This can be interpreted as proof of transitivity when `Morphism` is interpreted as a binary relation.
    morphism-transitivity : Transitivity(_⟶_)
    morphism-transitivity = intro(swap(_∘_))

    module ArrowNotation = Names.ArrowNotation(_⟶_)

record SemicategoryObject : Stmt{Lvl.𝐒(ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {Object}           : Type{ℓₒ}
    {Morphism}         : Object → Object → Type{ℓₘ}
    ⦃ morphism-equiv ⦄ : ∀{x y} → Equiv{ℓₑ}(Morphism x y)
    semicategory       : Semicategory(Morphism)

  open Semicategory(semicategory) public
  instance
    semicategory-instance = semicategory

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:
module New.LangOps where

open import New.Lang
open import New.Changes
open import New.LangChanges

oplusτo : ∀ {Γ} τ → Term Γ (τ ⇒ Δt τ ⇒ τ)
ominusτo : ∀ {Γ} τ → Term Γ (τ ⇒ τ ⇒ Δt τ)

onilτo : ∀ {Γ} τ → Term Γ (τ ⇒ Δt τ)
onilτo τ = abs (app₂ (ominusτo τ) (var this) (var this))

-- Do NOT try to read this, such terms are write-only. But the behavior is
-- specified to be oplusτ-equiv and ominusτ-equiv.
oplusτo (σ ⇒ τ) = abs (abs (abs
  (app₂ (oplusτo τ)
    (app (var (that (that this))) (var this))
    (app₂ (var (that this)) (var this) (app (onilτo σ) (var this))))))
oplusτo int = const plus
oplusτo (pair σ τ) = abs (abs (app₂ (const cons)
  (app₂ (oplusτo σ) (app (const fst) (var (that this))) (app (const fst) (var this)))
  (app₂ (oplusτo τ) (app (const snd) (var (that this))) (app (const snd) (var this)))))
oplusτo (sum σ τ) = abs (abs (app₃ (const match) (var (that this))
  (abs (app₃ (const match) (var (that this))
    (abs (app₃ (const match) (var this)
      (abs (app (const linj) (app₂ (oplusτo σ) (var (that (that this))) (var this))))
      (abs (app (const linj) (var (that (that this)))))))
    (abs (var this))))
  (abs (app₃ (const match) (var (that this))
    (abs (app₃ (const match) (var this)
      (abs (app (const rinj) (var (that (that this)))))
      (abs (app (const rinj) (app₂ (oplusτo τ) (var (that (that this))) (var this))))))
    (abs (var this))))))

ominusτo (σ ⇒ τ) = abs (abs (abs (abs (app₂ (ominusτo τ)
  (app (var (that (that (that this)))) (app₂ (oplusτo σ) (var (that this)) (var this)))
  (app (var (that (that this))) (var (that this)))))))
ominusτo int = const minus
ominusτo (pair σ τ) = abs (abs (app₂ (const cons)
  (app₂ (ominusτo σ) (app (const fst) (var (that this))) (app (const fst) (var this)))
  (app₂ (ominusτo τ) (app (const snd) (var (that this))) (app (const snd) (var this)))))
ominusτo (sum σ τ) = abs (abs (app₃ (const match) (var (that this))
  (abs (app₃ (const match) (var (that this))
    (abs (app (const linj) (app (const linj) (app₂ (ominusτo σ) (var (that this)) (var this)))))
    (abs (app (const rinj) (var (that (that (that this))))))))
  (abs (app₃ (const match) (var (that this))
    (abs (app (const rinj) (var (that (that (that this))))))
    (abs (app (const linj) (app (const rinj) (app₂ (ominusτo τ) (var (that this)) (var this)))))))))

oplusτ-equiv : ∀ Γ (ρ : ⟦ Γ ⟧Context) τ a da → ⟦ oplusτo τ ⟧Term ρ a da ≡ a ⊕ da
ominusτ-equiv : ∀ Γ (ρ : ⟦ Γ ⟧Context) τ b a → ⟦ ominusτo τ ⟧Term ρ b a ≡ b ⊝ a

oplusτ-equiv-ext : ∀ τ Γ → ⟦ oplusτo {Γ} τ ⟧Term ≡ λ ρ → _⊕_
oplusτ-equiv-ext τ _ = ext³ (λ ρ a da → oplusτ-equiv _ ρ τ a da)
ominusτ-equiv-ext : ∀ τ Γ → ⟦ ominusτo {Γ} τ ⟧Term ≡ λ ρ → _⊝_
ominusτ-equiv-ext τ _ = ext³ (λ ρ a da → ominusτ-equiv _ ρ τ a da)

oplusτ-equiv Γ ρ (σ ⇒ τ) f df = ext (λ a → lemma a)
  where
    module _ (a : ⟦ σ ⟧Type) where
      ρ′ = a • df • f • ρ
      ρ′′ = a • ρ′
      lemma : ⟦ oplusτo τ ⟧Term ρ′ (f a)
         (df a (⟦ ominusτo σ ⟧Term ρ′′ a a))
         ≡ f a ⊕ df a (nil a)
      lemma
        rewrite ominusτ-equiv _ ρ′′ σ a a
        | oplusτ-equiv _ ρ′ τ (f a) (df a (nil a))
        = refl
oplusτ-equiv Γ ρ int a da = refl
oplusτ-equiv Γ ρ (pair σ τ) (a , b) (da , db)
  rewrite oplusτ-equiv _ ((da , db) • (a , b) • ρ) σ a da
  | oplusτ-equiv _ ((da , db) • (a , b) • ρ) τ b db
  = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₁ x) (inj₁ (inj₁ dx))
  rewrite oplusτ-equiv-ext σ (Δt σ • sum (Δt σ) (Δt τ) • σ • Δt (sum σ τ) • sum σ τ • Γ)
  = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₁ x) (inj₁ (inj₂ dy)) = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₁ x) (inj₂ y) = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₂ y) (inj₁ (inj₁ dx)) = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₂ y) (inj₁ (inj₂ dy))
  rewrite oplusτ-equiv-ext τ (Δt τ • sum (Δt σ) (Δt τ) • τ • Δt (sum σ τ) • sum σ τ • Γ)
  = refl
oplusτ-equiv Γ ρ (sum σ τ) (inj₂ y) (inj₂ y₁) = refl

ominusτ-equiv Γ ρ (σ ⇒ τ) g f = ext (λ a → ext (lemma a))
  where
    module _ (a : ⟦ σ ⟧Type) (da : Chτ σ) where
      ρ′ = da • a • f • g • ρ
      lemma : ⟦ ominusτo τ ⟧Term (da • a • f • g • ρ)
        (g (⟦ oplusτo σ ⟧Term (da • a • f • g • ρ) a da)) (f a)
        ≡ g (a ⊕ da) ⊝ f a
      lemma
        rewrite oplusτ-equiv _ ρ′ σ a da
        | ominusτ-equiv _ ρ′ τ (g (a ⊕ da)) (f a) = refl
ominusτ-equiv Γ ρ int b a = refl
ominusτ-equiv Γ ρ (pair σ τ) (a2 , b2) (a1 , b1)
  rewrite ominusτ-equiv _ ((a1 , b1) • (a2 , b2) • ρ) σ a2 a1
  | ominusτ-equiv _ ((a1 , b1) • (a2 , b2) • ρ) τ b2 b1
  = refl
ominusτ-equiv Γ ρ (sum σ τ) (inj₁ x) (inj₁ x₁)
  rewrite ominusτ-equiv-ext σ (σ • σ • sum σ τ • sum σ τ • Γ)
  = refl
ominusτ-equiv Γ ρ (sum σ τ) (inj₁ x) (inj₂ y) = refl
ominusτ-equiv Γ ρ (sum σ τ) (inj₂ y) (inj₁ x) = refl
ominusτ-equiv Γ ρ (sum σ τ) (inj₂ y) (inj₂ y₁)
  rewrite ominusτ-equiv-ext τ (τ • τ • sum σ τ • sum σ τ • Γ)
  = refl

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import HIT.Interval
open import PathOperations
open import PathStructure.Id.Tr
open import Types

funext : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) → f ≡ g
funext {A = A} {B = B} {f = f} {g = g} p = ap h seg
  where
    h : I → (x : A) → B x
    h i x = I-rec (f x) (g x) (p x) i

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures