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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Properties {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Irrelevance
     using (irrelevanceSubst′)
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
import Definition.LogicalRelation.Weakening as LR

open import Tools.Unit
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Valid substitutions are well-formed
wellformedSubst : ∀ {Γ Δ σ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
      → Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ
      → Δ ⊢ˢ σ ∷ Γ
wellformedSubst ε′ ⊢Δ [σ] = id
wellformedSubst ([Γ] ∙′ [A]) ⊢Δ ([tailσ] , [headσ]) =
  wellformedSubst [Γ] ⊢Δ [tailσ]
  , escapeTerm (proj₁ ([A] ⊢Δ [tailσ])) [headσ]

-- Valid substitution equality is well-formed
wellformedSubstEq : ∀ {Γ Δ σ σ′} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
      ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
      → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]
      → Δ ⊢ˢ σ ≡ σ′ ∷ Γ
wellformedSubstEq ε′ ⊢Δ [σ] [σ≡σ′] = id
wellformedSubstEq ([Γ] ∙′ [A]) ⊢Δ ([tailσ] , [headσ]) ([tailσ≡σ′] , [headσ≡σ′]) =
  wellformedSubstEq [Γ] ⊢Δ [tailσ] [tailσ≡σ′]
  , ≅ₜ-eq (escapeTermEq (proj₁ ([A] ⊢Δ [tailσ])) [headσ≡σ′])

-- Extend a valid substitution with a term
consSubstS : ∀ {l σ t A Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
           ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
           ([t] : Δ ⊩⟨ l ⟩ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ]))
         → Δ ⊩ˢ consSubst σ t ∷ Γ ∙ A / [Γ] ∙″ [A] / ⊢Δ
consSubstS [Γ] ⊢Δ [σ] [A] [t] = [σ] , [t]

-- Extend a valid substitution equality with a term
consSubstSEq : ∀ {l σ σ′ t A Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
             ([σ]    : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σ≡σ′] : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
             ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
             ([t] : Δ ⊩⟨ l ⟩ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ]))
           → Δ ⊩ˢ consSubst σ t ≡ consSubst σ′ t ∷ Γ ∙ A / [Γ] ∙″ [A] / ⊢Δ
               / consSubstS {t = t} {A = A} [Γ] ⊢Δ [σ] [A] [t]
consSubstSEq [Γ] ⊢Δ [σ] [σ≡σ′] [A] [t] =
  [σ≡σ′] , reflEqTerm (proj₁ ([A] ⊢Δ [σ])) [t]

-- Weakening of valid substitutions
wkSubstS : ∀ {ρ σ Γ Δ Δ′} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
           ([ρ] : ρ ∷ Δ′ ⊆ Δ)
           ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
         → Δ′ ⊩ˢ ρ •ₛ σ ∷ Γ / [Γ] / ⊢Δ′
wkSubstS ε′ ⊢Δ ⊢Δ′ ρ [σ] = tt
wkSubstS {σ = σ} {Γ = Γ ∙ A} ([Γ] ∙′ x) ⊢Δ ⊢Δ′ ρ [σ] =
  let [tailσ] = wkSubstS [Γ] ⊢Δ ⊢Δ′ ρ (proj₁ [σ])
  in  [tailσ]
   ,  irrelevanceTerm′ (wk-subst A)
        (LR.wk ρ ⊢Δ′ (proj₁ (x ⊢Δ (proj₁ [σ]))))
        (proj₁ (x ⊢Δ′ [tailσ]))
        (LR.wkTerm ρ ⊢Δ′ (proj₁ (x ⊢Δ (proj₁ [σ]))) (proj₂ [σ]))

-- Weakening of valid substitution equality
wkSubstSEq : ∀ {ρ σ σ′ Γ Δ Δ′} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ) (⊢Δ′ : ⊢ Δ′)
             ([ρ] : ρ ∷ Δ′ ⊆ Δ)
             ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σ≡σ′] : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
           → Δ′ ⊩ˢ ρ •ₛ σ ≡ ρ •ₛ σ′ ∷ Γ / [Γ]
                / ⊢Δ′ / wkSubstS [Γ] ⊢Δ ⊢Δ′ [ρ] [σ]
wkSubstSEq ε′ ⊢Δ ⊢Δ′ ρ [σ] [σ≡σ′] = tt
wkSubstSEq {Γ = Γ ∙ A} ([Γ] ∙′ x) ⊢Δ ⊢Δ′ ρ [σ] [σ≡σ′] =
  wkSubstSEq [Γ] ⊢Δ ⊢Δ′ ρ (proj₁ [σ]) (proj₁ [σ≡σ′])
  , irrelevanceEqTerm′ (wk-subst A) (LR.wk ρ ⊢Δ′ (proj₁ (x ⊢Δ (proj₁ [σ]))))
                            (proj₁ (x ⊢Δ′ (wkSubstS [Γ] ⊢Δ ⊢Δ′ ρ (proj₁ [σ]))))
                            (LR.wkEqTerm ρ ⊢Δ′ (proj₁ (x ⊢Δ (proj₁ [σ]))) (proj₂ [σ≡σ′]))

-- Weaken a valid substitution by one type
wk1SubstS : ∀ {F σ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
            (⊢F : Δ ⊢ F)
            ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
          → (Δ ∙ F) ⊩ˢ wk1Subst σ ∷ Γ / [Γ]
                            / (⊢Δ ∙ ⊢F)
wk1SubstS {F} {σ} {Γ} {Δ} [Γ] ⊢Δ ⊢F [σ] =
  wkSubstS [Γ] ⊢Δ (⊢Δ ∙ ⊢F) (step id) [σ]

-- Weaken a valid substitution equality by one type
wk1SubstSEq : ∀ {F σ σ′ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
              (⊢F : Δ ⊢ F)
              ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
              ([σ≡σ′] : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
            → (Δ ∙ F) ⊩ˢ wk1Subst σ ≡ wk1Subst σ′ ∷ Γ / [Γ]
                            / (⊢Δ ∙ ⊢F) / wk1SubstS [Γ] ⊢Δ ⊢F [σ]
wk1SubstSEq {l} {F} {σ} {Γ} {Δ} [Γ] ⊢Δ ⊢F [σ] [σ≡σ′] =
  wkSubstSEq [Γ] ⊢Δ (⊢Δ ∙ ⊢F) (step id) [σ] [σ≡σ′]

-- Lift a valid substitution
liftSubstS : ∀ {l F σ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
             ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           → (Δ ∙ subst σ F) ⊩ˢ liftSubst σ ∷ Γ ∙ F / [Γ] ∙″ [F]
                             / (⊢Δ ∙ escape (proj₁ ([F] ⊢Δ [σ])))
liftSubstS {F = F} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [F] [σ] =
  let ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
      [tailσ] = wk1SubstS {F = subst σ F} [Γ] ⊢Δ (escape (proj₁ ([F] ⊢Δ [σ]))) [σ]
      var0 = var (⊢Δ ∙ ⊢F) (PE.subst (λ x → 0 ∷ x ∈ (Δ ∙ subst σ F))
                                     (wk-subst F) here)
  in  [tailσ] , neuTerm (proj₁ ([F] (⊢Δ ∙ ⊢F) [tailσ])) (var 0)
                        var0 (~-var var0)

-- Lift a valid substitution equality
liftSubstSEq : ∀ {l F σ σ′ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
             ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σ≡σ′] : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
           → (Δ ∙ subst σ F) ⊩ˢ liftSubst σ ≡ liftSubst σ′ ∷ Γ ∙ F / [Γ] ∙″ [F]
                             / (⊢Δ ∙ escape (proj₁ ([F] ⊢Δ [σ])))
                             / liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
liftSubstSEq {F = F} {σ = σ} {σ′ = σ′} {Δ = Δ} [Γ] ⊢Δ [F] [σ] [σ≡σ′] =
  let ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
      [tailσ] = wk1SubstS {F = subst σ F} [Γ] ⊢Δ (escape (proj₁ ([F] ⊢Δ [σ]))) [σ]
      [tailσ≡σ′] = wk1SubstSEq [Γ] ⊢Δ (escape (proj₁ ([F] ⊢Δ [σ]))) [σ] [σ≡σ′]
      var0 = var (⊢Δ ∙ ⊢F) (PE.subst (λ x → 0 ∷ x ∈ (Δ ∙ subst σ F)) (wk-subst F) here)
  in  [tailσ≡σ′] , neuEqTerm (proj₁ ([F] (⊢Δ ∙ ⊢F) [tailσ])) (var 0) (var 0)
                         var0 var0 (~-var var0)

mutual
  -- Valid contexts are well-formed
  soundContext : ∀ {Γ} → ⊩ᵛ Γ → ⊢ Γ
  soundContext ε′ = ε
  soundContext (x ∙′ x₁) =
    soundContext x ∙ escape (irrelevance′ (subst-id _)
                                             (proj₁ (x₁ (soundContext x)
                                                        (idSubstS x))))

  -- From a valid context we can constuct a valid identity substitution
  idSubstS : ∀ {Γ} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ˢ idSubst ∷ Γ / [Γ] / soundContext [Γ]
  idSubstS ε′ = tt
  idSubstS {Γ = Γ ∙ A} ([Γ] ∙′ [A]) =
    let ⊢Γ = soundContext [Γ]
        ⊢Γ∙A = soundContext ([Γ] ∙″ [A])
        ⊢Γ∙A′ = ⊢Γ ∙ escape (proj₁ ([A] ⊢Γ (idSubstS [Γ])))
        [A]′ = wk1SubstS {F = subst idSubst A} [Γ] ⊢Γ
                         (escape (proj₁ ([A] (soundContext [Γ])
                                                (idSubstS [Γ]))))
                         (idSubstS [Γ])
        [tailσ] = irrelevanceSubst′ (PE.cong (_∙_ Γ) (subst-id A))
                                    [Γ] [Γ] ⊢Γ∙A′ ⊢Γ∙A [A]′
        var0 = var ⊢Γ∙A (PE.subst (λ x → 0 ∷ x ∈ (Γ ∙ A))
                                  (wk-subst A)
                                  (PE.subst (λ x → 0 ∷ wk1 (subst idSubst A)
                                                     ∈ (Γ ∙ x))
                                            (subst-id A) here))
    in  [tailσ]
    ,   neuTerm (proj₁ ([A] ⊢Γ∙A [tailσ]))
                (var 0)
                var0 (~-var var0)

-- Reflexivity valid substitutions
reflSubst : ∀ {σ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
            ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
          → Δ ⊩ˢ σ ≡ σ ∷ Γ / [Γ] / ⊢Δ / [σ]
reflSubst ε′ ⊢Δ [σ] = tt
reflSubst ([Γ] ∙′ x) ⊢Δ [σ] =
  reflSubst [Γ] ⊢Δ (proj₁ [σ]) , reflEqTerm (proj₁ (x ⊢Δ (proj₁ [σ]))) (proj₂ [σ])

-- Reflexivity of valid identity substitution
reflIdSubst : ∀ {Γ} ([Γ] : ⊩ᵛ Γ)
            → Γ ⊩ˢ idSubst ≡ idSubst ∷ Γ / [Γ] / soundContext [Γ] / idSubstS [Γ]
reflIdSubst [Γ] = reflSubst [Γ] (soundContext [Γ]) (idSubstS [Γ])

-- Symmetry of valid substitution
symS : ∀ {σ σ′ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
       ([σ]  : Δ ⊩ˢ σ  ∷ Γ / [Γ] / ⊢Δ)
       ([σ′] : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
     → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]
     → Δ ⊩ˢ σ′ ≡ σ ∷ Γ / [Γ] / ⊢Δ / [σ′]
symS ε′ ⊢Δ [σ] [σ′] [σ≡σ′] = tt
symS ([Γ] ∙′ x) ⊢Δ [σ] [σ′] [σ≡σ′] =
  symS [Γ] ⊢Δ (proj₁ [σ]) (proj₁ [σ′]) (proj₁ [σ≡σ′])
  , let [σA]           = proj₁ (x ⊢Δ (proj₁ [σ]))
        [σ′A]          = proj₁ (x ⊢Δ (proj₁ [σ′]))
        [σA≡σ′A]       = (proj₂ (x ⊢Δ (proj₁ [σ]))) (proj₁ [σ′]) (proj₁ [σ≡σ′])
        [headσ′≡headσ] = symEqTerm [σA] (proj₂ [σ≡σ′])
    in  convEqTerm₁ [σA] [σ′A] [σA≡σ′A] [headσ′≡headσ]

-- Transitivity of valid substitution
transS : ∀ {σ σ′ σ″ Γ Δ} ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
         ([σ]   : Δ ⊩ˢ σ   ∷ Γ / [Γ] / ⊢Δ)
         ([σ′]  : Δ ⊩ˢ σ′  ∷ Γ / [Γ] / ⊢Δ)
         ([σ″] : Δ ⊩ˢ σ″ ∷ Γ / [Γ] / ⊢Δ)
       → Δ ⊩ˢ σ  ≡ σ′  ∷ Γ / [Γ] / ⊢Δ / [σ]
       → Δ ⊩ˢ σ′ ≡ σ″ ∷ Γ / [Γ] / ⊢Δ / [σ′]
       → Δ ⊩ˢ σ  ≡ σ″ ∷ Γ / [Γ] / ⊢Δ / [σ]
transS ε′ ⊢Δ [σ] [σ′] [σ″] [σ≡σ′] [σ′≡σ″] = tt
transS ([Γ] ∙′ x) ⊢Δ [σ] [σ′] [σ″] [σ≡σ′] [σ′≡σ″] =
  transS [Γ] ⊢Δ (proj₁ [σ]) (proj₁ [σ′]) (proj₁ [σ″])
         (proj₁ [σ≡σ′]) (proj₁ [σ′≡σ″])
  , let [σA]   = proj₁ (x ⊢Δ (proj₁ [σ]))
        [σ′A]  = proj₁ (x ⊢Δ (proj₁ [σ′]))
        [σ″A] = proj₁ (x ⊢Δ (proj₁ [σ″]))
        [σ′≡σ″]′ = convEqTerm₂ [σA] [σ′A]
                                ((proj₂ (x ⊢Δ (proj₁ [σ]))) (proj₁ [σ′])
                                        (proj₁ [σ≡σ′])) (proj₂ [σ′≡σ″])
    in  transEqTerm [σA] (proj₂ [σ≡σ′]) [σ′≡σ″]′


text:
module Self where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)

data B : Set where
  T : B
  F : B

_&&_ : B -> B -> B
infixl 20 _&&_
T && T = T
T && F = F
F && _ = F

_||_ : B -> B -> B
infixl 15 _||_
T || _ = T
F || T = T
F || F = F

p||p≡p : ∀ (p : B) -> p || p ≡ p
p||p≡p T = refl
p||p≡p F = refl

p&&p≡p : ∀ (p : B) -> p && p ≡ p
p&&p≡p T = refl
p&&p≡p F = refl

-- 交换律

a&&b≡b&&a : ∀ (a b : B) -> a && b ≡ b && a
a&&b≡b&&a T T = refl
a&&b≡b&&a T F = refl
a&&b≡b&&a F T = refl
a&&b≡b&&a F F = refl

a||b≡b||a : ∀ (a b : B) -> a || b ≡ b || a
a||b≡b||a T T = refl
a||b≡b||a T F = refl
a||b≡b||a F T = refl
a||b≡b||a F F = refl

abc||abc : ∀ (a b c : B) -> (a || b) || c ≡ a || (b || c)
abc||abc T b c = refl
abc||abc F T c = refl
abc||abc F F T = refl
abc||abc F F F = refl

abc&&abc : ∀ (a b c : B) -> a && b && c ≡ a && (b && c)
abc&&abc T T T = refl
abc&&abc T T F = refl
abc&&abc T F c = refl
abc&&abc F b c = refl

-- 分配律

a&&b||c≡a&&b||a&&c : ∀ (a b c : B) -> a && (b || c) ≡ a && b || a && c
a&&b||c≡a&&b||a&&c T T c = refl
a&&b||c≡a&&b||a&&c T F T = refl
a&&b||c≡a&&b||a&&c T F F = refl
a&&b||c≡a&&b||a&&c F T c = refl
a&&b||c≡a&&b||a&&c F F c = refl

a||b&&c≡a||b&&a||c : ∀ (a b c : B) -> a || b && c ≡ (a || b) && (a || c)
a||b&&c≡a||b&&a||c T b c = refl
a||b&&c≡a||b&&a||c F T T = refl
a||b&&c≡a||b&&a||c F T F = refl
a||b&&c≡a||b&&a||c F F c = refl

T&&p≡p : ∀ (p : B) -> T && p ≡ p
T&&p≡p T = refl
T&&p≡p F = refl

F||p≡p : ∀ (p : B) -> F || p ≡ p
F||p≡p T = refl
F||p≡p F = refl

¬_ : B -> B
infix 25 ¬_
¬ F = T
¬ T = F

-- 负负得正
¬¬p≡p : ∀ (p : B) -> ¬ (¬ p) ≡ p
¬¬p≡p T = refl
¬¬p≡p F = refl

-- 德·摩根律

¬a&&b≡¬a||¬b : ∀ (a b : B) -> ¬ (a && b) ≡ ¬ a || ¬ b
¬a&&b≡¬a||¬b T T = refl
¬a&&b≡¬a||¬b T F = refl
¬a&&b≡¬a||¬b F T = refl
¬a&&b≡¬a||¬b F F = refl

¬a||b≡¬a&&¬b : ∀ (a b : B) -> ¬ (a || b) ≡ ¬ a && ¬ b
¬a||b≡¬a&&¬b T T = refl
¬a||b≡¬a&&¬b T F = refl
¬a||b≡¬a&&¬b F T = refl
¬a||b≡¬a&&¬b F F = refl

-- 自反律

p&&¬p≡F : ∀ (p : B) -> p && ¬ p ≡ F
p&&¬p≡F T = refl
p&&¬p≡F F = refl

-- 排中律

¬p||p≡T : ∀ (p : B) -> ¬ p || p ≡ T
¬p||p≡T T = refl
¬p||p≡T F = refl

-- 蕴含 如果 .. 就

_to_ : B -> B -> B
infixl 10 _to_
T to F = F
T to T = T
F to _ = T

-- 蕴含等值推演
ptoq≡¬p||q : ∀ (p q : B) -> p to q ≡ ¬ p || q
ptoq≡¬p||q T T = refl
ptoq≡¬p||q T F = refl
ptoq≡¬p||q F q = refl

Ttop≡p : ∀ (p : B) -> T to p ≡ p
Ttop≡p T = refl
Ttop≡p F = refl

Ftop≡T : ∀ (p : B) -> F to p ≡ T
Ftop≡T p = refl

-- 等价

_<>_ : B -> B -> B
infixl 10 _eq_
T <> T = T
F <> T = F
T <> F = F
F <> F = T

-- 等价等值式
p<>q≡ptoq&&qtop : ∀ (p q : B) -> p <> q ≡ (p to q) && (q to p)
p<>q≡ptoq&&qtop T T = refl
p<>q≡ptoq&&qtop T F = refl
p<>q≡ptoq&&qtop F T = refl
p<>q≡ptoq&&qtop F F = refl

-- lemma 01

p||q&&¬q≡p : ∀ (p q : B) -> p || q && ¬ q ≡ p
p||q&&¬q≡p T T = refl
p||q&&¬q≡p T F = refl
p||q&&¬q≡p F q rewrite p&&¬p≡F q = refl

-- proof 01

p&&q||p&&¬q≡p : ∀ (p q : B) -> p && q || p && ¬ q ≡ p
p&&q||p&&¬q≡p T T = refl
p&&q||p&&¬q≡p T F = refl
p&&q||p&&¬q≡p F q = refl

-- proof 02

atob≡¬bto¬a : ∀ (a b : B) -> a to b ≡ ¬ b to ¬ a
atob≡¬bto¬a a b
  rewrite ptoq≡¬p||q a b
    | ptoq≡¬p||q (¬ b) (¬ a)
    | a||b≡b||a (¬ a) b
    | ¬¬p≡p b = refl

implies₁ : ∀ (p q r s : B) -> ((p to (q to r)) && (¬ s || p) && q) to (s to r) ≡ T
implies₁ T T T T = refl
implies₁ T T T F = refl
implies₁ T T F s = refl
implies₁ T F T T = refl
implies₁ T F T F = refl
implies₁ T F F T = refl
implies₁ T F F F = refl
implies₁ F T T T = refl
implies₁ F T T F = refl
implies₁ F T F T = refl
implies₁ F T F F = refl
implies₁ F F r T = refl
implies₁ F F r F = refl

ext: agda

max_stars_repo_name: kands-code/agda-exercise

max_issues_repo_name: kands-code/agda-exercise

max_forks_repo_name: kands-code/agda-exercise


text:
module my-vector where

open import nat
open import bool
open import eq

data 𝕍 {ℓ}(A : Set ℓ) : ℕ → Set ℓ where
  [] : 𝕍 A 0
  _::_ : {n : ℕ} (x : A) (xs : 𝕍 A n) → 𝕍 A (suc n)

infixr 6 _::_ _++𝕍_

_++𝕍_ : ∀ {ℓ} {A : Set ℓ}{n m : ℕ} →
        𝕍 A n → 𝕍 A m → 𝕍 A (n + m)
[] ++𝕍 ys = ys
(x :: xs) ++𝕍 ys = x :: (xs ++𝕍 ys)

test-vector : 𝕍 𝔹 4
test-vector = ff :: tt :: ff :: ff :: []

test-vector-append : 𝕍 𝔹 8
test-vector-append = test-vector ++𝕍 test-vector

head𝕍 : ∀{ℓ}{A : Set ℓ}{n : ℕ} → 𝕍 A (suc n) → A
head𝕍 (x :: _) = x

tail𝕍 : ∀{ℓ}{A : Set ℓ}{n : ℕ} → 𝕍 A n → 𝕍 A (pred n)
tail𝕍 [] = []
tail𝕍 (_ :: xs) = xs

map𝕍 : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{n : ℕ} →
       (A → B) → 𝕍 A n → 𝕍 B n
map𝕍 f [] = []
map𝕍 f (x :: xs) = f x :: map𝕍 f xs

concat𝕍 : ∀{ℓ}{A : Set ℓ}{n m : ℕ} →
          𝕍 (𝕍 A n) m → 𝕍 A (m * n)
concat𝕍 [] = []
concat𝕍 (xs :: xs₁) = xs ++𝕍 (concat𝕍 xs₁)

nth𝕍 : ∀{ℓ}{A : Set ℓ}{m : ℕ} →
       (n : ℕ) → n < m ≡ tt → 𝕍 A m → A
nth𝕍 zero () []
nth𝕍 zero _ (x :: _) = x
nth𝕍 (suc _) () []
nth𝕍 (suc n₁) p (_ :: xs) = nth𝕍 n₁ p xs

repeat𝕍 : ∀{ℓ}{A : Set ℓ} → (a : A)(n : ℕ) → 𝕍 A n
repeat𝕍 a zero = []
repeat𝕍 a (suc n) = a :: (repeat𝕍 a n)

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
-- 2016-01-05, Jesper: In some cases, the new unifier is still too restrictive
-- when --cubical-compatible is enabled because it doesn't do generalization of datatype
-- indices. This should be fixed in the future.

-- 2016-06-23, Jesper: Now fixed.

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

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

data Bar : Set₁ where
  bar : Bar
  baz : (A : Set) → Bar

data Foo : Bar → Set₁ where
  foo : Foo bar

test : foo ≡ foo → Set₁
test refl = Set


text:
module _ where

module M (A : Set) where
  record R : Set where
    postulate
      B : Set

postulate
  A : Set
  r : M.R A

module M' = M A

open import Agda.Builtin.Reflection
open import Agda.Builtin.List

postulate
  any : {A : Set} → A

macro
  m : Term → TC _
  m goal =
    bindTC (inferType goal) λ goal-type →
    bindTC (normalise goal-type) λ goal-type →
    bindTC (inferType goal-type) λ _ →
    unify goal (def (quote any) [])

g : M'.R.B r
g = m

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Clowns where

import Equality
import Isomorphism
import Derivative
import ChainRule
open import Sets
open import Functor
open import Zipper
open import Dissect

open Functor.Recursive
open Functor.Semantics

-- Natural numbers
NatF : U
NatF = K [1] + Id

Nat : Set
Nat = μ NatF

zero : Nat
zero = inn (inl <>)

suc : Nat -> Nat
suc n = inn (inr n)

plus : Nat -> Nat -> Nat
plus n m = fold NatF φ n where
  φ : ⟦ NatF ⟧ Nat -> Nat
  φ (inl <>) = m
  φ (inr z)  = suc z

-- Lists
ListF : (A : Set) -> U
ListF A = K [1] + K A × Id

List' : (A : Set) -> Set
List' A = μ (ListF A)

nil : {A : Set} -> List' A
nil = inn (inl <>)

cons : {A : Set} -> A -> List' A -> List' A
cons x xs = inn (inr < x , xs >)

sum : List' Nat -> Nat
sum = fold (ListF Nat) φ where
  φ : ⟦ ListF Nat ⟧ Nat -> Nat
  φ (inl <>) = zero
  φ (inr < n , m >) = plus n m

TreeF : U
TreeF = K [1] + Id × Id

Tree : Set
Tree = μ TreeF

leaf : Tree
leaf = inn (inl <>)

node : Tree -> Tree -> Tree
node l r = inn (inr < l , r >)


text:
module Numeric.Nat.GCD.Properties where

open import Prelude
open import Numeric.Nat.Properties
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.GCD
open import Numeric.Nat.GCD.Extended
open import Tactic.Nat
open import Tactic.Cong

gcd-is-gcd : ∀ d a b → gcd! a b ≡ d → IsGCD d a b
gcd-is-gcd d a b refl with gcd a b
... | gcd-res _ isgcd = isgcd

gcd-divides-l : ∀ a b → gcd! a b Divides a
gcd-divides-l a b with gcd a b
... | gcd-res _ i = IsGCD.d|a i

gcd-divides-r : ∀ a b → gcd! a b Divides b
gcd-divides-r a b with gcd a b
... | gcd-res _ i = IsGCD.d|b i

is-gcd-unique : ∀ {a b} d₁ d₂ (g₁ : IsGCD d₁ a b) (g₂ : IsGCD d₂ a b) → d₁ ≡ d₂
is-gcd-unique d d′ (is-gcd d|a d|b gd) (is-gcd d′|a d′|b gd′) =
  divides-antisym (gd′ d d|a d|b)
                  (gd  d′ d′|a d′|b)

gcd-unique : ∀ a b d → IsGCD d a b → gcd! a b ≡ d
gcd-unique a b d pd with gcd a b
... | gcd-res d′ pd′ = is-gcd-unique d′ d pd′ pd

is-gcd-commute : ∀ {d a b} → IsGCD d a b → IsGCD d b a
is-gcd-commute (is-gcd d|a d|b g) = is-gcd d|b d|a (flip ∘ g)

gcd-commute : ∀ a b → gcd! a b ≡ gcd! b a
gcd-commute a b with gcd b a
gcd-commute a b | gcd-res d p = gcd-unique a b d (is-gcd-commute p)

gcd-factor-l : ∀ {a b} → a Divides b → gcd! a b ≡ a
gcd-factor-l {a} (factor! b) =
  gcd-unique a (b * a) a
             (is-gcd divides-refl (divides-mul-r b divides-refl) λ _ k|a _ → k|a)

gcd-factor-r : ∀ {a b} → b Divides a → gcd! a b ≡ b
gcd-factor-r {a} {b} b|a = gcd-commute a b ⟨≡⟩ gcd-factor-l b|a

gcd-idem : ∀ a → gcd! a a ≡ a
gcd-idem a = gcd-factor-l divides-refl

gcd-zero-l : ∀ n → gcd! 0 n ≡ n
gcd-zero-l n = gcd-unique 0 n n (is-gcd (factor! 0) divides-refl λ _ _ k|n → k|n)

gcd-zero-r : ∀ n → gcd! n 0 ≡ n
gcd-zero-r n = gcd-commute n 0 ⟨≡⟩ gcd-zero-l n

zero-is-gcd-l : ∀ {a b} → IsGCD 0 a b → a ≡ 0
zero-is-gcd-l (is-gcd 0|a _ _) = divides-zero 0|a

zero-is-gcd-r : ∀ {a b} → IsGCD 0 a b → b ≡ 0
zero-is-gcd-r (is-gcd _ 0|b _) = divides-zero 0|b

zero-gcd-l : ∀ a b → gcd! a b ≡ 0 → a ≡ 0
zero-gcd-l a b eq with gcd a b
zero-gcd-l a b refl | gcd-res .0 p = zero-is-gcd-l p

zero-gcd-r : ∀ a b → gcd! a b ≡ 0 → b ≡ 0
zero-gcd-r a b eq with gcd a b
zero-gcd-r a b refl | gcd-res .0 p = zero-is-gcd-r p

nonzero-is-gcd-l : ∀ {a b d} {{_ : NonZero a}} → IsGCD d a b → NonZero d
nonzero-is-gcd-l {0} {{}} _
nonzero-is-gcd-l {a@(suc _)} {d = suc _} _ = _
nonzero-is-gcd-l {a@(suc _)} {d = 0} (is-gcd (factor q eq) _ _) = refute eq

nonzero-is-gcd-r : ∀ {a b d} {{_ : NonZero b}} → IsGCD d a b → NonZero d
nonzero-is-gcd-r isgcd = nonzero-is-gcd-l (is-gcd-commute isgcd)

nonzero-gcd-l : ∀ a b {{_ : NonZero a}} → NonZero (gcd! a b)
nonzero-gcd-l a b = nonzero-is-gcd-l (GCD.isGCD (gcd a b))

nonzero-gcd-r : ∀ a b {{_ : NonZero b}} → NonZero (gcd! a b)
nonzero-gcd-r a b = nonzero-is-gcd-r (GCD.isGCD (gcd a b))

private
  _|>_ = divides-trans

gcd-assoc : ∀ a b c → gcd! a (gcd! b c) ≡ gcd! (gcd! a b) c
gcd-assoc a b c with gcd a b | gcd b c
... | gcd-res ab (is-gcd ab|a ab|b gab)
    | gcd-res bc (is-gcd bc|b bc|c gbc) with gcd ab c
...    | gcd-res ab-c (is-gcd abc|ab abc|c gabc) =
  gcd-unique a bc ab-c
             (is-gcd (abc|ab |> ab|a)
                     (gbc ab-c (abc|ab |> ab|b) abc|c)
                     λ k k|a k|bc → gabc k (gab k k|a (k|bc |> bc|b))
                                           (k|bc |> bc|c))

-- Coprimality properties

coprime-sym : ∀ a b → Coprime a b → Coprime b a
coprime-sym a b p = gcd-commute b a ⟨≡⟩ p

coprimeByDivide : ∀ a b → (∀ k → k Divides a → k Divides b → k Divides 1) → Coprime a b
coprimeByDivide a b g = gcd-unique a b 1 (is-gcd one-divides one-divides g)

divide-coprime : ∀ d a b → Coprime a b → d Divides a → d Divides b → d Divides 1
divide-coprime d a b p d|a d|b with gcd a b
divide-coprime d a b refl d|a d|b | gcd-res _ (is-gcd _ _ g) =
  g d d|a d|b

mul-coprime-l : ∀ a b c → Coprime a (b * c) → Coprime a b
mul-coprime-l a b c a⊥bc =
  coprimeByDivide a b λ k k|a k|b →
    divide-coprime k a (b * c) a⊥bc k|a (divides-mul-l c k|b)

mul-coprime-r : ∀ a b c → Coprime a (b * c) → Coprime a c
mul-coprime-r a b c a⊥bc = mul-coprime-l a c b (transport (Coprime a) auto a⊥bc)

is-gcd-factors-coprime : ∀ {a b d} (p : IsGCD d a b) {{_ : NonZero d}} →
                           Coprime (is-gcd-factor₁ p) (is-gcd-factor₂ p)
is-gcd-factors-coprime {a} {b} {0} _ {{}}
is-gcd-factors-coprime {a} {b} {d@(suc _)} p@(is-gcd (factor qa refl) (factor qb refl) g) with gcd qa qb
... | gcd-res j (is-gcd j|qa j|qb gj) = lem₃ j lem₂
  where
    lem : IsGCD (j * d) a b
    lem = is-gcd (divides-mul-cong-r d j|qa) (divides-mul-cong-r d j|qb) λ k k|a k|b →
                 divides-mul-r j (g k k|a k|b)

    lem₂ : d ≡ j * d
    lem₂ = is-gcd-unique d (j * d) p lem

    lem₃ : ∀ j → d ≡ j * d → j ≡ 1
    lem₃ 0 ()
    lem₃ 1 _ = refl
    lem₃ (suc (suc n)) eq = refute eq

private
  mul-gcd-distr-l' : ∀ a b c ⦃ a>0 : NonZero a ⦄ ⦃ b>0 : NonZero b ⦄ → gcd! (a * b) (a * c) ≡ a * gcd! b c
  mul-gcd-distr-l' a b c with gcd b c | gcd (a * b) (a * c)
  ... | gcd-res d gcd-bc@(is-gcd (factor! b′) (factor! c′) _)
      | gcd-res δ gcd-abac@(is-gcd (factor u uδ=ab) (factor v vδ=ac) g) =
    let instance _ = nonzero-is-gcd-l gcd-bc
                 _ : NonZero (d * a)
                 _ = mul-nonzero d a
    in case g (d * a) (factor b′ auto) (factor c′ auto) of λ where
         (factor w wda=δ) →
           let dab′=dauw =
                 d * a * b′        ≡⟨ by uδ=ab ⟩
                 u * δ             ≡⟨ u *_ $≡ wda=δ ⟩ʳ
                 u * (w * (d * a)) ≡⟨ auto ⟩
                 d * a * (u * w)   ∎
               dac′=davw =
                 d * a * c′        ≡⟨ by vδ=ac ⟩
                 v * δ             ≡⟨ v *_ $≡ wda=δ ⟩ʳ
                 v * (w * (d * a)) ≡⟨ auto ⟩
                 d * a * (v * w) ∎

               uw=b′ : u * w ≡ b′
               uw=b′ = sym (mul-inj₂ (d * a) b′ (u * w) dab′=dauw)
               vw=c′ : v * w ≡ c′
               vw=c′ = sym (mul-inj₂ (d * a) c′ (v * w) dac′=davw)
               w=1 : w ≡ 1
               w=1 = divides-one (divide-coprime w b′ c′ (is-gcd-factors-coprime gcd-bc)
                                 (factor u uw=b′)
                                 (factor v vw=c′))
           in case w=1 of λ where refl → by wda=δ

mul-gcd-distr-l : ∀ a b c → gcd! (a * b) (a * c) ≡ a * gcd! b c
mul-gcd-distr-l zero b c = refl
mul-gcd-distr-l a zero c = (λ z → gcd! z (a * c)) $≡ mul-zero-r a
mul-gcd-distr-l a@(suc _) b@(suc _) c = mul-gcd-distr-l' a b c

mul-gcd-distr-r : ∀ a b c → gcd! (a * c) (b * c) ≡ gcd! a b * c
mul-gcd-distr-r a b c =
  gcd! (a * c) (b * c)
    ≡⟨ gcd! $≡ mul-commute a c *≡ mul-commute b c ⟩
  gcd! (c * a) (c * b)
    ≡⟨ mul-gcd-distr-l c a b ⟩
  c * gcd! a b
    ≡⟨ auto ⟩
  gcd! a b * c ∎

-- Divide two numbers by their gcd and return the result, the gcd, and some useful properties.
-- Continuation-passing for efficiency reasons.
gcdReduce' : ∀ {a} {A : Set a} (a b : Nat) ⦃ _ : NonZero b ⦄ →
           ((a′ b′ d : Nat) → (⦃ _ : NonZero a ⦄ → NonZero a′) →
                              ⦃ nzb : NonZero b′ ⦄ → ⦃ nzd : NonZero d ⦄ →
                               a′ * d ≡ a → b′ * d ≡ b →
                               Coprime a′ b′ → A) → A
gcdReduce' a b ret with gcd a b
gcdReduce' a b ret | gcd-res d isgcd@(is-gcd d|a@(factor a′ eqa) d|b@(factor b′ eqb) g)=
  let instance _ = nonzero-is-gcd-r isgcd in
  ret a′ b′ d (nonzero-factor d|a) ⦃ nonzero-factor d|b ⦄
              eqa eqb
              (is-gcd-factors-coprime isgcd)

-- Both arguments are non-zero.
gcdReduce : ∀ {a} {A : Set a} (a b : Nat) ⦃ _ : NonZero a ⦄ ⦃ _ : NonZero b ⦄ →
           ((a′ b′ d : Nat) ⦃ a′>0 : NonZero a′ ⦄ ⦃ b′>0 : NonZero b′ ⦄ ⦃ nzd : NonZero d ⦄ →
            a′ * d ≡ a → b′ * d ≡ b → Coprime a′ b′ → A) → A
gcdReduce a b k = gcdReduce' a b λ a′ b′ d a′>0 eq₁ eq₂ a′⊥b′ →
  let instance _ = a′>0 in k a′ b′ d eq₁ eq₂ a′⊥b′

-- Only the right argument is guaranteed to be non-zero.
gcdReduce-r : ∀ {a} {A : Set a} (a b : Nat) ⦃ _ : NonZero b ⦄ →
           ((a′ b′ d : Nat) ⦃ nzb : NonZero b′ ⦄ ⦃ nzd : NonZero d ⦄ →
            a′ * d ≡ a → b′ * d ≡ b → Coprime a′ b′ → A) → A
gcdReduce-r a b k = gcdReduce' a b λ a′ b′ d _ eq₁ eq₂ a′⊥b′ →
  k a′ b′ d eq₁ eq₂ a′⊥b′

--- Properties ---

coprime-divide-mul-l : ∀ a b c → Coprime a b → a Divides (b * c) → a Divides c
coprime-divide-mul-l a b c p a|bc with extendedGCD a b
coprime-divide-mul-l a b c p a|bc | gcd-res d i e with gcd-unique _ _ _ i ʳ⟨≡⟩ p
coprime-divide-mul-l a b c p (factor q qa=bc) | gcd-res d i (bézoutL x y ax=1+by) | refl =
  factor (x * c - y * q) $
    (x * c - y * q) * a
      ≡⟨ auto ⟩
    a * x * c - y * (q * a)
      ≡⟨ by-cong ax=1+by ⟩
    suc (b * y) * c - y * (q * a)
      ≡⟨ by-cong qa=bc ⟩
    suc (b * y) * c - y * (b * c)
      ≡⟨ auto ⟩
    c ∎
coprime-divide-mul-l a b c p (factor q qa=bc) | gcd-res d i (bézoutR x y by=1+ax) | refl =
  factor (y * q - x * c) $
    (y * q - x * c) * a
      ≡⟨ auto ⟩
    y * (q * a) - a * x * c
      ≡⟨ by-cong qa=bc ⟩
    y * (b * c) - a * x * c
      ≡⟨ auto ⟩
    (b * y) * c - a * x * c
      ≡⟨ by-cong by=1+ax ⟩
    suc (a * x) * c - a * x * c
      ≡⟨ auto ⟩
    c ∎

coprime-divide-mul-r : ∀ a b c → Coprime a c → a Divides (b * c) → a Divides b
coprime-divide-mul-r a b c p a|bc =
  coprime-divide-mul-l a c b p (transport (a Divides_) auto a|bc)

is-gcd-by-coprime-factors : ∀ d a b (d|a : d Divides a) (d|b : d Divides b) ⦃ nzd : NonZero d ⦄ →
                            Coprime (get-factor d|a) (get-factor d|b) →
                            IsGCD d a b
is-gcd-by-coprime-factors d a b d|a@(factor! q) d|b@(factor! r) q⊥r =
  is-gcd d|a d|b λ k k|a k|b →
    let lem : ∀ j → j Divides q → j Divides r → j ≡ 1
        lem j j|q j|r = divides-one (divide-coprime j q r q⊥r j|q j|r)
    in
    case gcd k d of λ where
      (gcd-res g isgcd@(is-gcd (factor k′ k′g=k@refl) (factor d′ d′g=d@refl) sup)) →
        let instance g>0 = nonzero-is-gcd-r isgcd
            k′⊥d′ : Coprime k′ d′
            k′⊥d′ = is-gcd-factors-coprime isgcd
            k′|qd′ : k′ Divides (q * d′)
            k′|qd′ = cancel-mul-divides-r k′ (q * d′) g
                       (transport ((k′ * g) Divides_) {x = q * (d′ * g)} {q * d′ * g} auto k|a)
            k′|rd′ : k′ Divides (r * d′)
            k′|rd′ = cancel-mul-divides-r k′ (r * d′) g
                       (transport ((k′ * g) Divides_) {x = r * (d′ * g)} {r * d′ * g} auto k|b)
            k′|q : k′ Divides q
            k′|q = coprime-divide-mul-r k′ q d′ k′⊥d′ k′|qd′
            k′|r : k′ Divides r
            k′|r = coprime-divide-mul-r k′ r d′ k′⊥d′ k′|rd′
            k′=1 = lem k′ k′|q k′|r
            k=g : k ≡ g
            k=g = case k′=1 of λ where refl → auto
        in factor d′ (d′ *_ $≡ k=g ⟨≡⟩ d′g=d)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.QuotientAlgebra where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset using (_∈_)

open import Cubical.HITs.SetQuotients hiding (_/_)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.QuotientRing renaming (_/_ to _/Ring_) hiding ([_]/)
open import Cubical.Algebra.CommRing.Ideal hiding (IdealsIn)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Ideal
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.Ideal using (isIdeal)

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
  open CommRingStr {{...}} hiding (_-_; -_; dist; ·Lid; ·Rdist+) renaming (_·_ to _·R_; _+_ to _+R_)
  open CommAlgebraStr {{...}}
  open RingTheory (CommRing→Ring (CommAlgebra→CommRing A)) using (-DistR·)
  instance
    _ : CommRingStr _
    _ = snd R
    _ : CommAlgebraStr _ _
    _ = snd A

  _/_ : (I : IdealsIn A) → CommAlgebra R ℓ
  _/_ I = commAlgebraFromCommRing
           ((CommAlgebra→CommRing A) /Ring I)
           (λ r → elim (λ _ → squash/) (λ x → [ r ⋆ x ]) (eq r))
           (λ r s → elimProp (λ _ → squash/ _ _)
                             λ x i → [ ((r ·R s) ⋆ x ≡⟨ ⋆-assoc r s x ⟩
                                         r ⋆ (s ⋆ x) ∎) i ])
           (λ r s → elimProp (λ _ → squash/ _ _)
                             λ x i → [ ((r +R s) ⋆ x ≡⟨ ⋆-ldist r s x ⟩
                                       r ⋆ x + s ⋆ x ∎) i ])
           (λ r → elimProp2 (λ _ _ → squash/ _ _)
                            λ x y i → [ (r ⋆ (x + y)  ≡⟨ ⋆-rdist r x y ⟩
                                        r ⋆ x + r ⋆ y ∎) i ])
           (elimProp (λ _ → squash/ _ _)
                     (λ x i →  [ (1r ⋆ x ≡⟨ ⋆-lid x ⟩ x ∎) i ]))
           λ r → elimProp2 (λ _ _ → squash/ _ _)
                           λ x y i → [ ((r ⋆ x) · y ≡⟨ ⋆-lassoc r x y ⟩
                                       r ⋆ (x · y) ∎) i ]

          where
                open CommIdeal using (isCommIdeal)
                eq : (r : fst R) (x y : fst A) → x - y ∈ (fst I) →  [ r ⋆ x ] ≡ [ r ⋆ y ]
                eq r x y x-y∈I = eq/ _ _
                  (subst (λ u → u ∈ fst I)
                  ((r ⋆ 1a) · (x - y)               ≡⟨ ·Rdist+ (r ⋆ 1a) x (- y)  ⟩
                    (r ⋆ 1a) · x + (r ⋆ 1a) · (- y) ≡[ i ]⟨ (r ⋆ 1a) · x + -DistR· (r ⋆ 1a) y i ⟩
                    (r ⋆ 1a) · x - (r ⋆ 1a) · y     ≡[ i ]⟨ ⋆-lassoc r 1a x i
                                                            - ⋆-lassoc r 1a y i ⟩
                    r ⋆ (1a · x) - r ⋆ (1a · y)     ≡[ i ]⟨ r ⋆ (·Lid x i) - r ⋆ (·Lid y i) ⟩
                    r ⋆ x - r ⋆ y ∎ )
                  (isCommIdeal.·Closed (snd I) _ x-y∈I))

[_]/ : {R : CommRing ℓ} {A : CommAlgebra R ℓ} {I : IdealsIn A}
       → (a : fst A) → fst (A / I)
[ a ]/ = [ a ]

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Example by Ian Orton

{-# OPTIONS --rewriting #-}

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

_∧_ : Bool → Bool → Bool
true ∧ y = y
false ∧ y = false

data ⊥ : Set where

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()

¬_ : ∀ {a} → Set a → Set a
¬ A = A → ⊥

contradiction : ∀ {a b} {A : Set a} {B : Set b} → A → ¬ A → B
contradiction a f = ⊥-elim (f a)

_≢_ : ∀ {a} {A : Set a} (x y : A) → Set a
x ≢ y = ¬ (x ≡ y)

postulate
  obvious : (b b' : Bool) (p : b ≢ b') → (b ∧ b') ≡ false

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE obvious #-}

oops : (b : Bool) → b ∧ b ≡ false
oops b = refl

true≢false : true ≡ false → ⊥
true≢false ()

bot : ⊥
bot = true≢false (oops true)

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

open import Base
open import Homotopy.Pushout
open import Homotopy.VanKampen.Guide

{-
  This module provides the function code⇒path
  for the homotopy equivalence for
  van Kampen theorem.
-}

module Homotopy.VanKampen.CodeToPath {i} (d : pushout-diag i)
  (l : legend i (pushout-diag.C d)) where

  open pushout-diag d
  open legend l

  open import Homotopy.Truncation
  open import Homotopy.PathTruncation
  open import Homotopy.VanKampen.Code d l

  private
    pgl : ∀ n → _≡₀_ {A = P} (left (f $ loc n)) (right (g $ loc n))
    pgl n = proj (glue $ loc n)

    p!gl : ∀ n → _≡₀_ {A = P} (right (g $ loc n)) (left (f $ loc n))
    p!gl n = proj (! (glue $ loc n))

    ap₀l : ∀ {a₁ a₂} → a₁ ≡₀ a₂ → _≡₀_ {A = P} (left a₁) (left a₂)
    ap₀l p = ap₀ left p

    ap₀r : ∀ {b₁ b₂} → b₁ ≡₀ b₂ → _≡₀_ {A = P} (right b₁) (right b₂)
    ap₀r p = ap₀ right p

  module _ {a₁ : A} where
    private
      ap⇒path-split : (∀ {a₂} → a-code-a a₁ a₂ → _≡₀_ {A = P} (left a₁) (left  a₂))
                    × (∀ {b₂} → a-code-b a₁ b₂ → _≡₀_ {A = P} (left a₁) (right b₂))
      ap⇒path-split = a-code-rec-nondep a₁
        (λ a₂ → left a₁ ≡₀ left  a₂)
        ⦃ λ a₂ → π₀-is-set _ ⦄
        (λ b₂ → left a₁ ≡₀ right b₂)
        ⦃ λ b₂ → π₀-is-set _ ⦄
        (λ p → ap₀l p)
        (λ n pco p → (pco ∘₀ p!gl n) ∘₀ ap₀l p)
        (λ n pco p → (pco ∘₀ pgl  n) ∘₀ ap₀r p)
        (λ n {co} pco →
          (((pco ∘₀ pgl n) ∘₀ refl₀) ∘₀ p!gl n) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ pgl n) ∘₀ refl₀) ∘₀ p!gl n
            ≡⟨ ap (λ x → x ∘₀ p!gl n)
                  $ refl₀-right-unit $ pco ∘₀ pgl n ⟩
          (pco ∘₀ pgl n) ∘₀ p!gl n
            ≡⟨ concat₀-assoc pco (pgl n) (p!gl n) ⟩
          pco ∘₀ (pgl n ∘₀ p!gl n)
            ≡⟨ ap (λ x → pco ∘₀ proj x)
                  $ opposite-right-inverse $ glue $ loc n ⟩
          pco ∘₀ refl₀
            ≡⟨ refl₀-right-unit pco ⟩∎
          pco
            ∎)
        (λ n {co} pco →
          (((pco ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n
            ≡⟨ ap (λ x → x ∘₀ pgl n)
                  $ refl₀-right-unit $ pco ∘₀ p!gl n ⟩
          (pco ∘₀ p!gl n) ∘₀ pgl n
            ≡⟨ concat₀-assoc pco (p!gl n) (pgl n) ⟩
          pco ∘₀ (p!gl n ∘₀ pgl n)
            ≡⟨ ap (λ x → pco ∘₀ proj x)
                  $ opposite-left-inverse $ glue $ loc n ⟩
          pco ∘₀ refl₀
            ≡⟨ refl₀-right-unit pco ⟩∎
          pco
            ∎)
        (λ n₁ {co} pco n₂ r →
          (((pco ∘₀ pgl n₁) ∘₀ ap₀r (ap₀ g r)) ∘₀ p!gl n₂) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ pgl n₁) ∘₀ ap₀r (ap₀ g r)) ∘₀ p!gl n₂
            ≡⟨ concat₀-assoc (pco ∘₀ pgl n₁) (ap₀r (ap₀ g r)) (p!gl n₂) ⟩
          (pco ∘₀ pgl n₁) ∘₀ (ap₀r (ap₀ g r) ∘₀ p!gl n₂)
            ≡⟨ ap (λ x → (pco ∘₀ pgl n₁) ∘₀ (x ∘₀ p!gl n₂)) $ ! $ ap₀-compose right g r ⟩
          (pco ∘₀ pgl n₁) ∘₀ (ap₀ (right ◯ g) r ∘₀ p!gl n₂)
            ≡⟨ ap (λ x → (pco ∘₀ pgl n₁) ∘₀ x)
                  $ homotopy₀-naturality (right ◯ g) (left ◯ f) (proj ◯ (! ◯ glue)) r ⟩
          (pco ∘₀ pgl n₁) ∘₀ (p!gl n₁ ∘₀ ap₀ (left ◯ f) r)
            ≡⟨ ! $ concat₀-assoc (pco ∘₀ pgl n₁) (p!gl n₁) (ap₀ (left ◯ f) r) ⟩
          ((pco ∘₀ pgl n₁) ∘₀ p!gl n₁) ∘₀ ap₀ (left ◯ f) r
            ≡⟨ ap (λ x → ((pco ∘₀ pgl n₁) ∘₀ p!gl n₁) ∘₀ x) $ ap₀-compose left f r ⟩
          ((pco ∘₀ pgl n₁) ∘₀ p!gl n₁) ∘₀ ap₀l (ap₀ f r)
            ≡⟨ ap (λ x → (x ∘₀ p!gl n₁) ∘₀ ap₀l (ap₀ f r))
                  $ ! $ refl₀-right-unit $ pco ∘₀ pgl n₁ ⟩∎
          (((pco ∘₀ pgl n₁) ∘₀ refl₀) ∘₀ p!gl n₁) ∘₀ ap₀l (ap₀ f r)
            ∎)

    aa⇒path : ∀ {a₂} → a-code-a a₁ a₂ → _≡₀_ {A = P} (left a₁) (left  a₂)
    aa⇒path = π₁ ap⇒path-split
    ab⇒path : ∀ {b₂} → a-code-b a₁ b₂ → _≡₀_ {A = P} (left a₁) (right b₂)
    ab⇒path = π₂ ap⇒path-split

    ap⇒path : ∀ {p₂ : P} → a-code a₁ p₂ → left a₁ ≡₀ p₂
    ap⇒path {p₂} = pushout-rec
      (λ p → a-code a₁ p → left a₁ ≡₀ p)
      (λ a → aa⇒path {a})
      (λ b → ab⇒path {b})
      (loc-fiber-rec l
        (λ c → transport (λ p → a-code a₁ p → left a₁ ≡₀ p) (glue c) aa⇒path
             ≡ ab⇒path)
        ⦃ λ c → →-is-set (π₀-is-set (left a₁ ≡ right (g c))) _ _ ⦄
        (λ n → funext λ co →
            transport (λ p → a-code a₁ p → left a₁ ≡₀ p) (glue $ loc n) aa⇒path co
                ≡⟨ trans-→ (a-code a₁) (λ x → left a₁ ≡₀ x) (glue $ loc n) aa⇒path co ⟩
            transport (λ p → left a₁ ≡₀ p) (glue $ loc n) (aa⇒path $ transport (a-code a₁) (! (glue $ loc n)) co)
                ≡⟨ ap (transport (λ p → left a₁ ≡₀ p) (glue $ loc n) ◯ aa⇒path) $ trans-a-code-!glue-loc n co ⟩
            transport (λ p → left a₁ ≡₀ p) (glue $ loc n) (aa⇒path $ ab⇒aa n co)
                ≡⟨ trans-cst≡₀id (glue $ loc n) (aa⇒path $ ab⇒aa n co) ⟩
            (aa⇒path $ ab⇒aa n co) ∘₀ pgl n
                ≡⟨ refl ⟩
            ((ab⇒path co ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n
                ≡⟨ ap (λ x → x ∘₀ pgl n) $ refl₀-right-unit $ ab⇒path co ∘₀ p!gl n ⟩
            (ab⇒path co ∘₀ p!gl n) ∘₀ pgl n
                ≡⟨ concat₀-assoc (ab⇒path co) (p!gl n) (pgl n) ⟩
            ab⇒path co ∘₀ (p!gl n ∘₀ pgl n)
                ≡⟨ ap (λ x → ab⇒path co ∘₀ proj x) $ opposite-left-inverse $ glue $ loc n ⟩
            ab⇒path co ∘₀ refl₀
                ≡⟨ refl₀-right-unit $ ab⇒path co ⟩∎
            ab⇒path co
                ∎))
      p₂

  -- FIXME
  -- There is tension between reducing duplicate code and
  -- maintaining definitional equality. I could not make
  -- the neccessary type conversion definitional, so
  -- I just copied and pasted the previous module.
  module _ {b₁ : B} where
    private
      bp⇒path-split : (∀ {b₂} → b-code-b b₁ b₂ → _≡₀_ {A = P} (right b₁) (right  b₂))
                    × (∀ {a₂} → b-code-a b₁ a₂ → _≡₀_ {A = P} (right b₁) (left a₂))
      bp⇒path-split = b-code-rec-nondep b₁
        (λ b₂ → right b₁ ≡₀ right  b₂)
        ⦃ λ b₂ → π₀-is-set _ ⦄
        (λ a₂ → right b₁ ≡₀ left a₂)
        ⦃ λ a₂ → π₀-is-set _ ⦄
        (λ p → ap₀r p)
        (λ n pco p → (pco ∘₀ pgl  n) ∘₀ ap₀r p)
        (λ n pco p → (pco ∘₀ p!gl n) ∘₀ ap₀l p)
        (λ n {co} pco →
          (((pco ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n
            ≡⟨ ap (λ x → x ∘₀ pgl n)
                  $ refl₀-right-unit $ pco ∘₀ p!gl n ⟩
          (pco ∘₀ p!gl n) ∘₀ pgl n
            ≡⟨ concat₀-assoc pco (p!gl n) (pgl n) ⟩
          pco ∘₀ (p!gl n ∘₀ pgl n)
            ≡⟨ ap (λ x → pco ∘₀ proj x)
                  $ opposite-left-inverse $ glue $ loc n ⟩
          pco ∘₀ refl₀
            ≡⟨ refl₀-right-unit pco ⟩∎
          pco
            ∎)
        (λ n {co} pco →
          (((pco ∘₀ pgl n) ∘₀ refl₀) ∘₀ p!gl n) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ pgl n) ∘₀ refl₀) ∘₀ p!gl n
            ≡⟨ ap (λ x → x ∘₀ p!gl n)
                  $ refl₀-right-unit $ pco ∘₀ pgl n ⟩
          (pco ∘₀ pgl n) ∘₀ p!gl n
            ≡⟨ concat₀-assoc pco (pgl n) (p!gl n) ⟩
          pco ∘₀ (pgl n ∘₀ p!gl n)
            ≡⟨ ap (λ x → pco ∘₀ proj x)
                  $ opposite-right-inverse $ glue $ loc n ⟩
          pco ∘₀ refl₀
            ≡⟨ refl₀-right-unit pco ⟩∎
          pco
            ∎)
        (λ n₁ {co} pco n₂ r →
          (((pco ∘₀ p!gl n₁) ∘₀ ap₀l (ap₀ f r)) ∘₀ pgl n₂) ∘₀ refl₀
            ≡⟨ refl₀-right-unit _ ⟩
          ((pco ∘₀ p!gl n₁) ∘₀ ap₀l (ap₀ f r)) ∘₀ pgl n₂
            ≡⟨ concat₀-assoc (pco ∘₀ p!gl n₁) (ap₀l (ap₀ f r)) (pgl n₂) ⟩
          (pco ∘₀ p!gl n₁) ∘₀ (ap₀l (ap₀ f r) ∘₀ pgl n₂)
            ≡⟨ ap (λ x → (pco ∘₀ p!gl n₁) ∘₀ (x ∘₀ pgl n₂)) $ ! $ ap₀-compose left f r ⟩
          (pco ∘₀ p!gl n₁) ∘₀ (ap₀ (left ◯ f) r ∘₀ pgl n₂)
            ≡⟨ ap (λ x → (pco ∘₀ p!gl n₁) ∘₀ x)
                  $ homotopy₀-naturality (left ◯ f) (right ◯ g) (proj ◯  glue) r ⟩
          (pco ∘₀ p!gl n₁) ∘₀ (pgl n₁ ∘₀ ap₀ (right ◯ g) r)
            ≡⟨ ! $ concat₀-assoc (pco ∘₀ p!gl n₁) (pgl n₁) (ap₀ (right ◯ g) r) ⟩
          ((pco ∘₀ p!gl n₁) ∘₀ pgl n₁) ∘₀ ap₀ (right ◯ g) r
            ≡⟨ ap (λ x → ((pco ∘₀ p!gl n₁) ∘₀ pgl n₁) ∘₀ x) $ ap₀-compose right g r ⟩
          ((pco ∘₀ p!gl n₁) ∘₀ pgl n₁) ∘₀ ap₀r (ap₀ g r)
            ≡⟨ ap (λ x → (x ∘₀ pgl n₁) ∘₀ ap₀r (ap₀ g r))
                  $ ! $ refl₀-right-unit $ pco ∘₀ p!gl n₁ ⟩∎
          (((pco ∘₀ p!gl n₁) ∘₀ refl₀) ∘₀ pgl n₁) ∘₀ ap₀r (ap₀ g r)
            ∎)

    bb⇒path : ∀ {b₂} → b-code-b b₁ b₂ → _≡₀_ {A = P} (right b₁) (right  b₂)
    bb⇒path = π₁ bp⇒path-split
    ba⇒path : ∀ {a₂} → b-code-a b₁ a₂ → _≡₀_ {A = P} (right b₁) (left a₂)
    ba⇒path = π₂ bp⇒path-split

    bp⇒path : ∀ {p₂ : P} → b-code b₁ p₂ → right b₁ ≡₀ p₂
    bp⇒path {p₂} = pushout-rec
      (λ p → b-code b₁ p → right b₁ ≡₀ p)
      (λ a → ba⇒path {a})
      (λ b → bb⇒path {b})
      (λ c → loc-fiber-rec l
        (λ c → transport (λ p → b-code b₁ p → right b₁ ≡₀ p) (glue c) ba⇒path
             ≡ bb⇒path)
        ⦃ λ c → →-is-set (π₀-is-set (right b₁ ≡ right (g c))) _ _ ⦄
        (λ n → funext λ co →
            transport (λ p → b-code b₁ p → right b₁ ≡₀ p) (glue $ loc n) ba⇒path co
                ≡⟨ trans-→ (b-code b₁) (λ x → right b₁ ≡₀ x) (glue $ loc n) ba⇒path co ⟩
            transport (λ p → right b₁ ≡₀ p) (glue $ loc n) (ba⇒path $ transport (b-code b₁) (! (glue $ loc n)) co)
                ≡⟨ ap (transport (λ p → right b₁ ≡₀ p) (glue $ loc n) ◯ ba⇒path) $ trans-b-code-!glue-loc n co ⟩
            transport (λ p → right b₁ ≡₀ p) (glue $ loc n) (ba⇒path $ bb⇒ba n co)
                ≡⟨ trans-cst≡₀id (glue $ loc n) (ba⇒path $ bb⇒ba n co) ⟩
            (ba⇒path $ bb⇒ba n co) ∘₀ pgl n
                ≡⟨ refl ⟩
            ((bb⇒path co ∘₀ p!gl n) ∘₀ refl₀) ∘₀ pgl n
                ≡⟨ ap (λ x → x ∘₀ pgl n) $ refl₀-right-unit $ bb⇒path co ∘₀ p!gl n ⟩
            (bb⇒path co ∘₀ p!gl n) ∘₀ pgl n
                ≡⟨ concat₀-assoc (bb⇒path co) (p!gl n) (pgl n) ⟩
            bb⇒path co ∘₀ (p!gl n ∘₀ pgl n)
                ≡⟨ ap (λ x → bb⇒path co ∘₀ proj x) $ opposite-left-inverse $ glue $ loc n ⟩
            bb⇒path co ∘₀ refl₀
                ≡⟨ refl₀-right-unit $ bb⇒path co ⟩∎
            bb⇒path co
                ∎)
        c)
      p₂

  module _ where

    private
      Lbaaa : ∀ n {a₂} → b-code-a (g $ loc n) a₂ → Set i
      Lbaaa n co = aa⇒path {f $ loc n} (ba⇒aa n co) ≡ pgl n ∘₀ ba⇒path co
      Lbbab : ∀ n {b₂} → b-code-b (g $ loc n) b₂ → Set i
      Lbbab n co = ab⇒path {f $ loc n} (bb⇒ab n co) ≡ pgl n ∘₀ bb⇒path co

    private
      bp⇒ap⇒path-split : ∀ n
        → (∀ {a₂} co → Lbbab n {a₂} co)
        × (∀ {b₂} co → Lbaaa n {b₂} co)
    abstract
      bp⇒ap⇒path-split n = b-code-rec (g $ loc n)
        (λ co → ab⇒path {f $ loc n} (bb⇒ab n co) ≡ pgl n ∘₀ bb⇒path co)
        ⦃ λ _ → ≡-is-set $ π₀-is-set _ ⦄
        (λ co → aa⇒path {f $ loc n} (ba⇒aa n co) ≡ pgl n ∘₀ ba⇒path co)
        ⦃ λ _ → ≡-is-set $ π₀-is-set _ ⦄
        (λ p →
          ab⇒path (bb⇒ab n (⟧b p))
            ≡⟨ refl ⟩
          (refl₀ ∘₀ pgl n) ∘₀ ap₀r p
            ≡⟨ ap (λ x → x ∘₀ ap₀r p) $ refl₀-left-unit $ pgl n ⟩
          pgl n ∘₀ ap₀r p
            ≡⟨ refl ⟩∎
          pgl n ∘₀ bb⇒path (⟧b p)
            ∎)
        (λ n₁ {co} eq p₁ →
          (aa⇒path (ba⇒aa n co) ∘₀ pgl n₁) ∘₀ ap₀r p₁
            ≡⟨ ap (λ x → (x ∘₀ pgl n₁) ∘₀ ap₀r p₁) eq ⟩
          ((pgl n ∘₀ ba⇒path co) ∘₀ pgl n₁) ∘₀ ap₀r p₁
            ≡⟨ ap (λ x → x ∘₀ ap₀r p₁)
                  $ concat₀-assoc (pgl n) (ba⇒path co) (pgl n₁) ⟩
          (pgl n ∘₀ (ba⇒path co ∘₀ pgl n₁)) ∘₀ ap₀r p₁
            ≡⟨ concat₀-assoc (pgl n) (ba⇒path co ∘₀ pgl n₁) (ap₀r p₁) ⟩∎
          pgl n ∘₀ ((ba⇒path co ∘₀ pgl n₁) ∘₀ ap₀r p₁)
            ∎)
        (λ n₁ {co} eq p₁ →
          (ab⇒path (bb⇒ab n co) ∘₀ p!gl n₁) ∘₀ ap₀l p₁
            ≡⟨ ap (λ x → (x ∘₀ p!gl n₁) ∘₀ ap₀l p₁) eq ⟩
          ((pgl n ∘₀ bb⇒path co) ∘₀ p!gl n₁) ∘₀ ap₀l p₁
            ≡⟨ ap (λ x → x ∘₀ ap₀l p₁)
                  $ concat₀-assoc (pgl n) (bb⇒path co) (p!gl n₁) ⟩
          (pgl n ∘₀ (bb⇒path co ∘₀ p!gl n₁)) ∘₀ ap₀l p₁
            ≡⟨ concat₀-assoc (pgl n) (bb⇒path co ∘₀ p!gl n₁) (ap₀l p₁) ⟩∎
          pgl n ∘₀ ((bb⇒path co ∘₀ p!gl n₁) ∘₀ ap₀l p₁)
            ∎)
        (λ _ co → prop-has-all-paths (π₀-is-set _ _ _) _ co)
        (λ _ co → prop-has-all-paths (π₀-is-set _ _ _) _ co)
        (λ _ _ _ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _)

    ba⇒aa⇒path : ∀ n {a₂} co → Lbaaa n {a₂} co
    ba⇒aa⇒path n = π₂ $ bp⇒ap⇒path-split n
    bb⇒ab⇒path : ∀ n {b₂} co → Lbbab n {b₂} co
    bb⇒ab⇒path n = π₁ $ bp⇒ap⇒path-split n

    private
      bp⇒ap⇒path : ∀ n {p₂} (co : b-code (g $ loc n) p₂)
        → ap⇒path {f $ loc n} {p₂} (bp⇒ap n {p₂} co)
        ≡ pgl n ∘₀ bp⇒path {g $ loc n} {p₂} co
    abstract
      bp⇒ap⇒path n {p₂} = pushout-rec
        (λ x → ∀ (co : b-code (g $ loc n) x)
               → ap⇒path {f $ loc n} {x} (bp⇒ap n {x} co)
               ≡ pgl n ∘₀ bp⇒path {g $ loc n} {x} co)
        (λ a₂ → ba⇒aa⇒path n {a₂})
        (λ b₂ → bb⇒ab⇒path n {b₂})
        (λ _ → funext λ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _)
        p₂

    code⇒path : ∀ {p₁ p₂} → code p₁ p₂ → p₁ ≡₀ p₂
    code⇒path {p₁} {p₂} = pushout-rec
      (λ p₁ → code p₁ p₂ → p₁ ≡₀ p₂)
      (λ a → ap⇒path {a} {p₂})
      (λ b → bp⇒path {b} {p₂})
      (loc-fiber-rec l
        (λ c → transport (λ x → code x p₂ → x ≡₀ p₂) (glue c) (ap⇒path {f c} {p₂})
             ≡ bp⇒path {g c} {p₂})
        ⦃ λ c → →-is-set (π₀-is-set (right (g c) ≡ p₂)) _ _ ⦄
        (λ n → funext λ (co : code (right $ g $ loc n) p₂) →
          transport (λ x → code x p₂ → x ≡₀ p₂) (glue $ loc n) (ap⇒path {f $ loc n} {p₂}) co
              ≡⟨ trans-→ (λ x → code x p₂) (λ x → x ≡₀ p₂) (glue $ loc n) (ap⇒path {f $ loc n} {p₂}) co ⟩
          transport (λ x → x ≡₀ p₂) (glue $ loc n) (ap⇒path {f $ loc n} {p₂}
            $ transport (λ x → code x p₂) (! (glue $ loc n)) co)
              ≡⟨ ap (transport (λ x → x ≡₀ p₂) (glue $ loc n) ◯ ap⇒path {f $ loc n} {p₂})
                    $ trans-!glue-code-loc n {p₂} co ⟩
          transport (λ x → x ≡₀ p₂) (glue $ loc n) (ap⇒path {f $ loc n} {p₂} $ bp⇒ap n {p₂} co)
              ≡⟨ ap (transport (λ x → x ≡₀ p₂) (glue $ loc n)) $ bp⇒ap⇒path n {p₂} co ⟩
          transport (λ x → x ≡₀ p₂) (glue $ loc n) (pgl n ∘₀ bp⇒path {g $ loc n} {p₂} co)
              ≡⟨ trans-id≡₀cst (glue $ loc n) (pgl n ∘₀ bp⇒path {g $ loc n} {p₂} co) ⟩
          p!gl n ∘₀ (pgl n ∘₀ bp⇒path {g $ loc n} {p₂} co)
              ≡⟨ ! $ concat₀-assoc (p!gl n) (pgl n) (bp⇒path {g $ loc n} {p₂} co) ⟩
          (p!gl n ∘₀ pgl n) ∘₀ bp⇒path {g $ loc n} {p₂} co
              ≡⟨ ap (λ x → proj x ∘₀ bp⇒path {g $ loc n} {p₂} co) $ opposite-left-inverse (glue $ loc n) ⟩
          refl₀ ∘₀ bp⇒path {g $ loc n} {p₂} co
              ≡⟨ refl₀-left-unit (bp⇒path {g $ loc n} {p₂} co) ⟩∎
          bp⇒path {g $ loc n} {p₂} co
              ∎))
      p₁

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Example.Test where

open import Data.Maybe using (Is-just)

open import Prelude.Init
open import Prelude.DecEq
open import Prelude.Decidable

_ : (¬ ¬ ((true , true) ≡ (true , true)))
  × (8 ≡ 18 ∸ 10)
_ = auto

max_stars_repo_name: omelkonian/setup-agda

max_issues_repo_name: omelkonian/setup-agda

max_forks_repo_name: omelkonian/setup-agda


text:
-- Export only the experiments that are expected to compile (without
-- any holes)
{-# OPTIONS --cubical --no-import-sorts #-}
module Cubical.Experiments.Everything where

open import Cubical.Experiments.Brunerie public
open import Cubical.Experiments.EscardoSIP public
open import Cubical.Experiments.Generic public
open import Cubical.Experiments.NatMinusTwo
open import Cubical.Experiments.Problem
open import Cubical.Experiments.FunExtFromUA public
open import Cubical.Experiments.HoTT-UF
open import Cubical.Experiments.Rng

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:
module Web.URI.Port where

open import Web.URI.Port.Primitive public using ( Port? ; :80 ; ε )

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:
{-# OPTIONS --experimental-irrelevance #-}
-- {-# OPTIONS -v tc:10 #-}
module ExplicitLambdaExperimentalIrrelevance where

postulate
  A : Set
  T : ..(x : A) -> Set  -- shape irrelevant type

test : .(a : A) -> T a -> Set
test a = λ (x : T a) -> A
-- this should type check and not complain about irrelevance of a

module M .(a : A) where

  -- should also work with module parameter
  test1 : T a -> Set
  test1 = λ (x : T a) -> A

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
module Numeral.Integer where

open import Data.Tuple
open import Logic
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Relator.Equals
open import Type
open import Type.Quotient

-- Equivalence relation of difference equality.
-- Essentially (if one would already work in the integers):
--   (a₁ , a₂) diff-≡_ (b₁ , b₂)
--   ⇔ a₁ + b₂ ≡ a₂ + b₁
--   ⇔ a₁ − a₂ ≡ b₁ − b₂
_diff-≡_ : (ℕ ⨯ ℕ) → (ℕ ⨯ ℕ) → Stmt{Lvl.𝟎}
(a₁ , a₂) diff-≡ (b₁ , b₂) = (a₁ + b₂ ≡ a₂ + b₁)

ℤ : Type{Lvl.𝟎}
ℤ = (ℕ ⨯ ℕ) / (_diff-≡_)

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 hello-world where

open import IO
open import Data.String
open import Data.Nat
open import Data.Vec

main = run (putStrLn "Hello World!")

data Bool : Set where
  true : Bool
  false : Bool

if_then_else_ :  {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

new : {A : Set} -> A -> A
new x = x

_plus_ : {A : Set} -> A -> A -> A
x plus y = x

vec : Vec Bool 1
vec = true ∷ []

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


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

open import Setoids.Setoids
open import Rings.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Ideals.Principal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.Ideals.Definition R
open import Rings.Divisible.Definition R
open Setoid S

record PrincipalIdeal {c : _} {pred : A → Set c} (ideal : Ideal pred) : Set (a ⊔ b ⊔ c) where
  field
    generator : A
    genIsInIdeal : pred generator
    genGenerates : {x : A} → pred x → generator ∣ x


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Morphism.Properties
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Level
open import Algebra.FunctionProperties as FP
import Algebra.Linear.Morphism.Definitions as LinearMorphismDefinitions
import Algebra.Morphism as Morphism
open import Relation.Binary using (Rel; Setoid)
open import Relation.Binary.Morphism.Structures
open import Algebra.Morphism
open import Algebra.Linear.Structures.VectorSpace K
open import Algebra.Linear.Structures.Bundles

module _
  {a₁ ℓ₁} (From : VectorSpace K a₁ ℓ₁)
  {a₂ ℓ₂} (To   : VectorSpace K a₂ ℓ₂)
  where

  open import Algebra.Linear.Morphism.VectorSpace K

  private
    module F = VectorSpace From
    module T = VectorSpace To

    open VectorSpaceField

  open F
    using ()
    renaming
      ( Carrier     to A
      ; _≈_         to _≈₁_
      ; refl        to ≈₁-refl
      ; sym         to ≈₁-sym
      ; trans       to ≈₁-trans
      ; setoid      to setoid₁
      ; _+_         to _+₁_
      ; +-cong      to +₁-cong
      ; +-identityˡ  to +₁-identityˡ
      ; _∙_         to _∙₁_
      ; ∙-identity  to ∙₁-identity
      ; ∙-absorbˡ    to ∙₁-absorbˡ
      ; ∙-absorbʳ    to ∙₁-absorbʳ
      ; 0#          to 0₁
      )

  open T
    using ()
    renaming
      ( Carrier    to B
      ; _≈_        to _≈₂_
      ; refl       to ≈₂-refl
      ; sym        to ≈₂-sym
      ; trans      to ≈₂-trans
      ; setoid     to setoid₂
      ; _+_        to _+₂_
      ; +-cong     to +₂-cong
      ; +-identityˡ to +₂-identityˡ
      ; _∙_        to _∙₂_
      ; ∙-identity to ∙₂-identity
      ; ∙-absorbˡ   to ∙₂-absorbˡ
      ; ∙-absorbʳ   to ∙₂-absorbʳ
      ; 0#         to 0₂
      )

  open import Function
  open import Function.Equality

  open LinearDefinitions (VectorSpace.Carrier From) (VectorSpace.Carrier To) _≈₂_

  linear : ∀ (f : setoid₁ ⟶ setoid₂)
         -> (∀ (a b : K') (u v : A) -> (f ⟨$⟩ (a ∙₁ u +₁ b ∙₁ v)) ≈₂ a ∙₂ (f ⟨$⟩ u) +₂ b ∙₂ (f ⟨$⟩ v))
         -> IsLinearMap From To (f ⟨$⟩_)
  linear f lin = record
    { isAbelianGroupMorphism = record
      { gp-homo = record
        { mn-homo = record
          { sm-homo = record
            { ⟦⟧-cong = cong f
            ; ∙-homo = λ x y →
              begin
                f ⟨$⟩ x +₁ y
              ≈⟨ cong f (+₁-cong (≈₁-sym (∙₁-identity x)) (≈₁-sym (∙₁-identity y))) ⟩
                f ⟨$⟩ (1ᵏ ∙₁ x +₁ 1ᵏ ∙₁ y)
              ≈⟨ lin 1ᵏ 1ᵏ x y ⟩
                1ᵏ ∙₂ (f ⟨$⟩ x) +₂ 1ᵏ ∙₂ (f ⟨$⟩ y)
              ≈⟨ +₂-cong (∙₂-identity (f ⟨$⟩ x)) (∙₂-identity (f ⟨$⟩ y)) ⟩
                (f ⟨$⟩ x) +₂ (f ⟨$⟩ y)
              ∎
            }
          ; ε-homo =
            begin
              f ⟨$⟩ 0₁
            ≈⟨ cong f (≈₁-trans (≈₁-sym (+₁-identityˡ 0₁)) (+₁-cong (≈₁-sym (∙₁-absorbˡ 0₁)) (≈₁-sym (∙₁-absorbˡ 0₁)))) ⟩
              f ⟨$⟩ 0ᵏ ∙₁ 0₁ +₁ 0ᵏ ∙₁ 0₁
            ≈⟨ lin 0ᵏ 0ᵏ 0₁ 0₁ ⟩
              0ᵏ ∙₂ (f ⟨$⟩ 0₁) +₂ 0ᵏ ∙₂ (f ⟨$⟩ 0₁)
            ≈⟨ ≈₂-trans (+₂-cong (∙₂-absorbˡ (f ⟨$⟩ 0₁)) (∙₂-absorbˡ (f ⟨$⟩ 0₁))) (+₂-identityˡ 0₂) ⟩
              0₂
            ∎
          }
        }
      }
    ; ∙-homo = λ c u →
      begin
        f ⟨$⟩ c ∙₁ u
      ≈⟨ cong f (≈₁-trans (≈₁-sym (+₁-identityˡ (c ∙₁ u))) (+₁-cong (≈₁-sym (∙₁-absorbˡ 0₁)) ≈₁-refl)) ⟩
        f ⟨$⟩ 0ᵏ ∙₁ 0₁ +₁ c ∙₁ u
      ≈⟨ lin 0ᵏ c 0₁ u ⟩
        0ᵏ ∙₂ (f ⟨$⟩ 0₁) +₂ c ∙₂ (f ⟨$⟩ u)
      ≈⟨ ≈₂-trans (+₂-cong (∙₂-absorbˡ (f ⟨$⟩ 0₁)) ≈₂-refl) (+₂-identityˡ (c ∙₂ (f ⟨$⟩ u))) ⟩
        c ∙₂ (f ⟨$⟩ u)
      ∎
    }
    where open import Relation.Binary.EqReasoning setoid₂

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Issue408 where

open import Common.Prelude
open import Common.Equality

-- 1. Agda should prefer to split on an argument that covers

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

wk : {n : Nat} → Fin n → Fin (suc n)
wk zero = zero
wk (suc n) = suc (wk n)

predFin : (n : Nat) → Fin n → Fin n
predFin (suc n) zero    = zero
predFin (suc n) (suc i) = wk i
-- predFin should be covering

data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)

_!!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A
(x ∷ xs) !! zero    = x
(x ∷ xs) !! (suc i) = xs !! i
-- should be covering, no need for absurd clause

test!!1 : ∀ {A}{n} (x : A) (xs : Vec A n) →   (x ∷ xs) !! zero    ≡ x
test!!1 x xs = refl

test!!2 : ∀ {A}{n} (x : A) (xs : Vec A n) i → (x ∷ xs) !! (suc i) ≡ xs !! i
test!!2 x xs i = refl

-- 2. Agda should prefer  to split on an argument that has only
-- constructor patterns.  For max below, split on 2nd, then on 1st.

max : Nat → Nat → Nat
max (suc n) (suc m) = suc (max n m)
max 0       (suc m) = suc m
max n        0      = n

testmax1 : {n m : Nat} → max (suc n) (suc m) ≡ suc (max n m)
testmax1 = refl

testmax2 : {m : Nat} → max 0 (suc m) ≡ suc m
testmax2 = refl

{- DOES NOT WORK YET
testmax3 : {n : Nat} → max n 0 ≡ n
testmax3 = refl
-- equation should hold definitionally
-}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Extensions.Bool where

open import Data.Unit
open import Data.Bool
open import Relation.Nullary public using (yes; no; ¬_; Dec)

data All {p} (P : Set p) : Bool → Set p where
  true  : P → All P true
  false : All P false

data Any {p} (P : Set p) : Bool → Set p where
  true  : P → Any P true

all-map : ∀ {p} {P Q : Set p} {b} → All P b → (f : P → Q) → All Q b
all-map (true x) f = true (f x)
all-map false f = false

Is-true : Bool → Set
Is-true t = Any ⊤ t

is-yes : ∀ {a} {A : Set a} → Dec A → Bool
is-yes (yes p) = true
is-yes (no ¬p) = false


text:
{-# OPTIONS --erased-cubical #-}

-- Modules that use --cubical can be imported when --erased-cubical is
-- used.

open import Erased-cubical-Import.Cubical

-- However, definitions from such modules can only be used in erased
-- contexts.

_ : {A : Set} → A → ∥ A ∥
_ = ∣_∣


text:
module CTL.Modalities.EN where

open import FStream.Core
open import Library

-- Eventually (in) Next : p ⊧ φ ⇔ ∃ p[1] ⊧ φ
EN' : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} → FStream' C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
EN' s = EPred head (inF (tail s))

EN : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} → FStream C (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
EN s = EPred EN' (inF s)

mutual
  EN'ₛ : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁}
       → FStream' C (Set ℓ₂) → FStream' {i} C (Set (ℓ₁ ⊔ ℓ₂))
  head (EN'ₛ props) = EN' props
  tail (EN'ₛ props) = ENₛ (tail props)

  ENₛ : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁}
      → FStream C (Set ℓ₂) → FStream {i} C (Set (ℓ₁ ⊔ ℓ₂))
  inF (ENₛ props) = fmap EN'ₛ (inF props)

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


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

module Dodo.Binary.Dec where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Relation.Nullary using (Dec)
open import Relation.Binary using (REL)

DecRel : {a b ℓ : Level} {A : Set a} {B : Set b}
  → REL A B ℓ → Set (a ⊔ b ⊔ ℓ)
DecRel R = ∀ x y → Dec (R x y)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-# OPTIONS --cubical --prop #-}
module Issue2487-2 where

import Issue2487.Infective

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module #2 where

open import Relation.Binary.PropositionalEquality
open import #1

{-
Exercise 2.2. Show that the three equalities of proofs constructed in the previous exercise form a
commutative triangle. In other words, if the three definitions of concatenation are denoted by
(p ∘ q), (p ∘ q), and (p ∘ q), then the concatenated equality

         (p ∘ q) = (p ∘ q) = (p ∘ q)

is equal to the equality (p ∘ q) = (p ∘ q).
-}

composite-commutative-triangle : ∀ {i} {A : Set i}{x y z : A} → (p : x ≡ y) (q : y ≡ z) →
    composite (composite=composite' p q) (composite'=composite'' p q) ≡ composite=composite'' p q
composite-commutative-triangle refl refl = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


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

open import HoTT

{- Useful lemmas for computing the effect of transporting a function
 - across an equivalence in the domain or codomain.
 - TODO: find a better place for this. -}

module cohomology.FunctionOver where

{- transporting a function along an equivalence or path in the domain -}
module _ {i} {j} {B : Type i} {C : Type j} (g : B → C) where

  domain-over-path : {A : Type i} (p : A == B)
    → g ∘ coe p == g [ (λ D → (D → C)) ↓ p ]
  domain-over-path idp = idp

  domain-over-equiv : {A : Type i} (e : A ≃ B)
    → g ∘ –> e == g [ (λ D → (D → C)) ↓ ua e ]
  domain-over-equiv e = ↓-app→cst-in $ λ q → ap g (↓-idf-ua-out e q)

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

  domain!-over-path : {B : Type i} (p : A == B)
    → f == f ∘ coe! p [ (λ D → (D → C)) ↓ p ]
  domain!-over-path idp = idp

  domain!-over-equiv : {B : Type i} (e : A ≃ B)
    → f == f ∘ <– e [ (λ D → (D → C)) ↓ ua e ]
  domain!-over-equiv e = ↓-app→cst-in $
    λ q → ap f (! (<–-inv-l e _) ∙ ap (<– e) (↓-idf-ua-out e q))

{- transporting a ptd function along a equivalence or path in the domain -}
module _ {i} {j} {Y : Ptd i} {Z : Ptd j} (g : fst (Y ⊙→ Z)) where

  domain-over-⊙path : {X : Ptd i} (p : fst X == fst Y)
    (q : coe p (snd X) == snd Y)
    → g ⊙∘ (coe p , q) == g [ (λ W → fst (W ⊙→ Z)) ↓ pair= p (↓-idf-in p q) ]
  domain-over-⊙path idp idp = idp

  domain-over-⊙equiv : {X : Ptd i} (e : X ⊙≃ Y)
    → g ⊙∘ ⊙–> e == g [ (λ W → fst (W ⊙→ Z)) ↓ ⊙ua e ]
  domain-over-⊙equiv {X = X} e =
    ap (λ w → g ⊙∘ w) (! $ ⊙λ= (coe-β (⊙≃-to-≃ e)) idp)
    ◃ domain-over-⊙path (ua (⊙≃-to-≃ e))
                        (coe-β (⊙≃-to-≃ e) (snd X) ∙ snd (⊙–> e))

module _ {i} {j} {X : Ptd i} {Z : Ptd j} (f : fst (X ⊙→ Z)) where

  domain!-over-⊙path : {Y : Ptd i} (p : fst X == fst Y)
    (q : coe p (snd X) == snd Y)
    → f == f ⊙∘ (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (snd X))
      [ (λ W → fst (W ⊙→ Z)) ↓ pair= p (↓-idf-in p q) ]
  domain!-over-⊙path idp idp = idp

  domain!-over-⊙equiv : {Y : Ptd i} (e : X ⊙≃ Y)
    → f == f ⊙∘ (⊙<– e) [ (λ W → fst (W ⊙→ Z)) ↓ ⊙ua e ]
  domain!-over-⊙equiv {Y = Y} e =
    (! (ap (λ w → f ⊙∘ w) (⊙<–-inv-l e)) ∙ ! (⊙∘-assoc f _ (⊙–> e)))
    ◃ domain-over-⊙equiv (f ⊙∘ (⊙<– e)) e

{- transporting a function along an equivalence or path in the codomain -}
module _ {i} {j} {A : Type i} {B : Type j} (f : A → B) where

  codomain-over-path : {C : Type j} (p : B == C)
    → f == coe p ∘ f [ (λ D → (A → D)) ↓ p ]
  codomain-over-path idp = idp

  codomain-over-equiv : {C : Type j} (e : B ≃ C)
    → f == –> e ∘ f [ (λ D → (A → D)) ↓ ua e ]
  codomain-over-equiv e = ↓-cst→app-in $ λ _ → ↓-idf-ua-in e idp

module _ {i} {j} {A : Type i} {C : Type j} (g : A → C) where

  codomain!-over-path : {B : Type j} (p : B == C)
    → coe! p ∘ g == g [ (λ D → (A → D)) ↓ p ]
  codomain!-over-path idp = idp

  codomain!-over-equiv : {B : Type j} (e : B ≃ C)
    → <– e ∘ g == g [ (λ D → (A → D)) ↓ ua e ]
  codomain!-over-equiv e = ↓-cst→app-in $ λ _ → ↓-idf-ua-in e (<–-inv-r e _)

{- transporting a ptd function along a equivalence or path in the codomain -}
module _ {i} {j} {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y)) where

  codomain-over-⊙path : {Z : Ptd j} (p : fst Y == fst Z)
    (q : coe p (snd Y) == snd Z)
    → f == (coe p , q) ⊙∘ f [ (λ W → fst (X ⊙→ W)) ↓ pair= p (↓-idf-in p q) ]
  codomain-over-⊙path idp idp = pair= idp (! (∙-unit-r _ ∙ ap-idf (snd f)))

  codomain-over-⊙equiv : {Z : Ptd j} (e : Y ⊙≃ Z)
    → f == (⊙–> e) ⊙∘ f [ (λ W → fst (X ⊙→ W)) ↓ ⊙ua e ]
  codomain-over-⊙equiv {Z = Z} e =
    codomain-over-⊙path (ua (⊙≃-to-≃ e))
      (coe-β (⊙≃-to-≃ e) (snd Y) ∙ snd (⊙–> e))
    ▹ ap (λ w → w ⊙∘ f) (⊙λ= (coe-β (⊙≃-to-≃ e)) idp)

module _ {i} {j} {X : Ptd i} {Z : Ptd j} (g : fst (X ⊙→ Z)) where

  codomain!-over-⊙path : {Y : Ptd j} (p : fst Y == fst Z)
    (q : coe p (snd Y) == snd Z)
    → (coe! p , ap (coe! p) (! q) ∙ coe!-inv-l p (snd Y)) ⊙∘ g == g
      [ (λ W → fst (X ⊙→ W)) ↓ pair= p (↓-idf-in p q) ]
  codomain!-over-⊙path idp idp = pair= idp (∙-unit-r _ ∙ ap-idf (snd g))

  codomain!-over-⊙equiv : {Y : Ptd j} (e : Y ⊙≃ Z)
    → (⊙<– e) ⊙∘ g == g [ (λ W → fst (X ⊙→ W)) ↓ ⊙ua e ]
  codomain!-over-⊙equiv {Y = Y} e =
    codomain-over-⊙equiv (⊙<– e ⊙∘ g) e
    ▹ ! (⊙∘-assoc (⊙–> e) _ g) ∙ ap (λ w → w ⊙∘ g) (⊙<–-inv-r e) ∙ ⊙∘-unit-l g

module _ {i j} where

  function-over-paths : {A₁ B₁ : Type i} {A₂ B₂ : Type j}
    {f : A₁ → A₂} {g : B₁ → B₂} (p₁ : A₁ == B₁) (p₂ : A₂ == B₂)
    → coe p₂ ∘ f == g ∘ coe p₁
    → f == g [ (λ {(A , B) → A → B}) ↓ pair×= p₁ p₂ ]
  function-over-paths idp idp α = α

  function-over-equivs : {A₁ B₁ : Type i} {A₂ B₂ : Type j}
    {f : A₁ → A₂} {g : B₁ → B₂} (e₁ : A₁ ≃ B₁) (e₂ : A₂ ≃ B₂)
    → –> e₂ ∘ f == g ∘ –> e₁
    → f == g [ (λ {(A , B) → A → B}) ↓ pair×= (ua e₁) (ua e₂) ]
  function-over-equivs {f = f} {g = g} e₁ e₂ α =
    function-over-paths (ua e₁) (ua e₂) $
      transport (λ {(h , k) → h ∘ f == g ∘ k})
        (pair×= (! (λ= (coe-β e₂))) (! (λ= (coe-β e₁)))) α

{- transporting a group homomorphism along an isomorphism -}

domain-over-iso : ∀ {i j} {G H : Group i} {K : Group j}
  {φ : G →ᴳ H} {ie : is-equiv (GroupHom.f φ)} {ψ : G →ᴳ K} {χ : H →ᴳ K}
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → A → Group.El K) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → J →ᴳ K) ↓ group-ua (φ , ie) ]
domain-over-iso {K = K} {φ = φ} {ie} {ψ} {χ} p =
  hom=-↓ _ _ $ ↓-ap-out _ Group.El _ $
    transport
      (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → A → Group.El K) ↓ q ])
      (! (group-ua-el (φ , ie)))
      p

codomain-over-iso : ∀ {i j} {G : Group i} {H K : Group j}
  {φ : H →ᴳ K} {ie : is-equiv (GroupHom.f φ)} {ψ : G →ᴳ H} {χ : G →ᴳ K}
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ A → Group.El G → A) ↓ ua (GroupHom.f φ , ie) ]
  → ψ == χ [ (λ J → G →ᴳ J) ↓ group-ua (φ , ie) ]
codomain-over-iso {G = G} {φ = φ} {ie} {ψ} {χ} p =
  hom=-↓ _ _ $ ↓-ap-out _ Group.El _ $
    transport
      (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ A → Group.El G → A) ↓ q ])
      (! (group-ua-el (φ , ie)))
      p

hom-over-isos : ∀ {i j} {G₁ H₁ : Group i} {G₂ H₂ : Group j}
  {φ₁ : G₁ →ᴳ H₁} {ie₁ : is-equiv (GroupHom.f φ₁)}
  {φ₂ : G₂ →ᴳ H₂} {ie₂ : is-equiv (GroupHom.f φ₂)}
  {ψ : G₁ →ᴳ G₂} {χ : H₁ →ᴳ H₂}
  → GroupHom.f ψ == GroupHom.f χ
    [ (λ {(A , B) → A → B}) ↓ pair×= (ua (GroupHom.f φ₁ , ie₁))
                                     (ua (GroupHom.f φ₂ , ie₂)) ]
  → ψ == χ [ uncurry _→ᴳ_ ↓ pair×= (group-ua (φ₁ , ie₁)) (group-ua (φ₂ , ie₂)) ]
hom-over-isos {φ₁ = φ₁} {ie₁} {φ₂} {ie₂} {ψ} {χ} p = hom=-↓ _ _ $
  ↓-ap-out (λ {(A , B) → A → B}) (λ {(G , H) → (Group.El G , Group.El H)}) _ $
    transport
      (λ q → GroupHom.f ψ == GroupHom.f χ [ (λ {(A , B) → A → B}) ↓ q ])
      (ap2 (λ p q → pair×= p q) (! (group-ua-el (φ₁ , ie₁)))
                                (! (group-ua-el (φ₂ , ie₂)))
       ∙ ! (lemma Group.El Group.El
             (group-ua (φ₁ , ie₁)) (group-ua (φ₂ , ie₂))))
      p
  where
  lemma : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
    (f : A → C) (g : B → D) {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap (λ {(a , b) → (f a , g b)}) (pair×= p q)
      == pair×= (ap f p) (ap g q)
  lemma f g idp idp = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
module Numeral.PositiveInteger.Oper.Proofs where

open import Functional
open import Function.Equals
open import Function.Iteration
open import Function.Iteration.Proofs
open import Logic.Propositional
open import Logic.Predicate
import      Numeral.Natural as ℕ
import      Numeral.Natural.Oper as ℕ
open import Numeral.PositiveInteger
open import Numeral.PositiveInteger.Oper
open import Relator.Equals
open import Relator.Equals.Proofs
import      Function.Names as Names
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Syntax.Transitivity
open import Type

-- TODO: Move stuff related to ℕ₊-to-ℕ

instance
  ℕ-ℕ₊-preserves-𝐒 : Preserving₁(ℕ₊-to-ℕ)(𝐒)(ℕ.𝐒)
  Preserving.proof ℕ-ℕ₊-preserves-𝐒 = p where
    p : Names.Preserving₁(ℕ₊-to-ℕ)(𝐒)(ℕ.𝐒)
    p {𝟏}   = [≡]-intro
    p {𝐒 x} = congruence₁(ℕ.𝐒) p

instance
  ℕ-ℕ₊-preserves-[+] : Preserving₂(ℕ₊-to-ℕ)(_+_)(ℕ._+_)
  Preserving.proof ℕ-ℕ₊-preserves-[+] = p where
    p : Names.Preserving₂(ℕ₊-to-ℕ)(_+_)(ℕ._+_)
    p {x} {𝟏}   = [≡]-intro
    p {x} {𝐒 y} = congruence₁(ℕ.𝐒) p

instance
  ℕ-ℕ₊-preserves-[⋅] : Preserving₂(ℕ₊-to-ℕ)(_⋅_)(ℕ._⋅_)
  Preserving.proof ℕ-ℕ₊-preserves-[⋅] {x}{y} = p{x}{y} where
    p : Names.Preserving₂(ℕ₊-to-ℕ)(_⋅_)(ℕ._⋅_)
    p {x} {𝟏}   = [≡]-intro
    p {x} {𝐒 y} =
      ℕ₊-to-ℕ (x + (x ⋅ y))                         🝖[ _≡_ ]-[ preserving₂(ℕ₊-to-ℕ)(_+_)(ℕ._+_) ]
      (ℕ₊-to-ℕ x) ℕ.+ (ℕ₊-to-ℕ (x ⋅ y))             🝖[ _≡_ ]-[ congruence₁((ℕ₊-to-ℕ x) ℕ.+_) (p{x}{y}) ]
      (ℕ₊-to-ℕ x) ℕ.+ ((ℕ₊-to-ℕ x) ℕ.⋅ (ℕ₊-to-ℕ y)) 🝖[ _≡_ ]-end

instance
  𝐒-from-ℕ-preserves-𝐒 : Preserving₁(𝐒-from-ℕ)(ℕ.𝐒)(𝐒)
  Preserving.proof 𝐒-from-ℕ-preserves-𝐒 = [≡]-intro

instance
  𝐒-from-ℕ-preserves-[+] : Preserving₂(𝐒-from-ℕ)(ℕ.𝐒 ∘₂ ℕ._+_)(_+_)
  Preserving.proof 𝐒-from-ℕ-preserves-[+] = p where
    p : Names.Preserving₂(𝐒-from-ℕ)(ℕ.𝐒 ∘₂ ℕ._+_)(_+_)
    p {x}{ℕ.𝟎}   = [≡]-intro
    p {x}{ℕ.𝐒 y} = congruence₁(𝐒) (p {x}{y})

{-instance
  𝐒-from-ℕ-preserves-[⋅] : Preserving₂(𝐒-from-ℕ)(ℕ.𝐒 ∘₂ ℕ._⋅_ )(_⋅_)
  Preserving.proof 𝐒-from-ℕ-preserves-[⋅] = p where
    p : Names.Preserving₂(𝐒-from-ℕ)(ℕ.𝐒 ∘₂ ℕ._⋅_ )(_⋅_)
    p {x}{ℕ.𝟎}   = {!!}
    p {x}{ℕ.𝐒 y} = {!!}
-}
{-      𝐒-from-ℕ (ℕ.𝐒(x ℕ.+ (x ℕ.⋅ ℕ.𝐒(y))))         🝖[ _≡_ ]-[ preserving₂(𝐒-from-ℕ)(ℕ.𝐒 ∘₂ ℕ._+_)(_+_) ]
      (𝐒-from-ℕ x) + (𝐒-from-ℕ (x ℕ.⋅ ℕ.𝐒(y)))     🝖[ _≡_ ]-[]
      (𝐒-from-ℕ x) + (𝐒-from-ℕ (x ℕ.+ (x ℕ.⋅ y)))  🝖[ _≡_ ]-[ congruence₁((𝐒-from-ℕ x) +_) (p{x}{y}) ]
      (𝐒-from-ℕ x) + ((𝐒-from-ℕ x) ⋅ (𝐒-from-ℕ y)) 🝖[ _≡_ ]-end
-}

{-
instance
  ℕ₊-to-ℕ-injective : Injective(ℕ₊-to-ℕ)
  Injective.proof ℕ₊-to-ℕ-injective {𝟏}   {𝟏}   p = [≡]-intro
  Injective.proof ℕ₊-to-ℕ-injective {𝟏}   {𝐒 y} p = {!congruence₁(\x → ℕ-to-ℕ₊ x ⦃ ? ⦄) p!}
  Injective.proof ℕ₊-to-ℕ-injective {𝐒 x} {𝟏}   p = {!preserving₁(ℕ₊-to-ℕ)(𝐒)(ℕ.𝐒) 🝖 p!}
  Injective.proof ℕ₊-to-ℕ-injective {𝐒 x} {𝐒 y} p = {!!}
-}

{-
module _ where
  [+]-repeatᵣ-𝐒 : ∀{x y z : ℕ} → (x + y ≡ repeatᵣ y (const 𝐒) z x)
  [+]-repeatᵣ-𝐒 {x} {𝟎}       = [≡]-intro
  [+]-repeatᵣ-𝐒 {x} {𝐒 y} {z} = congruence₁(𝐒) ([+]-repeatᵣ-𝐒 {x} {y} {z})

  [+]-repeatₗ-𝐒 : ∀{x y z : ℕ} → (x + y ≡ repeatₗ y (const ∘ 𝐒) x z)
  [+]-repeatₗ-𝐒 {x} {𝟎}       = [≡]-intro
  [+]-repeatₗ-𝐒 {x} {𝐒 y} {z} = congruence₁(𝐒) ([+]-repeatₗ-𝐒 {x} {y} {z})

  [⋅]-repeatᵣ-[+] : ∀{x y} → (x ⋅ y ≡ repeatᵣ y (_+_) x 0)
  [⋅]-repeatᵣ-[+] {x} {𝟎}   = [≡]-intro
  [⋅]-repeatᵣ-[+] {x} {𝐒 y} = congruence₁(x +_) ([⋅]-repeatᵣ-[+] {x} {y})

  [^]-repeatᵣ-[⋅] : ∀{x y} → (x ^ y ≡ repeatᵣ y (_⋅_) x 1)
  [^]-repeatᵣ-[⋅] {x} {𝟎}   = [≡]-intro
  [^]-repeatᵣ-[⋅] {x} {𝐒 y} = congruence₁(x ⋅_) ([^]-repeatᵣ-[⋅] {x} {y})
-}

instance
  [𝐒]-injective : Injective(𝐒)
  Injective.proof [𝐒]-injective [≡]-intro = [≡]-intro

[1+]-𝐒 : ∀{x : ℕ₊} → (𝟏 + x ≡ 𝐒(x))
[1+]-𝐒 {𝟏}   = [≡]-intro
[1+]-𝐒 {𝐒 x} = congruence₁(𝐒) ([1+]-𝐒 {x})
{-# REWRITE [1+]-𝐒 #-}

[+]-step : ∀{x y : ℕ₊} → (𝐒(x) + y) ≡ (x + 𝐒(y))
[+]-step {x} {𝟏}   = [≡]-intro
[+]-step {x} {𝐒 y} = congruence₁(𝐒) ([+]-step {x} {y})
{-# REWRITE [+]-step #-}

[+]-commutativity-raw : Names.Commutativity(_+_)
[+]-commutativity-raw {𝟏}   {𝟏}   = [≡]-intro
[+]-commutativity-raw {𝟏}   {𝐒 y} = congruence₁(𝐒) ([+]-commutativity-raw {𝟏} {y})
[+]-commutativity-raw {𝐒 x} {𝟏}   = congruence₁(𝐒) ([+]-commutativity-raw {x} {𝟏})
[+]-commutativity-raw {𝐒 x} {𝐒 y} = congruence₁(𝐒) (congruence₁(𝐒) ([+]-commutativity-raw {x} {y}))

instance
  [+]-commutativity : Commutativity(_+_)
  [+]-commutativity = intro [+]-commutativity-raw

[+]-associativity-raw : Names.Associativity(_+_)
[+]-associativity-raw {x} {y} {𝟏} = [≡]-intro
[+]-associativity-raw {x} {y} {𝐒 z} = congruence₁(𝐒) ([+]-associativity-raw {x} {y} {z})

instance
  [+]-associativity : Associativity(_+_)
  [+]-associativity = intro [+]-associativity-raw

[⋅]-identityₗ-raw : Names.Identityₗ(_⋅_)(𝟏)
[⋅]-identityₗ-raw {𝟏}   = [≡]-intro
[⋅]-identityₗ-raw {𝐒 x} = congruence₁(𝐒) ([⋅]-identityₗ-raw {x}) -- commutativity(_+_) 🝖 congruence₁(𝐒) ([⋅]-identityₗ-raw {x})
{-# REWRITE [⋅]-identityₗ-raw #-}

[⋅]-identityᵣ-raw : Names.Identityᵣ(_⋅_)(𝟏)
[⋅]-identityᵣ-raw = [≡]-intro

instance
  [⋅]-identityₗ : Identityₗ(_⋅_)(𝟏)
  [⋅]-identityₗ = intro [⋅]-identityₗ-raw

instance
  [⋅]-identityᵣ : Identityᵣ(_⋅_)(𝟏)
  [⋅]-identityᵣ = intro [⋅]-identityᵣ-raw

instance
  [⋅]-identity : Identity(_⋅_)(𝟏)
  [⋅]-identity = intro

[⋅]-commutativity-raw : Names.Commutativity(_⋅_) -- TODO: Extract the proof of (x + (𝐒 x + 𝐒 y) ≡ y + (𝐒 x + 𝐒 y)). Note that the properties here can probably also be proven using Function.Repeat.Proofs
[⋅]-commutativity-raw {x} {𝟏}   = [≡]-intro
[⋅]-commutativity-raw {𝟏} {𝐒 y} = [≡]-intro
[⋅]-commutativity-raw {𝐒 x} {𝐒 y} =
  𝐒 x ⋅ 𝐒 y           🝖[ _≡_ ]-[]
  𝐒 x + (𝐒 x ⋅ y)     🝖-[ congruence₁(𝐒) (congruence₂ᵣ(_+_)(x) ([⋅]-commutativity-raw {𝐒 x} {y})) ]
  𝐒 x + (y ⋅ 𝐒 x)     🝖[ _≡_ ]-[]
  𝐒 x + (y ⋅ 𝐒 x)     🝖[ _≡_ ]-[]
  𝐒 x + (y + (y ⋅ x)) 🝖-[ congruence₁(𝐒) (associativity(_+_)) ]-sym
  (𝐒 x + y) + (y ⋅ x) 🝖[ _≡_ ]-[]
  𝐒(x + y) + (y ⋅ x)  🝖-[ congruence₁(𝐒) (congruence₂(_+_) ([+]-commutativity-raw {x}{y}) ([⋅]-commutativity-raw {y}{x})) ]
  𝐒(y + x) + (x ⋅ y)  🝖[ _≡_ ]-[]
  (𝐒 y + x) + (x ⋅ y) 🝖-[ congruence₁(𝐒) (associativity(_+_)) ]
  𝐒 y + (x + (x ⋅ y)) 🝖[ _≡_ ]-[]
  𝐒 y + (x ⋅ 𝐒 y)     🝖-[ congruence₁(𝐒) (congruence₂ᵣ(_+_)(y) ([⋅]-commutativity-raw {𝐒 y} {x})) ]-sym
  𝐒 y + (𝐒 y ⋅ x)     🝖[ _≡_ ]-[]
  𝐒 y ⋅ 𝐒 x           🝖-end

instance
  [⋅]-commutativity : Commutativity(_⋅_)
  [⋅]-commutativity = intro(\{x}{y} → [⋅]-commutativity-raw {x}{y})

[⋅][+]-distributivityᵣ-raw : Names.Distributivityᵣ(_⋅_)(_+_)
[⋅][+]-distributivityᵣ-raw {x} {y} {𝟏}   = [≡]-intro
[⋅][+]-distributivityᵣ-raw {x} {y} {𝐒 z} =
  (x + y) + ((x + y) ⋅ z)       🝖[ _≡_ ]-[ congruence₁((x + y) +_) ([⋅][+]-distributivityᵣ-raw {x} {y} {z}) ]
  (x + y) + ((x ⋅ z) + (y ⋅ z)) 🝖[ _≡_ ]-[ One.associate-commute4 {a = x}{y}{x ⋅ z}{y ⋅ z} ([+]-commutativity-raw{x = y}) ]
  (x + (x ⋅ z)) + (y + (y ⋅ z)) 🝖[ _≡_ ]-[]
  (x ⋅ 𝐒(z)) + (y ⋅ 𝐒(z))       🝖[ _≡_ ]-end

instance
  [⋅][+]-distributivityᵣ : Distributivityᵣ(_⋅_)(_+_)
  [⋅][+]-distributivityᵣ = intro(\{x}{y}{z} → [⋅][+]-distributivityᵣ-raw {x}{y}{z})

instance
  [⋅][+]-distributivityₗ : Distributivityₗ(_⋅_)(_+_)
  [⋅][+]-distributivityₗ = [↔]-to-[←] OneTypeTwoOp.distributivity-equivalence-by-commutativity [⋅][+]-distributivityᵣ

[⋅]-associativity-raw : Names.Associativity(_⋅_)
[⋅]-associativity-raw {x} {y} {𝟏} = [≡]-intro
[⋅]-associativity-raw {x} {y} {𝐒 z} =
  (x ⋅ y) + (x ⋅ y ⋅ z)   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(x ⋅ y) ([⋅]-associativity-raw {x}{y}{z}) ]
  (x ⋅ y) + (x ⋅ (y ⋅ z)) 🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_+_) {x = x}{y = y}{z = y ⋅ z} ]-sym
  x ⋅ (y + (y ⋅ z))       🝖-end

instance
  [⋅]-associativity : Associativity(_⋅_)
  [⋅]-associativity = intro(\{x}{y}{z} → [⋅]-associativity-raw {x}{y}{z})

instance
  ℕ₊-multiplicative-monoid : Monoid(_⋅_)
  Monoid.binary-operator    ℕ₊-multiplicative-monoid = [≡]-binary-operator
  Monoid.identity-existence ℕ₊-multiplicative-monoid = [∃]-intro(𝟏)

[⋅]-with-[𝐒]ₗ : ∀{x y} → (𝐒(x) ⋅ y ≡ (x ⋅ y) + y)
[⋅]-with-[𝐒]ₗ {x}{y} =
  𝐒(x) ⋅ y          🝖[ _≡_ ]-[ congruence₁(_⋅ y) [1+]-𝐒 ]-sym
  (x + 𝟏) ⋅ y       🝖[ _≡_ ]-[ [⋅][+]-distributivityᵣ-raw{x}{𝟏}{y} ]
  (x ⋅ y) + (𝟏 ⋅ y) 🝖[ _≡_ ]-[ congruence₁((x ⋅ y) +_) ([⋅]-identityₗ-raw {y}) ]
  (x ⋅ y) + y       🝖[ _≡_ ]-end

[⋅]-with-[𝐒]ᵣ : ∀{x y} → (x ⋅ 𝐒(y) ≡ x + (x ⋅ y))
[⋅]-with-[𝐒]ᵣ = [≡]-intro


text:
-- Andreas, 2017-01-26, issue #2436
-- Outlaw coinductive records with eta-equality

record U : Set where
  coinductive
  eta-equality
  field f : U

-- Infinite eta-expansion would make Agda loop

test : U
test = _


text:
module Isos.Isomorphism where

open import Logics.And public


text:
{-
 - Prelude: Play with some basic theorems...
 -}

{-# OPTIONS --rewriting #-}

module Prelude where

open import Agda.Builtin.Equality public
open import Agda.Builtin.Nat renaming (Nat to ℕ) public

{-# BUILTIN REWRITE _≡_ #-}

-- Identity function
id : ∀ {ℓ} {A : Set ℓ} → A → A
id x = x

_ : id 42 ≡ 42
_ = refl

-- Composition
_∘_ :
  ∀ {ℓ m n}
  {A : Set ℓ}
  {B : Set m}
  {C : B → Set n}
  (g : (b : B) → C b)
  (f : A → B)
  → ---------
  (a : A) → C (f a)
(g ∘ f) x = g (f x)

_ : (id ∘ id) 42 ≡ id (id 42)
_ = refl

-- Transitivity
trans :
  ∀ {ℓ}
  {A : Set ℓ}
  {x y z : A}
  (q : y ≡ z)
  (p : x ≡ y)
  → ---------
  x ≡ z
trans n refl = n

-- Symmetry
symm :
  ∀ {ℓ}
  {A : Set ℓ}
  {x y : A}
  (p : x ≡ y)
  → ---------
  y ≡ x
symm refl = refl

-- Congruence
cong :
  ∀ {ℓ ℓ′}
  {A : Set ℓ}
  {B : Set ℓ′}
  (f : A → B)
  {x y : A}
  (p : x ≡ y)
  → ---------
  f x ≡ f y
cong _ refl = refl

cong₂ :
  ∀ {ℓ ℓ′}
  {A A′ : Set ℓ}
  {B : Set ℓ′}
  (f : A → A′ → B)
  {x y : A}
  {x′ y′ : A′}
  (p : x ≡ y)
  (q : x′ ≡ y′)
  → -----------
  f x x′ ≡ f y y′
cong₂ _ refl refl = refl

-- Substitution
subst :
  ∀ {ℓ ℓ′}
  {A : Set ℓ}
  (B : A → Set ℓ′)
  {x y : A}
  (p : x ≡ y)
  → ---------
  B x → B y
subst _ refl = λ a → a

-- Type coercion
coe :
  ∀ {ℓ}
  {A B : Set ℓ}
  → -----------
  A ≡ B → A → B
coe r a = subst id r a

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
-- Andreas, 2018-10-17, re issue #2757
--
-- Matching on runtime-irrelevant arguments is fine
-- as long as it produces only one branch.

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

-- Matching on empty types can be erased.

data ⊥ : Set where

⊥-elim : ∀{A : Set} → @0 ⊥ → A
⊥-elim ()

-- Accessibility.

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

-- Accessibility proofs can be erased.

wfrec : {A : Set} (R : A → A → Set) {P : A → Set}
  → (∀{x} → (∀{y} (@0 y<x : R y x) → P y) → P x)
  → ∀{x} (@0 ax : Acc R x) → P x
wfrec R f (acc h) = f λ y<x → wfrec R f (h y<x)

-- Non-branching matches can be erased.

diag : ∀(@0 x) (y : Bool) (@0 eq : x ≡ y) → Bool
diag false false refl = false
diag true  y     refl = y

diag' : ∀ x (@0 y : Bool) (@0 eq : x ≡ y) → Bool
diag' false false refl = false
diag' true  y     refl = y

-- Also for literals.

nonBranchLit : ∀ (@0 x) (eq : x ≡ 0) → Set
nonBranchLit 0 refl = Nat

-- The attribute syntax collides lexically with the as-pattern syntax.

userConfusingClashOfAttributesAndAsPatterns : ∀ (@0 x) (eq : x ≡ 0) → Set
userConfusingClashOfAttributesAndAsPatterns (x @0) refl = Nat


text:
open import Relation.Nullary using (¬_)

module AKS.Fin where

open import AKS.Nat using (ℕ; _+_; _<_)

record Fin (n : ℕ) : Set where
  constructor Fin✓
  field
    i : ℕ
    i<n : i < n

¬Fin0 : ¬ (Fin 0)
¬Fin0 ()

from< : ∀ {i n} → i < n → Fin n
from< {i} i<n = Fin✓ i i<n

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Record types with manifest fields and "with", based on Randy
-- Pollack's "Dependently Typed Records in Type Theory"
------------------------------------------------------------------------

-- For an example of how this module can be used, see README.Record.

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

open import Data.Bool.Base using (if_then_else_)
open import Data.Empty
open import Data.List.Base
open import Data.Product hiding (proj₁; proj₂)
open import Data.Unit
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable

-- The module is parametrised by the type of labels, which should come
-- with decidable equality.

module Record {ℓ : Level} (Label : Set ℓ) (_≟_ : Decidable (_≡_ {A = Label})) where

------------------------------------------------------------------------
-- A Σ-type with a manifest field

-- A variant of Σ where the value of the second field is "manifest"
-- (given by the first).

infix 4 _,

record Manifest-Σ {a b} (A : Set a) {B : A → Set b}
                  (f : (x : A) → B x) : Set a where
  constructor _,
  field proj₁ : A

  proj₂ : B proj₁
  proj₂ = f proj₁

------------------------------------------------------------------------
-- Signatures and records

mutual

  infixl 5 _,_∶_ _,_≔_

  data Signature s : Set (suc s ⊔ ℓ) where
    ∅     : Signature s
    _,_∶_ : (Sig : Signature s)
            (ℓ : Label)
            (A : Record Sig → Set s) →
            Signature s
    _,_≔_ : (Sig : Signature s)
            (ℓ : Label)
            {A : Record Sig → Set s}
            (a : (r : Record Sig) → A r) →
            Signature s

  -- Record is a record type to ensure that the signature can be
  -- inferred from a value of type Record Sig.

  record Record {s} (Sig : Signature s) : Set s where
    eta-equality
    inductive
    constructor rec
    field fun : Record-fun Sig

  Record-fun : ∀ {s} → Signature s → Set s
  Record-fun ∅             = Lift _ ⊤
  Record-fun (Sig , ℓ ∶ A) =          Σ (Record Sig) A
  Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a

------------------------------------------------------------------------
-- Labels

-- A signature's labels, starting with the last one.

labels : ∀ {s} → Signature s → List Label
labels ∅             = []
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig

-- Inhabited if the label is part of the signature.

infix 4 _∈_

_∈_ : ∀ {s} → Label → Signature s → Set
ℓ ∈ Sig =
  foldr (λ ℓ′ → if ⌊ ℓ ≟ ℓ′ ⌋ then (λ _ → ⊤) else id) ⊥ (labels Sig)

------------------------------------------------------------------------
-- Projections

-- Signature restriction and projection. (Restriction means removal of
-- a given field and all subsequent fields.)

Restrict : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig →
           Signature s
Restrict ∅              ℓ ()
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no  _ = Restrict Sig ℓ ℓ∈
Restrict (Sig , ℓ′ ≔ a) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no  _ = Restrict Sig ℓ ℓ∈

Restricted : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig → Set s
Restricted Sig ℓ ℓ∈ = Record (Restrict Sig ℓ ℓ∈)

Proj : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
       Restricted Sig ℓ ℓ∈ → Set s
Proj ∅              ℓ {}
Proj (Sig , ℓ′ ∶ A) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = A
... | no  _ = Proj Sig ℓ {ℓ∈}
Proj (_,_≔_ Sig ℓ′ {A = A} a) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = A
... | no  _ = Proj Sig ℓ {ℓ∈}

-- Record restriction and projection.

infixl 5 _∣_

_∣_ : ∀ {s} {Sig : Signature s} → Record Sig →
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈
_∣_ {Sig = ∅}            r       ℓ {}
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₁ r
... | no  _ = _∣_ (Σ.proj₁ r) ℓ {ℓ∈}
_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₁ r
... | no  _ = _∣_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

infixl 5 _·_

_·_ : ∀ {s} {Sig : Signature s} (r : Record Sig)
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
      Proj Sig ℓ {ℓ∈} (r ∣ ℓ)
_·_ {Sig = ∅}            r       ℓ {}
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₂ r
... | no  _ = _·_ (Σ.proj₁ r) ℓ {ℓ∈}
_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₂ r
... | no  _ = _·_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

------------------------------------------------------------------------
-- With

-- Sig With ℓ ≔ a is the signature Sig, but with the ℓ field set to a.

mutual

  infixl 5 _With_≔_

  _With_≔_ : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
             ((r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r) → Signature s
  _With_≔_ ∅ ℓ {} a
  _With_≔_ (Sig , ℓ′ ∶ A)   ℓ {ℓ∈} a with ℓ ≟ ℓ′
  ... | yes _ = Sig                   , ℓ′ ≔ a
  ... | no  _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ∶ A ∘ drop-With
  _With_≔_  (Sig , ℓ′ ≔ a′) ℓ {ℓ∈} a with ℓ ≟ ℓ′
  ... | yes _ = Sig                   , ℓ′ ≔ a
  ... | no  _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ≔ a′ ∘ drop-With

  drop-With : ∀ {s} {Sig : Signature s} {ℓ : Label} {ℓ∈ : ℓ ∈ Sig}
              {a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r} →
              Record (_With_≔_ Sig ℓ {ℓ∈} a) → Record Sig
  drop-With {Sig = ∅} {ℓ∈ = ()}      r
  drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
  ... | no  _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
  drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r ,)
  ... | no  _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)


text:
-- making sure that the fun clauses are kept in declaration order
-- in an interleaved mutual block

open import Agda.Builtin.Nat

interleaved mutual

  plus  : Nat → Nat → Nat
  minus : Nat → Nat → Nat

  -- 0 being neutral
  plus 0 n = n
  minus n 0 = n

  -- other 0 case
  plus n 0 = n
  minus 0 n = 0

  -- suc suc
  plus (suc m) (suc n) = suc (suc (plus m n))
  minus (suc m) (suc n) = minus m n

-- All of these test cases should be true by computation
-- It will not be the case if the definitions have been interleaved
-- the wrong way around (because the resulting definition would be
-- strict in a different argument)

open import Agda.Builtin.Equality

_ : ∀ {n} → plus 0 n ≡ n
_ = refl

_ : ∀ {n} → minus n 0 ≡ n
_ = refl

-- The following should not check with refl; for the same reasons

-- _ : ∀ {n} → plus n 0 ≡ n
-- _ = refl

-- _ : ∀ {n} → minus 0 n ≡ 0
-- _ = refl

-- but they are of course provable by case analysis:

_ : ∀ n → plus n 0 ≡ n
_ = λ where
      zero → refl
      (suc _) → refl

_ : ∀ n → minus 0 n ≡ 0
_ = λ where
      zero → refl
      (suc _) → refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Reported by nils.anders.danielsson, Feb 17, 2015

-- See also  Issue 292 ,  Issue 1406 , and Issue 1427.

-- The code below is accepted by Agda 2.4.2.2, but not by the current
-- maintenance or master branches.

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

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

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

-- C could be a typed DSEL.

data C : Set → Set₁ where
  c₁ c₂ : (A : Set) → C (Box A)
-- If A is considered forced, the code no longer type-checks.

-- D could be some kind of semantics for C.

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

module Doesn't-work where

  -- Let's try to write an eliminator for the part of the semantics
  -- that concerns c₁ programs. The basic approach doesn't work:

  D-elim-c₁ : (P : {A : Set} → D (c₁ A) → Set₂) →
              ((A : Set) → P (d₁ A)) →
              {A : Set} (x : D (c₁ A)) → P x
  D-elim-c₁ P p (d₁ A) = p A

  -- The following trick also fails (but for some reason the absurd
  -- case is accepted):

  -- Jesper 2015-12-18 update: this is no longer accepted by the new unifier.
  --D-elim-c₁-helper :
  --  (P : {A B : Set} {c : C A} →
  --       D c → A ≡ Box B → c ≅ c₁ B → Set₂) →
  --  ((A : Set) → P (d₁ A) refl refl) →
  --  {A B : Set} {c : C A}
  --  (x : D c) (eq₂ : c ≅ c₁ B) (eq₁ : A ≡ Box B) → P x eq₁ eq₂
  --D-elim-c₁-helper P p (d₂ A) ()   _
  --D-elim-c₁-helper P p (d₁ A) refl refl = p A

module Works where

  -- I can define the eliminators by first defining and proving no
  -- confusion (following McBride, Goguen and McKinna). However, this
  -- requires a fair amount of work, and easy dependent pattern
  -- matching is arguably one of the defining features of Agda.
  --
  -- A quote from "A Few Constructions on Constructors": "The Epigram
  -- language and system [25, 23] takes these constructions for
  -- granted. We see no reason why the users of other systems should
  -- work harder than we do."

  data ⊥ : Set₁ where

  No-confusion : ∀ {A B} → C A → C B → Set₁
  No-confusion (c₁ A) (c₁ B) = A ≡ B
  No-confusion (c₂ A) (c₂ B) = A ≡ B
  No-confusion _      _      = ⊥

  no-confusion :
    ∀ {A B} (x : C A) (y : C B) → A ≡ B → x ≅ y → No-confusion x y
  no-confusion (c₁ A) .(c₁ A) refl refl = refl
  no-confusion (c₂ A) .(c₂ A) refl refl = refl

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

  cast : {A B : Set} {x : C A} {y : C B} →
         A ≡ B → x ≅ y → D x → D y
  cast refl refl x = x

  D-elim-c₁ :
    (P : {A : Set} → D (c₁ A) → Set₂) →
    ((A : Set) → P (d₁ A)) →
    {A : Set} (x : D (c₁ A)) → P x
  D-elim-c₁ P p x =
    D-elim-c₁-helper (λ x eq₁ eq₂ → P (cast eq₁ eq₂ x)) p x refl refl

-- should type-check


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma

Π∙ : ∀ {ℓ ℓ'} (A : Type ℓ) (B∙ : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Π∙ A B∙ = (∀ a → typ (B∙ a)) , (λ a → pt (B∙ a))

Σ∙ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : typ A∙ → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Σ∙ A∙ B∙ = (Σ[ a ∈ typ A∙ ] typ (B∙ a)) , (pt A∙ , pt (B∙ (pt A∙)))

_×∙_ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
A∙ ×∙ B∙ = ((typ A∙) × (typ B∙)) , (pt A∙ , pt B∙)

{- composition of pointed maps -}
_∘∙_ : ∀ {ℓA ℓB ℓC} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC}
       (g : B →∙ C) (f : A →∙ B) → (A →∙ C)
(g , g∙) ∘∙ (f , f∙) = (λ x → g (f  x)) , ((cong g f∙) ∙ g∙)

{- pointed identity -}
id∙ : ∀ {ℓA} (A : Pointed ℓA) → (A →∙ A)
id∙ A = ((λ x → x) , refl)

{- constant pointed map -}
const∙ : ∀ {ℓA ℓB} (A : Pointed ℓA) (B : Pointed ℓB) → (A →∙ B)
const∙ _ (_ , b) = (λ _ → b) , refl

{- left identity law for pointed maps -}
∘∙-idˡ : ∀ {ℓA ℓB} {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → f ∘∙ id∙ A ≡ f
∘∙-idˡ (_ , f∙) = ΣPathP ( refl , (lUnit f∙) ⁻¹ )

{- right identity law for pointed maps -}
∘∙-idʳ : ∀ {ℓA ℓB} {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → id∙ B ∘∙ f ≡ f
∘∙-idʳ (_ , f∙) = ΣPathP ( refl , (rUnit f∙) ⁻¹ )

{- associativity for composition of pointed maps -}
∘∙-assoc : ∀ {ℓA ℓB ℓC ℓD} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC} {D : Pointed ℓD}
           (h : C →∙ D) (g : B →∙ C) (f : A →∙ B)
           → (h ∘∙ g) ∘∙ f ≡ h ∘∙ (g ∘∙ f)
∘∙-assoc (h , h∙) (g , g∙) (f , f∙) = ΣPathP (refl , q)
  where
    q : (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙) ≡ cong h (cong g f∙ ∙ g∙) ∙ h∙
    q = ( (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ refl ⟩
        (cong h (cong g f∙)) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ assoc (cong h (cong g f∙)) (cong h g∙) h∙ ⟩
        (cong h (cong g f∙) ∙ cong h g∙) ∙ h∙
        ≡⟨ cong (λ p → p ∙ h∙) ((cong-∙ h (cong g f∙) g∙) ⁻¹) ⟩
        (cong h (cong g f∙ ∙ g∙) ∙ h∙) ∎ )

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical